Workshop on Verification of Distributed Systems (VDS)

On Program Verification under the Release-Acquire Semantics (Keynote talk)

Communication closed asynchronous protocols

Fault-tolerant distributed systems are implemented over asynchronous networks, so that they use algorithms for asynchronous models with faults. Due to asynchronous communication and the occurrence of faults (e.g., process crashes or the network dropping messages) the implementations are hard to understand and analyze. In contrast, synchronous computation models simplify design and reasoning. In this paper, we bridge the gap between these two worlds. For a class of asynchronous protocols, we introduce a procedure that, given an asynchronous protocol, soundly computes its round-based synchronous counterpart. This class is defined by properties of the sequential code. We computed the synchronous counterpart of known consensus and leader election protocols, such as, Paxos, and Chandra and Toueg’s consensus. Using Verifast we checked the sequential properties required by the rewriting. We verified the round-based synchronous counter-part of Multi-Paxos, and other algorithms, using existing deductive verification methods for synchronous protocols.

On the Complexity of Checking Transactional Consistency

Transactions simplify concurrent programming by enabling computations on shared data that are isolated from other concurrent computations and resilient to failures. Modern databases provide different consistency models for transactions corresponding to different tradeoffs between consistency and availability. In this work, we investigate the problem of checking whether a given execution of a transactional database adheres to some consistency model. We show that consistency models like read committed, read atomic, and causal consistency are polynomial time checkable while prefix consistency and snapshot isolation are NP-complete in general. These results complement a previous NP-completeness result concerning serializability. Moreover, in the context of NP-complete consistency models, we devise algorithms which are polynomial time assuming that certain parameters in the input executions, e.g., the number of sessions, are fixed. We evaluate the scalability of these algorithms in the context of several production databases.

Robust contract evolution in a microservice architecture

Microservice architecture allow for short deployment cycles and immediate effects, but offer no safety mechanisms when service contracts need to be changed. Maintaining the soundness of microservice architectures is an error-prone task only accessible to disciplined development teams. In this talk, we present a microservice management model that statically checks new service versions, preventing breaking deployments, and certifying the capability of the system to adapt to compatible changes. The proposed underlying compatibility relation captures real evolution patterns and embodies known good practices on the evolution of interfaces, in particular adding, reordering, removing, and renaming fields. The evolution of interfaces is supported by runtime generated proxy components that dynamically adapt the data exchanged between services, avoiding communication errors and data loss. This adaptive approach allows for gradual deployment of services, without halting the whole system and avoiding losing or misinterpreting data exchanged between services.

Pretend Synchrony: Synchronous Verification of Asynchronous Distributed Programs

In this talk, I will present pretend synchrony, a new approach to verifying distributed systems, based on the observation that while distributed programs must execute asynchronously, we can often soundly treat them as if they were synchronous, when verifying their correctness. To do so, we compute a synchronization, a semantically equivalent program where all sends, receives, and message buffers, have been replaced by simple assignments, yielding a program that can be verified using Floyd-Hoare style verification conditions and SMT. We have implement our approach as a framework for writing verified distributed programs in Go. Pretend synchrony allows us to develop performant systems while making verification of functional correctness simpler by reducing manually specified invariants by a factor of 6, and faster, by reducing checking time by three orders of magnitude.

Polygraph: Accountable Byzantine Agreement

In this paper, we introduce Polygraph, the first accountable Byzantine consensus algorithm for partially synchronous systems. If among $n$ users $t<\frac{n}{3}$ are malicious then it ensures consensus, otherwise it eventually detects malicious users that cause disagreement. Polygraph is appealing for blockchain applications as it allows them, if $t<\frac{n}{3}$, to totally order blocks in a chain, hence avoiding forks and double spending and, otherwise, to punish malicious users when a fork occurs. We first show that stronger forms of the problem including a fixed time detection are impossible to solve before proving our solution. We also show that Polygraph has a bounded justification size so that each of its asynchronous rounds exchanges only $O(n^2)$ messages. Finally, we use the Red Belly Blockchain application to evaluate Polygraph on a geodistributed system of 80 machines and show that accountability reduces the performance of the non-accountable baseline by about a third, still committing thousands of transactions per second.

Atomic Transaction Commit for Modern Data Stores

Modern data stores often need to provide both high scalability and strong transactional semantics. They achieve scalability by partitioning data into shards and fault-tolerance by replicating each shard across several servers. A key component of such systems is the protocol for atomically committing a transaction spanning multiple shards, which is usually integrated with concurrency control. Unfortunately, the classical theory of atomic commit is too restrictive to capture the complexities of such protocols. I will present a new problem statement for atomic commit that more faithfully reflects modern requirements and will describe solutions to this problem in different classes of data stores.

This is joint work with Manuel Bravo (IMDEA) and Gregory Chockler (Royal Holloway, University of London).

Automated Reasoning for Weak Consistency (Keynote Talk)

Making TLA+ model checking symbolic

TLA+ is a language for formal specification of all kinds of computer systems. System designers use this language to specify concurrent, distributed, and fault-tolerant protocols, which are traditionally presented in pseudo-code. TLA+ is extremely concise yet expressive: The language primitives include Booleans, integers, functions, tuples, records, sequences, and sets thereof, which can be also nested. This is probably why the only model checker for TLA+ (called TLC) relies on explicit enumeration of values and states. In this talk, we present a first symbolic model checker for TLA+. Like TLC, it assumes that all specification parameters are fixed and all states are finite structures. Unlike TLC, our model checker translates the underlying transition relation into quantifier-free SMT constraints, which allows us to exploit the power of SMT solvers.

Joint work with Jure Kukovec and Thanh Hai Tran (TU Wien, Austria).

Reliable State Machines: A Framework for Programming Reliable Cloud Services

Building reliable applications for the cloud is challenging because of unpredictable failures during a program's execution. This paper presents a programming framework called Reliable State Machines (RSMs), that offers fault-tolerance by construction. Using our framework, a programmer can build an application as several (possibly distributed) RSMs that communicate with each other via messages, much in the style of actor-based programming. Each RSM is additionally fault-tolerant by design and offers the illusion of being "always-alive". An RSM is guaranteed to process each input request exactly once, as one would expect in a failure-free environment. The RSM runtime automatically takes care of persisting state and rehydrating it on a failover. We present the core syntax and semantics of RSMs, along with a formal proof of failure-transparency. We provide an implementation of the RSM framework and runtime on the .NET platform for deploying services to Microsoft Azure. We carried out an extensive performance evaluation on micro-benchmarks to show that one can build high-throughput applications with RSMs. We also present a case study where we rewrote a significant part of a production cloud service using RSMs. The resulting service has simpler code and exhibits production-grade performance.

Verifying the Stellar Consensus Protocol

We describe a methodology deployed to formally verify safety and liveness properties of the Stellar Consensus Protocol (SCP). Using ideas taken from distributed computing theory, we derive an axiomatic model of the system which allows us to perform interactive verification of SCP's balloting protocol, for an arbitrary number of participants, using the decidable logic EPR. We then demonstrate that the axiomatic model is a correct abstraction of the original Stellar model using Isabelle/HOL. Thanks to this decomposition, the proof effort is modest despite the complexity of the protocol.

BMC for Weak Memory Models

We present Dartagnan, a bounded model checker for concurrent programs under weak memory models. Its distinguishing feature is the fact that the memory model is part of the input. Dartagnan reads CAT, the standard language for memory models which can express x86/TSO, ARMv7, ARMv8, Power, C/C++, and the Linux kernel concurrency primitives. BMC with memory models as input is challenging. One has to encode into SMT not only the program but also its semantics as defined by the memory model. In this talk, we report on the tricks we have developed to optimize this encoding.

Model Checking in Bits and Pieces

State explosion is the central, fundamental obstacle to fully automated verification of distributed protocols. Modular verification methods are one way of ameliorating this problem. These methods side-step state explosion by reasoning locally and separately about each component of a program, subsequently combining those local results into a global proof. Although approximate, localized reasoning is often surprisingly effective, especially when a program is built out of "loosely coupled" components. For distributed protocols, which are typically composed of isomorphic processes, a recently developed notion of neighborhood symmetry further simplifies the task of modular reasoning. The symmetries also make it easier to construct a modular correctness proof for _all_ (i.e., an unbounded number of) instances of a protocol, by generalizing from modular proofs that are automatically constructed for small-scale instances. In the talk, I will also touch upon less understood but important questions about the scope of modular verification methods, and the potential for automatic synthesis of modularly-correct protocols from specifications of their behavior.

Randomized Testing of Distributed Systems with Probabilistic Guarantees

Several randomized testing tools for concurrent systems come with theoretical guarantees on their success. However, these results either assume shared-memory multithreading, or that the underlying partial ordering of events is known statically and has special structure. These assumptions are not met by distributed message-passing applications. We present a randomized algorithm for testing distributed systems which works for arbitrary partially ordered sets of events revealed online as the program is being executed. The key to the probabilistic guarantee is a notion of bug depth—the minimum length of a sequence of events sufficient to expose the bug—and a characterization of d-hitting families of schedules—a set of schedules guaranteed to cover every bug of given depth d. In the last part of the talk, we briefly discuss how we can exploit state-space reduction strategies for better guarantees. This will move us towards a randomized algorithm which brings together two orthogonal reductions of the search space: depth-bounded testing and dependency-aware testing.
(Joint work with Rupak Majumdar, Filip Niksic, Simin Oraee, Mitra Tabaei Befrouei, Georg Weissenbacher).

Finding Rare Concurrent Programming Bugs

Developing correct, scalable and efficient concurrent programs is known to be a complex and difficult task. This is due to the difficulty for humans to reason about all the possible non-deterministic interactions among threads. Further, modern multi-core processors with weak memory models and lock-free algorithms are sources of additional nondeterministic behaviours that make this task even more intricate. As a result, concurrent programs often contain bugs that are difficult to find, reproduce, and fix. We have recently proposed a novel automatic approach for finding rare bugs in concurrent programs. The key idea is to generate a set of simpler program instances, each capturing a reduced set of the original program’s interleavings. These instances can then be verified independently in parallel. Our approach is parametrizable and allows us to fine-tune the nondeterminism and randomness used for the analysis. In our experiments, by using parallel analysis, we show that this approach is able, even with a small number of cores, to find bugs in the hardest known concurrency benchmarks in a matter of minutes, whereas other dynamic and static tools fail to do so in hours. I will give an overview of the key ingredients of this approach and discuss challenges to be overcome in order to handle larger real-world concurrent programs.
Joint work with Truc Nguyen Lam (U. Southampton, UK), Peter Schrammel (U. Sussex, UK), Bernd Fischer (U. Stellenbosch, South Africa), and Salvatore La Torre (U. Salerno, Italy).

Distributed Ledgers Consistency

Distributed Ledgers (e.g. Bitcoin, Algorand, Byzcoin, Hyperledger, RedBelly, Tendermint) became a game changer in the distributed storage area due to their ability to mimic the functioning of a classical traditional ledger such as transparency and falsification-proof of documentation in an untrusted environment where the computation is distributed, the set of participants to the system are not known and it varies during the execution. However, the massive integration of distributed ledgers in industrial applications strongly depends on the formal guaranties of the quality of services requiered by these applications, especially in terms of consistency. Our work continues the line of recent distributed computing community effort dedicated to the theoretical aspects of blockchains. We specified the distributed shared ledgers first as distributed shared registers, then as a composition of abstract data types all together with an hierarchy of consistency criteria that formally characterizes the histories admissible for distributed programs that use them. Our work extends the consistency criteria theory with new consistency definitions that capture the eventual convergence process in blockchain systems. Furthermore, we map representative existing blockchains from both academia and industry in our framework and identify the necessary communication conditions in order to implement the new defined consistency criteria.

Specifying and Verifying Non-Volatile Memory

Computer storage is traditionally divided into two categories: fast, volatile, byte-addressable memory (e.g. RAM), which loses its contents in case of a crash (e.g. a power failure), and slow, persistent, block-addressable storage (e.g. hard dis drives), which preserves its contents in case of a power failure. However, emerging new technologies in non-volatile memory (NVM) may soon render this dichotomy obsolete by enabling processors to access data guaranteed to persist a power failure at byte-level granularity and at performance comparable to RAM. It is widely believed that NVM will eventually supplant volatile memory, allowing for efficient access to persistent data. However, using NVM correctly is not easy. A key challenge is ensuring correct recovery after a crash by maintaining the consistency of data in memory. In this talk I will describe our ongoing work on formally specifying the NVM semantics of mainstream hardware architectures such as Intel-x86 and ARMv8. I will then talk about our research into clear and simple abstractions for programming on NVM, including a transactional NVM library with strong guarantees and intuitive semantics. This is crucial for simplifying the development and verification of software for NVM.

Deciding the existence of cut-off in rendez-vous networks

In networks of processes where the communication is performed by rendez-vous and the number of processes is a parameter, it is not always possible to find a cut-off, i.e. a minimal number of processes, which guarantees that the behavior of the network is correct. We show that for some reachability objective requiring all the processes to end in some specific states, the existence of a cut-off is a decidable problem and we provide algorithms to solve it for different hypothesis on the rendez-vous communication and on the presence of a leader in the network.

Title The programming continuum, from core to edge and back

Current cloud architectures, centralised in a few massive data centres, are increasingly moving towards support of edge resources, including localised data centres, points-of-presence, 5G tower micro-DCs, IoT gateways, and far-edge devices. Computing models offered across this spectrum differ vastly, from database-centric in the core, to stream- and notification based at the far edge. When a database system supports notifications, and vice-versa, these are tacked on as an afterthought and not well integrated. Data-sharing models themselves range from weakly to strongly consistent, with blockchains being a bit of both. Indeed, at this scale, CAP and the conflict between correctness and availability is inescapable. Security is often a second-class citizen in distributed system design, as is deployment, monitoring and run-time control. However, we argue that there is no good reason for this proliferation of incompatible models. Developers need access to the full power of distributed computing; they need a common programming model across the whole spectrum, forming a programming continuum. For instance, data access and notifications can be designed to be mutually consistent. Replication can be available-first (based on CRDTs) but designed to seamlessly support stronger synchronisation when required by application semantics. A large system being a composition of parts, composable verification techniques are a key to success. The designer should be able to create and reason about distributed abstractions. To enforce these abstractions, and for security reasons, requires arms-length isolation boundaries. This may use encryption and to branching/merging consistency models, inspired by distributed version control and blockchains. Deployment and monitoring can be programmed using the same abstractions as ordinary computations. The above can be implemented in many different (but mutually compatible) ways, for instance in the core vs. at the far edge.

Living on the edge, safely or: Life without consensus (Keynote talk)

The centre-of-gravity of cloud is moving towards the edge. At edge scale, the opposition between the requirements of availability and ensuring correctness precludes any single simple answer. Choosing the right trade-off is a most vexing issue for application developers. To address this, we propose an application-driven approach, Just-Right Consistency (JRC). JRC derives a consistency model that is adapted to the specific application, being sufficient to maintain its invariants, otherwise remaining as available as possible. In order to maintain its invariants, even sequential code follows some standard patterns. We leverage mechanisms that uphold several of these patterns while maintaining availability: • Conflict-Free Replicated Data Types (CRDTs) ensure that concurrent updates can be merged; • Causal Consistency preserves relative ordering; Available Transactions preserve grouping. Together, these mechanisms form the TCC+ model. Furthermore, our CISE logic and analysis tools distinguish cases, in the remaining pattern, where the application's semantics requires synchronisation or not. This talk presents the challenges of edge-scale computing and the basics of the JRC approach by following the concrete example of a healthcare network. This research is supported in part by European projects SyncFree and LightKone, and by ANR project RainbowFS.

On the correctness of Egalitarian Paxos

In this talk, we present a problem in both the TLA + specification and the implementation of the Egalitarian Paxos protocol. This problem is related to how replicas switch from one ballot to another when computing the dependencies of a command. We show that it may lead replicas to diverge and break the linearizability of the replicated service.

Verifying Safety of Synchronous Fault-Tolerant Algorithms by Bounded Model Checking

Owing to well-known limitations of what can be achieved in purely asynchronous systems, many fault-tolerant distributed algorithms are designed for synchronous or round-based semantics. In this paper, we introduce the synchronous variant of threshold automata, and study their applicability and limitations for the verification of synchronous distributed algorithms. We show that in general, the reachability problem is undecidable for synchronous threshold automata. Still, we show that many synchronous fault-tolerant distributed algorithms have a bounded diameter, although the algorithms are parameterized by the number of processes. Hence, we use bounded model checking for verifying these algorithms. The existence of bounded diameters is the main conceptual insight in this paper. We compute the diameter of several algorithms and check their safety properties, using SMT queries that contain quantifiers for dealing with the parameters symbolically. Surprisingly, performance of the SMT solvers on these queries is very good, reflecting the recent progress in dealing with quantified queries. We found that the diameter bounds of synchronous algorithms in the literature are tiny (from 1 to 4), which makes our approach applicable in practice. For a specific class of algorithms we also establish a theoretical result on the existence of a diameter, providing a first explanation for our experimental results.
Joint work with Ilina Stoilkovska, Igor Konnov, and Florian Zuleger

Decoupling Lock-Free Data Structures from Memory Reclamation for Static Analysis

Verification of concurrent data structures is one of the most challenging tasks in software verification. The topic has received considerable attention over the course of the last decade. Nevertheless, human-driven techniques remain cumbersome and notoriously difficult while automated approaches suffer from limited applicability. The main obstacle for automation is the complexity of concurrent data structures. This is particularly true in the absence of garbage collection. The intricacy of lock-free memory management paired with the complexity of concurrent data structures makes automated verification prohibitive. In this work we present a method for verifying concurrent data structures and their memory management separately. We suggest two simpler verification tasks that imply the correctness of the data structure. The first task establishes an over-approximation of the reclamation behavior of the memory management. The second task exploits this over-approximation to verify the data structure without the need to consider the implementation of the memory management itself. To make the resulting verification tasks tractable for automated techniques, we establish a second result. We show that a verification tool needs to consider only executions where a single memory location is reused. We implemented our approach and were able to verify linearizability of Michael&Scott's queue and the DGLM queue for both hazard pointers and epoch-based reclamation. To the best of our knowledge, we are the first to verify such implementations fully automatically.

On Structuring Communication and Verification

Verification of message-passing systems is a challenging task. With a perfect network, the problem is undecidable. While considering fault makes the verification problem simpler in theory (lossy channel systems), the problem is still intractable. Furthermore, considering faults create other problems for the verification. A fault-tolerant consensus algorithms which can be described in ~50 lines of pseudo code can turns into a few thousand lines of actual code that needs to be verified. The blow-up in code size between an algorithm and its implementation points to some form of impedance mismatch between the algorithm and the tools to implement them. Current tools do not provide adequate support for detecting and handling errors in a distributed setting. Furthermore, messages are side-effects in most programming languages (untyped, no scoping mechanism). This leads to a control-flow inversion problem which partly explains the blow-up in code size and makes the verification harder. In this talk, I will discuss how we used communication-closed rounds to avoid these issues. Unfortunately, communication-closed rounds have their own limitations and I will discuss our current work on lifting these limitations by borrowing ideas from multiparty session types.