ABSTRACT. IVy is a language and a tool focused on building verified distributed systems using decidable logics. The talk will discuss the philosophy underlying IVy and give examples of the use of Ivy to prove distributed systems.

ABSTRACT. Tendermint is a new protocol for ordering events in a distributed network under adversarial conditions. More commonly known as Byzantine Fault Tolerant (BFT) consensus or atomic broadcast, the problem has attracted significant attention in recent years due to the widespread success of blockchain-based digital currencies, such as Bitcoin and Ethereum, which successfully solve the problem in a public setting without a central authority. Tendermint modernizes classic academic work on the subject and simplifies the design of the BFT algorithm by relying on a peer-to-peer gossip protocol among nodes. Furthermore, Tendermint uses a simple socket protocol to enable BFT state machine replication of arbitrary deterministic state machines, written in any programming language. Our implementation in Go achieves thousands of transactions per second on dozens of nodes distributed around the globe, with latencies of about one second, and performance degrading moderately in the face of adversarial attacks. This talk will provide an overview of how Tendermint works and how to build BFT applications with it, including scalable crypto-currencies.

ABSTRACT. We apply infinite-state model checking to formally verify Internet of Things protocols such as the Pub/Sub consistency protocol adopted by the REDIS distributed file system.

The verification method is based on a combination of SMT-solvers and overapproximations as those implemented in the Cubicle verification tool.

ABSTRACT. Effective software specifications enable modular reasoning, allowing clients to establish program properties without knowing the details of module implementations. While some modules’ operations behave atomically, others admit weaker consistencies to increase performance. Consequently, since current methodologies do not capture the guarantees provided by operations of varying non-atomic consistencies, specifications are ineffective, forfeiting the ability to establish properties of programs that invoke non-atomic operations.

In this work we develop a methodology for specifying software modules whose operations satisfy multiple distinct consistency levels. In particular, we develop a simple annotation language for specifying weakly-consistent operations, wherein annotations impose varying constraints on the visibility among operations. To validate annotations, we identify a novel characterization of consistency, called happens-before agnostic consistency, which admits effective consistency-checking automation. Empirically, we demonstrate the efficacy of our approach by deriving and validating relaxed-visibility specifications for Java concurrent objects. Furthermore, we demonstrate an optimality of our annotation language, empirically, by establishing that even finer-grained languages do not capture stronger specifications for Java objects.

ABSTRACT. This talk introduces Peregrine, the first tool for the analysis and parameterized verification of population protocols. Population protocols are a model of distributed computation in which mobile anonymous agents interact stochastically to achieve a common task. Peregrine allows users to design protocols, to simulate them both manually and automatically, to gather statistics of properties such as convergence speed, and to verify correctness automatically.
 

In this talk, I provide a short introduction to population protocols through a live demonstration of Peregrine's user interface, and explain the theory behind Peregrine's automatic verification capabilities.

ABSTRACT. One great issue in conceiving and specifying distributed algorithms is the sheer number of models, differing in subtle and often qualitative ways: synchrony, kind of faults, number of faults... In the context of message-passing, one solution is to restrict communication to proceed by round. A great variety of models can then be captured in the Heard-Of model, with predicates on the communication graph at each round. However, this raises another issue: how to characterize a given model by such a predicate? It depends on how to implement rounds in the model. This is straightforward in synchronous models, thanks to the upper bound on communication delay. On the other hand, asynchronous models allow unbounded message delays, which makes the implementation of rounds dependent on the specific message-passing model.

I will present our formalization of this implementation of rounds for asynchronous message-passing models. We proceed through games: the environment captures the non- determinism of a scheduler while processes decide, in turn, whether to change round or wait for more messages. Strategies of processes for these games, capturing the decision of when to change rounds, are studied through a dominance relation: a dominant strategy for a game implements the communication predicate which characterize the corresponding message-passing model. I will walk you through a classical message-passing model, the asynchronous one with reliable communication and at most f permanent crashes, and present its dominating strategy. Then I will develop our existence results for large classes of strategies, and for all games.

This is joint work with Aurélie Hurault and Philippe Quéinnec.

ABSTRACT. Modern software developments kits simplify the programming of concurrent applications by providing shared state abstractions which encapsulate low-level accesses into higher-level abstract data types (ADTs). Programming such abstractions is however error prone. To minimize synchronization overhead between concurrent ADT invocations, implementors avoid blocking operations like lock acquisition, allowing methods to execute concurrently. However, concurrency risks unintended inter-operation interference, and risks conformance to well-established correctness criteria like linearizability. We present several results concerning the theoretical limits of verifying such concurrent ADTs and testing-based methods for discovering violations in practical implementations.

ABSTRACT. To achieve scalability and availability, modern Internet services often rely on  large-scale transactional databases that replicate and partition data across a large number of nodes. Achieving serializability on such databases is often impractical,  as it limits scalability and increases latency. For this reason, recent 
years have seen a plethora of new transactional consistency models for  large-scale databases. 

In this talk, we propose SPSI, a novel consistency model for such systems  that fits in between the well-known snapshot isolation (SI) 
and parallel snapshot isolation (PSI).  SPSI assumes a partitioning of objects in the databases into entity-groups: it then mandates that PSI guarantees are satisfied by 
the database when considered as a whole, while it also requires the stronger consistency guarantees provided by SI to be satisfied by individual entity groups. 
We show that SPSI can be effectively implemented in a sharded database.

One main feature of SPSI is that, by carefully choosing the grouping of objects of the database into entity groups, one can ensure that transactional applications are robust: they only produce serializable behaviours. We propose a static criterion for determining whether an application running under SPSI is  robust.

This is a joint work with Giovanni Bernardi, Borja de Regil, Andrea Cerone and Alexey Gotsman.

ABSTRACT. Threshold automata, and the counter systems they define, were introduced as a framework for parameterized model checking of fault-tolerant distributed algorithms. This application domain suggested natural constraints on the automata structure, and a specific form of acceleration, called single-rule acceleration: consecutive occurrences of the same automaton rule are executed as a single transition in the counter system. These accelerated systems have bounded diameter, and can be verified in a complete manner with bounded model checking.

We go beyond the original domain, and investigate extensions of threshold automata: non-linear guards, increments and decrements of shared variables, increments of shared variables within loops, etc., and show that the bounded diameter property holds for several extensions. Finally, we put single-rule acceleration in the scope of flat counter automata: although increments in loops may break the bounded diameter property, the corresponding counter automaton is flattable, and reachability can be verified using more permissive forms of acceleration.

ABSTRACT. Verifying concurrent systems is notoriously hard due to the inherent non-determinism in interprocess communication. Effective verification methods rely on dynamic partial order reduction (DPOR) techniques, which can reason about system correctness without exploring all concurrent traces explicitly. DPOR is traditionally based on the Mazurkiewicz equivalence, which distinguishes between traces based on the relative order of their conflicting events.

In this talk I will present the recently introduced Observation equivalence for DPOR. In contrast to reordering conflicting events, this equivalence is data centric: it distinguishes traces based on which write events are observed by which read events. This equivalence induces a partitioning that is exponentially coarser than the Mazurkiewicz partitioning without sacrificing completeness of bug finding. It also admits natural, efficient DPOR-like algorithms for exploring the partitioning optimally, leading to speedups over the standard methods. I will conclude with some new challenges posed by this data-centric view.

ABSTRACT. Parameterized verification of fault-tolerant distributed algorithms has recently gained more and more attention. Most of the existing work considers asynchronous distributed systems (interleaving semantics). However, there exists a considerable distributed computing literature on synchronous fault-tolerant distributed algorithms: conceptually, all processes proceed in lock-step rounds, that is, synchronized steps of all (correct) processes bring the system into the next state.

We introduce an abstraction technique for synchronous fault-tolerant distributed algorithms that reduces parameterized verification of synchronous fault-tolerant distributed algorithms to finite-state model checking of an abstract system. Using the TLC model checker, we automatically verified several algorithms from the literature, some of which were not automatically verified before. Our benchmarks include fault-tolerant algorithms that solve atomic commitment, 2-set agreement, and consensus.