I/O automata and verification of group communications software

We expect to use the LPE in the on-going verification of Ensemble. We will explore using PVS formalizations of protocols in terms of I/O automata of Lynch [] being done at the Naval Research Laboratory. Below we illustrate this method on a simple example.

One of the protocols of the Ensemble group communication systems is implemented by the Elect layer. Its purpose is to elect a coordinator for the group from among the processes which are not suspected to have failed. Initially and on specific request, one coordinator is selected externally while at runtime each process has to decide whether it has to elect himself coordinator if other processes have failed. To make sure, that the subgroup of correct processes will always have exactly one coordinator, each process maintains a list of suspected processes, which will be updated in each cycle, and its own rank in the group. The following extract from the original code of Ensemble's Elect layer shows how the election algorithm is realized.

let hdlrs s (ls,vs) {up_out=up;upnm_out=upnm;dn_out=dn;dnlm_out=dnlm;dnnm_out=dnnm} =
  .
  let upnm_hdlr ev = match getType ev with
  | EInit ->  upnm ev ;
              if ls.rank = vs.coord then (
                Once.set s.elect ;
                dnnm (Event.create EElect[])
              )
  | EElect -> Once.set s.elect ;
              upnm ev
  | ESuspect ->  s.suspects <- Arrayf.map2 (||) s.suspects (getSuspects ev) ;
                 if Arrayf.min_false s.suspects >= ls.rank then (
                       Once.set s.elect ;
                       dnnm (Event.create Elect[])
                     )
  | _ -> upnm ev
  .

This code corresponds to a finite I/O automaton whose states are encoded in the (parameterized) variable s , whose outputs are described by calls to outgoing event handlers (upnm ev, dnnm (Event.create ...). The automation distinguishes the direction of an input event (Up,Dn), its type ( Init, Elect, Suspect, ...), and a list of suspected processes which is empty if the type is not Suspect. Its transition table begins as follows

 

$$s_{\mbox{\footnotesize\em coord,sus,e}} s_{\mbox{\footnotesize\em r,sus,true}} s_{\mbox{\footnotesize\em r,sus,e}}$$ Up,Init, S

Since we have developed tools for importing Ensembles code into the Nuprl system, we can treat the actual implementation of Ensemble as Nuprl terms and reason about them. This makes it possible to relate the running code to the I/O automaton and prove by partial evaluation (i.e. Nuprl's computation rules) that the code computes the correct state and output events for each line in the automaton's transition table.

Furthermore we can now state the above mentioned properties of the layer and prove formally that the code makes sure that there is always exactly one coordinator.