(** % How to build a simple system in Verdi % James Wilcox % April 24, 2016 *) (*raw *) (** [verdi]: http://verdi.uwplse.org [github]: https://github.com/uwplse/verdi > _In this long-awaited post, we'll show how to implement and verify > a simple distributed system._ [Last time](NetworkSemantics.html) we described how Verdi models the execution environment of distributed systems using _network semantics_. In this post, we'll use those semantics to verify a simple primary-backup distributed counter. The system maintains a counter, which external clients can increment by sending a request. Internally, the system consists of two nodes, a primary and a backup, each of which maintains a copy of the counter. Clients send increment requests to the primary, which increments its local copy of the counter and forwards the increment request to the backup node. When the backup receives the request, it increments its local copy of the counter and responds to the primary with an acknowledgment. Finally, when the primary receives the acknowledgment, it informs the external client that the request has been completed. This is a very simple system. Most glaringly, it is write-only; there is no way for the external clients to ask what the current value of the counter is. However, this system already illustrates the basic ideas and proof techniques required to use Verdi. After understanding the code and proof below, it's a good exercise to extend the system with reads. The property we will prove of this system is that the backup's copy of the counter is always less than or equal to the primary's copy. The backup's copy might be strictly less than the primary's due to pending requests in the network, but the backup can never be ahead of the primary. There are a few things to note about this property. First, it does not guarantee that the backup ever does any work. An implementation in which the primary immediately responded to client requests without contacting the backup would also satisfy the property. Second, the property is internal and state-based; it says nothing about how the system interacts with external clients. Verdi also supports proving external properties by reasoning about the trace, but we will not show how to do that here. Despite these shortcomings, this property illustrates the basics of reasoning about systems in Verdi. This blog post is a [literal Coq file](Counter.v). For the purposes of presentation, I've omitted some low-level details, but you can always refer to the source for the full story. Also, this series of blog posts presents a simplification of the actual Verdi sources. If you're curious the Verdi distribution [contains](https://github.com/uwplse/verdi/blob/master/systems/Counter.v) an implementation of this system as an example. ## Implementing the Primary-Backup Counter System We will use the network semantics from last time, so we first import that code. *) (*begin code*) Require Import NetworkSemantics. (*end code*) Require Import List. Import ListNotations. Require Import Bool. Require Import Omega. Require Import JRWTactics. (** To implement a system using the network semantics, we have to declare types describing the nodes of the system, the messages exchanged internally by the system, the type of state kept at each node, the type of input requests made by external clients, and the type of output responses. These types for the counter system are given below. There are two nodes, the primary and the backup. They exchange two messages: increments and acknowledgments. The local state of each node is just a natural number representing the counter. The system expects increment requests as inputs and sends increment responses as output. *) (*begin code*) Inductive node := primary | backup. (*end code*) Definition node_eq_dec : forall x y : node, {x = y} + {x <> y}. Proof. decide equality. Defined. Definition node_eqb (x y : node) : bool := if node_eq_dec x y then true else false. (*begin code*) Inductive msg := inc | ack. (*end code*) Definition msg_eq_dec : forall x y : msg, {x = y} + {x <> y}. Proof. decide equality. Defined. Definition msg_eqb (x y : msg) : bool := if msg_eq_dec x y then true else false. (*begin code*) Definition state := nat. Inductive input := request_inc. Inductive output := inc_response. (*end code*) (** With the types out of the way, we're ready to implement the system. The implementation consists of an initialization function that computes the initial state of each node, a function that processes external inputs, and a function that processes internal messages from other nodes. The initial state of each node's copy of the counter is 0. *) (*begin code*) Definition initState (_ : node) : state := 0. (*end code*) (** The functions for handling input and messages are written in a monadic style, with read-write access to the local state, the ability to send messages to other nodes, and the ability to send output to external clients. *) Notation packet := (packet node msg). (*begin code*) Definition handler_monad A := state -> A * state * list packet * list output. Definition handler := state -> state * list packet * list output. Definition do {A : Type} (m : handler_monad A) : handler := fun s => let '(a, s', ps, os) := m s in (s', ps, os). (*end code*) (** `handler_monad` is the type of these monadic actions, while `handler` is isomorphic to `handler_monad unit`. The latter is used by the network semantics, which has no notion of the monad. The suggestively named function `do` converts a monadic action into a `handler` by ignoring the return value. *) Definition ret {A : Type} (x : A) : handler_monad A := fun s => (x, s, [], []). Definition bind {A B : Type} (ma : handler_monad A) (f : A -> handler_monad B) : handler_monad B := fun s => let '(a, s', ps, os) := ma s in let '(b, s'', ps', os') := f a s' in (b, s'', ps ++ ps', os ++ os'). Notation "x <- c1 ;; c2" := (@bind _ _ c1 (fun x => c2)) (at level 100, c1 at next level, right associativity). Notation "e1 ;; e2" := (_ <- e1 ;; e2) (at level 100, right associativity). Definition nop := ret tt. Definition send to msg : handler_monad unit := fun s => (tt, s, [Build_packet to msg], []). Definition out o : handler_monad unit := fun s => (tt, s, [], [o]). Definition get : handler_monad state := fun s => (s, s, [], []). Definition set s : handler_monad unit := fun _ => (tt, s, [], []). (** At this point in the code are definitions for the usual `ret` (aka `return`) and `bind` operations, and of monadic actions for reading and writing the local state, and for sending messages and external output. While these definitions are left out this post, you can view the source for the details. The core action of the implementation is incrementing the local counter. We factor this out into a helper function `do_inc`, as follows. *) (*begin code*) Definition do_inc : handler_monad unit := x <- get ;; set (x + 1). (*end code*) (** `do_inc` uses the monad to `get` the local state and then `set` it to be one more, as expected. The function `processInput` handles external inputs from clients. *) (*begin code*) Definition processInput (h : node) (i : input) : handler := do match h with | primary => match i with | request_inc => do_inc;; send backup inc end | _ => nop end. (*end code*) (** `processInput` takes the name of the node it's running on as its first argument, and the input being processed as its second argument. It returns a `handler`, which is defined (not shown) to be It then does case analysis to see if it is running on the primary or the backup. If it is running on the primary, then it performs the increment locally and sends an `inc` message to the backup. On the other hand, if `processInput` is running on the backup, it does nothing, effectively ignoring the request. External clients are expected to communicate only with the primary. Note that there is an unnecessary case analysis on the input above. In this simple system, there is only one possible input, but I've included the useless pattern matching because typically systems will have more than one possible input. The function `processMsg` handles messages from other nodes in the system. *) (*begin code*) Definition processMsg (h : node) (m : msg) : handler := do match h with | backup => match m with | inc => do_inc ;; send primary ack | _ => nop end | primary => match m with | ack => out inc_response | _ => nop end end. (*end code*) (** If `processMsg` is running on the backup and receives an increment message, it performs an increment and sends an acknowledgment to the primary. If `processMsg` is running on the primary and receives an acknowledgment, it outputs an `inc_response` to the outside world. In all other cases, `processMsg` ignores the incoming message. It is an invariant of the system that the only messages in the network are increments to the backup or acknowledgments to the primary, so these cases never arise. When we get around to verifying the system we will either have to *prove* that these cases never arise, or at least show that they do not violate our specification. *) Notation reliable_step := (reliable_step processMsg processInput msg_eq_dec node_eq_dec). Notation world := (world node state msg input output). Notation reliable_step_star := (reliable_step_star processMsg processInput msg_eq_dec node_eq_dec). Notation reachable := (reachable initState processMsg processInput msg_eq_dec node_eq_dec). Notation update := (@update node nat node_eq_dec). Notation remove_one := (@remove_one node msg msg_eq_dec node_eq_dec). Notation initWorld := (initWorld msg input output initState). (** This completes the implementation of the system. ## Verifying the Counter System We're now ready to formalize our correctness property, that the backup never gets ahead of the primary. *) (*begin code*) Definition backup_le_primary (w : world) : Prop := localState w backup <= localState w primary. (*end code*) (** We can then state the correctness theorem, which says that in any reachable world of the system, the property is true. *) (*begin code*) Theorem backup_le_primary_true : forall w, reachable w -> backup_le_primary w. (*end code*) (** At this point we might be tempted to proceed by induction on reachable worlds, showing that the property is true of the initial world, and that it is preserved by every step of the system. However, a moment's thought shows that our property is not inductive! That is, it is *not* preserved by arbitrary steps of the system. In particular, the property constrains only the state of the nodes, and says nothing at all about what messages are in flight in the network. For example, consider a world where the primary and backup each have the value 10 for their local copy of the counter, but where there are also 5 increment requests in the network on their way from the primary to the backup. Note that this world satisfies the property, so if we were to reason inductively, we would be obliged to show that any step from this world also satisfies the property. But this is not true, since a step that delivers one the requests in the network to the backup will cause it to get ahead of the primary! The resolution is that even though the world where both counters are 10 and there are 5 increments destined to the backup satisfies `backup_le_primary`, this world is not actually reachable. In order to prove that the backup never gets ahead of the primary, we need to find an *inductive invariant*. That is, a property which is true in the initial world and is preserved by all possible steps of the system. We also need the inductive invariant to imply our desired property. The discussion above shows why our property itself cannot be used as an inductive invariant. Since the above counterexample exploited the fact that `backup_le_primary` placed no constraints on the messages in the network, it stands to reason that an inductive invariant for this property will constrain the network in some way. If you've never done this kind of thing before, I'd recommend stopping here and trying to come up with an inductive invariant on your own. This is where all the creativity in program verification is; it's really fun, and it's a good thing to get good at. Welcome back. One way to come up with an inductive invariant in this case is to think about why the counterexample world above is not reachable. Recall that the primary and backup both had a counter value of 10, but there were 5 additional increments in the network. Something is already wrong here: in some sense the primary has already given the backup permission to get 5 steps ahead of it. But looking at the code for the primary, this can never happen. The primary never sends an increment message without also incrementing its local counter. There are a couple ways of formalizing this intuition. One would be to say that the local state of the backup plus the number of increments in the network on their way to the backup is less than or equal to the local state of the primary. This would work fine (it is inductive and implies the desired property), but the proof is a little bit simpler if we use an even stronger invariant, namely, that the above inequality is actually an equality. That is, the local state of the backup plus the number of increments on their ways is *equal* to the local state of the primary. You should take a moment to convince yourself informally that this really is an inductive invariant. To sum up this discussion, to prove that the backup never gets ahead of the primary, we will first prove the inductive invariant, and then show that the property we actually care about follows. First, let's give up on completing the proof directly. *) (*begin code*) Abort. (*end code*) (** To define the inductive invariant, we will need to count the number of increment messages in the network that are destined to the backup. This is the job of the function `count`.[^incs-to-backup] [^incs-to-backup]: Note that we only count increment messages that are destined to the backup, instead of all increment messages. While these quantities are actually equal in all reachable states of the system, this fact would require an additional (inductive) proof. By counting only increments to the backup, we avoid this complication. *) (*begin code*) Definition count (l : list packet) : nat := length (filter (fun p : packet => node_eqb (dest p) backup && msg_eqb (payload p) inc) l). (*end code*) (** The network semantics models the collection of in-flight packets as a list, so our packet-counting function takes a list of packets and returns a `nat`. It first filters the list, retaining only increment messages destined to the backup, and then takes the length of the list. I have omitted the definitions of `node_eqb` and `msg_eqb`, which check for equality of nodes and messages, but they are available in the source (and do what you expect). Now we can state our inductive invariant. *) (*begin code*) Definition backup_plus_count_eq_primary (w : world) : Prop := localState w backup + count (inFlightMsgs w) = localState w primary. (*end code*) (** In practice, when developing an inductive invariant, it is a good idea at this point to first prove that the stated invariant implies the desired top-level specification. This is true in this case because our inductive invariant is an equation of the form `a + b = c`, and our specification is `a <= c`, which follows because `a`, `b`, and `c` are all nonnegative. We're now ready to prove the inductive invariant. Here's how I might convince a human of this. The invariant is true in the initial world because the local state of each node is 0 and there are no in flight packets, so the count is also 0. Now suppose we're in an arbitrary world satisfying the invariant and consider all possible steps of the system. There are only two interesting cases. 1. An external input is delivered to the primary. The primary increments its local state and sends an increment to the backup. This preserves the equality because it adds one to both sides. 2. An increment message is delivered to the backup. The backup increments its local state and sends an acknowledgment to the primary. This preserves the equality because it subtracts one from the count but adds one to the backup's local state. These cancel out because they are on the same side of the equation. In all other cases, no quantities mentioned in the invariant change. Let's now convince Coq of this argument. *) Lemma count_cons_backup_inc : forall l, count (Build_packet backup inc :: l) = S (count l). Proof. reflexivity. Qed. Lemma count_cons_primary : forall l m, count (Build_packet primary m :: l) = count l. Proof. reflexivity. Qed. Lemma count_cons_ack : forall l h, count (Build_packet h ack :: l) = count l. Proof. destruct h; reflexivity. Qed. Lemma count_remove_backup_inc : forall l, In (Build_packet backup inc) l -> S (count (remove_one (Build_packet backup inc) l)) = count l. Proof. induction l; simpl; intuition. - subst. break_if; try congruence. now rewrite count_cons_backup_inc. - break_if. + find_inversion. now rewrite count_cons_backup_inc. + destruct dest, payload; try congruence; now rewrite ?count_cons_primary, ?count_cons_ack. Qed. Lemma count_remove_ack: forall l h, count (remove_one (Build_packet h ack) l) = count l. Proof. induction l; simpl; intuition. break_if. + find_inversion. now rewrite count_cons_ack. + destruct dest, payload. * now rewrite !count_cons_primary. * now rewrite !count_cons_primary. * rewrite !count_cons_backup_inc. auto. * now rewrite !count_cons_ack. Qed. Lemma count_remove_primary : forall l m, count (remove_one (Build_packet primary m) l) = count l. Proof. induction l; simpl; intuition. break_if. - find_inversion. now rewrite count_cons_primary. - destruct dest, payload. * now rewrite !count_cons_primary. * now rewrite !count_cons_primary. * rewrite !count_cons_backup_inc. auto. * now rewrite !count_cons_ack. Qed. Lemma update_same : forall f x v, update f x v x = v. Proof. intros. unfold update. break_if; congruence. Qed. Lemma update_diff : forall f x v y, x <> y -> update f x v y = f y. Proof. intros. unfold update. break_if; congruence. Qed. (*begin code*) Lemma backup_plus_count_eq_primary_true : forall w, reachable w -> backup_plus_count_eq_primary w. Proof. (*context ============================ forall w : world, reachable w -> backup_plus_count_eq_primary w
intros w Hreach.
w : world Hreach : reachable w ============================ backup_plus_count_eq_primary w *) intros w Hreach. (*context w : world Hreach : reachable w ============================ backup_plus_count_eq_primary w
induction Hreach as [|w1 w2 Hstep _ IH].
============================ backup_plus_count_eq_primary initWorld *) induction Hreach as [|w1 w2 Hstep _ IH]. (*context ============================ backup_plus_count_eq_primary initWorld *) - (* base case *) (*end code*) (** Our goal is to prove that the inductive invariant is true in all reachable worlds. We proceed by induction on the execution leading to `w`. (You can hover over the proof script to see the context.) *) (*begin code*) (*context ============================ backup_plus_count_eq_primary initWorld
reflexivity.
This subproof is complete, but there are some unfocused goals. *) reflexivity. (*end code*) (** The base case is easy because in the initial world, each node has a local state of 0, and the network is empty. *) (*begin code*) (*context w1, w2 : world Hstep : reliable_step w1 w2 IH : backup_plus_count_eq_primary w1 ============================ backup_plus_count_eq_primary w2
- invc Hstep.
w1 : world IH : backup_plus_count_eq_primary w1 i : input n : node st' : state ms : list packet outs : list output H : processInput n i (localState w1 n) = (st', ms, outs) ============================ backup_plus_count_eq_primary {| localState := NetworkSemantics.update node_eq_dec (localState w1) n st'; inFlightMsgs := ms ++ inFlightMsgs w1; trace := trace w1 ++ [(n, inl i)] ++ record_outputs input n outs |} *) - invc Hstep. (*context w1 : world IH : backup_plus_count_eq_primary w1 i : input n : node st' : state ms : list packet outs : list output H : processInput n i (localState w1 n) = (st', ms, outs) ============================ backup_plus_count_eq_primary {| localState := NetworkSemantics.update node_eq_dec (localState w1) n st'; inFlightMsgs := ms ++ inFlightMsgs w1; trace := trace w1 ++ [(n, inl i)] ++ record_outputs input n outs |} *) + (* input step *) (*end code*) (** We begin the inductive case by considering each possible step of the system. The first case to consider is when an external input `i` is delivered to a node `n`. *) (*begin code*) (*context w1 : world IH : backup_plus_count_eq_primary w1 i : input n : node st' : state ms : list packet outs : list output H : processInput n i (localState w1 n) = (st', ms, outs) ============================ backup_plus_count_eq_primary {| localState := NetworkSemantics.update node_eq_dec (localState w1) n st'; inFlightMsgs := ms ++ inFlightMsgs w1; trace := trace w1 ++ [(n, inl i)] ++ record_outputs input n outs |}
unfold processInput in *.
w1 : world IH : backup_plus_count_eq_primary w1 i : input n : node st' : state ms : list packet outs : list output H : do match n with | primary => match i with | request_inc => do_inc;; send backup inc end | backup => nop end (localState w1 n) = (st', ms, outs) ============================ backup_plus_count_eq_primary {| localState := NetworkSemantics.update node_eq_dec (localState w1) n st'; inFlightMsgs := ms ++ inFlightMsgs w1; trace := trace w1 ++ [(n, inl i)] ++ record_outputs input n outs |} *) unfold processInput in *. (*context w1 : world IH : backup_plus_count_eq_primary w1 i : input n : node st' : state ms : list packet outs : list output H : do match n with | primary => match i with | request_inc => do_inc;; send backup inc end | backup => nop end (localState w1 n) = (st', ms, outs) ============================ backup_plus_count_eq_primary {| localState := NetworkSemantics.update node_eq_dec (localState w1) n st'; inFlightMsgs := ms ++ inFlightMsgs w1; trace := trace w1 ++ [(n, inl i)] ++ record_outputs input n outs |}
destruct i, n; invc H; unfold backup_plus_count_eq_primary, state in *; simpl; rewrite update_same, update_diff by congruence.
w1 : NetworkSemantics.world node nat msg input output IH : localState w1 backup + count (inFlightMsgs w1) = localState w1 primary ============================ localState w1 backup + count ({| dest := backup; payload := inc |} :: inFlightMsgs w1) = localState w1 primary + 1 *) destruct i, n; invc H; (*context w1 : world IH : backup_plus_count_eq_primary w1 i : input n : node st' : state ms : list packet outs : list output H : do match n with | primary => match i with | request_inc => do_inc;; send backup inc end | backup => nop end (localState w1 n) = (st', ms, outs) ============================ backup_plus_count_eq_primary {| localState := NetworkSemantics.update node_eq_dec (localState w1) n st'; inFlightMsgs := ms ++ inFlightMsgs w1; trace := trace w1 ++ [(n, inl i)] ++ record_outputs input n outs |}
destruct i, n; invc H; unfold backup_plus_count_eq_primary, state in *; simpl; rewrite update_same, update_diff by congruence.
w1 : NetworkSemantics.world node nat msg input output IH : localState w1 backup + count (inFlightMsgs w1) = localState w1 primary ============================ localState w1 backup + count ({| dest := backup; payload := inc |} :: inFlightMsgs w1) = localState w1 primary + 1 *) unfold backup_plus_count_eq_primary, state in *; (*context w1 : world IH : backup_plus_count_eq_primary w1 i : input n : node st' : state ms : list packet outs : list output H : do match n with | primary => match i with | request_inc => do_inc;; send backup inc end | backup => nop end (localState w1 n) = (st', ms, outs) ============================ backup_plus_count_eq_primary {| localState := NetworkSemantics.update node_eq_dec (localState w1) n st'; inFlightMsgs := ms ++ inFlightMsgs w1; trace := trace w1 ++ [(n, inl i)] ++ record_outputs input n outs |}
destruct i, n; invc H; unfold backup_plus_count_eq_primary, state in *; simpl; rewrite update_same, update_diff by congruence.
w1 : NetworkSemantics.world node nat msg input output IH : localState w1 backup + count (inFlightMsgs w1) = localState w1 primary ============================ localState w1 backup + count ({| dest := backup; payload := inc |} :: inFlightMsgs w1) = localState w1 primary + 1 *) simpl; rewrite update_same, update_diff by congruence. (*context w1 : NetworkSemantics.world node nat msg input output IH : localState w1 backup + count (inFlightMsgs w1) = localState w1 primary ============================ localState w1 backup + count ({| dest := backup; payload := inc |} :: inFlightMsgs w1) = localState w1 primary + 1 *) * (* input delivered to primary *) (*end code*) (** We proceed by case analysis on `i` and `n`, use `inv` to "execute" the monadic handler action, unfold the definition of the invariant, and then rewrite by some helper lemmas about `update`. (Recall from the network semantics that `update` takes a function modeling the global state `name -> state`, a host, and a new local state for that host, and returns a function modeling the new global state, where the local state of the given host has been updated.) The first subgoal is when the input is delivered to the primary. *) (*begin code*) (*context w1 : NetworkSemantics.world node nat msg input output IH : localState w1 backup + count (inFlightMsgs w1) = localState w1 primary ============================ localState w1 backup + count ({| dest := backup; payload := inc |} :: inFlightMsgs w1) = localState w1 primary + 1
rewrite count_cons_backup_inc.
w1 : NetworkSemantics.world node nat msg input output IH : localState w1 backup + count (inFlightMsgs w1) = localState w1 primary ============================ localState w1 backup + S (count (inFlightMsgs w1)) = localState w1 primary + 1 *) rewrite count_cons_backup_inc. (*context w1 : NetworkSemantics.world node nat msg input output IH : localState w1 backup + count (inFlightMsgs w1) = localState w1 primary ============================ localState w1 backup + S (count (inFlightMsgs w1)) = localState w1 primary + 1
omega.
This subproof is complete, but there are some unfocused goals. *) omega. (*end code*) (** We use a lemma that states that `count` counts increments to the backup (lemma statement not shown). The next case is when the input is delivered to the backup, and it's easy. *) (*begin code*) (*context w1 : NetworkSemantics.world node nat msg input output IH : localState w1 backup + count (inFlightMsgs w1) = localState w1 primary ============================ localState w1 backup + count (inFlightMsgs w1) = localState w1 primary
* auto.
This subproof is complete, but there are some unfocused goals. *) * auto. (*context w1 : world IH : backup_plus_count_eq_primary w1 p : packet st' : state ms : list packet outs : list output H : In p (inFlightMsgs w1) H0 : processMsg (dest p) (payload p) (localState w1 (dest p)) = (st', ms, outs) ============================ backup_plus_count_eq_primary {| localState := NetworkSemantics.update node_eq_dec (localState w1) (dest p) st'; inFlightMsgs := ms ++ remove_one p (inFlightMsgs w1); trace := trace w1 ++ record_outputs input (dest p) outs |} *) + (* msg step *) (*end code*) (** That takes care of all possible input steps. We now consider steps that deliver a message. *) (*begin code*) (*context backup_plus_count_eq_primary {| localState := NetworkSemantics.update node_eq_dec (localState w1) (dest p) st'; inFlightMsgs := ms ++ remove_one p (inFlightMsgs w1); trace := trace w1 ++ record_outputs input (dest p) outs |}
unfold processMsg in *.
w1 : world IH : backup_plus_count_eq_primary w1 p : packet st' : state ms : list packet outs : list output H : In p (inFlightMsgs w1) H0 : do match dest p with | primary => match payload p with | inc => nop | ack => out inc_response end | backup => match payload p with | inc => do_inc;; send primary ack | ack => nop end end (localState w1 (dest p)) = (st', ms, outs) ============================ backup_plus_count_eq_primary {| localState := NetworkSemantics.update node_eq_dec (localState w1) (dest p) st'; inFlightMsgs := ms ++ remove_one p (inFlightMsgs w1); trace := trace w1 ++ record_outputs input (dest p) outs |} *) unfold processMsg in *. (*context w1 : world IH : backup_plus_count_eq_primary w1 p : packet st' : state ms : list packet outs : list output H : In p (inFlightMsgs w1) H0 : do match dest p with | primary => match payload p with | inc => nop | ack => out inc_response end | backup => match payload p with | inc => do_inc;; send primary ack | ack => nop end end (localState w1 (dest p)) = (st', ms, outs) ============================ backup_plus_count_eq_primary {| localState := NetworkSemantics.update node_eq_dec (localState w1) (dest p) st'; inFlightMsgs := ms ++ remove_one p (inFlightMsgs w1); trace := trace w1 ++ record_outputs input (dest p) outs |}
destruct p. simpl in *.
w1 : world IH : backup_plus_count_eq_primary w1 dest : node payload : msg st' : state ms : list packet outs : list output H : In {| dest := dest; payload := payload |} (inFlightMsgs w1) H0 : do match dest with | primary => match payload with | inc => nop | ack => out inc_response end | backup => match payload with | inc => do_inc;; send primary ack | ack => nop end end (localState w1 dest) = (st', ms, outs) ============================ backup_plus_count_eq_primary {| localState := NetworkSemantics.update node_eq_dec (localState w1) dest st'; inFlightMsgs := ms ++ remove_one {| dest := dest; payload := payload |} (inFlightMsgs w1); trace := trace w1 ++ record_outputs input dest outs |} *) destruct p. simpl in *. (*context w1 : world IH : backup_plus_count_eq_primary w1 dest : node payload : msg st' : state ms : list packet outs : list output H : In {| dest := dest; payload := payload |} (inFlightMsgs w1) H0 : do match dest with | primary => match payload with | inc => nop | ack => out inc_response end | backup => match payload with | inc => do_inc;; send primary ack | ack => nop end end (localState w1 dest) = (st', ms, outs) ============================ backup_plus_count_eq_primary {| localState := NetworkSemantics.update node_eq_dec (localState w1) dest st'; inFlightMsgs := ms ++ remove_one {| dest := dest; payload := payload |} (inFlightMsgs w1); trace := trace w1 ++ record_outputs input dest outs |}
destruct dest, payload;
w1 : NetworkSemantics.world node nat msg input output IH : localState w1 backup + count (inFlightMsgs w1) = localState w1 primary H : In {| dest := primary; payload := inc |} (inFlightMsgs w1) ============================ localState w1 backup + count (remove_one {| dest := primary; payload := inc |} (inFlightMsgs w1)) = localState w1 primary *) destruct dest, payload; (*context w1 : world IH : backup_plus_count_eq_primary w1 dest : node payload : msg st' : state ms : list packet outs : list output H : In {| dest := dest; payload := payload |} (inFlightMsgs w1) H0 : do match dest with | primary => match payload with | inc => nop | ack => out inc_response end | backup => match payload with | inc => do_inc;; send primary ack | ack => nop end end (localState w1 dest) = (st', ms, outs) ============================ backup_plus_count_eq_primary {| localState := NetworkSemantics.update node_eq_dec (localState w1) dest st'; inFlightMsgs := ms ++ remove_one {| dest := dest; payload := payload |} (inFlightMsgs w1); trace := trace w1 ++ record_outputs input dest outs |}
destruct dest, payload;
w1 : NetworkSemantics.world node nat msg input output IH : localState w1 backup + count (inFlightMsgs w1) = localState w1 primary H : In {| dest := primary; payload := inc |} (inFlightMsgs w1) ============================ localState w1 backup + count (remove_one {| dest := primary; payload := inc |} (inFlightMsgs w1)) = localState w1 primary *) invc H0; unfold backup_plus_count_eq_primary, state in *; (*context w1 : world IH : backup_plus_count_eq_primary w1 dest : node payload : msg st' : state ms : list packet outs : list output H : In {| dest := dest; payload := payload |} (inFlightMsgs w1) H0 : do match dest with | primary => match payload with | inc => nop | ack => out inc_response end | backup => match payload with | inc => do_inc;; send primary ack | ack => nop end end (localState w1 dest) = (st', ms, outs) ============================ backup_plus_count_eq_primary {| localState := NetworkSemantics.update node_eq_dec (localState w1) dest st'; inFlightMsgs := ms ++ remove_one {| dest := dest; payload := payload |} (inFlightMsgs w1); trace := trace w1 ++ record_outputs input dest outs |}
destruct dest, payload;
w1 : NetworkSemantics.world node nat msg input output IH : localState w1 backup + count (inFlightMsgs w1) = localState w1 primary H : In {| dest := primary; payload := inc |} (inFlightMsgs w1) ============================ localState w1 backup + count (remove_one {| dest := primary; payload := inc |} (inFlightMsgs w1)) = localState w1 primary *) simpl; rewrite update_same, update_diff by congruence. (*context w1 : NetworkSemantics.world node nat msg input output IH : localState w1 backup + count (inFlightMsgs w1) = localState w1 primary H : In {| dest := primary; payload := inc |} (inFlightMsgs w1) ============================ localState w1 backup + count (remove_one {| dest := primary; payload := inc |} (inFlightMsgs w1)) = localState w1 primary *) * (* primary, inc *) (*end code*) (** We proceed by case analysis on the destination and payload of the message. The first case to consider is when an increment message arrives at the primary. In fact, this will never happen in any reachable world, but instead of explicitly ruling it out, we have stated our invariant so that it is preserved even in this case. This case follows formally from a lemma stating that increments to the primary are not `count`ed (lemma statement not shown) and the induction hypothesis. *) (*begin code*) (*context w1 : NetworkSemantics.world node nat msg input output IH : localState w1 backup + count (inFlightMsgs w1) = localState w1 primary H : In {| dest := primary; payload := inc |} (inFlightMsgs w1) ============================ localState w1 backup + count (remove_one {| dest := primary; payload := inc |} (inFlightMsgs w1)) = localState w1 primary
now rewrite <- IH, count_remove_primary.
This subproof is complete, but there are some unfocused goals. *) now rewrite <- IH, count_remove_primary. (*end code*) (** The next case is when an acknowledgment is delivered to the primary. This case follows from a lemma stating that acknowledgments are not `count`ed and the induction hypothesis. *) (*begin code*) (*context w1 : NetworkSemantics.world node nat msg input output IH : localState w1 backup + count (inFlightMsgs w1) = localState w1 primary H : In {| dest := primary; payload := ack |} (inFlightMsgs w1) ============================ localState w1 backup + count (remove_one {| dest := primary; payload := ack |} (inFlightMsgs w1)) = localState w1 primary
* now rewrite <- IH, count_remove_ack.
This subproof is complete, but there are some unfocused goals. *) * now rewrite <- IH, count_remove_ack. (*end code*) (** The next case is the only interesting kind of message delivery: when an increment is delivered to the backup. In addition to incrementing the local state, the backup sends an acknowledgment to the primary, so we use a lemma stating that messages to the primary do not affect the count. The execution of this step implies that the world before the step contained an increment on its way to the backup, so we use a lemma stating that this contributes exactly 1 to the count, which justifies the backup incrementing its count by 1. *) (*begin code*) (*context w1 : NetworkSemantics.world node nat msg input output IH : localState w1 backup + count (inFlightMsgs w1) = localState w1 primary H : In {| dest := backup; payload := inc |} (inFlightMsgs w1) ============================ localState w1 backup + 1 + count ({| dest := primary; payload := ack |} :: remove_one {| dest := backup; payload := inc |} (inFlightMsgs w1)) = localState w1 primary
* rewrite count_cons_primary.
w1 : NetworkSemantics.world node nat msg input output IH : localState w1 backup + count (inFlightMsgs w1) = localState w1 primary H : In {| dest := backup; payload := inc |} (inFlightMsgs w1) ============================ localState w1 backup + 1 + count (remove_one {| dest := backup; payload := inc |} (inFlightMsgs w1)) = localState w1 primary *) * rewrite count_cons_primary. (*context w1 : NetworkSemantics.world node nat msg input output IH : localState w1 backup + count (inFlightMsgs w1) = localState w1 primary H : In {| dest := backup; payload := inc |} (inFlightMsgs w1) ============================ localState w1 backup + 1 + count (remove_one {| dest := backup; payload := inc |} (inFlightMsgs w1)) = localState w1 primary
find_apply_lem_hyp count_remove_backup_inc.
w1 : NetworkSemantics.world node nat msg input output IH : localState w1 backup + count (inFlightMsgs w1) = localState w1 primary H : S (count (remove_one {| dest := backup; payload := inc |} (inFlightMsgs w1))) = count (inFlightMsgs w1) ============================ localState w1 backup + 1 + count (remove_one {| dest := backup; payload := inc |} (inFlightMsgs w1)) = localState w1 primary *) find_apply_lem_hyp count_remove_backup_inc. (*context w1 : NetworkSemantics.world node nat msg input output IH : localState w1 backup + count (inFlightMsgs w1) = localState w1 primary H : S (count (remove_one {| dest := backup; payload := inc |} (inFlightMsgs w1))) = count (inFlightMsgs w1) ============================ localState w1 backup + 1 + count (remove_one {| dest := backup; payload := inc |} (inFlightMsgs w1)) = localState w1 primary
omega.
This subproof is complete, but there are some unfocused goals. *) omega. (*end code*) (** The very last case to consider is when an acknowledgment is delivered to the backup. Again, this cannot actually happen in a reachable world, but our inductive invariant is still preserved. The case follows from the induction hypothesis and a lemma stating that acknowledgments do not affect the count. *) (*begin code*) (*context w1 : NetworkSemantics.world node nat msg input output IH : localState w1 backup + count (inFlightMsgs w1) = localState w1 primary H : In {| dest := backup; payload := ack |} (inFlightMsgs w1) ============================ localState w1 backup + count (remove_one {| dest := backup; payload := ack |} (inFlightMsgs w1)) = localState w1 primary
* now rewrite <- IH, count_remove_ack.
No more subgoals. *) * now rewrite <- IH, count_remove_ack. Qed. (*end code*) (** This completes the proof that the inductive invariant is true in all reachable worlds. We can finally conclude that our desired top-level specification is true. The proof considers a reachable world `w`, uses the above lemma to establish the inductive invariant in `w`, and then concludes by showing that the inductive invariant implies the specification. *) (*begin code*) Theorem backup_le_primary_true : forall w, reachable w -> backup_le_primary w. Proof. (*context ============================ forall w : world, reachable w -> backup_le_primary w
intros w Hreach.
w : world Hreach : reachable w ============================ backup_le_primary w *) intros w Hreach. (*context w : world Hreach : reachable w ============================ backup_le_primary w
apply backup_plus_count_eq_primary_true in Hreach.
w : world Hreach : backup_plus_count_eq_primary w ============================ backup_le_primary w *) apply backup_plus_count_eq_primary_true in Hreach. (*context w : world Hreach : backup_plus_count_eq_primary w ============================ backup_le_primary w
unfold backup_plus_count_eq_primary, backup_le_primary in *.
w : world Hreach : localState w backup + count (inFlightMsgs w) = localState w primary ============================ localState w backup <= localState w primary *) unfold backup_plus_count_eq_primary, backup_le_primary in *. (*context w : world Hreach : localState w backup + count (inFlightMsgs w) = localState w primary ============================ localState w backup <= localState w primary
omega.
No more subgoals. *) omega. Qed. (*end code*) (** ## Conclusion In this post, we've seen how to implement and verify a simple system using network semantics in the style of Verdi. Please do look at [the source](Counter.v) for more detail. If you want to play around with extending the system in various ways, here are some suggested exercises: * Extend the system with an "increment by `n`" operation. Find a new state-based specification that characterizes the behavior of your system and prove it. * Extend the system with a decrement operation. Find a new state-based specification that characterizes the behavior of your system and prove it. What difficulties arise? * Extend the system with reads and prove that the specification is still true. * In a version of the system without the decrement extension, prove that the backup's state is always at least as large as the number of responses in the trace. This rules out a buggy implementation that doesn't actually replicate requests. You'll need to look at the network semantics to figure out how to prove properties of the execution trace, which I haven't discussed at all here. * Prove that the number of responses in the trace is less than or equal to the number of responses. This is a completely trace-based/external specification. * Notice that this system does not tolerate duplicate messages: if an increment message to the backup gets duplicated by the network, then the backup could get ahead of the primary. Implement a version of this system that tolerates duplicates and prove that it does so. (This is harder than the previous exercises. You'll need to complete the exercise from the network semantics post to get a semantics with duplication.) Is there anything about the way you tolerate duplicate messages that is specific to this counter system? In the next post on Verdi, we'll discuss *verified system transformers*, which are a way of implementing and verifying fault tolerance mechanisms in a system-agnostic way. *)