FRIDA 2018

The 5th Workshop on Formal Reasoning in Distributed Algorithms

CAV workshop at FLoC 2018 (Oxford, UK) on July 13, 2018

FLoC 2018

Important Dates

FLoC early registration June 6, 2018
FLoC regular registration June 25, 2018
Workshop date July  13, 2018

Preliminary program

The program of FRIDA is available from the website of FLoC. However, we will publish the last minute changes at this workshop page, as it make some time for the updates to propagate to the official FLoC program.

9:30-10:30 Session 1
Ethan Buchman TBA
Giorgio Delzanno Formal Verification of Internet of Things Protocols
11:00-12:30 Session 2
Michael Emmi Specifying Non-Atomic Methods of Concurrent Objects
Stefan Jaax Peregrine – A Tool for Population Protocols
Adam Shimi From Asynchronous Message-Passing Models To Rounds
14:00-15:30 Session 3
Constantin Enea Specifying and Verifying Concurrent Objects
Andrea Cerone Making Parallel Snapshot Isolation Serializable
Jure Kukovec Parameterized Reachability for All Flavors of Threshold Automata
16:00-17:30 Session 4
Andreas Pavlogiannis Stateless model-checking under the data-centric view
Ilina Stoilkovska Parameterized Model Checking of Synchronous Distributed Algorithms by Abstraction

Talks

If you like to give a talk at FRIDA, but have not been invited yet, send the talk title and a short abstract (max. one page) to the organizers. Presentation of papers published elsewhere is acceptable and encouraged, provided that the material fits the scope of the workshop. There will be no formal workshop proceedings — therefore, the work will be considered “unpublished”.

Registration

Please register at the FLoC registration site.

Abstracts

Adam Shimi. From Asynchronous Message-Passing Models To Rounds.

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.

Andrea Cerone. Making Parallel Snapshot Isolation Serializable.

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.

Giorgio Delzanno. Formal Verification of Internet of Things Protocols

TBA

Michael Emmi. Specifying Non-Atomic Methods of Concurrent Objects

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.
Constantin Enea. Specifying and Verifying Concurrent Objects
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.

Stefan Jaax. Peregrine – A Tool for Population Protocols

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.

Jure Kukovec. Parameterized Reachability for All Flavors of Threshold Automata
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.

Andreas Pavlogiannis. Stateless model-checking under the data-centric view.

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.

Ilina Stoilkovska. Parameterized Model Checking of Synchronous Distributed Algorithms by Abstraction

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.

Summary of the workshop

Distributed algorithms is an active research field; their applications range from Internet applications over cloud computing to safety-critical control systems. Whereas many applications are of critical importance, the correctness of distributed algorithms is usually based on very subtle mathematical arguments. Consequently, one easily can make mistakes with hand-written proofs, which reduces the trust in the correctness of these systems.

In the last decades, formal methods were proven to be useful for the verification of many hardware and software systems. For distributed algorithms, the application of formal methods was limited: formal methods have been used for finding bugs in distributed algorithms, and to a much smaller extent formal methods were used in computer-aided verification of simple distributed algorithms. However, to verify more involved distributed algorithms, one cannot easily apply existing verification tools. To be eventually able to do this, an interdisciplinary effort from the concerned fields of formal methods, logic in computer science, and distributed algorithm theory is required.

The topics of interest for the third FRIDA workshop are:

  • models for distributed algorithms
  • model checking
  • proof assistants & theorem proving
  • parameterized model checking
  • integration of different verification techniques
  • concurrency
  • distributed algorithm theory
  • benchmark distributed algorithms
  • fault tolerance
  • synthesis
  • automated code generation for distributed systems
  • run-time verification of distributed systems

Organization

Previous editions

Starting a productive dialogue between distributed algorithms and verification communities was the goal of a successful Dagstuhl Seminar “Formal Verification of Distributed Algorithms” which was held in April 2013. During this seminar, the participants agreed that a series of workshops should be held in order to strengthen the community that does research on these issues. The 1st workshop on Formal Reasoning in Distributed Algorithms took place in Vienna as part of the Vienna Summer of Logic’14 and Federated Logic Conference’14. The 2nd FRIDA workshop took place in Grenoble as part of FORTE’15. The 3rd FRIDA workshop was organized in Marrakech as part of NETYS’16. The 4th FRIDA workshop took place in Vienna as part of DISC 2017.