Search: L773:1433 2779 OR L773:1433 2787 >
Counting dynamicall...
Counting dynamically synchronizing processes
-
- Ganjei, Zeinab (author)
- Linköpings universitet,Programvara och system,Tekniska fakulteten
-
- Rezine, Ahmed (author)
- Linköpings universitet,Programvara och system,Tekniska fakulteten
-
- Eles, Petru (author)
- Linköpings universitet,Programvara och system,Tekniska fakulteten
-
show more...
-
- Peng, Zebo (author)
- Linköpings universitet,Programvara och system,Tekniska fakulteten
-
show less...
-
(creator_code:org_t)
- 2016-01-21
- 2016
- English.
-
In: International Journal on Software Tools for Technology Transfer. - : Springer Berlin/Heidelberg. - 1433-2779 .- 1433-2787. ; 18:5, s. 517-534
- Related links:
-
https://liu.diva-por... (primary) (Raw object)
-
show more...
-
http://liu.diva-port...
-
https://urn.kb.se/re...
-
https://doi.org/10.1...
-
show less...
Abstract
Subject headings
Close
- We address the problem of automatically establishing correctness for programs generating an arbitrary number of concurrent processes and manipulating variables ranging over an infinite domain. The programs we consider can make use of the shared variables to count and synchronize the spawned processes. This allows them to implement intricate synchronization mechanisms, such as barriers. Automatically verifying correctness, and deadlock freedom, of such programs is beyond the capabilities of current techniques. For this purpose, we make use of counting predicates that mix counters referring to the number of processes satisfying certain properties and variables directly manipulated by the concurrent processes. We then combine existing works on counter, predicate, and constrained monotonic abstraction and build a nested counter example based refinement scheme for establishing correctness (expressed as non-reachability of configurations satisfying counting predicates formulas). We have implemented a tool (Pacman, for predicated constrained monotonic abstraction) and used it to perform parameterized verification on several programs whose correctness crucially depends on precisely capturing the number of processes synchronizing using shared variables.
Subject headings
- NATURVETENSKAP -- Data- och informationsvetenskap -- Datavetenskap (hsv//swe)
- NATURAL SCIENCES -- Computer and Information Sciences -- Computer Sciences (hsv//eng)
Keyword
- Parameterized verification
- Counting predicate
- Barrier synchronization
- Deadlock freedom
- Multithreaded programs
- Counter abstraction
- Predicate abstraction
- Constrained monotonic abstraction
Publication and Content Type
- ref (subject category)
- art (subject category)
Find in a library
To the university's database