Dropbox Paper

Deductive Verification of Distributed Algorithms with Why3

Leader Election Problem

The nodes in a network need to designate exactly one of them (the leader) for a given purpose.

One way to solve the problem is to assign a unique ID to each node and use a notion of order. If IDs are integer numbers, then the maximum (or minimum) is unique and can be designated as leader.

Chang-Roberts Algorithm

This is a maximum-finding algorithm for a unidirectional ring network.

Each node sends id to successor in the ring and enters a message-handling loop

Messages with id higher/lower than the receiver’s are respectively forwarded/discarded

A node receiving its own id claims to be leader

We model the ring as follows:

type node = int

val constant n_nodes : int

axiom n_nodes_ax : 2 <= n_nodes

let function next (x:node) : node

requires { 0<=x<n_nodes }

ensures { 0<=result<n_nodes }

ensures { (0<=x<n_nodes-1 /\ result=x+1) \/ (x=n_nodes-1 /\ result=0) }

ensures { (0<result<n_nodes /\ x=result-1) \/ (result=0 /\ x=n_nodes-1) }

= mod (x+1) n_nodes

let function pred (x:node) : node

requires { 0<=x<n_nodes }

ensures { 0<=result<n_nodes }

ensures { x = next result }

= mod (x-1) n_nodes

Nodes have unique IDs:

type id = int

val function id node : id

axiom uniqueIds : forall i j :node. id i = id j <-> i=j

Note that we do not fix any ID-assigning function. It suffices that this function assigns unique IDs.

System configurations are modeled by two local state variables (i.e. node maps):

a Boolean that becomes true when the node claims to be the leader;

a list of incoming messages.

​​Leader Election Problem

Leader Election Problem