| 1. |
- Abdulla, Parosh Aziz, et al.
(författare)
-
Automatic fence insertion in integer programs via predicate abstraction
- 2012
-
Ingår i: Static Analysis. - Berlin, Heidelberg : Springer Berlin/Heidelberg. - 9783642331244 - 9783642331251 ; , s. 164-180
-
Konferensbidrag (refereegranskat)abstract
- We propose an automatic fence insertion and verification framework for concurrent programs running under relaxed memory. Unlike previous approaches to this problem, which allow only variables of finite domain, we target programs with (unbounded) integer variables. The problem is difficult because it has two different sources of infiniteness: unbounded store buffers and unbounded integer variables. Our framework consists of three main components: (1) a finite abstraction technique for the store buffers, (2) a finite abstraction technique for the integer variables, and (3) a counterexample guided abstraction refinement loop of the model obtained from the combination of the two abstraction techniques. We have implemented a prototype based on the framework and run it successfully on all standard benchmarks together with several challenging examples that are beyond the applicability of existing methods.
|
|
| 2. |
- Abdulla, Parosh Aziz, et al.
(författare)
-
Counter-Example Guided Fence Insertion under TSO
- 2012
-
Ingår i: TACAS 2012. - Berlin, Heidelberg : Springer. - 9783642287558 - 9783642287565
-
Konferensbidrag (refereegranskat)abstract
- We give a sound and complete fence insertion procedure for concurrentfinite-state programs running under the classical TSO memory model. Thismodel allows “write to read” relaxation corresponding to the addition of an unboundedstore buffer between each processor and the main memory. We introducea novel machine model, called the Single-Buffer (SB) semantics, and show thatthe reachability problem for a program under TSO can be reduced to the reachabilityproblem under SB. We present a simple and effective backward reachabilityanalysis algorithm for the latter, and propose a counter-example guided fence insertionprocedure. The procedure is augmented by a placement constraint thatallows the user to choose places inside the program where fences may be inserted.For a given placement constraint, we automatically infer all minimal setsof fences that ensure correctness. We have implemented a prototype and run itsuccessfully on all standard benchmarks together with several challenging examplesthat are beyond the applicability of existing methods.
|
|
| 3. |
|
|
| 4. |
- Abdulla, Parosh Aziz, et al.
(författare)
-
Memorax, a Precise and Sound Tool for Automatic Fence Insertion under TSO
- 2013
-
Ingår i: Tools and Algorithms for the Construction and Analysis of Systems. - Berlin, Heidelberg : Springer Berlin/Heidelberg. - 9783642367410 - 9783642367427 ; , s. 530-536
-
Konferensbidrag (refereegranskat)abstract
- We introduce MEMORAX, a tool for the verification of control state reachability (i.e., safety properties) of concurrent programs manipulating finite range and integer variables and running on top of weak memory models. The verification task is non-trivial as it involves exploring state spaces of arbitrary or even infinite sizes. Even for programs that only manipulate finite range variables, the sizes of the store buffers could grow unboundedly, and hence the state spaces that need to be explored could be of infinite size. In addition, MEMORAX in- corporates an interpolation based CEGAR loop to make possible the verification of control state reachability for concurrent programs involving integer variables. The reachability procedure is used to automatically compute possible memory fence placements that guarantee the unreachability of bad control states under TSO. In fact, for programs only involving finite range variables and running on TSO, the fence insertion functionality is complete, i.e., it will find all minimal sets of memory fence placements (minimal in the sense that removing any fence would result in the reachability of the bad control states). This makes MEMORAX the first freely available, open source, push-button verification and fence insertion tool for programs running under TSO with integer variables.
|
|
| 5. |
- Abdulla, Parosh Aziz, et al.
(författare)
-
Mending fences with self-invalidation and self-downgrade
- 2018
-
Ingår i: Logical Methods in Computer Science. - 1860-5974. ; 14:1
-
Tidskriftsartikel (refereegranskat)abstract
- Cache coherence protocols based on self-invalidation and self-downgrade have recently seen increased popularity due to their simplicity, potential performance efficiency, and low energy consumption. However, such protocols result in memory instruction reordering, thus causing extra program behaviors that are often not intended by the programmers. We propose a novel formal model that captures the semantics of programs running under such protocols, and features a set of fences that interact with the coherence layer. Using the model, we design an algorithm to analyze the reachability and check whether a program satisfies a given safety property with the current set of fences. We describe a method for insertion of optimal sets of fences that ensure correctness of the program under such protocols. The method relies on a counter-example guided fence insertion procedure. One feature of our method is that it can handle a variety of fences (with different costs). This diversity makes optimization more difficult since one has to optimize the total cost of the inserted fences, rather than just their number. To demonstrate the strength of our approach, we have implemented a prototype and run it on a wide range of examples and benchmarks. We have also, using simulation, evaluated the performance of the resulting fenced programs.
|
|
| 6. |
- Abdulla, Parosh Aziz, et al.
(författare)
-
Stateless model checking for POWER
- 2016
-
Ingår i: Computer Aided Verification. - Cham : Springer. - 9783319415390 - 9783319415406 ; , s. 134-156
-
Konferensbidrag (refereegranskat)abstract
- We present the first framework for efficient application of stateless model checking (SMC) to programs running under the relaxed memory model of POWER. The framework combines several contributions. The first contribution is that we develop a scheme for systematically deriving operational execution models from existing axiomatic ones. The scheme is such that the derived execution models are well suited for efficient SMC. We apply our scheme to the axiomatic model of POWER from [8]. Our main contribution is a technique for efficient SMC, called Relaxed Stateless Model Checking (RSMC), which systematically explores the possible inequivalent executions of a program. RSMC is suitable for execution models obtained using our scheme. We prove that RSMC is sound and optimal for the POWER memory model, in the sense that each complete program behavior is explored exactly once. We show the feasibility of our technique by providing an implementation for programs written in C/pthreads.
|
|
| 7. |
- Abdulla, Parosh Aziz, et al.
(författare)
-
Stateless model checking for TSO and PSO
- 2015
-
Ingår i: Tools and Algorithms for the Construction and Analysis of Systems. - Berlin, Heidelberg : Springer Berlin/Heidelberg. - 9783662466803 ; , s. 353-367
-
Konferensbidrag (refereegranskat)
|
|
| 8. |
- Abdulla, Parosh Aziz, et al.
(författare)
-
Stateless model checking for TSO and PSO
- 2017
-
Ingår i: Acta Informatica. - : Springer Science and Business Media LLC. - 0001-5903 .- 1432-0525. ; 54:8, s. 789-818
-
Tidskriftsartikel (refereegranskat)
|
|
| 9. |
- Abdulla, Parosh, Professor, 1961-, et al.
(författare)
-
On the State Reachability Problem for Concurrent Programs Under Power
- 2020
-
Ingår i: Networked Systems - 8th International Conference, {NETYS} 2020, Morocco, Revised Selected Papers. - : Springer Nature Switzerland AG.
-
Konferensbidrag (refereegranskat)abstract
- We consider the problem of safety verification, formalized as control-state reachability, for concurrent programs running on the Power architecture. Our main result shows that safety verification under Power is undecidable for programs with just two threads.
|
|
| 10. |
|
|
