Past PPLV Seminars

Separation Logic works because it merges the software engineer's conceptual model of a program's manipulation of computer memory with the logical model that interprets what sentences in the logic are true. Separation Logic is an interesting case because of its widespread success in verification tools used by Facebook and others daily.

For these two senses of model — the engineering/conceptual and the logical — to merge in a genuine sense, each must maintain their norms of use from their home disciplines. When this occurs, the development of both the logic and engineering benefit greatly. Seeking this intersection of two different senses of the concept of model provides a strategy for how computer scientists and logicians may be successful. In this talk, we will focus on an exploration of the extent to which models merging leads to success in computer science, and thereby the extent to which it is a strategy for future development.

Adaptive systems modify their behaviour in order to run always and everywhere. Their structure is therefore subject to continuous changes, which however could compromise the correct behaviour of applications and break the guarantees on their non-functional requirements.

Recently, Context Oriented Programming (COP) was proposed as a viable paradigm to develop adaptive and context-aware software. It advocates languages with peculiar constructs that express context-dependent behaviour in a modular manner. In this way context-awareness is built-in, and the provided linguistic abstractions impose a good practice to programmers.

This talk introduces COP, focusing in particular on ML_CoDa, a functional context-oriented language, and its two steps static analysis, to detect if adaptation errors may occur at run time.

Termination is the property of a program that regardless of the input, execution of the program will always come to a halt eventually. Although this property is undecidable, since the early 2000s fully automated techniques and tools for termination analysis have flourished in several communities: term rewriting, imperative programs, functional programs, logic programs, ...

A common theme behind most of these tools is the use of constraint-based techniques to advance the proof of (non-)termination. Recently, in particular SAT and SMT solvers are used as back-ends to automate these techniques. In my talk, I will give an overview of automated termination analysis from an SMT solving perspective.

Distributed systems are difficult to implement correctly because they must handle both concurrency and failures. Further, their behavior is often too complex to permit exhaustive testing. Bugs in these systems have led to the loss of critical data and unacceptable service outages.

We present Verdi, a framework for implementing and formally verifying distributed systems in Coq. Verdi formalizes various network semantics with different faults, and the developer chooses the most appropriate fault model when verifying their implementation. Furthermore, Verdi's verified system transformers (VSTs) ease the verification burden by enabling the developer to first verify their system under an idealized fault model, then transfer the resulting correctness guarantees to a more realistic fault model without any additional proof burden.

We have used Verdi to implement and verify the Raft consensus protocol. We proved that our implementation of Raft correctly provides linearizable state machine replication. This proof required iteratively discovering and proving 90 system invariants, consisting of over 50000 lines of code. At such a large scale, the primary challenge we faced during the verification process was proof maintenance. We will discuss proof engineering practices that were critical to our success.

Programming languages are islands, each disconnected from the rest. We choose a language for a task and, for better or worse, stick with it. Communicating between programs written in different languages is such a slow, arduous, task that we avoid doing it whenever possible.

In this talk I will first show how language composition can lower, and even remove, the barriers between languages. We have pioneered new approaches to the two major challenges in language composition: editing and running composed programs. Using our novel editor 'Eco', users can write source files that contain fragments of multiple languages. We then run multi-language programs using composed meta-tracing VMs. Our preliminary results suggest that performance of composed programs is often competitive with traditional mono-language VMs.

Joint work with Edd Barrett, Carl Friedrich Bolz, Lukas Diekmann, Geoff French, Sarah Mount, and Jasper Schulz. More at http://soft-dev.org/

We present a data-driven verification framework to automatically prove memory safety and functional correctness of heap programs. For this, we introduce a novel statistical machine learning technique that maps observed program states to (possibly disjunctive) separation logic formulas describing the invariant shape of data structures at relevant program locations. We then attempt to verify these predictions using a theorem prover, where counterexamples to a predicted invariant are used as additional input to the shape predictor in a refinement loop. After obtaining valid shape invariants, we use a second learning algorithm to strengthen them with data invariants, again employing a refinement loop using the underlying theorem prover.

We have implemented our techniques in Cricket, an extension of the GRASShopper verification tool. Cricket is able to automatically prove memory safety and correctness of implementations of a variety of classical list-manipulating algorithms such as insertionsort.

Joint work with Marc Brockschmidt, Yuxin Chen, Byron Cook, Pushmeet Kohli, Daniel Tarlow, and He Zhu.

Denotational semantics started in Oxford in late 1969. It was hoped that domain theory would provide a basis both for recursive definitions in programs and recursive definitions of semantical structures. Early troubles were encountered in using tops and bottoms, and soon researchers turned to operational semantics. Others wanted to expand work to communicating and parallel processes. Axiomatic and synthetic theories did not solve the problems, and as a result much research effort in domain theory faded. Late work by Reynolds and collaborators, however, has opened up new and promising approaches for programming-language semantics. Perhaps the much simplified modeling using enumeration operators can spark some new investigations, especially since it is so easy to add a rich type structure to the calculus.

Video recording: part 1   part 2.

• The notions of labelled transition system (a set of states, starting from which an action may be performed, leading to another state), trace (a possible sequence of actions from a starting state) and bisimulation (a relation that guarantees two states have matching behaviour) have provided a useful way of reasoning about computational systems.
• Game semantics is a compositional way of describing the behaviour of higher-order programs employing private state, providing a high-level description in the sense that state is not mentioned.

We want to represent game semantics using transition systems, but traditional systems are too rigid because they have a fixed set of actions. So instead we develop a version of transition system in which each state sits over a position of our game. The actions are the currently available moves.

To make this into a compositional semantics, we give a “transfer”, kind of program that converts moves between two games, giving an operation on strategies. The agreement between the transition systems and the transfer is given by a relation called a “stepped bisimulation”.

(Joint work with Sam Staton)

Software of distributed, safety-critical embedded systems, as e.g. found in the automotive, railway or avionics domain, has to satisfy very high requirements concerning correctness and fault tolerance. Therefore standards for the development of such systems highly recommend the usage of formal methods. For many complex control tasks the preferred architecture is a system composed from components that operate synchronously but communicate asynchronously with other components – a paradigm called GALS (globally asynchronous – locally synchronous) architecture.

In this talk we present an approach to close the "methodological" gap between the formal verification of synchronous components and asynchronous system of components. We mainly focus on systems where the synchronous components are implemented in SCADE (a language and modelling tool for synchronous controller software). The idea is then to abstract such concrete components with contracts, which are a mixture of temporal logic formulas and non-deterministic state machines. Formal verification of global system properties is then done on a network of contracts that has a lower complexity than the original network of concrete components. We will first explain the verification approach in general. Then we introduce a modelling language for the specification of contracts, and we then explain the transformations used for model checking GALS systems. Our model checking method is based on bounded model checking using SAT and SMT solvers. Finally, we demonstrate the results of our approach and tool on an industrial case study.

Security vulnerabilities plague modern systems because writing secure systems code is hard. Promising approaches can retrofit security automatically via runtime checks that implement the desired security policy; these checks guard critical operations, like memory accesses. Alas, the induced slowdown usually exceeds by a wide margin what system users are willing to tolerate in production, so these tools are hardly ever used. As a result, the insecurity of real-world systems persists. We present an approach in which developers/operators can specify what level of overhead they find acceptable for a given workload (e.g., 5%); our proposed tool ASAP then automatically instruments the program to maximize its security while staying within the specified "overhead budget." Two insights make this approach effective: most overhead in existing tools is due to only a few "hot" checks, whereas the checks most useful to security are typically "cold"and cheap. We evaluate ASAP on programs from the Phoronix and SPEC benchmark suites. It can precisely select the best points in the security-performance spectrum. Moreover, we analyzed existing bugs and security vulnerabilities in RIPE, OpenSSL, and the Python interpreter, and found that the protection level offered by the ASAP approach is sufficient to protect against all of them.

Joint work with Jonas Wagner, Volodymyr Kuznetsov and George Candea (EPFL), presented at IEEE S&P (Oakland) 2015.

Concurrent data-structures, such as stacks, queues, and deques, often implicitly enforce a total order over elements in their underlying memory layout. However, much of this order is unnecessary: linearizability only requires that elements are ordered if the insert methods ran in sequence. We propose a new approach which uses timestamping to avoid unnecessary ordering. Pairs of elements can be left unordered if their associated insert operations ran concurrently, and order imposed as necessary at the eventual removal.

We realise our approach in a new non-blocking data structure, the TS (timestamped) stack. Using the same approach, we can define corresponding queue and deque datastructures. In experiments on x86, the TS stack outperforms and outscales all its competitors – for example, it outperforms the elimination-backoff stack by factor of two. In our approach, more concurrency translates into less ordering, giving less-contended removal and thus higher performance and scalability. Despite this, the TS stack is linearizable with respect to stack semantics.

The weak internal ordering in the TS stack presents a challenge when establishing linearizability: standard techniques such as linearization points work well when there exists a total internal order. We present a new stack theorem, mechanised in Isabelle, which characterises the orderings sufficient to establish stack semantics. By applying our stack theorem, we show that the TS stack is indeed linearizable. Our theorem constitutes a new, generic proof technique for concurrent stacks, and it paves the way for future weakly ordered data-structure designs.

Associated paper: http://www-users.cs.york.ac.uk/~miked/publications/POPL.15.ts_stack.pdf

Concurrency is pervasive and perplexing, particularly on graphics processing units (GPUs). Current specifications of languages and hardware are inconclusive; thus programmers often rely on folklore assumptions when writing software. To remedy this state of affairs, we conducted a large empirical study of the concurrent behaviour of deployed GPUs. Armed with litmus tests (i.e. short concurrent programs), we questioned the assumptions in programming guides and vendor documentation about the guarantees provided by hardware. We developed a tool to generate thousands of litmus tests and run them under stressful workloads. We observed a litany of previously elusive weak behaviours, and exposed folklore beliefs about GPU programming—often supported by official tutorials—as false.

As a way forward, we propose a model of Nvidia GPU hardware, which correctly models every behaviour witnessed in our experiments. The model is a variant of SPARC Relaxed Memory Order (RMO), structured following the GPU concurrency hierarchy.

Verification techniques that can scale to reasoning about real, rather than synthetic or toy, programs are essential for practical program verifiers. GPUVerify is a verification tool, built at MSR and Imperial, to reason about data-parallel programs. In particular, massively-parallel Graphics Processing Unit (GPU) programs. In this domain we have explored different characteristics of scalability: verifier precision, performance and automation.

After covering the core verification method that enables GPUVerify to scale to realistic problem sizes, I will talk about:

1. An empirical study of candidate-based invariant generation exploring the trade-offs between precision and performance.
2. Barrier invariants: an abstraction for precise and scalable reasoning about data-dependent GPU programs.

In parallel programs, threads communicate according to the memory consistency model: the set of memory ordering rules enforced by a given architecture. A great deal of research effort has gone into rigorous formalization of memory models. However, comparatively little attention has been paid to the microarchitectural implementation of these models. Standard testing-based techniques are insufficient: unobserved behaviors are not guarantees of non-observability, and failed tests offer little insight into the microarchitectural reason behind failure.

I will present PipeCheck, a methodology and automated tool for verifying that a given microarchitecture correctly implements the memory consistency model specified by its architectural specification. PipeCheck adapts the formal notion of a "happens before" graph to the microarchitecture space. Architectural specifications such as preserved program order are then treated as propositions to be verified, rather than simply as assumptions. We also specify and analyze the behavior of common microarchitectural optimizations such as speculative load reordering. Using PipeCheck, we were able to validate the OpenSPARC T2 in just minutes, and we found and fixed a bug in a architectural simulator widely used in academia.PipeCheck has been nominated for the Best Paper award at MICRO 2014, to be held in Cambridge, UK this December. At the end, I will also briefly introduce ArMOR, a framework for defining dynamic binary translation layers that seamlessly translate between memory consistency models such as those used by x86, ARM, and Power.

Bio: Daniel Lustig is a PhD candidate in Electrical Engineering at Princeton University. His research interests lie in the field of computer architecture, with a particular emphasis on designing memory systems for heterogeneous architectures. His recent work focuses verification of microarchitectural implementations of memory consistency models. Daniel earned his BSE from the University of Pennsylvania in 2009 and his MA from Princeton University in 2011. He also received an Intel PhD Fellowship in 2013.

Dynamic symbolic execution is an automated program analysis technique that employs an SMT solver to systematically explore paths through a program. It has been acknowledged in recent years as a highly effective technique for generating high-coverage test suites as well as for uncovering deep corner-case bugs in complex real-world software, and one of the key factors responsible for that success are the tremendous advances in SMT-solving technology. Nevertheless, constraint solving remains one of the fundamental challenges of symbolic execution, and for many programs it is the main performance bottleneck.

In this talk, I will first give a very general introduction to symbolic execution, and then I will present the results reported in our CAV 2013 paper on integrating support for multiple SMT solvers in the dynamic symbolic execution engine KLEE. In particular, I will outline the key characteristics of the SMT queries generated during symbolic execution, describe several high-level optimisations that KLEE employs to exploit those characteristics, introduce an extension of KLEE that uses a number of state-of-the-art SMT solvers (Boolector, STP and Z3) through the metaSMT solver framework, and compare the solvers' performance when run under KLEE. In addition, I will discuss several options for designing a parallel portfolio solver for symbolic execution tools. This is joint work with Cristian Cadar.

Around fifteen years ago, Nakano introduced an extension to a system of recursive types for the Lambda Calculus consisting of a unary type constructor, or modality, guarding the occurrences of recursive references. This modest extension afforded a powerful result: the guarantee of a particular kind of termination (specifically, head normalisation). That is, programs typeable in this system are guaranteed to produce output.

Since then, much research has been done to understand the semantics of this modality, and utilise it in more sophisticated type systems. Notable contributions to this effort include: the work of Birkedal et al. and Benton and Krishnaswami, who study semantic models induced by the modality; research by Appel at al. and Pottier who employ the modality in typed intermediate representations of programs; and Atkey and McBride’s work on co-programming for infinite data.

While some of this work explicitly addresses the possibility of type checking (e.g., that of Pottier), to the best of our knowledge type inference is still an unsolved problem. The lack of a type inference procedure presents a significant barrier to the wider adoption of Nakano’s technique in practice. In this talk, I will describe a (conservative) extension to Nakano’s system which allows for the development of a (sound but incomplete) unification-based algorithm for deciding whether a term is typeable by constructing a suitably general type.