ABSTRACT. Consistent shareable data services supporting atomic (linearizable) objects provide convenient building blocks for dynamic distributed systems. In general it is notoriously challenging to combine provable correctness guarantees with efficiency in distributed systems subject to perturbations in the computing medium. We overview our work on specification and implementation of distributed system services. Then we focus on a general framework for dynamic consistent data services that can be tailored to yield implementations for various target network settings and that incorporates on-the-fly reconfiguration that only modestly interferes with on-going operations. Here the goal is to guarantee safety (atomicity) for arbitrary patterns of asynchrony, crashes, and message loss, while enabling practical implementations.  We describe examples of specification, rigorous reasoning about correctness, provable optimizations, and methodical implementations of consistent data services in distributed systems.

ABSTRACT. ...

ABSTRACT. Efficient and scalable concurrent data-structures are key to high-performance multicore systems. Algorithms such as stacks and queues are widely used to handle synchronisation and distribute work between cores. We present the TS stack, a new concurrent stack implementation which allows elements to remain unordered in the stack if they were pushed concurrently. We use a new proof technique to show the correctness of the TS stack according to linearizability as the common linearization point technique cannot be applied.

ABSTRACT. We show how correct, analyzable distributed programs can be implemented in Scala using our framework, FooPar. Both performance and correctness proofs can be modularized in terms of the distributed data structures and functions available in the framework. We go on to show how we can further the connection between the correctness proofs and implementation using specification testing.

ABSTRACT. Software-defined networks (SDNs) is a new type computer networks where data planes and control planes are separated from each other and a centralized controller manages a distributed set of switches. A set of commands for packet forwarding and flow-table updating was defined in the form of a protocol known as OpenFlow. SDNs can both simplify existing network applications and serve as a platform for developing new ones. The main advantage of this network architecture is that programmers are able to control the behaviour of the whole network by configuring appropriately the packet forwarding rules installed on the switches. Nevertheless, correct and safe management of SDNs is not an easy task. Every time the current load of flow tables should satisfy certain requirements: some packets have to reach their destination, although some other packets have to be dropped, certain switches are forbidden for some packets, whereas some other switches have to be obligatorily traversed. These and some other requirements constitute a Packet Forwarding Policies (PFPs). One of the aims of network engineering is to provide such a loading of switches with forwarding rules as to guarantee compliance with the PFP. The solution is to develop a toolset which could be able 1) to check correctness of a separate application operating on the controller w.r.t. a specified forwarding policy, 2) to check consistency of forwarding policies implemented by various applications, and 3) to monitor and check correctness and safety of the entire SDN. In an attempt to produce such a toolset we developed 1) a combined (relational and automata based) formal model which captures the most essential features of SDN behavior, 2) a multi-level formal language for specification of SDN forwarding policies which uses transitive closure operator to specify reachability properties of packet forwarding relation and temporal operators to specify behaviour of SDN as a whole, and 3) a BDD-based model-checking techniques for verification of SDN models against PFP specifications.

ABSTRACT. Fault-tolerant distributed algorithms are central to ensuring reliability and availability of many on-line services that we use on a daily basis. However, they are difficult to build correctly. On top of the usual implementation challenges, one has to consider non-determinism in the scheduling of the participants and faults such as machine failures, and dropped messages. Using round models as a layer of abstraction simplify the design of such systems. Rounds are communication-closed and have a deterministic schedule. From a theoretical perspective, those models are justified by partial synchrony assumptions and simulation relations that map non-determinism to faults. From a practical perspective, many asynchronous algorithms are structured around logical rounds. For instance, in the Paxos algorithm, a replica becomes a leader in the first round and proposes its value during the second round. However, rounds are an abstraction and real systems are asynchronous. Therefore, such models are popular in theoretical publications, but less so in system ones. This talk will describe ongoing efforts in the automated verification of round-based algorithms and the synthesis of asynchronous implementations from round-based descriptions.

ABSTRACT. Recent advances in Distributed Computing highlights models and algorithms for autonomous swarms of mobile robots that self-organize and cooperate to solve global objectives. The overwhelming majority of works so far considers handmade algorithm and correctness proofs.

This paper is the first to propose a formal framework to automatically design distributed algorithms that are dedicated to autonomous mobile robots evolving in a discrete space. As a case study, we consider the problem of gathering all robots at a particular location, not known beforehand. Our contribution is threefold. First, we propose an encoding of the gathering problem as a reachability game. Then, we automatically generate an optimal distributed algorithm for three robots evolving on a fixed size uniform ring. Finally, we prove by induction that the generated algorithm is also correct for any ring size except when an impossibility result holds (that is, when the number of robots divides the ring size).

ABSTRACT. I propose a framework for the automatic verification of autonomous mobile agents (robot protocols), moving on unknown finite graphs. The framework reduces the parameterised verification problem (i.e., does a given set of robots solve a given task on all graphs from a given infinite set of graphs) to questions in automata theory and monadic second order logic. I will provide some preliminary results, discuss the limitations of this approach, and suggest future research directions.

ABSTRACT. In this talk, I will present our recent work on the synthesis of self-stabilizing, Byzantine fault-tolerant distributed algorithms for the synchronous counting problem.

We have examined two types of SAT solver-based techniques for synthesis. In the first approach, we have encoded the search problems into CNF SAT instances. This allows us to use highly-optimized, off-the-shelf SAT solvers. The second approach is inspired by CEGAR-style bounded model checking techniques. We have developed a search algorithm based on incremental SAT solving using assumptions on top of MiniSAT.

Both techniques have yielded novel algorithms for the synchronous counting problem. During the talk, I will present these results, discuss the trade-offs between the techniques for synthesis, and highlight open problems for future research.

This is joint work with Danny Dolev, Keijo Heljanko, Matti Järvisalo, Janne H. Korhonen, Christoph Lenzen, Ulrich Schmid, Jukka Suomela and Siert Wieringa.

ABSTRACT. The implementation of distributed algorithms is error-prone, and manually constructed programs may not be optimal with respect to desired properties like size or stabilisation time. We propose to use computational methods to synthesise distributed algorithms from formal specifications, with guaranteed correctness and optimality. We present novel synthesis approaches for two general classes of specifications, and show that they are complete for realisable specifications and guaranteed to terminate for given bounds on certain parameters of the desired implementation. The resulting system components are correct by construction for distributed systems of arbitrary size, and have strong failure-resilience properties.

ABSTRACT. We present our work on the synthesis of finite-state component implementations for concurrent systems with a parametric number of components. We show how the parameterized synthesis problem can be reduced to a synthesis problem for a fixed number of components, using cutoff results from parameterized model checking. To make the approach practical for synthesis, we both extend the existing cutoff results, and optimize the synthesis method for the class of systems and specifications under consideration. With this approach, we have recently solved a parameterized version of a well-known industrial case study for the first time: we synthesize a component implementation for a (simplified) AMBA bus controller, such that copies of this component can be composed to obtain correct controllers for an arbitrary number of clients.