arXiv subjects
Publications and source records attributed to Roland Meyer.
Reachability in pushdown vector addition systems with states (PVASS) is among the longest standing open problems in Theoretical Computer Science. We show that the problem is decidable in full generality. Our decision procedure is similar in spirit to the KLMST algorithm for VASS reachability, but works over objects that support an elaborate form of procedure summarization as known from pushdown reachability.
In syntax-guided synthesis, one of the challenges is to reduce the enormous size of the search space. We observe that most search spaces are not just flat sets of programs, but can be endowed with a structure that we call an oriented metric. Oriented metrics measure the distance between programs, like ordinary metrics do, but are designed for settings in which operations have an orientation. Our focus is on the string and the bitvector domains, where operations like concatenation and bitwise conjunction transform an input into an output in a way that is not symmetric. We develop several new oriented metrics for these domains. Oriented metrics are designed for search space reduction, and we present four techniques: (i) pruning the search space to a ball around the ground truth, (ii) factorizing the search space by an equivalence that is induced by the oriented metric, (iii) abstracting the oriented metric (and hence the equivalence) and refining it, and (iv) improving the enumeration order by learning from abstract information. We acknowledge that these techniques are inspired by developments in the literature. By understanding their roots in oriented metrics, we can substantially increase their applicability and efficiency. We have integrated these techniques into a new synthesis algorithm and implemented the algorithm in a new solver. Notably, our solver is generic in the oriented metric over which it computes. We conducted experiments in the string and the bitvector domains, and consistently improve the performance over the state-of-the-art by more than an order of magnitude.
We show that the regular separability problem of VASS reachability languages is decidable and $\mathbf{F}_ω$-complete. At the heart of our decision procedure are doubly-marked graph transition sequences, a new proof object that tracks a suitable product of the VASS we wish to separate. We give a decomposition algorithm for DMGTS that not only achieves perfectness as known from MGTS, but also a new property called faithfulness. Faithfulness allows us to construct, from a regular separator for the $\mathbb{Z}$-versions of the VASS, a regular separator for the $\mathbb{N}$-versions. Behind faithfulness is the insight that, for separability, it is sufficient to track the counters of one VASS modulo a large number that is determined by the decomposition.
We address the problem of preserving non-interference across compiler transformations under speculative semantics. We develop a proof method that ensures the preservation uniformly across all source programs. The basis of our proof method is a new form of simulation relation. It operates over directives that model the attacker's control over the micro-architectural state, and it accounts for the fact that the compiler transformation may change the influence of the micro-architectural state on the execution (and hence the directives). Using our proof method, we show the correctness of dead code elimination. When we tried to prove register allocation correct, we identified a previously unknown weakness that introduces violations to non-interference. We have confirmed the weakness for a mainstream compiler on code from the libsodium cryptographic library. To reclaim security once more, we develop a novel static analysis that operates on a product of source program and register-allocated program. Using the analysis, we present an automated fix to existing register allocation implementations. We prove the correctness of the fixed register allocations with our proof method.
Separation logic is often praised for its ability to closely mimic the locality of state updates when reasoning about them at the level of assertions. The prover only needs to concern themselves with the footprint of the computation at hand, i.e., the part of the state that is actually being accessed and manipulated. Modern concurrent separation logics lift this local reasoning principle from the physical state to abstract ghost state. For instance, these logics allow one to abstract the state of a fine-grained concurrent data structure by a predicate that provides a client the illusion of atomic access to the underlying state. However, these abstractions inadvertently increase the footprint of a computation: when reasoning about a local low-level state update, one needs to account for its effect on the abstraction, which encompasses a possibly unbounded portion of the low-level state. Often this gives the reasoning a global character. We present context-aware (concurrent) separation logic (Co(Co)SL) to provide new opportunities for local reasoning in the presence of rich ghost state abstractions. Co(Co)SL introduces the notion of a context of a computation, the part of the concrete state that is only affected on the abstract level. Contexts give rise to a new proof rule that allows one to reduce the footprint by the context, provided the computation preserves the context as an invariant. The context rule complements the frame rule of separation logic by enabling more local reasoning in cases where the predicate to be framed is known in advance. We instantiate our developed theory for the flow framework, enabling contextual reasoning about programs manipulating general heap graphs, and describe two other applications of the logic. We have implemented the flow instantiation of the logic in a proof outline checker and used it to verify two highly-concurrent binary search trees.
The omega-regular separability problem for Büchi VASS coverability languages has recently been shown to be decidable, but with an EXPSPACE lower and a non-primitive recursive upper bound -- the exact complexity remained open. We close this gap and show that the problem is EXPSPACE-complete. A careful analysis of our complexity bounds additionally yields a PSPACE procedure in the case of fixed dimension >= 1, which matches a pre-established lower bound of PSPACE for one dimensional Büchi VASS. Our algorithm is a non-deterministic search for a witness whose size, as we show, can be suitably bounded. Part of the procedure is to decide the existence of runs in VASS that satisfy certain non-linear properties. Therefore, a key technical ingredient is to analyze a class of systems of inequalities where one variable may occur in non-linear (polynomial) expressions. These so-called singly non-linear systems (SNLS) take the form A(x).y >= b(x), where A(x) and b(x) are a matrix resp. a vector whose entries are polynomials in x, and y ranges over vectors in the rationals. Our main contribution on SNLS is an exponential upper bound on the size of rational solutions to singly non-linear systems. The proof consists of three steps. First, we give a tailor-made quantifier elimination to characterize all real solutions to x. Second, using the root separation theorem about the distance of real roots of polynomials, we show that if a rational solution exists, then there is one with at most polynomially many bits. Third, we insert the solution for x into the SNLS, making it linear and allowing us to invoke standard solution bounds from convex geometry. Finally, we combine the results about SNLS with several techniques from the area of VASS to devise an EXPSPACE decision procedure for omega-regular separability of Büchi VASS.
We study the languages recognized by well-structured transition systems (WSTS) with upward and downward compatibility. Our first result shows that every pair of disjoint WSTS languages is regularly separable: there is a regular language containing one of them while being disjoint from the other. As a consequence, if a language as well as its complement are both recognized by WSTS, then they are necessarily regular. Our second result shows that the languages recognized by deterministic WSTS form a strict subclass of the languages recognized by all WSTS: we give a non-deterministic WSTS language that we prove cannot be recognized by a deterministic WSTS. The proof relies on a novel characterization of the languages accepted by deterministic WSTS.
The source code of a program not only defines its semantics but also contains subtle clues that can identify its author. Several studies have shown that these clues can be automatically extracted using machine learning and allow for determining a program's author among hundreds of programmers. This attribution poses a significant threat to developers of anti-censorship and privacy-enhancing technologies, as they become identifiable and may be prosecuted. An ideal protection from this threat would be the anonymization of source code. However, neither theoretical nor practical principles of such an anonymization have been explored so far. In this paper, we tackle this problem and develop a framework for reasoning about code anonymization. We prove that the task of generating a $k$-anonymous program -- a program that cannot be attributed to one of $k$ authors -- is not computable in the general case. As a remedy, we introduce a relaxed concept called $k$-uncertainty, which enables us to measure the protection of developers. Based on this concept, we empirically study candidate techniques for anonymization, such as code normalization, coding style imitation, and code obfuscation. We find that none of the techniques provides sufficient protection when the attacker is aware of the anonymization. While we observe a notable reduction in attribution performance on real-world code, a reliable protection is not achieved for all developers. We conclude that code anonymization is a hard problem that requires further attention from the research community.
We present realizability and realization logic, two program logics that jointly address the problem of finding solutions in semantics-guided synthesis. What is new is that we proceed eagerly and not only analyze a single candidate program but a whole set. Realizability logic computes information about the set of candidate programs in a forward fashion. Realization logic uses this information as guidance to identify a suitable candidate in a backward fashion. Realizability logic is able to analyze a set of programs due to a new form of assertions that tracks synthesis alternatives. Realizability logic then picks alternatives to arrive at a program, and we give the guarantee that this process will not need backtracking. We show how to implement the program logics using verification conditions, and report on experiments with a prototype in the context of safe memory reclamation for lock-free data structures.
We propose urgency programs, a new programming model with support for alternation, imperfect information, and recursion. The novelty are urgency annotations that decorate the (angelic and demonic) choice operators and control the order in which alternation is resolved. We study standard notions of contextual equivalence for urgency programs. Our first main result are fully abstract characterizations of these relations based on sound and complete axiomatizations. Our second main result settles their computability via a normal form construction. Notably, we show that the contextual preorder is (2h-1)-EXPTIME-complete for programs of maximal urgency h when the regular observable is given as an input resp. PTIME-complete when the regular observable is fixed. We designed urgency programs as a framework in which it is convenient to formulate and study verification and synthesis problems. We demonstrate this on a number of examples including the verification of concurrent and recursive programs and hyper model checking.
Proving linearizability of concurrent data structures remains a key challenge for verification. We present temporal interpolation as a new proof principle to conduct such proofs using hindsight arguments within concurrent separation logic. Temporal reasoning offers an easy-to-use alternative to prophecy variables and has the advantage of structuring proofs into easy-to-discharge hypotheses. To hindsight theory, our work brings the formal rigor and proof machinery of concurrent program logics. We substantiate the usefulness of our development by verifying the linearizability of the Logical Ordering (LO-)tree and RDCSS. Both of these involve complex proof arguments due to future-dependent linearization points. The LO-tree additionally features complex structure overlays. Our proof of the LO-tree is the first formal proof of this data structure. Interestingly, our formalization revealed an unknown bug and an existing informal proof as erroneous.
We present a new flow framework for separation logic reasoning about programs that manipulate general graphs. The framework overcomes problems in earlier developments: it is based on standard fixed point theory, guarantees least flows, rules out vanishing flows, and has an easy to understand notion of footprint as needed for soundness of the frame rule. In addition, we present algorithms for automating the frame rule, which we evaluate on graph updates extracted from linearizability proofs for concurrent data structures. The evaluation demonstrates that our algorithms help to automate key aspects of these proofs that have previously relied on user guidance or heuristics.
We study the ($ω$-)regular separability problem for Büchi VASS languages: Given two Büchi VASS with languages $L_1$ and $L_2$, check whether there is a regular language that fully contains $L_1$ while remaining disjoint from $L_2$. We show that the problem is decidable in general and PSPACE-complete in the 1-dimensional case, assuming succinct counter updates. The results rely on several arguments. We characterize the set of all regular languages disjoint from $L_2$. Based on this, we derive a (sound and complete) notion of inseparability witnesses, non-regular subsets of $L_1$. Finally, we show how to symbolically represent inseparability witnesses and how to check their existence.
Intensive testing using model-based approaches is the standard way of demonstrating the correctness of automotive software. Unfortunately, state-of-the-art techniques leave a crucial and labor intensive task to the test engineer: identifying bugs in failing tests. Our contribution is a model-based classification algorithm for failing tests that assists the engineer when identifying bugs. It consists of three steps. (i) Fault localization replays the test on the model to identify the moment when the two diverge. (ii) Fault explanation then computes the reason for the divergence. The reason is a subset of actions from the test that is sufficient for divergence. (iii) Fault classification groups together tests that fail for similar reasons. Our approach relies on machinery from formal methods: (i) symbolic execution, (ii) Hoare logic and a new relationship between the intermediary assertions constructed for a test, and (iii) a new relationship among Hoare proofs. A crucial aspect in automotive software is timing requirements, for which we develop appropriate Hoare logic theory. We also briefly report on our prototype implementation for the CAN bus Unified Diagnostic Services in an industrial project.
Verifying fine-grained optimistic concurrent programs remains an open problem. Modern program logics provide abstraction mechanisms and compositional reasoning principles to deal with the inherent complexity. However, their use is mostly confined to pencil-and-paper or mechanized proofs. We devise a new separation logic geared towards the lacking automation. While local reasoning is known to be crucial for automation, we are the first to show how to retain this locality for (i) reasoning about inductive properties without the need for ghost code, and (ii) reasoning about computation histories in hindsight. We implemented our new logic in a tool and used it to automatically verify challenging concurrent search structures that require inductive properties and hindsight reasoning, such as the Harris set.
Developing concurrent software is challenging, especially if it has to run on modern architectures with Weak Memory Models (WMMs) such as ARMv8, Power, or RISC-V. For the sake of performance, WMMs allow hardware and compilers to aggressively reorder memory accesses. To guarantee correctness, developers have to carefully place memory barriers in the code to enforce ordering among critical memory operations. While WMM architectures are growing in popularity, identifying the necessary and sufficient barriers of complex synchronization primitives is notoriously difficult. Unfortunately, publications often consider barriers to be just implementation details and omit them. In this technical note, we report our efforts in verifying the correctness of the Compact NUMA-Aware (CNA) lock algorithm on WMMs. The CNA lock is of special interest because it has been proposed as a new slowpath for Linux qspinlock, the main spinlock in Linux. Besides determining a correct and efficient set of barriers for the original CNA algorithm on WMMs, we investigate the correctness of Linux qspinlock and the latest Linux CNA patch (v15) on the memory models LKMM, ARMv8, and Power. Surprisingly, we have found that Linux qspinlock and, consequently, Linux CNA are incorrect according to LKMM, but are still correct when compiled to ARMv8 or Power.
We study the safety verification problem for parameterized systems under the release-acquire (RA) semantics. It has been shown that the problem is intractable for systems with unlimited access to atomic compare-and-swap (CAS) instructions. We show that, from a verification perspective where approximate results help, this is overly pessimistic. We study parameterized systems consisting of an unbounded number of environment threads executing identical but CAS-free programs and a fixed number of distinguished threads that are unrestricted. Our first contribution is a new semantics that considerably simplifies RA but is still equivalent for the above systems as far as safety verification is concerned. We apply this (general) result to two subclasses of our model. We show that safety verification is only \pspace-complete for the bounded model checking problem where the distinguished threads are loop-free. Interestingly, we can still afford the unbounded environment. We show that the complexity jumps to \nexp-complete for thread-modular verification where an unrestricted distinguished `ego' thread interacts with an environment of CAS-free threads plus loop-free distinguished threads (as in the earlier setting). Besides the usefulness for verification, the results are strong in that they delineate the tractability border for an established semantics.
We study liveness and model checking problems for broadcast networks, a system model of identical clients communicating via message passing. The first problem that we consider is Liveness Verification. It asks whether there is a computation such that one of the clients visits a final state infinitely often. The complexity of the problem has been open since 2010 when it was shown to be P-hard and solvable in EXPSPACE. We close the gap by a polynomial-time algorithm. The algorithm relies on a characterization of live computations in terms of paths in a suitable graph, combined with a fixed-point iteration to efficiently check the existence of such paths. The second problem is Fair Liveness Verification. It asks for a computation where all participating clients visit a final state infinitely often. We adjust the algorithm to also solve fair liveness in polynomial time. Both problems can be instrumented to answer model checking questions for broadcast networks against linear time temporal logic specifications. The first problem in this context is Fair Model Checking. It demands that for all computations of a broadcast network, all participating clients satisfy the specification. We solve the problem via the Vardi-Wolper construction and a reduction to Liveness Verification. The second problem is Sparse Model Checking. It asks whether each computation has a participating client that satisfies the specification. We reduce the problem to Fair Liveness Verification.