liu.seSearch for publications in DiVA
Change search
Link to record
Permanent link

Direct link
BETA
Ganjei, Zeinab
Publications (5 of 5) Show all publications
Ganjei, Z., Rezine, A., Eles, P. & Peng, Z. (2016). Counting dynamically synchronizing processes. International Journal on Software Tools for Technology Transfer (STTT), 18(5), 517-534
Open this publication in new window or tab >>Counting dynamically synchronizing processes
2016 (English)In: International Journal on Software Tools for Technology Transfer (STTT), ISSN 1433-2779, E-ISSN 1433-2787, Vol. 18, no 5, p. 517-534Article in journal (Refereed) Published
Abstract [en]

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.

Place, publisher, year, edition, pages
Springer Berlin/Heidelberg, 2016
Keywords
Parameterized verification, Counting predicate, Barrier synchronization, Deadlock freedom, Multithreaded programs, Counter abstraction, Predicate abstraction, Constrained monotonic abstraction
National Category
Computer Sciences
Identifiers
urn:nbn:se:liu:diva-124406 (URN)10.1007/s10009-015-0411-0 (DOI)000382011100004 ()
Note

Funding agencies: 12.04 CENIIT project

Available from: 2016-01-28 Created: 2016-01-28 Last updated: 2018-01-10
Ganjei, Z., Rezine, A., Eles, P. & Peng, Z. (2016). Lazy Constrained Monotonic Abstraction. In: Barbara Jobstmann; K. Rustan M. Leino (Ed.), Verification, Model Checking, and Abstract Interpretation: 17th International Conference, VMCAI 2016, St. Petersburg, FL, USA, January 17-19, 2016. Proceedings. Paper presented at 17th International Conference, VMCAI 2016, St. Petersburg, FL, USA, January 17-19, 2016 (pp. 147-165). Springer Berlin/Heidelberg, 9583
Open this publication in new window or tab >>Lazy Constrained Monotonic Abstraction
2016 (English)In: Verification, Model Checking, and Abstract Interpretation: 17th International Conference, VMCAI 2016, St. Petersburg, FL, USA, January 17-19, 2016. Proceedings / [ed] Barbara Jobstmann; K. Rustan M. Leino, Springer Berlin/Heidelberg, 2016, Vol. 9583, p. 147-165Conference paper, Published paper (Refereed)
Abstract [en]

We introduce Lazy Constrained Monotonic Abstraction (lazy CMA for short) for lazily and soundly exploring well structured abstractions of infinite state non-monotonic systems. CMA makes use of infinite state and well structured abstractions by forcing monotonicity wrt. refinable orderings. The new orderings can be refined based on obtained false positives in a CEGAR like fashion. This allows for the verification of systems that are not monotonic and are hence inherently beyond the reach of classical analysis based on the theory of well structured systems. In this paper, we consistently improve on the existing approach by localizing refinements and by avoiding to trash the explored state space each time a refinement step is required for the ordering. To this end, we adapt ideas from classical lazy predicate abstraction and explain how we address the fact that the number of control points (i.e., minimal elements to be visited) is a priori unbounded. This is unlike the case of plain lazy abstraction which relies on the fact that the number of control locations is finite. We propose several heuristics and report on our experiments using our open source prototype. We consider both backward and forward explorations on non-monotonic systems automatically derived from concurrent programs. Intuitively, the approach could be regarded as using refinable upward closure operators as localized widening operators for an a priori arbitrary number of control points.

Place, publisher, year, edition, pages
Springer Berlin/Heidelberg, 2016
Series
Lecture Notes in Computer Science, ISSN 0302-9743, E-ISSN 1611-3349
Keywords
Constrained monotonic abstraction, Lazy exploration, Well structured systems, Safety properties, Counter machines reachability
National Category
Computer Sciences
Identifiers
urn:nbn:se:liu:diva-123739 (URN)10.1007/978-3-662-49122-5_7 (DOI)000375148800007 ()9783662491218 (ISBN)9783662491225 (ISBN)
Conference
17th International Conference, VMCAI 2016, St. Petersburg, FL, USA, January 17-19, 2016
Available from: 2016-01-11 Created: 2016-01-11 Last updated: 2018-02-06Bibliographically approved
Ganjei, Z., Rezine, A., Ion Eles, P. & Peng, Z. (2015). Abstracting and Counting Synchronizing Processes. In: Verification, Model Checking, and Abstract Interpretation: 16th International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI 2015), Mumbai, India, Jan. 12-14, 2015.. Paper presented at VMCAI 15 (pp. 227-244). Springer
Open this publication in new window or tab >>Abstracting and Counting Synchronizing Processes
2015 (English)In: Verification, Model Checking, and Abstract Interpretation: 16th International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI 2015), Mumbai, India, Jan. 12-14, 2015., Springer, 2015, p. 227-244Conference paper, Published paper (Refereed)
Abstract [en]

We address the problem of automatically establishing synchronization dependent correctness (e.g. due to using barriers or ensuring absence of deadlocks) of programs generating an arbitrary number of concurrent processes and manipulating variables ranging over an infinite domain. Automatically checking such properties for these programs is beyond the capabilities of current verification techniques. For this purpose, we describe an original logic that mixes two sorts of variables: those shared and manipulated by the concurrent processes, and ghost variables referring to the number of processes satisfying predicates on shared and local program variables. We then combine existing works on counter, predicate, and constrained monotonic abstraction and nest two cooperating counter example based refinement loops for establishing correctness (safety expressed as non reachability of configurations satisfying formulas in our logic). We have implemented a tool (Pacman, for predicated constrained monotonic abstraction) and used it to perform parameterized verification for several programs whose correctness crucially depends on precisely capturing the number of synchronizing processes.

Place, publisher, year, edition, pages
Springer, 2015
Series
Lecture Notes in Computer Science, ISSN 0302-9743 ; 8931
National Category
Computer and Information Sciences
Identifiers
urn:nbn:se:liu:diva-114467 (URN)10.1007/978-3-662-46081-8_13 (DOI)000354784200013 ()978-3-662-46080-1 (ISBN)978-3-662-46081-8 (ISBN)
Conference
VMCAI 15
Available from: 2015-02-20 Created: 2015-02-20 Last updated: 2018-01-11
Abdulla, P. A., Atig, M. F., Ganjei, Z., Rezine, A. & Zhu, Y. (2015). Verification of Cache Coherence Protocols wrt. Trace Filters. In: : . Paper presented at Formal Methods in Computer-Aided Design (FMCAD). IEEE
Open this publication in new window or tab >>Verification of Cache Coherence Protocols wrt. Trace Filters
Show others...
2015 (English)Conference paper, Published paper (Refereed)
Abstract [en]

We address the problem of parameterized verification of cache coherence protocols for hardware accelerated transactional memories. In this setting, transactional memories leverage on the versioning capabilities of the underlying cache coherence protocol. The length of the transactions, their number, and the number of manipulated variables (i.e., cache lines) are parameters of the verification problem. Caches in such systems are finite-state automata communicating via broadcasts and shared variables. We augment our system with filters that restrict the set of possible executable traces according to existing conflict resolution policies. We show that the verification of coherence for parameterized cache protocols with filters can be reduced to systems with only a finite number of cache lines. For verification, we show how to account for the effect of the adopted filters in a symbolic backward reachability algorithm based on the framework of constrained monotonic abstraction. We have implemented our method and used it to verify transactional memory coherence protocols with respect to different conflict resolution policies.

Place, publisher, year, edition, pages
IEEE, 2015
National Category
Computer Sciences
Identifiers
urn:nbn:se:liu:diva-128860 (URN)9780983567851 (ISBN)
Conference
Formal Methods in Computer-Aided Design (FMCAD)
Available from: 2016-06-02 Created: 2016-06-02 Last updated: 2018-01-10
Ganjei, Z., Rezine, A., Eles, P. & Peng, Z. (2014). Abstracting and Counting Synchronizing Processes.
Open this publication in new window or tab >>Abstracting and Counting Synchronizing Processes
2014 (English)Report (Other academic)
Abstract [en]

We address the problem of automatically establishing synchronization dependent correctness (e.g. due to using barriers or ensuring absence of deadlocks) of programs generating an arbitrary number of concurrent processes and manipulating variables ranging over an infinite domain. Automatically checking such properties for these programs is beyond the capabilities of current verification techniques. For this purpose, we describe an original logic that mixes two sorts of variables: those shared and manipulated by the concurrent processes, and ghost variables refering to the number of processes satisfying predicates on shared and local program variables. We then combine existing works on counter, predicate, and constrained monotonic abstraction and nest two cooperating counter example based refinement loops for establishing correctness (safety expressed as non reachability of configurations satisfying formulas in our logic). We have implemented a tool (Pacman, for predicated constrained monotonic abstraction) and used it to perform parameterized verification for several programs whose correctness crucially depends on precisely capturing the number of synchronizing processes. 

Publisher
p. 35
Series
Technical reports in Computer and Information Science, ISSN 1654-7233
Keywords
Parameterized verification, counting logic, barrier synchronization, deadlock freedom, multithreaded programs, counter abstraction, predicate abstraction, constrained monotonic abstraction
National Category
Engineering and Technology
Identifiers
urn:nbn:se:liu:diva-111739 (URN)
Available from: 2014-10-30 Created: 2014-10-30 Last updated: 2014-10-31Bibliographically approved
Organisations

Search in DiVA

Show all publications