My encoding of liveness properties of distributed systems in Verdi primarily uses three sources of previous work:
- The treatment of fairness in actor systems by Agha et al. [1].
- Coq's mechanisms for coinductive predicates and corecursive functions, originally by Eduardo Gimenez [2].
- Verification of self-stabilizing population protocols in Coq by Deng and Monin [3].
Agha et al. define an operational semantics of actor systems, where the reduction rules are parameterized on certain variables (e.g., the name of the actor involved). They then define executions of actor systems as infinite sequences of system configurations, with each transition labeled with the name of the reduction rule applied, along with the arguments used as parameters. This allows them to consider only fair executions starting from some initial configuration.
A label is said to be enabled at some point in an execution if it is possible to make valid transition using the label to some new configuration. Intuitively, in the work of Agha et al., fair executions are those where no transition label becomes continuously enabled without the associated rule ever being applied to trigger the transition. In other words, under fairness, if a transition is possible, then it either occurs eventually or becomes permanently disabled after a finite number of steps.
My approach to liveness and fairness in Verdi follows Agha et al. quite closely. In a nutshell, my extension to Verdi:
- defines labeled step relations;
- defines a coinductive notion of infinite sequences (executions) following some such relation;
- defines two notions of fairness using coinductive predicates;
- completes the collection of temporal operators of Deng and Monin to all those supported by the SPIN model checker.
In combination with suitable protocol definitions and network semantics, this is enough to reason about liveness properties of systems in Verdi.
Let A be the type of configurations, let L be the type of labels, and trace be the type of trace entries. These are normally defined when encoding a protocol in Verdi. Note that labels will never be included after code extraction to OCaml.
Labeled step relations and enabledness are defined as follows:
Definition lb_step_relation := A -> L -> A -> list trace -> Prop.
Definition enabled (step : lb_step_relation) (l : L) (a : A) : Prop := exists a' tr, step a l a' tr.
We define an event, which encapsulates a certain point in an execution:
Record event := { evt_a : A ; evt_l : L ; evt_trace : list trace }.
This enables us to talk about a certain label being enabled and occurring in an event:
Definition l_enabled (step : lb_step_relation) (l : L) (e : event) : Prop := enabled step l (evt_a e).
Definition occurred (l : L) (e : event) : Prop := l = evt_l e.
We can then define the type of infinite sequences of events:
CoInductive infseq : Type := Cons : event -> infseq -> infseq.
We also define "head" and "tail" operations on such sequences:
Definition hd (s:infseq event) : event := match s with Cons x _ => x end.
Definition tl (s:infseq event) : infseq event := match s with Cons _ s => s end.
To constrain events to follow our step relation and generate the proper traces, we define the following coinductive predicate:
CoInductive lb_step_execution (step : lb_step_relation) : infseq event -> Prop :=
Cons_lb_step_exec : forall (e e' : event) (tr : list trace) (s : infseq event),
step (evt_a e) (evt_l e) (evt_a e') tr ->
evt_trace e' = evt_trace e ++ tr ->
lb_step_execution step (Cons e' s) ->
lb_step_execution step (Cons e (Cons e' s)).
A very simple operator used to express properties about the first event in an execution is the following:
Definition now (P: event -> Prop) (s: infseq event) : Prop := match s with Cons x s => P x end.
To be able to talk about a label being continuously or infinitely often enabled in an execution, we need the familiar eventually (diamond) and always (box) operators from temporal logic (other operators are defined similarly):
Inductive eventually (P: infseq event -> Prop) : infseq event -> Prop :=
| E0 : forall s, P s -> eventually P s
| E_next : forall x s, eventually P s -> eventually P (Cons x s).
CoInductive always (P: infseq event -> Prop) : infseq event -> Prop :=
| Always : forall s, P s -> always P (tl s) -> always P s.
Together, they allow us to define the notions we need for fairness:
Definition inf_often (P: infseq event -> Prop) (s: infseq event) : Prop :=
always (eventually P) s.
Definition continuously (P: infseq event -> Prop) (s: infseq event) : Prop :=
eventually (always P) s.
Definition inf_enabled (step : lb_step_relation) (l : L) (s : infseq event) : Prop :=
inf_often (now (l_enabled step l)) s.
Definition cont_enabled (step : lb_step_relation) (l : L) (s : infseq event) : Prop :=
continuously (now (l_enabled step l)) s.
Definition inf_occurred (l : L) (s : infseq event) : Prop :=
inf_often (now (occurred l)) s.
Standard textbooks give two practical notions of fairness, weak and strong:
Definition strong_local_fairness (step : lb_step_relation) (s : infseq event) : Prop :=
forall l : L, inf_enabled step l s -> inf_occurred l s.
Definition weak_local_fairness (step : lb_step_relation) (s : infseq event) : Prop :=
forall l : L, cont_enabled step l s -> inf_occurred l s.
Note that the notion of fairness by Agha et al. mentioned above is roughly equivalent to strong_local_fairness.
To actually verify liveness properties of distributed system implementations using these definitions, we need labelled network semantics and protocol definitions. Here is one example of such a semantics, consistent with Verdi's crash failure semantics, but without the possibility of actual failures:
Inductive lb_step_failure : lb_step_relation (list name * network) label (name * (input + list output)) :=
| LStepFailure_deliver : forall net net' failed p xs ys out d l lb,
nwPackets net = xs ++ p :: ys ->
~ In (pDst p) failed ->
lb_net_handlers (pDst p) (pSrc p) (pBody p) (nwState net (pDst p)) = (lb, out, d, l) ->
net' = mkNetwork (send_packets (pDst p) l ++ xs ++ ys)
(update name_eq_dec (nwState net) (pDst p) d) ->
lb_step_failure (failed, net) lb (failed, net') [(pDst p, inr out)]
| LStepFailure_input : forall h net net' failed out inp d l lb,
~ In h failed ->
lb_input_handlers h inp (nwState net h) = (lb, out, d, l) ->
net' = mkNetwork (send_packets h l ++ nwPackets net)
(update name_eq_dec (nwState net) h d) ->
lb_step_failure (failed, net) lb (failed, net') [(h, inl inp); (h, inr out)]
| LStepFailure_stutter : forall net failed, lb_step_failure (failed, net) label_silent (failed, net) [].
The stutter action is used to prolong possibly-finite executions to become infinite (since our sequences cannot be finite). Note that the first argument returned by both the network message handler (lb_net_handlers) and the input handler (lb_input_handlers) is a label.
To define a protocol, we first need to define the type of labels; here is one example:
Inductive Label : Type :=
| RecvFail : name -> name -> Label
| RecvLevel : name -> name -> Label.
Using Verdi's handler monad, we can now define node protocol actions with labels, like the following:
Definition NetHandler (me src : name) (msg : Msg) : Handler Data :=
st <- get ;;
match msg with
| Level _ => ret (RecvLevel me src)
| Fail =>
put {| adjacent := NSet.remove src st.(adjacent) ;
broadcast := st.(broadcast) ;
levels := st.(levels) |} ;;
ret (RecvFail me src)
end.
For nodes using this handler, the RecvLevel label constructor is used whenever a Level message is received, and the RecvFail constructor whenever a Fail message is received.
Putting it all together, we can now specify and prove liveness properties about the protocol. For example, the property that at some point there will forever not be any Fail messages in transit can be expressed as follows:
Lemma Tree_continuously_no_fail :
forall s, lb_step_execution lb_step_failure s ->
weak_local_fairness lb_step_failure s ->
continuously (now (fun e => forall p, In p (snd e.(evt_a)).(nwPackets) -> p.(pBody) <> Fail)) s.
Proof.
...
Qed.
For a list of all temporal operators supported, see README.md in my repository for the infinite sequence library derived from Deng and Monin's work.
- Gul A. Agha, Ian A. Mason, Scott F. Smith, and Carolyn L. Talcott. 1997. A foundation for actor computation. J. Funct. Program. 7, 1 (January 1997), pp. 1-72.
- Eduardo Gimenez. Codifying guarded definitions with recursive schemes. In Peter Dybjer, Bengt Nordstrom, and Jan M. Smith, editors, TYPES, volume 996 of Lecture Notes in Computer Science, pp. 39-59. Springer, 1994.
- Yuxin Deng and Jean-Francois Monin. Verifying Self-stabilizing Population Protocols with Coq. TASE, 2009, 2012 Sixth International Symposium on Theoretical Aspects of Software Engineering, 2012 Sixth International Symposium on Theoretical Aspects of Software Engineering 2009, pp. 201-208.