| 1. |
- Abdulla, Parosh Aziz, et al.
(author)
-
A load-buffer semantics for total store ordering
- 2018
-
In: Logical Methods in Computer Science. - 1860-5974. ; 14:1
-
Journal article (peer-reviewed)abstract
- We address the problem of verifying safety properties of concurrent programs running over the Total Store Order (TSO) memory model. Known decision procedures for this model are based on complex encodings of store buffers as lossy channels. These procedures assume that the number of processes is fixed. However, it is important in general to prove the correctness of a system/algorithm in a parametric way with an arbitrarily large number of processes. In this paper, we introduce an alternative (yet equivalent) semantics to the classical one for the TSO semantics that is more amenable to efficient algorithmic verification and for the extension to parametric verification. For that, we adopt a dual view where load buffers are used instead of store buffers. The flow of information is now from the memory to load buffers. We show that this new semantics allows (1) to simplify drastically the safety analysis under TSO, (2) to obtain a spectacular gain in efficiency and scalability compared to existing procedures, and (3) to extend easily the decision procedure to the parametric case, which allows obtaining a new decidability result, and more importantly, a verification algorithm that is more general and more efficient in practice than the one for bounded instances.
|
|
| 2. |
- Abdulla, Parosh Aziz, Professor, et al.
(author)
-
Complexity of reachability for data-aware dynamic systems
- 2018
-
In: Proc. 18th International Conference on Application of Concurrency to System Design. - : IEEE Computer Society. - 9781538670132 ; , s. 11-20
-
Conference paper (peer-reviewed)abstract
- A formal model called database manipulating systems was introduced to model data-aware dynamic systems. Its semantics is given by an infinite labelled transition systems where a label can be an unbounded relational database. Reachability problem is undecidable over schemas consisting of either a binary relation or two unary relations. We study the reachability problem under schema restrictions and restrictions on the query language. We provide tight complexity bounds for different combinations of schema and query language, by reductions to/from standard formalism of infinite state systems such as Petri nets and counter systems. Our reductions throw light into the connections between these two seemingly unrelated models.
|
|
| 3. |
|
|
| 4. |
- Abdulla, Parosh Aziz, et al.
(author)
-
Mending fences with self-invalidation and self-downgrade
- 2018
-
In: Logical Methods in Computer Science. - 1860-5974. ; 14:1
-
Journal article (peer-reviewed)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.
|
|
| 5. |
- Abdulla, Parosh Aziz, Professor, et al.
(author)
-
Model checking parameterized systems
- 2018
-
In: Handbook of Model Checking. - Cham : Springer. - 9783319105741 ; , s. 685-725
-
Book chapter (peer-reviewed)
|
|
| 6. |
- Abdulla, Parosh Aziz, Professor, et al.
(author)
-
Replacing store buffers by load buffers in TSO
- 2018
-
In: Verification and Evaluation of Computer and Communication Systems. - Cham : Springer. - 9783030003586 - 9783030003593 ; , s. 22-28
-
Conference paper (peer-reviewed)abstract
- We consider the weak memory model of Total Store Ordering (TSO). In the classical definition of TSO, an unbounded buffer is inserted between each process and the shared memory. The buffers contains pending store operations of the processes. We introduce a new model where we replace the store buffers by load buffers. In contrast to the classical model, the buffers now contain load operations. We show that the models have equivalent behaviors in the sense that the processes reach identical sets of states when the input program is run under the two models.
|
|
| 7. |
- Abdulla, Parosh Aziz, Professor, et al.
(author)
-
TRAU : SMT solver for string constraints
- 2018
-
In: PROCEEDINGS OF THE 2018 18TH CONFERENCE ON FORMAL METHODS IN COMPUTER AIDED DESIGN (FMCAD). - : IEEE. - 9780983567882 ; , s. 165-169
-
Conference paper (peer-reviewed)abstract
- We introduce TRAU, an SMT solver for an expressive constraint language, including word equations, length constraints, context-free membership queries, and transducer constraints. The satisfiability problem for such a class of constraints is in general undecidable. The key idea behind TRAU is a technique called flattening, which searches for satisfying assignments that follow simple patterns. TRAU implements a Counter-Example Guided Abstraction Refinement (CEGAR) framework which contains both an under- and an over-approximation module. The approximations are refined in an automatic manner by information flow between the two modules. The technique implemented by TRAU can handle a rich class of string constraints and has better performance than state-of-the-art string solvers.
|
|
| 8. |
- Abdulla, Parosh Aziz, Professor, et al.
(author)
-
Universal safety for timed Petri nets is PSPACE-complete
- 2018
-
In: 29th International Conference on Concurrency Theory. - Dagstuhl, Germany : Leibniz-Zentrum für Informatik. - 9783959770873 ; , s. 6:1-15
-
Conference paper (peer-reviewed)
|
|
| 9. |
- Abdulla, Parosh Aziz, Professor, et al.
(author)
-
Verification of timed asynchronous programs
- 2018
-
In: IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science. - Dagstuhl, Germany : Leibniz-Zentrum für Informatik. - 9783959770934 ; , s. 8:1-16
-
Conference paper (peer-reviewed)
|
|
| 10. |
- Abdulla, Parosh, 1961-, et al.
(author)
-
Optimal Stateless Model Checking under the Release-Acquire Semantics
- 2018
-
In: SPLASH OOPSLA 2018, Boston, Nov 4-9, 2018. - : ACM Digital Library.
-
Conference paper (peer-reviewed)abstract
- We present a framework for efficient application of stateless model checking (SMC) to concurrent programs running under the Release-Acquire (RA) fragment of the C/C++11 memory model. Our approach is based on exploring the possible program orders, which define the order in which instructions of a thread are executed, and read-from relations, which define how reads obtain their values from writes. This is in contrast to previous approaches, which in addition explore the possible coherence orders, i.e., orderings between conflicting writes. Since unexpected test results such as program crashes or assertion violations depend only on the read-from relation, we avoid a potentially large source of redundancy. Our framework is based on a novel technique for determining whether a particular read-from relation is feasible under the RA semantics. We define an SMC algorithm which is provably optimal in the sense that it explores each program order and read-from relation exactly once. This optimality result is strictly stronger than previous analogous optimality results, which also take coherence order into account. We have implemented our framework in the tool Tracer. Experiments show that Tracer can be significantly faster than state-of-the-art tools that can handle the RA semantics.
|
|
