Improved leader election

multi_actris/examples/leader_election.v

@@ -4,29 +4,28 @@ From iris.heap_lang.lib Require Import assert.
 (** Inspired by https://en.wikipedia.org/wiki/Chang_and_Roberts_algorithm *)
 
 Definition process : val :=
-  rec: "go" "c" "idl" "id" "idr" "isp" "id_max" :=
+  rec: "go" "c" "idl" "id" "idr" "isp" :=
     if: recv "c" "idr"
     then let: "id'" := recv "c" "idr" in
-         if: "id_max" < "id'"          (** Case 1 *)
+         if: "id" < "id'"          (** Case 1 *)
          then send "c" "idl" #true;; send "c" "idl" "id'";;
-              "go" "c" "idl" "id" "idr" "isp" "id'"
-         else if: "id_max" = "id'"     (** Case 4 *)
-         then send "c" "idl" #false;; send "c" "idl" "id_max";;
-              "go" "c" "idl" "id" "idr" #false "id_max"
+              "go" "c" "idl" "id" "idr" #true
+         else if: "id" = "id'"     (** Case 4 *)
+         then send "c" "idl" #false;; send "c" "idl" "id";;
+              "go" "c" "idl" "id" "idr" #false
          else if: "isp" (** Case 3 *)
-         then "go" "c" "idl" "id" "idr" "isp" "id_max" (** Case 2 *)
-         else send "c" "idl" #true;; send "c" "idl" "id_max";;
-              "go" "c" "idl" "id" "idr" #true "id_max"
+         then "go" "c" "idl" "id" "idr" "isp" (** Case 2 *)
+         else send "c" "idl" #true;; send "c" "idl" "id";;
+              "go" "c" "idl" "id" "idr" #true
     else let: "id'" := recv "c" "idr" in
-         assert: ("id_max" = "id'");;
          if: "id" = "id'" then "id'"
-         else send "c" "idl" #false;; send "c" "idl" "id_max";; "id_max".
+         else send "c" "idl" #false;; send "c" "idl" "id'";; "id'".
 
 Definition init : val :=
   λ: "c" "idl" "id" "idr",
     (* Notice missing leader *)
     send "c" "idl" #true;; send "c" "idl" "id";;
-    process "c" "idl" "id" "idr" #true "id".
+    process "c" "idl" "id" "idr" #true.
 
 Definition program : val :=
   λ: <>,
@@ -36,7 +35,7 @@ Definition program : val :=
      let: "c2" := get_chan "cs" #2 in
      let: "c3" := get_chan "cs" #3 in
      Fork (let: "id_max" := init "c1" #3 #1 #2 in send "c1" #0 "id_max");;
-     Fork (let: "id_max" := process "c2" #1 #2 #3 #false #2 in
+     Fork (let: "id_max" := process "c2" #1 #2 #3 #false in
            send "c2" #0 "id_max");;
      Fork (let: "id_max" := init "c3" #2 #3 #1 in send "c3" #0 "id_max");;
      let: "res1" := recv "c0" #1 in
@@ -52,44 +51,42 @@ Section ring_leader_election_example.
   Context `{!heapGS Σ, chanG Σ, spawnG Σ, mono_natG Σ}.
 
   Definition my_recv_prot (il i ir : nat) (p : nat → iProto Σ)
-             (rec : bool -d> nat -d> iProto Σ) : bool -d> nat -d> iProto Σ :=
-    λ (isp:bool) (i_max:nat),
+             (rec : bool -d> iProto Σ) : bool -d> iProto Σ :=
+    λ (isp:bool),
       iProto_choice (Recv,ir)
         (<(Recv,ir) @ (i':nat)> MSG #i' ;
-         if bool_decide (i_max < i')
-         then <(Send,il)> MSG #true ; <(Send,il)> MSG #(max i' i_max) ;
-              rec isp (max i' i_max)
-         else if bool_decide (i_max = i')
-         then <(Send,il)> MSG #false ; <(Send, il)> MSG #i_max ; rec false i_max
-         else if isp then rec isp i_max
-         else <(Send,il)> MSG #true ; <(Send,il)> MSG #(max i' i_max) ;
-              rec true (max i' i_max))%proto
-        (<(Recv,ir)> MSG #i_max ;
-         if (bool_decide (i = i_max)) then p i_max
-         else <(Send,il)> MSG #false; <(Send,il)> MSG #i_max; p i_max)%proto.
+         if bool_decide (i < i')
+         then <(Send,il)> MSG #true ; <(Send,il)> MSG #i' ; rec true
+         else if bool_decide (i = i')
+         then <(Send,il)> MSG #false ; <(Send, il)> MSG #i ; rec false
+         else if isp then rec isp
+         else <(Send,il)> MSG #true ; <(Send,il)> MSG #i ; rec true)%proto
+        (<(Recv,ir) @ (i':nat)> MSG #i' ;
+         if (bool_decide (i = i')) then p i
+         else <(Send,il)> MSG #false; <(Send,il)> MSG #i'; p i')%proto.
 
   Instance rle_prot_aux_contractive il i ir p : Contractive (my_recv_prot il i ir p).
   Proof. rewrite /my_recv_prot. solve_proto_contractive. Qed.
   Definition rle_prot il i ir p := fixpoint (my_recv_prot il i ir p).
-  Instance rle_prot_unfold il i ir isp max_id p :
-    ProtoUnfold (rle_prot il i ir p isp max_id) (my_recv_prot il i ir p (rle_prot il i ir p) isp max_id).
+  Instance rle_prot_unfold il i ir isp p :
+    ProtoUnfold (rle_prot il i ir p isp) (my_recv_prot il i ir p (rle_prot il i ir p) isp).
   Proof. apply proto_unfold_eq, (fixpoint_unfold (my_recv_prot il i ir p)). Qed.
-  Lemma rle_prot_unfold' il i ir isp max_id p :
-    (rle_prot il i ir p isp max_id) ≡
-    (my_recv_prot il i ir p (rle_prot il i ir p) isp max_id).
+  Lemma rle_prot_unfold' il i ir isp p :
+    (rle_prot il i ir p isp) ≡
+    (my_recv_prot il i ir p (rle_prot il i ir p) isp).
   Proof. apply (fixpoint_unfold (my_recv_prot il i ir p)). Qed.
 
   Definition rle_preprot (il i ir : nat) p : iProto Σ :=
     (<(Send, il)> MSG #true; <(Send, il)> MSG #i ;
-    rle_prot il i ir p true i)%proto.
+    rle_prot il i ir p true)%proto.
 
-  Lemma process_spec il i ir p i_max c (isp:bool) :
-    {{{ c ↣ (rle_prot il i ir p isp i_max) }}}
-      process c #il #i #ir #isp #i_max
+  Lemma process_spec il i ir p c (isp:bool) :
+    {{{ c ↣ (rle_prot il i ir p isp) }}}
+      process c #il #i #ir #isp
     {{{ i', RET #i'; c ↣ p i' }}}.
   Proof.
     iIntros (Φ) "Hc HΦ".
-    iLöb as "IH" forall (Φ isp i_max).    
+    iLöb as "IH" forall (Φ isp).
     wp_lam. wp_recv (b) as "_".
     destruct b.
     - wp_pures. wp_recv (i') as "_".
@@ -97,40 +94,30 @@ Section ring_leader_election_example.
       case_bool_decide as Hlt.
       { case_bool_decide; [|lia].
         wp_pures. wp_send with "[//]".
-        iEval (replace i' with (max i' i_max) by lia).
-        wp_send with "[//]". wp_pures.        
+        wp_send with "[//]". wp_pures.
         iApply ("IH" with "Hc HΦ"). }
       case_bool_decide as Hlt2.
       { case_bool_decide; [lia|].
         wp_pures. case_bool_decide; [|simplify_eq;lia].
         wp_send with "[//]".
-        iEval (replace i' with (max i' i_max) by lia).
         wp_send with "[//]". wp_pures.
         iApply ("IH" with "Hc HΦ"). }
       case_bool_decide; [lia|].
       wp_pures.
       case_bool_decide; [simplify_eq;lia|].
-      wp_pures. 
+      wp_pures.
       destruct isp.
       { wp_pures. iApply ("IH" with "Hc HΦ"). }
       wp_pures.
       wp_send with "[//]".
-      iEval (replace i_max with (max i' i_max) by lia).
       wp_send with "[//]".
       wp_pures. iApply ("IH" with "Hc HΦ").
     - wp_pures.
-      wp_recv as "_".
-      wp_smart_apply wp_assert.
-      wp_pures. iModIntro.
-      iSplitR.
-      { iPureIntro. f_equiv. f_equiv. apply bool_decide_eq_true_2. done. }
-      iNext.
-      wp_pures.
-      case_bool_decide.
-      { wp_pures. simplify_eq.
-        case_bool_decide; [|simplify_eq;lia]. wp_pures.
-        iModIntro. by iApply "HΦ". }
-      wp_pures. case_bool_decide; [simplify_eq;lia|]. wp_pures.
+      wp_recv (id') as "_". wp_pures.
+      case_bool_decide as Hlt.
+      { case_bool_decide; [|simplify_eq;lia].
+        wp_pures. subst. by iApply "HΦ". }
+      case_bool_decide; [simplify_eq;lia|].
       wp_send with "[//]". wp_send with "[//]". wp_pures. by iApply "HΦ".
   Qed.
 
@@ -165,7 +152,7 @@ Section ring_leader_election_example.
              <(Recv,3)> MSG #id_max ;
              END)%proto ]>
     (<[1 := rle_preprot 3 1 2 prot_tail ]>
-    (<[2 := rle_prot 1 2 3 prot_tail false 2 ]>
+    (<[2 := rle_prot 1 2 3 prot_tail false ]>
     (<[3 := rle_preprot 2 3 1 prot_tail ]> ∅))).
 
   Lemma prot_pool_consistent : ⊢ iProto_consistent prot_pool.