Project

General

Profile

Actions

Feature #5287

open

Experiment with sound implementation of rerouter

Added by Evgeny Novikov about 10 years ago. Updated almost 9 years ago.

Status:
New
Priority:
Low
Assignee:
-
Category:
-
Start date:
09/24/2014
Due date:
% Done:

0%

Estimated time:
Published in build:

Description

From http://forge.ispras.ru/issues/2462#note-10:
It seems that sound implementation of rerouter needs rule models to be extended rather considerably. When argument signature for, say, mutex_lock can't be calculated we need to call something like ldv_all_mutex_lock that will try to lock all known mutexes nondeterministically. "All" means that we should use template foreach like for ldv_initialize and ldv_check_final_state. Since there is neither iteration through model states nor nondeterminism in model for mutex_lock we better need to develop a separate model (that was called ldv_all_mutex_lock before). Since different functions have different sematics (some returns void, some returns error codes, some decrease counters) we need to develop such the separate models for all functions that have corresponding models already.
That's why some experiments should be executed before implementation. May be these experiments will show that we do can distinguish different object not only just by their names but also by names of references to them.

Actions #1

Updated by Evgeny Novikov almost 9 years ago

  • Priority changed from Normal to Low
Actions

Also available in: Atom PDF