# FRIDA 2018

# The 5^{th} Workshop on Formal Reasoning in Distributed Algorithms

### CAV workshop at FLoC 2018 (Oxford, UK) on **July 13, 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*

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

**Swen Jacobs (Saarland University)****Igor Konnov (INRIA Nancy and TU Wien)****Stephan Merz (INRIA Nancy & LORIA)****Josef Widder (TU Wien)**

### 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 1^{st} 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 2^{nd} FRIDA workshop took place in Grenoble as part of FORTE’15. The 3^{rd} FRIDA workshop was organized in Marrakech as part of NETYS’16. The 4^{th} FRIDA workshop took place in Vienna as part of DISC 2017.