Formal Reasoning in Distributed Algorithms (FRIDA 2016)
May 17, 2016
Satellite workshop of NETYS 2016 (Marrakech, Morocco)
The workshop will take place on May 17, instead of May 16-17, as was originally planned. We will announce the workshop program soon.
|9:00-10:00||Parosh Aziz Abdulla||Automatic Verification of Linearization Policies|
|10:00-10:30||Hugues Fauconnier||Proving a distributed algorithm with TLA+: an experience|
|11:00-12:00||Ahmed Bouajjani||Verifying concurrent objects: from Linearizability to Reachability (joint work with Constantin Enea, Michael Emmi, and Jad Hamza)|
|12:00-12:30||Gadi Taubenfeld||The Computability of Relaxed Data Structures: Queues and Stacks as Examples (joint work with Nir Shavit)|
|14:00-15:30||Rachid Guerraoui||Understanding Universality in Distributed Computing (joint session with METIS)|
|16:00-16:30||Gustavo Petri||Safe and Scalable Programming for the Cloud (joint work with Bo Sang, Masoud Saeida Ardekani, Srivatsan Ravi, and Patrick Eugster)|
|16:30-17:00||Marijana Lazic||Completeness of Bounded Model Checking for Threshold-Based Distributed Algorithms: Safety & Liveness (joint work with Igor Konnov, Helmut Veith, and Josef Widder)|
|17:00-17:30||Ilyass El Kassmi||Reasoning on Security Requirements in Web Service Composition (joint work with Zahi Jarir)|
Do not forget to register at the NETYS registration page. Since FRIDA takes place on May 17, please pay the METIS registration fee.
|Deadline for NETYS special accommodation rates||April 15, 2016|
|Workshop date||May 17, 2016|
Parosh Aziz Abdulla
We consider the problem of proving linearizability for concurrent threads that access a shared data structure. Such systems give rise to unbounded numbers of threads that operate on an bounded data domain and that access dynamically allocated memory. Furthermore, proving linearizability is harder than proving control state reachability due to existentially quantified linearization points. The problem is further complicated by the presence of advanced features such as non-fixed linearization points, speculation, and helping. In this presentation, we present a framework that can automatically verify linearizability for concurrent data structures that implement sets, stacks, and queues. We use a specification formalism for linearization techniques which allows the user to specify, in a simple and and concise manner, complex patterns including non-fixed linearization points. Then, we define abstraction techniques that allow to make the size of the data domain and the number of threads finite.
Most concurrent data structures being designed today are versions of known sequential data structures. However, in various cases it makes sense to relax the semantics of traditional concurrent data structures in order to get simpler and possibly more efficient and scalable implementations. For example, when solving the classical producer-consumer problem by implementing a concurrent queue, it might be enough to allow the dequeue operation (by a consumer) to return and remove one of the two oldest values in the queue, and not necessarily the oldest one. We define infinitely many possible relaxations of several traditional data structures and objects: queues, stacks, multisets and registers, and examine their relative computational power.
Replicated state machine is a fundamental computing construct for it essentially makes a distributed system emulate a highly available, centralized one, using a consensus abstraction through which processes agree on common decisions. The idea is at the heart of the fault-tolerance of most data centers today. Any sequential object is modeled by a state machine that can be replicated over all processes of the system and accessed in a wait-free manner: we talk about the universality of the construct and of its underlying consensus abstraction. Yet, consensus is just a special case of a more general abstraction, k-set consensus, where processes agree on at most k different decisions. It is natural to ask whether there exists a generalization of state machine replication with k-set agreement, for otherwise distributed computing would not deserve the aura of having an underpinning Theory as 1 (k-set consensus with k=1) would be special. The talk will recall the classical state machine replication construct and show how, using k-set consensus as an underlying abstraction, the construct can be generalized to implement k state machines of which at least one makes progress, generalizing in a precise sense the very notion of consensus universality. The work is joint with Eli Gafni Rachid Guerraoui is professor of Computer Science at the Swiss Federal Institute of Technology in Lausanne where he leads the Distributed Programming Laboratory.
Rachid is fellow of the ACM and has recently been awarded an advanced ERC grant and a Google focused award. He has also been affiliated in the past with the Research Center of Ecole des Mines de Paris, the Commissariat a l’Energie Atomique in Saclay, Hewlett-Packard Laboratories in Palo Alto and the Massachusetts Institute of Technology.
In this talk I will present AEON (Atomic Events and Ownership Networks), a programming model for safe and scalable cloud computing. AEON is based on the well-known paradigms of object-orientation and event-driven programming. AEON’s runtime system guarantees a linearizable and deadlock-free semantics for events that span across multiple objects and servers. Moreover, to achieve an economical and scalable solution, our runtime system provides seamless elasticity (the capability to adapt the resources usage to the actual workload), and exploits the object graph — the ownership network — to enhance parallelism. In this talk will concentrate on the safety aspects of the semantics of AEON, and show some experimental scalability results.
The interplay of safety and liveness is essential for fault-tolerant distributed algorithms. Still, existing parameterized verification literature heavily focuses
on safety properties, e.g., reachability. We introduce an automated method for parameterized model checking of liveness properties of distributed algorithms. Our method is based on a small counterexample property that states that, despite parameterization, counterexamples have a predictable size and structure. We substantiate our theoretical results by an experimental evaluation in which we verify liveness of state-of-the-art fault-tolerant distributed algorithms, most of which were out of reach for existing techniques.
Ilyass El Kassmi
The purpose of this work is to suggest an approach for the formalization, integration and verification of security requirements in composition of Web services. This approach is based on the finite state machine to model both functional and non-functional requirements. Our main focus concerns dependencies between security requirements that will be attached to functional requirements in order to avoid feature interaction. To support the reasoning on failures and faults detection, the proposed architecture used the model checking tool UPPAAL.
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
- distributed algorithm theory
- benchmark distributed algorithms
- fault tolerance
- automated code generation for distributed systems
- run-time verification of distributed systems
- Swen Jacobs (Saarland University)
- Igor Konnov (TU Wien)
- Stephan Merz (INRIA Nancy & LORIA)
- Josef Widder (TU Wien)
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 first workshop on Formal Reasoning in Distributed Algorithms (FRIDA’14) took place in Vienna as part of the Vienna Summer of Logic’14 and Federated Logic Conference’14. The second FRIDA workshop (FRIDA’15) took place in Grenoble as part of FORTE’15.