arXiv subjects

Parosh Aziz Abdulla

Publications and source records attributed to Parosh Aziz Abdulla.

At least 37 records · Page 2Linked to original sources

arXiv2020

The Decidability of Verification under Promising 2.0

In PLDI'20, Lee et al. introduced the \emph{promising } semantics PS 2.0 of the C++ concurrency that captures most of the common program transformations while satisfying the DRF guarantee. The reachability problem for finite-state programs under PS 2.0 with only release-acquire accesses is already known to be undecidable. Therefore, we address, in this paper, the reachability problem for programs running under PS 2.0 with relaxed accesses together with promises. We show that this problem is undecidable even in the case where the input program has finite state. Given this undecidability result, we consider the fragment of PS 2.0 with only relaxed accesses allowing bounded number of promises. We show that under this restriction, the reachability is decidable, albeit very expensive: it is non-primitive recursive. Given this high complexity with bounded number of promises and the undecidability result for the RA fragment of PS 2.0, we consider a bounded version of the reachability problem. To this end, we bound both the number of promises and the "view-switches", i.e, the number of times the processes may switch their local views of the global memory. We provide a code-to-code translation from an input program under PS 2.0, with relaxed and release-acquire memory accesses along with promises, to a program under SC. This leads to a reduction of the bounded reachability problem under PS 2.0 to the bounded context-switching problem under SC. We have implemented a prototype tool and tested it on a set of benchmarks, demonstrating that many bugs in programs can be found using a small bound.

cs.PL↗

arXiv2020

On the Separability Problem of String Constraints

We address the separability problem for straight-line string constraints. The separability problem for languages of a class C by a class S asks: given two languages A and B in C, does there exist a language I in S separating A and B (i.e., I is a superset of A and disjoint from B)? The separability of string constraints is the same as the fundamental problem of interpolation for string constraints. We first show that regular separability of straight line string constraints is undecidable. Our second result is the decidability of the separability problem for straight-line string constraints by piece-wise testable languages, though the precise complexity is open. In our third result, we consider the positive fragment of piece-wise testable languages as a separator, and obtain an EXPSPACE algorithm for the separability of a useful class of straight-line string constraints, and a PSPACE-hardness result.

cs.FL↗

arXiv2019

Context-Bounded Model Checking for POWER

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 intitiated 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.

cs.PL↗

arXiv2018

Optimal Stateless Model Checking under the Release-Acquire Semantics

We present a framework for the 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 specify how reads obtain their values from writes. This is in contrast to previous approaches, which also 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 significant 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.

cs.PL↗

arXiv2018

Universal Safety for Timed Petri Nets is PSPACE-complete

A timed network consists of an arbitrary number of initially identical 1-clock timed automata, interacting via hand-shake communication. In this setting there is no unique central controller, since all automata are initially identical. We consider the universal safety problem for such controller-less timed networks, i.e., verifying that a bad event (enabling some given transition) is impossible regardless of the size of the network. This universal safety problem is dual to the existential coverability problem for timed-arc Petri nets, i.e., does there exist a number $m$ of tokens, such that starting with $m$ tokens in a given place, and none in the other places, some given transition is eventually enabled. We show that these problems are PSPACE-complete.

cs.LO↗

arXiv2018

Communicating Timed Processes with Perfect Timed Channels

We introduce the model of communicating timed automata (CTA) that extends the classical models of finite-state processes communicating through FIFO perfect channels and timed automata, in the sense that the finite-state processes are replaced by timed automata, and messages inside the perfect channels are equipped with clocks representing their ages. In addition to the standard operations (resetting clocks, checking guards of clocks) each automaton can either (1) append a message to the tail of a channel with an initial age or (2) receive the message at the head of a channel if its age satisfies a set of given constraints. In this paper, we show that the reachability problem is undecidable even in the case of two timed automata connected by one unidirectional timed channel if one allows global clocks (that the two automata can check and manipulate). We prove that this undecidability still holds even for CTA consisting of three timed automata and two unidirectional timed channels (and without any global clock). However, the reachability problem becomes decidable (in $\mathsf{EXPTIME}$) in the case of two automata linked with one unidirectional timed channel and with no global clock. Finally, we consider the bounded-context case, where in each context, only one timed automaton is allowed to receive messages from one channel while being able to send messages to all the other timed channels. In this case we show that the reachability problem is decidable.

cs.FL↗

arXiv2018

A Load-Buffer Semantics for Total Store Ordering

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.

cs.FL↗

arXiv2018

Mending Fences with Self-Invalidation and Self-Downgrade

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.

cs.LO↗

arXiv2016

Stateless Model Checking for POWER

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 an axiomatic model of POWER. 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.

cs.LO↗

arXiv2016

Recency-Bounded Verification of Dynamic Database-Driven Systems (Extended Version)

We propose a formalism to model database-driven systems, called database manipulating systems (DMS). The actions of a DMS modify the current instance of a relational database by adding new elements into the database, deleting tuples from the relations and adding tuples to the relations. The elements which are modified by an action are chosen by (full) first-order queries. DMS is a highly expressive model and can be thought of as a succinct representation of an infinite state relational transition system, in line with similar models proposed in the literature. We propose monadic second order logic (MSO-FO) to reason about sequences of database instances appearing along a run. Unsurprisingly, the linear-time model checking problem of DMS against MSO-FO is undecidable. Towards decidability, we propose under-approximate model checking of DMS, where the under-approximation parameter is the "bound on recency". In a $k$-recency-bounded run, only the most recent $k$ elements in the current active domain may be modified by an action. More runs can be verified by increasing the bound on recency. Our main result shows that recency-bounded model checking of DMS against MSO-FO is decidable, by a reduction to the satisfiability problem of MSO over nested words.

cs.DB↗

arXiv2016

Qualitative Analysis of VASS-Induced MDPs

We consider infinite-state Markov decision processes (MDPs) that are induced by extensions of vector addition systems with states (VASS). Verification conditions for these MDPs are described by reachability and Buchi objectives w.r.t. given sets of control-states. We study the decidability of some qualitative versions of these objectives, i.e., the decidability of whether such objectives can be achieved surely, almost-surely, or limit-surely. While most such problems are undecidable in general, some are decidable for large subclasses in which either only the controller or only the random environment can change the counter values (while the other side can only change control-states).

cs.LO↗

arXiv2015

Stochastic Parity Games on Lossy Channel Systems

We give an algorithm for solving stochastic parity games with almost-sure winning conditions on {\it lossy channel systems}, under the constraint that both players are restricted to finite-memory strategies. First, we describe a general framework, where we consider the class of 2 1/2-player games with almost-sure parity winning conditions on possibly infinite game graphs, assuming that the game contains a {\it finite attractor}. An attractor is a set of states (not necessarily absorbing) that is almost surely re-visited regardless of the players' decisions. We present a scheme that characterizes the set of winning states for each player. Then, we instantiate this scheme to obtain an algorithm for {\it stochastic game lossy channel systems}.

cs.LO↗

arXiv2014

Infinite-State Energy Games

Energy games are a well-studied class of 2-player turn-based games on a finite graph where transitions are labeled with integer vectors which represent changes in a multidimensional resource (the energy). One player tries to keep the cumulative changes non-negative in every component while the other tries to frustrate this. We consider generalized energy games played on infinite game graphs induced by pushdown automata (modelling recursion) or their subclass of one-counter automata. Our main result is that energy games are decidable in the case where the game graph is induced by a one-counter automaton and the energy is one-dimensional. On the other hand, every further generalization is undecidable: Energy games on one-counter automata with a 2-dimensional energy are undecidable, and energy games on pushdown automata are undecidable even if the energy is one-dimensional. Furthermore, we show that energy games and simulation games are inter-reducible, and thus we additionally obtain several new (un)decidability results for the problem of checking simulation preorder between pushdown automata and vector addition systems.

cs.GT↗

arXiv2014

Zenoness for Timed Pushdown Automata

Timed pushdown automata are pushdown automata extended with a finite set of real-valued clocks. Additionaly, each symbol in the stack is equipped with a value representing its age. The enabledness of a transition may depend on the values of the clocks and the age of the topmost symbol. Therefore, dense-timed pushdown automata subsume both pushdown automata and timed automata. We have previously shown that the reachability problem for this model is decidable. In this paper, we study the zenoness problem and show that it is EXPTIME-complete.

cs.FL↗

arXiv2013

Priced Timed Petri Nets

We consider priced timed Petri nets, i.e., unbounded Petri nets where each token carries a real-valued clock. Transition arcs are labeled with time intervals, which specify constraints on the ages of tokens. Furthermore, our cost model assigns token storage costs per time unit to places, and firing costs to transitions. This general model strictly subsumes both priced timed automata and unbounded priced Petri nets. We study the cost of computations that reach a given control-state. In general, a computation with minimal cost may not exist, due to strict inequalities in the time constraints. However, we show that the infimum of the costs to reach a given control-state is computable in the case where all place and transition costs are non-negative. On the other hand, if negative costs are allowed, then the question whether a given control-state is reachable with zero overall cost becomes undecidable. In fact, this negative result holds even in the simpler case of discrete time (i.e., integer-valued clocks).

cs.LO↗

arXiv2013

Stochastic Parity Games on Lossy Channel Systems

We give an algorithm for solving stochastic parity games with almost-sure winning conditions on lossy channel systems, for the case where the players are restricted to finite-memory strategies. First, we describe a general framework, where we consider the class of 2.5-player games with almost-sure parity winning conditions on possibly infinite game graphs, assuming that the game contains a finite attractor. An attractor is a set of states (not necessarily absorbing) that is almost surely re-visited regardless of the players' decisions. We present a scheme that characterizes the set of winning states for each player. Then, we instantiate this scheme to obtain an algorithm for stochastic game lossy channel systems.

cs.GT↗

arXiv2013

Solving Parity Games on Integer Vectors

We consider parity games on infinite graphs where configurations are represented by control-states and integer vectors. This framework subsumes two classic game problems: parity games on vector addition systems with states (vass) and multidimensional energy parity games. We show that the multidimensional energy parity game problem is inter-reducible with a subclass of single-sided parity games on vass where just one player can modify the integer counters and the opponent can only change control-states. Our main result is that the minimal elements of the upward-closed winning set of these single-sided parity games on vass are computable. This implies that the Pareto frontier of the minimal initial credit needed to win multidimensional energy parity games is also computable, solving an open question from the literature. Moreover, our main result implies the decidability of weak simulation preorder/equivalence between finite-state systems and vass, and the decidability of model checking vass with a large fragment of the modal mu-calculus.

cs.LO↗

arXiv2013

Petri Nets with Time and Cost

We consider timed Petri nets, i.e., unbounded Petri nets where each token carries a real-valued clock. Transition arcs are labeled with time intervals, which specify constraints on the ages of tokens. Our cost model assigns token storage costs per time unit to places, and firing costs to transitions. We study the cost to reach a given control-state. In general, a cost-optimal run may not exist. However,we show that the infimum of the costs is computable.

cs.LO↗