206
23 March 2017 - 14h00
Automated generation of a distributed implementation from a formal model of concurrent processes interacting via multiway rendezvous.
by Hugues Evrard from Imperial College, London
Abstract: Formal verification often targets the model of a system, although the
actual implementation may still be written by hand, in which case even a
small semantics difference between the model and its implementation can
ruin the verification effort. Such risky discrepancies are avoided by
using automatic code generator from models.
In this talk, we focus on the generation of a distributed implementation
from the formal model of concurrent non-deterministic processes
interacting via multiway rendezvous. The implementation
is made of several executable distributed over machines connected by a
network, and relies on a protocol to achieve multiway rendezvous over
asynchronous message passing (e.g. TCP). We set up a formal verification
framework based on model-checking for such multiway rendezvous
protocols, and we applied it to three existing protocols, what led to
the discovery of possible deadlocks previously undocumented.
Equipped with this verification framework, we iteratively design a
protocol that gather the best existing ideas, to reach the most
efficient multiway rendezvous protocol that we are aware of, achieving
more than a thousand rendezvous per seconds between processes on
different machines. We implemented this protocol into the Distributed
LNT Compiler (DLC), which generates distributed C programs from a formal
model expressed in LNT. As a case study, we model the Raft consensus (à
la Paxos) algorithm in LNT, compile it down to a distributed
implementation via DLC, and compare its performance with a commercial
hand-written implementation.
