1,721,079 research outputs found
Reducing Context-Bounded Concurrent Reachability to Sequential Reachability
Get PDFWe give a translation from concurrent programs to sequential programs that reduces the context-bounded reachability problem in the concurrent program to a reachability problem in the sequential one. The translation has two salient features: (a) the sequential program tracks, at any time, the local state of only one thread (though it does track multiple copies of shared variables), and (b) all reachable states of the sequential program correspond to reachable states of the concurrent program. We also implement our transformation in the setting of concurrent recursive programs with finite data domains, and show that the resulting sequential program can be model-checked efficiently using existing recursive sequential program reachability tools
Model-Checking Parameterized Concurrent Programs Using Linear Interfaces
No full textWe consider the verification of parameterized Boolean programs— abstractions of shared-memory concurrent programs with an unbounded number of threads. We propose that such programs can be model-checked by iteratively considering the program under k-round schedules, for increasing values of k, using a novel compositional construct called linear interfaces that summarize the effect of a block of threads in a k-round schedule. We also develop a game-theoretic sound technique to show that k rounds of schedule suffice to explore the entire search-space, which allows us to prove a parameterized program entirely correct. We implement a symbolic model-checker, and report on experiments verifying parameterized predicate abstractions of Linux device drivers interacting with a kernel to show the efficacy of our technique
The Language Theory of Bounded Context-Switching
No full textConcurrent compositions of recursive programs with finite data are a natural abstraction model for concurrent programs. Since reachability is undecidable for this class, a restricted form of reachability has become popular in the formal verification literature, where the set of states reached within k context-switches, for a fixed small constant k, is explored. In this paper, we consider the language theory of these models: concurrent recursive programs with finite data domains that communicate using shared memory and work within k round-robin rounds of context-switches, and where further the stack operations are made visible (as in visibly pushdown automata). We show that the corresponding class of languages, for any fixed k, forms a robust subclass of context-sensitive languages, closed under all the Boolean operations. Our main technical contribution is to show that these automata are determinizable as well. This is the first class we are aware of that includes non-context-free languages, and yet has the above properties
An Infinite Automaton Characterization of Double Exponential Time
No full textInfinite-state automata are a new invention: they are automata that have an infinite number of states represented by words, transitions defined using rewriting, and with sets of initial and final states. Infinite-state automata have gained recent interest due to a remarkable result by Morvan and Stirling, which shows that automata with transitions defined using rational rewriting precisely capture context-sensitive (NLinSpace) languages. In this paper, we show that infinite automata defined using a form of multi-stack rewriting precisely defines double exponential time (more precisely, 2ETime, the class of problems solvable in 22O(n) time). The salient aspect of this characterization is that the automata have no ostensible limits on time nor space, and neither direction of containment with respect to 2ETime is obvious. In this sense, the result captures the complexity class qualitatively, by restricting the power of rewriting
Sequentializing parameterized programs
No full textWe exhibit assertion-preserving (reachability-preserving) transformations from parameterized concurrent shared-memory programs, under a k-round scheduling of processes, to sequential programs. The salient feature of the sequential program is that it tracks the local variables of only one thread at any point, and uses only O(k) copies of shared variables (it does not use extra counters, not even one counter to keep track of the number of threads). Sequentialization is achieved using the concept of a linear interface that captures the effect an unbounded block of processes have on the shared state in a k-round schedule. Linear interfaces in fact serve as summaries for parallel processes, and the sequentialization compiles these linear interfaces to procedural summaries in the sequential program. Our transformation utilizes linear interfaces to sequentialize the program, and to ensure the sequential program explores only reachable states and preserves local invariants
The tree width of auxiliary storage
Get PDFWe propose a generalization of results on the decidability of emptiness for several restricted classes of sequential and distributed automata with auxiliary storage (stacks, queues) that have recently been proved. Our generalization relies on reducing emptiness of these automata to finite-state graph automata (without storage) restricted to monadic second-order (MSO) definable graphs of bounded tree-width, where the graph structure encodes the mechanism provided by the auxiliary storage. Our results outline a uniform mechanism to derive emptiness algorithms for automata, explaining and simplifying several existing results, as well as proving new decidability results
Context-Bounded Analysis of Concurrent Queue Systems
No full textWe show that the bounded context-switching reachability problem for concurrent finite systems communicating using unbounded FIFO queues is decidable, where in each context a process reads from only one queue (but is allowed to write onto all other queues). Our result also holds when individual processes are finite-state recursive programs provided a process dequeues messages only when its local stack is empty. We then proceed to classify architectures that admit a decidable (unbounded context switching) reachability problem, using the decidability of bounded context switching. We show that the precise class of decidable architectures for recursive programs are the forest architectures, while the decidable architectures for non-recursive programs are those that do not have an undirected cycle
Decidable logics combining heap structures and data
No full textWe define a new logic, STRAND, that allows reasoning with heap-manipulating programs using deductive verification and SMT solvers. STRAND logic (“STRucture ANd Data” logic) formulas express constraints involving heap structures and the data they contain; they are defined over a class of pointer-structures R defined using MSO-defined relations over trees, and are of the form ?x?y.?(x, y), where ? is a monadic second-order logic (MSO) formula with additional quantification that combines structural constraints as well as data-constraints, but where the data-constraints are only allowed to refer to x and y. The salient aspects of the logic are: (a) the logic is powerful, allowing existential and universal quantification over the nodes, and complex combinations of data and structural constraints; (b) checking Hoare-triples for linear blocks of statements with pre-conditions and post-conditions expressed as Boolean combinations of existential and universal STRAND formulas reduces to satisfiability of a STRAND formula; (c) there are powerful decidable fragments of STRAND, one semantically defined and one syntactically defined, where the decision procedure works by combining the theory of MSO over trees and the quantifier-free theory of the underlying data-logic. We demonstrate the effectiveness and practicality of the logic by checking verification conditions generated in proving properties of several heap-manipulating programs, using a tool that combines an MSO decision procedure over trees (MONA) with an SMT solver for integer constraints (Z3)
Modular Strategies for Infinite Games on Recursive Graphs
Get PDFIn this paper, we focus on solving games in recursive game graphs that can model the control flow of sequential programs with recursive procedure calls. The winning condition is given as an ω-regular specification over the observable, and, unlike traditional pushdown games, the strategy is required to be modular: resolution of choices within a component should not depend on the context in which the component is invoked, but only on the history within the current invocation of the component. We first consider the case when the specification is given as a deterministic Büchi automaton. We show the problem to be decidable, and present a solution based on two-way alternating tree automata with time complexity that is polynomial in the number of internal nodes, exponential in the specification and exponential in the number of exits of the components. We show that the problem is EXPTIME-complete in general, and NP-complete for fixed-size specifications. Then, we show that the same complexity bounds apply if the specification is given as a universal co-Büchi automaton. Finally, for specifications given as formulas of linear temporal logic LTL, we obtain a synthesis algorithm that is doubly-exponential in the formula and singly exponential in the number of exits of components
- …
