| 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)
-
Chain-Free String Constraints
- 2019
-
In: Automated Technology for Verification and Analysis. - Cham : Springer. - 9783030317836 - 9783030317843 ; , s. 277-293
-
Conference paper (peer-reviewed)abstract
- We address the satisfiability problem for string constraints that combine relational constraints represented by transducers, word equations, and string length constraints. This problem is undecidable in general. Therefore, we propose a new decidable fragment of string constraints, called weakly chaining string constraints, for which we show that the satisfiability problem is decidable. This fragment pushes the borders of decidability of string constraints by generalising the existing straight-line as well as the acyclic fragment of the string logic. We have developed a prototype implementation of our new decision procedure, and integrated it into in an existing framework that uses CEGAR with under-approximation of string constraints based on flattening. Our experimental results show the competitiveness and accuracy of the new framework.
|
|
| 3. |
- 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.
|
|
| 4. |
- Abdulla, Parosh Aziz, et al.
(author)
-
Context-bounded analysis for POWER
- 2017
-
In: Tools and Algorithms for the Construction and Analysis of Systems. - Berlin, Heidelberg : Springer. - 9783662545799 ; , s. 56-74
-
Conference paper (peer-reviewed)abstract
- We propose an under-approximate reachability analysis algorithm for programs running under the POWER memory model, in the spirit of the work on context-bounded analysis initiated by Qadeer et al. in 2005 for detecting bugs in concurrent programs (supposed to be running under the classical SC model). To that end, we first introduce a new notion of context-bounding that is suitable for reasoning about computations under POWER, which generalizes the one defined by Atig et al. in 2011 for the TSO memory model. Then, we provide a polynomial size reduction of the context-bounded state reachability problem under POWER to the same problem under SC: Given an input concurrent program P, our method produces a concurrent program P' such that, for a fixed number of context switches, running P' under SC yields the same set of reachable states as running P under POWER. The generated program P' contains the same number of processes as P and operates on the same data domain. By leveraging the standard model checker CBMC, we have implemented a prototype tool and applied it on a set of benchmarks, showing the feasibility of our approach.
|
|
| 5. |
|
|
| 6. |
- Abdulla, Parosh Aziz, et al.
(author)
-
Data Communicating Processes with Unreliable Channels
- 2016
-
In: Proceedings Of The 31St Annual ACM-IEEE Symposium On Logic In Computer Science (LICS 2016). - 9781450343916 ; , s. 166-175
-
Conference paper (peer-reviewed)abstract
- We extend the classical model of lossy channel systems by considering systems that operate on a finite set of variables ranging over an infinite data domain. Furthermore, each message inside a channel is equipped with a data item representing its value. Although we restrict the model by allowing the variables to be only tested for (dis-)equality, we show that the state reachability problem is undecidable. In light of this negative result, we consider bounded-phase reachability, where the processes are restricted to performing either send or receive operations during each phase. We show decidability of state reachability in this case by computing a symbolic encoding of the set of system configurations that are reachable from a given configuration.
|
|
| 7. |
- Abdulla, Parosh Aziz, Professor, 1961-, et al.
(author)
-
Dynamic Partial Order Reduction Under the Release-Acquire Semantics (Tutorial)
- 2019
-
In: Networked Systems. - Cham : Springer Nature. - 9783030312770 - 9783030312763 ; , s. 3-18
-
Conference paper (peer-reviewed)abstract
- We describe at a high-level the main concepts in the Release-Acquire (RA) semantics that is part of the C11 language. Furthermore, we describe the ideas behind an optimal dynamic partial order reduction technique that can be used for systematic analysis of concurrent programs running under RA. This tutorial is based on the material presented in [5], which also contains the formal definitions of all the models, concepts, and algorithms.
|
|
| 8. |
|
|
| 9. |
- Abdulla, Parosh Aziz, 1961-, et al.
(author)
-
Flatten and Conquer : A Framework for Efficient Analysis of String Constraints
- 2017
-
In: SIGPLAN notices. - New York, NY, USA : ACM. - 0362-1340 .- 1558-1160. - 9781450349888 ; 52:6, s. 602-617, s. 602-617
-
Journal article (peer-reviewed)abstract
- We describe a uniform and efficient framework for checking the satisfiability of a large class of string constraints. The framework is based on the observation that both satisfiability and unsatisfiability of common constraints can be demonstrated through witnesses with simple patterns. These patterns are captured using flat automata each of which consists of a sequence of simple loops. We build a Counter-Example Guided Abstraction Refinement (CEGAR) framework which contains both an under-and an over-approximation module. The flow of information between the modules allows to increase the precision in an automatic manner. We have implemented the framework as a tool and performed extensive experimentation that demonstrates both the generality and efficiency of our method.
|
|
| 10. |
|
|
