Reviews

Adapted from:

[DG+01] M.C.A. Devillers, W.O.D. GriAEoen, J.M.T Romijn, and F.W. Vaandrager. Verification of a leader election protocol — formal methods applied to IEEE 1394. Technical Report CSI-R9728, Computing Science Institute, University of Nijmegen, December 1997. Also, Formal Methods in System Design, 2001.

This model describes a leader election protocol used in Firewire, an IEEEstandard for connecting consumer electronic devices. The model is a straightforward translation into Alloy of a model [DG+01] developed in Lynch’s IO Automata which has been analyzed using PVS, a theorem prover, but which, as far as we know, has not been subjected to fully automatic analysis. We are able to express the key correctness property — that exactly one leader is elected — more directly, as a trace property rather than a refinement property, and can check it without the need for the 15 invariants used in the more traditional proof. And the analysis does not hardwire a particular topology, so would be tricky to do with a standard model checker.

The network is assumed to consist of a collection of nodes connected by links. Each link between a pair of nodes is matched by a link in the other direction. Viewing a link and its dual as a single, undirected edge, the network as a whole is assumed to form a tree. The purpose of the algorithm is to construct such a tree; in the model, this is achieved by labelling some subset of the links as parent links (each pointing from a node to its parent), and by marking a single node as the root.

The algorithm, described in detail elsewhere [DG+01], works briefly as follows. When a node detects that all of its incoming links (or all but one) has been marked as a parent link, it sends a message on each outgoing link, either an acknowledgment (indicating its willingness to act as parent), or a request (indicating its desire to be a child), according to whether the dual of the outgoing link has been marked or not. Leaf nodes (with only one incoming link) may thus initiate the algorithm by sending requests to their adjacent nodes. Performing this action changes a node’s status from {\em waiting} to {\em active}. A node that is still waiting, and which receives a message on a link, may label that link a parent link. Once active, a node that receives an acknowledgment on a link may also label the link, but if it receives a request, instead changes its node status to {\em contending}. The resolving of contentions is modelled simplistically by a single action that arbitrarily
labels one of the two links a pair of contending nodes. Finally, a node all of whose incoming links are parent links designates itself a root.

The specification is given below. Each signature introduces a basic type and some relations whose first column has that type:

\begin{itemize}

\item {\em Msg} represents the type of messages. {\em Req} is the request message and {\em Ack} is the acknowledgment message; these are actually declared as singleton (keyword {\em static}) subsets of {\em Msg}, the set of all messages, that form a partition (keyword {\em part}).

\item {\em Node} represents the nodes of the network. The relations {\em to} and {\em from} associate each node with a set of incoming and outgoing links
respectively.

\item {\em Link} represents the links. The relations {\em target} and {\em source} map a link to its end nodes; {\em reverse} maps a link to its dual. The
facts in the signatures {\em Node} and {\em Link} ensure that all these relations are consistent with one another: that the incoming links of a node are those whose target is that node, etc.

\item {\em Op} introduces a set of names for the operations of the protocol. This is merely for convenience; it allows us to ask for an execution in which named operations occur, or example.

\item {\em State} represents the global states. Each state has a partition of the nodes into one of four statuses: {\em waiting} to participate, {\em active} (having sent messages on outgoing links), {\em contending} (having sent a request on a link and received a request on its dual), and {\em elected} (having designated itself as a root). A set of links are labelled as parent links. There is a message queue associated with each link. Finally, the state is associated with the operation that produced it.

\item {\em Queue} represents the message queues. Each queue has a slot that optionally contains a message; the relation {\em slot} is a partial function from queues to messages. In our first attempt at a model, we represented a queue as a sequence (a partial function from a prefix of the integers to messages), but having checked that no queue ever contained more than one message, we simplified the model. The {\em overflow} field is included just in case this was a mistake; a write to a queue that already contains a message puts an arbitrary value there, which is easily detected.

\end{itemize}

The {\em facts} record the assumptions about the topology. The one named {\em Topology} says that there is some partial function on nodes and some root such
that (1) every node is reachable from the root ({\tt *r} being the reflexive transitive closure of the relation {\tt r}); (2) there are no cycles (expressed by saying that the transitive closure has no intersection with the identity relation on nodes); and (3) the relation obtained by following the {\em source} relation backwards (from a node to the link for which it is a source), and then the {\em target} relation forwards (from the link to its target) is this relation, plus its transpose (so that each tree edge becomes two links). Although the quantifier appears to be higher-order, it will be skolemized away by the analyzer.

The {\em functions} of the model are parameterized formulas. The function {\em Trans} relates a pre-state {\tt s} to a post-state {\tt s‘}. It has a case for each operation. Look at the clause for the operation {\em WriteReqOrAck}, for example. If this operation is deemed to have occurred, each of the constraints in the curly braces must hold. The first says that the labelling of links as parent links is unchanged. The second constraint (the quantified formula) constrains with respect to the node at which the operation occurs. The subformulas, from first to last, say that the node belongs to the waiting set before and the active set afterwards; that there is at most one ({\em sole}) link that is incoming but not a parent link in the pre-state; that there are no changes to node status except at this node; that a message is queued onto each outgoing link; and that queues on all other links are unchanged.

An ‚invoked‘ function is simply short for the formula in its body with the formal arguments replaced by the actual expressions. {\em WriteQueue}, for example, says that if the queue’s slot is not filled in the pre-state, then the new queue in the post-state (given the local name {\tt q}) contains the message {\tt m} in its slot, and has no message in its overflow. Otherwise, some message is placed arbitrarily in the overflow, and the slot is unconstrained. In {\em WriteReqOrAck}, the arguments {\tt s} and {\tt s‘} are bound to the {\tt s} and {\tt s‘} of {\em Trans}; {\tt x} is bound to one of the outgoing links from the set {\tt n.from}; and {\tt msg} is bound either to the acknowledgment or request message.

The function {\em Execution} constrains the set of states. It makes use of a library module that defines a polymorphic ordering relation. The expression {\tt Ord[State]} gives an ordering on all states. The two formulas of the function say that {\tt Initialization} holds in the first state, and that any pair of adjacent states is related by {\tt Trans}. The function {\em NoRepeats} adds the constraints that there are no equivalent states in the trace, and that no stuttering occurs.

The three assertions are theorems for which the analyzer will search for counterexamples. They assert respectively that: in every state of the trace, there is at most one node that has been elected; that there is some state in which a node has been elected; and that no queue overflows.

The rest of the model is a collection of commands executed to find instances of the functions or counterexamples to the theorems. We started by presenting a variety of functions as a sanity check; here, only one is given, that asks for an execution involving 2 nodes, 4 links, 4 queues and a trace of 6 states. The standard semantics of these {\em scope} declarations in Alloy is that the numbers represent an upper bound, so an instance may involve fewer than 4 queues, for example. The ordering module (not shown here), however, for technical reasons, constrains the ordered set to match its scope, so a trace with fewer than 6 states will not be acceptable.

We then established some bounds on the diameter of the state machine for various topology bounds. For 2 nodes and 2 links, for example, there are no non-repeating traces of length 4; checking traces of length 3 is thus sufficient in this case. The number of queues was limited to 5, to accommodate the empty queue, a queue containing an {\tt Ack} or {\tt Req}, and each of these with overflow. For 3 nodes and 6 links, a trace length of 8 suffices.

We then checked that for these various topology bounds, the queues never overflow. Finally, we checked the correctness properties, taken advantage of the earlier results that justify the short traces and queues. We are thus able to verify the properties for all topologies involving the given number of nodes and links, without any assumptions about trace length, queue size or the particular topological structure.

*/

module firewire_leader_election
open models/ord

sig Msg {}
static part sig Req, Ack extends Msg {}

sig Node {to, from: set Link} {
 to = {x: Link | x.target = this}
 from = {x: Link | x.source = this}
 }

sig Link {target, source: Node, reverse: Link} {
 reverse::source = target
 reverse::target = source
 }

— at most one link between a pair of nodes in a given direction
fact {no disj x,y: Link | x.source = y.source && x.target = y.target}

— topology is tree-like: acyclic when viewed as an undirected graph
fact Topology {
some tree: Node ?-> Node, root: Node {
 Node in root.*tree
 no ^tree & iden [Node -> Node]
 tree + ~tree = ~Link$source.Link$target
 }
}

sig Op {}
static disj sig Init, AssignParent, ReadReqOrAck, Elect, WriteReqOrAck,
ResolveContention, Stutter extends Op {}

sig State {
 part waiting, active, contending, elected: set Node,
 parentLinks: set Link,
 queue: Link ->! Queue,
 op: Op — the operation that produced the state
 }

fun SameState (s, s‘: State) {
 s.waiting = s‘.waiting
 s.active = s‘.active
 s.contending = s‘.contending
 s.elected = s‘.elected
 s.parentLinks = s‘.parentLinks
 all x: Link | SameQueue (s.queue[x], s‘.queue[x])
 }

fun Trans (s, s‘: State) {
 s‘.op != Init
 s‘.op = Stutter => SameState (s, s‘)
 s‘.op = AssignParent => {
  some x: Link {
   x.target in s.waiting & s‘.waiting
   NoChangeExceptAt (s, s‘, x.target)
   ! IsEmptyQueue (s, x)
   s‘.parentLinks = s.parentLinks + x
   ReadQueue (s, s‘, x)
   }}
 s‘.op = ReadReqOrAck => {
  s‘.parentLinks = s.parentLinks
  some x: Link {
   x.target in s.(active + contending)
    & if PeekQueue (s, x, Ack) then s‘.contending else s‘.active
   NoChangeExceptAt (s, s‘, x.target)
   ! IsEmptyQueue (s, x)
   ReadQueue (s‘, s, x)
   }}
 s‘.op = Elect => {
  s‘.parentLinks = s.parentLinks
  some n: Node {
   n in s.active & s‘.elected
   NoChangeExceptAt (s, s‘, n)
   n.to in s.parentLinks
   QueuesUnchanged (s, s‘, Link)
   }}
 s‘.op = WriteReqOrAck => {
  — note how this requires access to child ptr
  s‘.parentLinks = s.parentLinks
  some n: Node {
   n in s.waiting & s‘.active
   sole n.to – s.parentLinks
   NoChangeExceptAt (s, s‘, n)
   all x: n.from |
    let msg = if x.reverse in s.parentLinks then Ack else Req |
     WriteQueue (s, s‘, x, msg)
   QueuesUnchanged (s, s‘, Link – n.from)
   }}
 s‘.op = ResolveContention => {
  some x: Link {
   let contenders = x.(source + target) {
    contenders in s.contending & s‘.active
    NoChangeExceptAt (s, s‘, contenders)
    }
   s‘.parentLinks = s.parentLinks + x
   }
  QueuesUnchanged (s, s‘, Link)
  }
}

fun NoChangeExceptAt (s, s‘: State, nodes: set Node) {
 let ns = Node – nodes {
 ns & s.waiting = ns & s‘.waiting
 ns & s.active = ns & s‘.active
 ns & s.contending = ns & s‘.contending
 ns & s.elected = ns & s‘.elected
 }}

sig Queue {slot: option Msg, overflow: option Msg}

fun SameQueue (q, q‘: Queue) {
  q.slot = q‘.slot && q.overflow = q‘.overflow
 }
 
fun ReadQueue (s, s‘: State, x: Link) {
— let q = s‘.queue[x] | no q.(slot + overflow)
 no s‘.queue[x].(slot + overflow)
 all x‘ != x | s‘.queue[x‘] = s.queue[x‘]
 }

fun PeekQueue (s: State, x: Link, m: Msg) {
 m = s.queue[x].slot
 }

fun WriteQueue (s, s‘: State, x: Link, m: Msg) {
        let q = s‘.queue[x] |
 no s.queue[x].slot =>
  ( q.slot = m && no q.overflow),
  some q.overflow
 }

fun QueuesUnchanged (s, s‘: State, xs: set Link) { 
 all x: xs | s‘.queue[x] = s.queue[x]
 }

fun IsEmptyQueue (s: State, x: Link) {
 no s.queue[x].(slot + overflow)
— let q = s.queue[x] | no q.(slot + overflow)
 }
 
fun Initialization (s: State) {
 s.op = Init
 Node in s.waiting
 no s.parentLinks
 all x: Link | IsEmptyQueue (s, x)
 }

fun Execution () {
 Initialization (Ord[State].first)
 all s: State – Ord[State].last | let s‘ = OrdNext(s) | Trans (s, s‘)
 }

fun NoRepeats () {
 Execution ()
 no disj s, s‘: State | SameState (s, s‘)
 no s: State | s.op = Stutter
 }

fun NoShortCuts () {
 all s: State | — remove this to speed up analysis – Ord[State].last – OrdPrev (Ord[State].last) |
  ! Trans (s, OrdNext(OrdNext(s)))
 }

assert AtMostOneElected {
 Execution () => all s: State | sole s.elected
 }

assert OneEventuallyElected {
 Execution () => some s: State | some s.elected
 }

assert NoOverflow {
 Execution () => all s: State, x: Link | no s.queue[x].overflow
 }

run Execution for 1 Ord[State],  7 Op, 2 Msg,
 2 Node, 4 Link, 4 Queue, 6 State

— solution for 3 State but not for 4 State
run NoRepeats for 1 Ord[State],  6 Op, 2 Msg,
 2 Node, 2 Link, 2 Queue, 4 State

— solution for 8 but not 9 State
run NoRepeats for 1 Ord[State],  6 Op, 2 Msg,
 3 Node, 6 Link, 6 Queue, 9 State

— only 5 queues needed: just count
— no solution: establishes at most 3 queues needed
check NoOverflow for 1 Ord[State],  6 Op, 2 Msg,
 3 Node, 6 Link, 5 Queue, 9 State

check AtMostOneElected for 1 Ord[State],  6 Op, 2 Msg,
 3 Node, 6 Link, 3 Queue, 9 State

check OneEventuallyElected for 1 Ord[State],  6 Op, 2 Msg,
 3 Node, 6 Link, 3 Queue, 9 State