Verification of Token-based Mutual Exclusion with Why3
Dijkstra’s Self-stabilizing Algorithms
Consider a locally-shared memory system model consisting of a set of nodes or processes arranged in a given topology or network. Nodes contain local state registers, to which some neighboring nodes have read(but not write) access.
These algorithms allow for the implementation of a mutual-exclusion policy based on tokens that grant the execution privilege. Note that:
Tokens are symbolic: nodes decide if they have a token by accessing their neighbors’ states and comparing them with their own state.
When a node has a token it may execute
When it executes it will change its own state, which will result in it losing the token, which is“passed” to one of its neighbors.
The most interesting aspect of these algorithms is that they are self-stabilizing, i.e. they converge to legal single-token configurations, and then stay in such configurations(circulating the token among all nodes) until a fault occurs that may again produce a higher number of tokens.
In this class we will
Formalize the algorithms
Prove the safety property of the closure phase of execution: under normal operation, legal configurations(i.e. with a single token) are preserved with system transitions
Notprove the convergence property: under certain conditions, ilegal configurations(with more than one token) inevitably converge to legal ones
Ring System
In this system the nodes are arranged in a ring. The ring is unidirectional: nodes have read access to the state of only onde node(their predecessor in the ring), and tokens are passed in only one direction.
Node states are integer numbers. Having a token is defined as follows:
Node 0 has a token if it has the same state as node N-1
Every other node j has a token if it has a different state w.r.t. node j-1
When a node executes it changes its state in the following way:
Node 0 increases(+1) its state
Every other node j just copies the state of its neighbor j-1
In fact node states can be incremented modulo any constant greater than the number of nodes.
We model the system as follows(note the arbitrary choice of initial configurations):
type world = { ring : map node state }
predicate initWorld_p (w:world) =
forall n :node. w.ring[n] = if n=n_nodes-1then1else0
predicate has_token (w:world) (i:node) =
(i = 0 /\ w.ring[i] = w.ring[n_nodes-1])
\/
(i > 0 /\ i < n_nodes /\ w.ring[i] <> w.ring[i-1])
The semantics of the system are easy to express, with only one action function:
Dijkstra’s Self-stabilizing Algorithms
Ring System
type world = { ring : map node state }
predicate initWorld_p (w:world) = forall n :node. w.ring[n] = if n=n_nodes-1 then 1 else 0
predicate has_token (w:world) (i:node) = (i = 0 /\ w.ring[i] = w.ring[n_nodes-1]) \/ (i > 0 /\ i < n_nodes /\ w.ring[i] <> w.ring[i-1])