-
PrideMM: A Solver for Relaxed Memory Models
Authors:
Simon Cooksey,
Sarah Harris,
Mark Batty,
Radu Grigore,
Mikoláš Janota
Abstract:
Relaxed memory models are notoriously delicate. To ease their study, several ad hoc simulators have been developed for axiomatic memory models. We show how axiomatic memory models can be simulated using a solver for $\exists$SO. Further, we show how memory models based on event structures can be simulated using a solver for MSO. Finally, we present a solver for SO, built on top of QBF solvers.
Relaxed memory models are notoriously delicate. To ease their study, several ad hoc simulators have been developed for axiomatic memory models. We show how axiomatic memory models can be simulated using a solver for $\exists$SO. Further, we show how memory models based on event structures can be simulated using a solver for MSO. Finally, we present a solver for SO, built on top of QBF solvers.
△ Less
Submitted 7 December, 2018;
originally announced January 2019.
-
Selective Monitoring
Authors:
Radu Grigore,
Stefan Kiefer
Abstract:
We study selective monitors for labelled Markov chains. Monitors observe the outputs that are generated by a Markov chain during its run, with the goal of identifying runs as correct or faulty. A monitor is selective if it skips observations in order to reduce monitoring overhead. We are interested in monitors that minimize the expected number of observations. We establish an undecidability result…
▽ More
We study selective monitors for labelled Markov chains. Monitors observe the outputs that are generated by a Markov chain during its run, with the goal of identifying runs as correct or faulty. A monitor is selective if it skips observations in order to reduce monitoring overhead. We are interested in monitors that minimize the expected number of observations. We establish an undecidability result for selectively monitoring general Markov chains. On the other hand, we show for non-hidden Markov chains (where any output identifies the state the Markov chain is in) that simple optimal monitors exist and can be computed efficiently, based on DFA language equivalence. These monitors do not depend on the precise transition probabilities in the Markov chain. We report on experiments where we compute these monitors for several open-source Java projects.
△ Less
Submitted 2 July, 2018; v1 submitted 15 June, 2018;
originally announced June 2018.
-
On the Quest for an Acyclic Graph
Authors:
Mikolas Janota,
Radu Grigore,
Vasco Manquinho
Abstract:
The paper aims at finding acyclic graphs under a given set of constraints. More specifically, given a propositional formula φ over edges of a fixed-size graph, the objective is to find a model of φ that corresponds to a graph that is acyclic. The paper proposes several encodings of the problem and compares them in an experimental evaluation using stateof-the-art SAT solvers.
The paper aims at finding acyclic graphs under a given set of constraints. More specifically, given a propositional formula φ over edges of a fixed-size graph, the objective is to find a model of φ that corresponds to a graph that is acyclic. The paper proposes several encodings of the problem and compares them in an experimental evaluation using stateof-the-art SAT solvers.
△ Less
Submitted 9 October, 2017; v1 submitted 5 August, 2017;
originally announced August 2017.
-
Java Generics are Turing Complete
Authors:
Radu Grigore
Abstract:
This paper describes a reduction from the halting problem of Turing machines to subtype checking in Java. It follows that subtype checking in Java is undecidable, which answers a question posed by Kennedy and Pierce in 2007. It also follows that Java's type checker can recognize any recursive language, which improves a result of Gil and Levy from 2016. The latter point is illustrated by a parser g…
▽ More
This paper describes a reduction from the halting problem of Turing machines to subtype checking in Java. It follows that subtype checking in Java is undecidable, which answers a question posed by Kennedy and Pierce in 2007. It also follows that Java's type checker can recognize any recursive language, which improves a result of Gil and Levy from 2016. The latter point is illustrated by a parser generator for fluent interfaces.
△ Less
Submitted 7 November, 2016; v1 submitted 17 May, 2016;
originally announced May 2016.
-
Abstraction Refinement Guided by a Learnt Probabilistic Model
Authors:
Radu Grigore,
Hongseok Yang
Abstract:
The core challenge in designing an effective static program analysis is to find a good program abstraction -- one that retains only details relevant to a given query. In this paper, we present a new approach for automatically finding such an abstraction. Our approach uses a pessimistic strategy, which can optionally use guidance from a probabilistic model. Our approach applies to parametric static…
▽ More
The core challenge in designing an effective static program analysis is to find a good program abstraction -- one that retains only details relevant to a given query. In this paper, we present a new approach for automatically finding such an abstraction. Our approach uses a pessimistic strategy, which can optionally use guidance from a probabilistic model. Our approach applies to parametric static analyses implemented in Datalog, and is based on counterexample-guided abstraction refinement. For each untried abstraction, our probabilistic model provides a probability of success, while the size of the abstraction provides an estimate of its cost in terms of analysis time. Combining these two metrics, probability and cost, our refinement algorithm picks an optimal abstraction. Our probabilistic model is a variant of the Erdos-Renyi random graph model, and it is tunable by what we call hyperparameters. We present a method to learn good values for these hyperparameters, by observing past runs of the analysis on an existing codebase. We evaluate our approach on an object sensitive pointer analysis for Java programs, with two client analyses (PolySite and Downcast).
△ Less
Submitted 10 November, 2015; v1 submitted 5 November, 2015;
originally announced November 2015.
-
Tree Buffers
Authors:
Radu Grigore,
Stefan Kiefer
Abstract:
In runtime verification, the central problem is to decide if a given program execution violates a given property. In online runtime verification, a monitor observes a program's execution as it happens. If the program being observed has hard real-time constraints, then the monitor inherits them. In the presence of hard real-time constraints it becomes a challenge to maintain enough information to p…
▽ More
In runtime verification, the central problem is to decide if a given program execution violates a given property. In online runtime verification, a monitor observes a program's execution as it happens. If the program being observed has hard real-time constraints, then the monitor inherits them. In the presence of hard real-time constraints it becomes a challenge to maintain enough information to produce error traces, should a property violation be observed. In this paper we introduce a data structure, called tree buffer, that solves this problem in the context of automata-based monitors: If the monitor itself respects hard real-time constraints, then enriching it by tree buffers makes it possible to provide error traces, which are essential for diagnosing defects. We show that tree buffers are also useful in other application domains. For example, they can be used to implement functionality of capturing groups in regular expressions. We prove optimal asymptotic bounds for our data structure, and validate them using empirical data from two sources: regular expression searching through Wikipedia, and runtime verification of execution traces obtained from the DaCapo test suite.
△ Less
Submitted 14 May, 2015; v1 submitted 18 April, 2015;
originally announced April 2015.
-
Proving the Herman-Protocol Conjecture
Authors:
Maria Bruna,
Radu Grigore,
Stefan Kiefer,
Joël Ouaknine,
James Worrell
Abstract:
Herman's self-stabilisation algorithm, introduced 25 years ago, is a well-studied synchronous randomised protocol for enabling a ring of $N$ processes collectively holding any odd number of tokens to reach a stable state in which a single token remains. Determining the worst-case expected time to stabilisation is the central outstanding open problem about this protocol. It is known that there is a…
▽ More
Herman's self-stabilisation algorithm, introduced 25 years ago, is a well-studied synchronous randomised protocol for enabling a ring of $N$ processes collectively holding any odd number of tokens to reach a stable state in which a single token remains. Determining the worst-case expected time to stabilisation is the central outstanding open problem about this protocol. It is known that there is a constant $h$ such that any initial configuration has expected stabilisation time at most $h N^2$. Ten years ago, McIver and Morgan established a lower bound of $4/27 \approx 0.148$ for $h$, achieved with three equally-spaced tokens, and conjectured this to be the optimal value of $h$. A series of papers over the last decade gradually reduced the upper bound on $h$, with the present record (achieved in 2014) standing at approximately $0.156$. In this paper, we prove McIver and Morgan's conjecture and establish that $h = 4/27$ is indeed optimal.
△ Less
Submitted 27 April, 2016; v1 submitted 5 April, 2015;
originally announced April 2015.
-
On QBF Proofs and Preprocessing
Authors:
Mikolas Janota,
Radu Grigore,
Joao Marques-Silva
Abstract:
QBFs (quantified boolean formulas), which are a superset of propositional formulas, provide a canonical representation for PSPACE problems. To overcome the inherent complexity of QBF, significant effort has been invested in develo** QBF solvers as well as the underlying proof systems. At the same time, formula preprocessing is crucial for the application of QBF solvers. This paper focuses on a m…
▽ More
QBFs (quantified boolean formulas), which are a superset of propositional formulas, provide a canonical representation for PSPACE problems. To overcome the inherent complexity of QBF, significant effort has been invested in develo** QBF solvers as well as the underlying proof systems. At the same time, formula preprocessing is crucial for the application of QBF solvers. This paper focuses on a missing link in currently-available technology: How to obtain a certificate (e.g. proof) for a formula that had been preprocessed before it was given to a solver? The paper targets a suite of commonly-used preprocessing techniques and shows how to reconstruct certificates for them. On the negative side, the paper discusses certain limitations of the currently-used proof systems in the light of preprocessing. The presented techniques were implemented and evaluated in the state-of-the-art QBF preprocessor bloqqer.
△ Less
Submitted 9 October, 2013;
originally announced October 2013.
-
Runtime Verification Based on Register Automata
Authors:
Radu Grigore,
Dino Distefano,
Rasmus Lerchedahl Petersen,
Nikos Tzevelekos
Abstract:
We propose TOPL automata as a new method for runtime verification of systems with unbounded resource generation. Paradigmatic such systems are object-oriented programs which can dynamically generate an unbounded number of fresh object identities during their execution. Our formalism is based on register automata, a particularly successful approach in automata over infinite alphabets which administ…
▽ More
We propose TOPL automata as a new method for runtime verification of systems with unbounded resource generation. Paradigmatic such systems are object-oriented programs which can dynamically generate an unbounded number of fresh object identities during their execution. Our formalism is based on register automata, a particularly successful approach in automata over infinite alphabets which administers a finite-state machine with boundedly many input-storing registers. We show that TOPL automata are equally expressive to register automata and yet suitable to express properties of programs. Compared to other runtime verification methods, our technique can handle a class of properties beyond the reach of current tools. We show in particular that properties which require value updates are not expressible with current techniques yet are naturally captured by TOPL machines. On the practical side, we present a tool for runtime verification of Java programs via TOPL properties, where the trade-off between the coverage and the overhead of the monitoring system is tunable by means of a number of parameters. We validate our technique by checking properties involving multiple objects and chaining of values on large open source projects.
△ Less
Submitted 20 January, 2015; v1 submitted 24 September, 2012;
originally announced September 2012.
-
History-Register Automata
Authors:
Radu Grigore,
Nikos Tzevelekos
Abstract:
Programs with dynamic allocation are able to create and use an unbounded number of fresh resources, such as references, objects, files, etc. We propose History-Register Automata (HRA), a new automata-theoretic formalism for modelling such programs. HRAs extend the expressiveness of previous approaches and bring us to the limits of decidability for reachability checks. The distinctive feature of o…
▽ More
Programs with dynamic allocation are able to create and use an unbounded number of fresh resources, such as references, objects, files, etc. We propose History-Register Automata (HRA), a new automata-theoretic formalism for modelling such programs. HRAs extend the expressiveness of previous approaches and bring us to the limits of decidability for reachability checks. The distinctive feature of our machines is their use of unbounded memory sets (histories) where input symbols can be selectively stored and compared with symbols to follow. In addition, stored symbols can be consumed or deleted by reset. We show that the combination of consumption and reset capabilities renders the automata powerful enough to imitate counter machines, and yields closure under all regular operations apart from complementation. We moreover examine weaker notions of HRAs which strike different balances between expressiveness and effectiveness.
△ Less
Submitted 29 March, 2016; v1 submitted 4 September, 2012;
originally announced September 2012.
-
The Design and Algorithms of a Verification Condition Generator
Authors:
Radu Grigore
Abstract:
This dissertation discusses several problems loosely related, because they all involve a verification condition generator. The Boogie language is introduced; the architecture of a verification-generator is described. Then come more interesting parts. (1) Moving to a passive form representation can be seen as an automatic transformation into a pure functional language. How to formalize this transfo…
▽ More
This dissertation discusses several problems loosely related, because they all involve a verification condition generator. The Boogie language is introduced; the architecture of a verification-generator is described. Then come more interesting parts. (1) Moving to a passive form representation can be seen as an automatic transformation into a pure functional language. How to formalize this transformation and what is its complexity? (2) How do various ways of describing the semantics of procedural languages (predicate transformers, operational semantics) relate to each other? (3) How to do incremental verification? That is, how to work less when re-verifying a program that changed only a little since the verifier was last run. (4) How to detect unreachable code, taking into account formal specifications?
△ Less
Submitted 30 April, 2012;
originally announced April 2012.
-
Counterexample Guided Abstraction Refinement Algorithm for Propositional Circumscription
Authors:
Mikoláš Janota,
Joao Marques-Silva,
Radu Grigore
Abstract:
Circumscription is a representative example of a nonmonotonic reasoning inference technique. Circumscription has often been studied for first order theories, but its propositional version has also been the subject of extensive research, having been shown equivalent to extended closed world assumption (ECWA). Moreover, entailment in propositional circumscription is a well-known example of a decisio…
▽ More
Circumscription is a representative example of a nonmonotonic reasoning inference technique. Circumscription has often been studied for first order theories, but its propositional version has also been the subject of extensive research, having been shown equivalent to extended closed world assumption (ECWA). Moreover, entailment in propositional circumscription is a well-known example of a decision problem in the second level of the polynomial hierarchy. This paper proposes a new Boolean Satisfiability (SAT)-based algorithm for entailment in propositional circumscription that explores the relationship of propositional circumscription to minimal models. The new algorithm is inspired by ideas commonly used in SAT-based model checking, namely counterexample guided abstraction refinement. In addition, the new algorithm is refined to compute the theory closure for generalized close world assumption (GCWA). Experimental results show that the new algorithm can solve problem instances that other solutions are unable to solve.
△ Less
Submitted 30 June, 2010;
originally announced June 2010.
-
How to Complete an Interactive Configuration Process?
Authors:
Mikolas Janota,
Goetz Botterweck,
Radu Grigore,
Joao Marques-Silva
Abstract:
When configuring customizable software, it is useful to provide interactive tool-support that ensures that the configuration does not breach given constraints.
But, when is a configuration complete and how can the tool help the user to complete it?
We formalize this problem and relate it to concepts from non-monotonic reasoning well researched in Artificial Intelligence. The results are inte…
▽ More
When configuring customizable software, it is useful to provide interactive tool-support that ensures that the configuration does not breach given constraints.
But, when is a configuration complete and how can the tool help the user to complete it?
We formalize this problem and relate it to concepts from non-monotonic reasoning well researched in Artificial Intelligence. The results are interesting for both practitioners and theoreticians. Practitioners will find a technique facilitating an interactive configuration process and experiments supporting feasibility of the approach. Theoreticians will find links between well-known formal concepts and a concrete practical application.
△ Less
Submitted 20 October, 2009;
originally announced October 2009.
-
Algorithms for finding dispensable variables
Authors:
Mikolas Janota,
Joao Marques-Silva,
Radu Grigore
Abstract:
This short note reviews briefly three algorithms for finding the set of dispensable variables of a boolean formula. The presentation is light on proofs and heavy on intuitions.
This short note reviews briefly three algorithms for finding the set of dispensable variables of a boolean formula. The presentation is light on proofs and heavy on intuitions.
△ Less
Submitted 30 September, 2009;
originally announced October 2009.
-
Edit and verify
Authors:
Radu Grigore,
Michał Moskal
Abstract:
Automated theorem provers are used in extended static checking, where they are the performance bottleneck. Extended static checkers are run typically after incremental changes to the code. We propose to exploit this usage pattern to improve performance. We present two approaches of how to do so and a full solution.
Automated theorem provers are used in extended static checking, where they are the performance bottleneck. Extended static checkers are run typically after incremental changes to the code. We propose to exploit this usage pattern to improve performance. We present two approaches of how to do so and a full solution.
△ Less
Submitted 6 August, 2007;
originally announced August 2007.
