| 1. |
- Ganjei, Zeinab, et al.
(författare)
-
Lazy Constrained Monotonic Abstraction
- 2016
-
Ingår i: Verification, Model Checking, and Abstract Interpretation. - Berlin, Heidelberg : Springer Berlin/Heidelberg. - 9783662491218 - 9783662491225 ; , s. 147-165
-
Konferensbidrag (refereegranskat)abstract
- 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.
|
|
| 2. |
- Haziza, Frédéric, et al.
(författare)
-
Pointer Race Freedom
- 2016
-
Ingår i: Verification, Model Checking, And Abstract Interpretation, VMCAI 2016. - Berlin, Heidelberg : Springer. - 9783662491225 - 9783662491218 ; , s. 393-412
-
Konferensbidrag (refereegranskat)abstract
- We propose a novel notion of pointer race for concurrent programs manipulating a shared heap. A pointer race is an access to a memory address which was freed, and it is out of the accessor's control whether or not the cell has been re-allocated. We establish two results. (1) Under the assumption of pointer race freedom, it is sound to verify a program running under explicit memory management as if it was running with garbage collection. (2) Even the requirement of pointer race freedom itself can be verified under the garbage-collected semantics. We then prove analogues of the theorems for a stronger notion of pointer race needed to cope with performance-critical code purposely using racy comparisons and even racy dereferences of pointers. As a practical contribution, we apply our results to optimize a thread-modular analysis under explicit memory management. Our experiments confirm a speedup of up to two orders of magnitude.
|
|
