FRIDA 2015

Formal Reasoning in Distributed Algorithms (FRIDA 2015)

Satellite workshop of DisCoTec 2015

Scope

In the past decades, formal methods proved useful for the verification of many classes of hardware and software systems. For distributed algorithms, the application of formal methods and corresponding tools has mostly been limited to finding bugs in distributed algorithms. To a much smaller extent, formal methods have been used for the computer-aided verification of simple distributed algorithms. However, existing verification techniques and tools do not easily scale to handle more involved distributed algorithms. We believe that an interdisciplinary effort involving specialists in formal methods, logic in computer science, and the theory and design of distributed algorithms is required.

The topics of interest for the second FRIDA workshop are:

  • models for concurrent and distributed algorithms
  • theory of distributed algorithms
  • design and verification of fault-tolerant algorithms
  • benchmarking of distributed algorithms
  • (parameterized) model checking
  • proof assistants and theorem proving
  • integration of different verification techniques
  • formal techniques for synthesis
  • automated code generation for distributed systems
  • run-time verification of distributed systems
  • performance analysis of distributed systems based on formal methods
  • analysis of probabilistic and real-time distributed systems

Program (download as pdf)

joint session with ICE 2015
09:00-10:00 Leslie Lamport (invited talk) TLA+ for Non-Dummies
10:00-10:30 Richard Trefler, Kedar Namjoshi Symmetry Reduction For Dynamic Process Networks [slides]
10:30-11:00 coffee break
11:00-11:30 Francesco Alberti, Silvio Ghilardi, Andrea Orsini and Elena Pagani SMT-based approaches to Model Checking of Distributed Broadcast Algorithms [slides]
11:30-12:00 Giovanni Tito Bernardi, Andrea Cerone, Alexey Gotsman and Hongseok Yang Analysing and Optimising Parallel Snapshot Isolation
12:00-12:30 Valter Balegas, Sérgio Duarte, Carla Ferreira, Marc Shapiro, Mahsa Najafzadeh, Rodrigo Rodrigues and Nuno Preguiça Putting Consistency Back into Eventual Consistency
12:30-13:30 lunch break
13:30-14:30 Vijay Garg (invited talk) Solved and Unsolved Problems in Monitoring Distributed Computations [slides]
14:30-15:00 C. Aiswarya, Benedikt Bollig and Paul Gastin An Automata-Theoretic Approach to the Verification of Distributed Algorithms [slides]
15:00-15:30 Pierre Courtieu, Lionel Rieg, Sebastien Tixeuil and Xavier Urbain Impossibility of Gathering, a Certification [slides]
15:30:16:00 coffee break 
16:00-16:30 C. Aiswarya, Paul Gastin and K. Narayan Kumar Maintaining Latest Information beyond Channel Bounds  [slides]
16:30-17:00  Ana Sokolova  Local Linearizability [slides]
17:00-17:30 Liana Hadarean, Alex Horn, and Tim King A Concurrency Problem with Exponential DPLL(T) Proofs [slides]

Format

This one-day workshop will include invited talks, presentations of position papers, including work-in-progress and published work, and discussion periods. We are planning to collect the abstracts and the presentations for publication on the workshop site. In addition to some invited talks, the program will include short presentations of contributed position papers, a challenge problem session, and ample room for lively discussion and debate on the issues raised.

Important Dates

Workshop day June 5, 2015

Submission instructions

We seek submissions reporting on theory, applications, case studies or open questions at the interface of formal methods and distributed algorithms. Contributions may range from extended abstracts of one or two pages to full papers of twenty pages — preferably, in Easychair format — and should be submitted as pdf files. Presentation of papers published elsewhere is acceptable and encouraged. There will be no formal workshop proceedings — therefore, the work will be considered “unpublished”. However, accepted contributions will be made accessible from the Workshop Web page. Use the following link to submit your abstract.

Organization

Contact

frida2015@easychair.org

Previous editions

Abstracts

Leslie Lamport, Microsoft Research (invited talk). TLA+ for Non-Dummies.

Abstract: The motivation underlying the TLA+ specification language and some of the language’s subtleties.

Vijay Garg, Cullen Trust Endowed Professor. The University of Texas at Austin (invited talk). Solved and Unsolved Problems in Monitoring Distributed Computations. [slides]

Abstract: Monitoring distributed computations is a fundamental technique for testing distributed programs and runtime verification. In this talk, I will discuss seven important topics related to monitoring distributed computations. These
topics are: online chain decomposition, distributed trigger counting, enumeration of consistent global states, detection of global safety predicates, abstraction of distributed computations, monitoring for liveness properties and controlling distributed computations. For each of these topics, I will give a quick survey of what we know and the statement of an open problem.

Richard Trefler, Kedar Namjoshi. Symmetry Reduction For Dynamic Process Networks.

Abstract: Dynamic process networks are used to model communication protocols and sensor networks. Each network instance has a fixed topology but the dynamic nature of the network means that the set of processes and their interconnections may change as the network computation unfolds. Local symmetries describe similarities between process neighborhoods. These similarities are used to establish equivalence classes of network processes across topologies of the dynamically changing network. Symmetry reduction replaces a given network with a fixed network whose elements span the equivalence classes of network symmetries.
We outline some of the challenges relating to automated symmetry detection, symmetry reduction and the analysis of the symmetry
reduced process network, that arise in the analysis of dynamic network descriptions.

Francesco Alberti, Silvio Ghilardi, Andrea Orsini, and Elena Pagani. SMT-based approaches to Model Checking of Distributed Broadcast Algorithms – Work In Progress –.

Abstract: The validation of distributed algorithms is a crucial, although challenging, task. The processes executing these algorithms communicate to one another, their actions depend on the messages received, and their number is arbitrary. These characteristics are captured by so called reactive parameterized systems. The task of validating or refuting properties of these systems is daunting, due to the difficulty of limiting the possible evolutions, thus having to deal with genuinely infinite-state systems.
In this paper, we consider distributed algorithms to solve the reliable broadcast problem in the presence of crash, send-omission, and byzantine failures. We study the properties of these algorithms using Model Checker Modulo Theories (MCMT). MCMT is able to verify safety properties of infinite-state reactive parameterized systems, for any number of processes. It adopts a pure SMT (Satisfiability Modulo Theories) approach, due to its flexibility. It uses some form of abstractions, and involves acceleration mechanisms in order to increase computation efficiency.
In this work, we study how to model the algorithms in MCMT according to two paradigms: array-based systems and counter abstraction. The former uses unbounded arrays to represent the states of the processes. The latter exploits a characteristic of the considered algorithms, which consists in determining the behavior of the processes de- pending on the number of messages they receive from other processes (threshold-guarded algorithms). The algorithms are modeled according to both paradigms, or using a hybrid approach mixing arrays with counter abstraction. We discuss the rationale of our modeling choices and show how to use the characteristics of MCMT to perform the validation. We report a performance evaluation of the computation with the different models, and (in the counter abstraction paradigm) compare the results with equivalent modelization in both Z3 and nuXmv, obtained by translating our models.

Giovanni Tito Bernardi, Andrea Cerone, Alexey Gotsman and Hongseok Yang. Analysing and Optimising Parallel Snapshot Isolation.

Abstract: Modern Internet services often rely on geo-replicated databases that provide consistency models for transactions weaker than serialisability. We investigate a promising model of parallel snapshot isolation (PSI), which weakens the classical snapshot isolation in a way that allows more scalable geo-replicated implementations. To facilitate writing applications using PSI databases, we propose two static analysis techniques. First, we present a criterion for checking if an application is robust, i.e., behaves the same whether using a PSI database or a serialisable one. Second, we propose a criterion for checking when a set of transactions executing on PSI can be chopped into smaller pieces without introducing new behaviours; this allows optimising transactions to execute more efficiently. Our results are initial steps towards understanding how the behaviour of applications is affected by consistency models of geo-replicated databases.

Valter Balegas, Sérgio Duarte, Carla Ferreira, Marc Shapiro, Mahsa Najafzadeh, Rodrigo Rodrigues and Nuno Preguiça. Putting Consistency Back into Eventual Consistency.

Abstract: Geo-replicated storage systems are at the core of current Internet services. The designers of the replication protocols used by these systems must choose between either supporting low-latency, eventually-consistent operations, or ensuring strong consistency to ease application correctness. We propose an alternative consistency model, Explicit Consistency, that strengthens eventual consistency with a guarantee to preserve specific invariants defined by the applications. Given these application-specific invariants, a system that supports Explicit Consistency identifies which operations would be unsafe under concurrent execution, and allows programmers to select either violation-avoidance or invariant-repair techniques. We show how to achieve the former, while allowing operations to complete locally in the common case, by relying on a reservation system that moves coordination off the critical path of operation execution. The latter, in turn, allows operations to execute without restriction, and restore invariants by applying a repair operation to the database state. We present the design and evaluation of Indigo, a middleware that provides Explicit Consistency on top of a causally-consistent data store. Indigo guarantees strong application invariants while providing similar latency to an eventually-consistent system in the common case.

Benedikt Bollig, C. Aiswarya, and Paul Gastin. An Automata-Theoretic Approach to the Verification of Distributed Algorithms.

Abstract: We introduce an automata-theoretic method for the verification of distributed algorithms running on ring networks. In a distributed algorithm, an arbitrary number of processes cooperate to achieve a common goal (e.g., elect a leader). Processes have unique identifiers (pids) from an infinite, totally ordered domain. An algorithm proceeds in synchronous rounds, each round allowing a process to perform a bounded sequence of actions such as send or receive a pid, store it in some register, and compare register contents wrt. the associated total order. An algorithm is supposed to be correct independently of the number of processes. To specify cor- rectness properties, we introduce a logic that can reason about processes and pids. Referring to leader election, it may say that, at the end of an execution, each process stores the maximum pid in some dedicated register. Since the verification of distributed algorithms is undecidable, we propose an underapproximation technique, which bounds the number of rounds. This is an appealing approach, as the number of rounds needed by a distributed algorithm to conclude is often exponentially smaller than the number of processes. We provide an automata-theoretic solution, reducing model checking to emptiness for alternating two-way automata on words. Overall, we show that round-bounded verification of distributed algorithms over rings is PSPACE-complete.

Pierre Courtieu, Lionel Rieg, Sebastien Tixeuil, and Xavier Urbain. Impossibility of Gathering, a Certification.

Abstract: Recent advances in Distributed Computing highlight models and algorithms for autonomous swarms of mobile robots that self-organise and cooperate to solve global objectives. The overwhelm- ing majority of works so far considers handmade algorithms and proofs of correctness.
This paper builds upon a previously proposed formal framework to certify the correctness of impossibility results regarding distributed algorithms that are dedicated to autonomous mobile robots evolving in a continuous space. As a case study, we consider the problem of gathering all robots at a particular location, not known beforehand. A fundamental (but not yet formally certified) result, due to Suzuki and Yamashita, states that this simple task is impossible for two robots executing deterministic code and initially located at distinct positions. Not only do we obtain a certified proof of the original impossibility result, we also get the more general impossibility of gathering with an even number of robots, when any two robots are possibly initially at the same exact location.

C. Aiswarya, Paul Gastin, and K. Narayan Kumar. Maintaining Latest Information beyond Channel Bounds.

Abstract: Consider distributed systems consisting of a number of processes communicating with each other asynchronously by sending messages via FIFO channels. It is crucial for such systems that every process can maintain deterministically the latest information about other processes. To do so, any process p, upon receiving a message from a process q, should determine for every process r, whether the latest event on r that p knows of is more recent than the latest event on r that q knows of. Solving this problem, while storing and exchanging only a bounded amount of information, is extremely challenging and not always possible. This is known as the gossip problem. A solution to this is the key to solving numerous important problems on distributed systems. So far, gossip has been solved only for channel bounded systems. In this paper we solve the gossip problem for a much richer class, going beyond a priori channel bounds.

Ana Sokolova. Local Linearizability.

Abstract: Linearizability is the most accepted consistency condition used to describe the semantics of concurrent data structures. One of its benefits is its intuitive definition that is well understandable to system designers and programmers. However, linearizability is very strong and often linearizable implementations show unsatisfactory performance and scalability. To open up possibilities for more efficient implementations of concurrent data structures, a plethora of consistency conditions has been considered in the literature.
In this paper, we utilise the idea of a \emph{decomposition principle} and define \emph{local linearizability}, a new consistency condition that is closely connected to linearizability. Local linearizability is weaker than linearizability for pools, queues, and stacks. Local linearizability is intuitive, verifiable, and opens up possibilities for new efficient implementations. In particular, we provide new well-performing and scalable implementations of locally linearizable concurrent queues and stacks.

Liana Hadarean (Oxford), Alex Horn (Oxford) and Tim King (Verimag). A Concurrency Problem with Exponential DPLL(T) Proofs.

Abstract: Many satisfiability modulo theories solvers (SMT) implement a variant
of the DPLL(T) framework which separates theory-specific reasoning from reasoning on the propositional abstraction of the formula. Such solvers conclude that a formula is unsatisfiable once they have learned enough theory conflicts to derive a propositional contradiction. However some problems, such as the diamonds problem, require learning exponentially many conflicts. We give a general criterion for establishing lower bounds on the number of theory conflicts in any DPLL(T) proof for a given problem. We apply our criterion to two different state-of-the-art symbolic partial-order
encodings of a simple, yet representative concurrency problem. Even though one of the encodings is asymptotically smaller than the other,
we establish the same exponential lower bound proof complexity for both. Our experiments confirm this theoretical lower bound across multiple solvers and theory combinations.