Prove group preparer

Use [n / 4 < x] directly as the safe proposing condition, rather than "not
reaching majority in some classic quorum"

external/Goose/github_com/mit_pdos/tulip/gcoord.v

@@ -4,6 +4,7 @@ From Goose Require github_com.mit_pdos.tulip.message.
 From Goose Require github_com.mit_pdos.tulip.params.
 From Goose Require github_com.mit_pdos.tulip.quorum.
 From Goose Require github_com.mit_pdos.tulip.tulip.
+From Goose Require github_com.mit_pdos.tulip.util.
 
 From Perennial.goose_lang Require Import ffi.grove_prelude.
 
@@ -150,10 +151,15 @@ Definition GroupCoordinator__Read: val :=
 Definition GroupPreparer := struct.decl [
   "nrps" :: uint64T;
   "phase" :: uint64T;
-  "fresps" :: mapT boolT;
-  "sresps" :: mapT boolT
+  "frespm" :: mapT boolT;
+  "vdm" :: mapT boolT;
+  "srespm" :: mapT boolT
 ].
 
+Definition GroupPreparer__in: val :=
+  rec: "GroupPreparer__in" "gpp" "phase" :=
+    (struct.loadF GroupPreparer "phase" "gpp") = "phase".
+
 Definition GPP_VALIDATING : expr := #0.
 
 Definition GPP_PREPARING : expr := #1.
@@ -187,32 +193,32 @@ Definition GPP_REFRESH : expr := #5.
    @action: Next action to perform. *)
 Definition GroupPreparer__action: val :=
   rec: "GroupPreparer__action" "gpp" "rid" :=
-    (if: (struct.loadF GroupPreparer "phase" "gpp") = GPP_VALIDATING
+    (if: GroupPreparer__in "gpp" GPP_VALIDATING
     then
-      let: (<>, "fresp") := MapGet (struct.loadF GroupPreparer "fresps" "gpp") "rid" in
+      let: (<>, "fresp") := MapGet (struct.loadF GroupPreparer "frespm" "gpp") "rid" in
       (if: (~ "fresp")
       then GPP_FAST_PREPARE
       else
-        let: (<>, "validated") := MapGet (struct.loadF GroupPreparer "sresps" "gpp") "rid" in
+        let: (<>, "validated") := MapGet (struct.loadF GroupPreparer "vdm" "gpp") "rid" in
         (if: (~ "validated")
         then GPP_VALIDATE
         else GPP_QUERY))
     else
-      (if: (struct.loadF GroupPreparer "phase" "gpp") = GPP_PREPARING
+      (if: GroupPreparer__in "gpp" GPP_PREPARING
       then
-        let: (<>, "prepared") := MapGet (struct.loadF GroupPreparer "sresps" "gpp") "rid" in
+        let: (<>, "prepared") := MapGet (struct.loadF GroupPreparer "srespm" "gpp") "rid" in
         (if: (~ "prepared")
         then GPP_PREPARE
         else GPP_QUERY)
       else
-        (if: (struct.loadF GroupPreparer "phase" "gpp") = GPP_UNPREPARING
+        (if: GroupPreparer__in "gpp" GPP_UNPREPARING
         then
-          let: (<>, "unprepared") := MapGet (struct.loadF GroupPreparer "sresps" "gpp") "rid" in
+          let: (<>, "unprepared") := MapGet (struct.loadF GroupPreparer "srespm" "gpp") "rid" in
           (if: (~ "unprepared")
           then GPP_UNPREPARE
           else GPP_QUERY)
         else
-          (if: (struct.loadF GroupPreparer "phase" "gpp") = GPP_WAITING
+          (if: GroupPreparer__in "gpp" GPP_WAITING
           then GPP_QUERY
           else GPP_REFRESH)))).
 
@@ -489,55 +495,80 @@ Definition GroupPreparer__tryResign: val :=
           #true
         else
           (if: "res" = tulip.REPLICA_STALE_COORDINATOR
-          then
-            struct.storeF GroupPreparer "phase" "gpp" GPP_WAITING;;
-            #true
+          then #true
           else #false)))).
 
-Definition countbm: val :=
-  rec: "countbm" "m" "b" :=
-    let: "n" := ref_to uint64T #0 in
-    MapIter "m" (λ: <> "v",
-      (if: "v" = "b"
-      then "n" <-[uint64T] ((![uint64T] "n") + #1)
-      else #()));;
-    ![uint64T] "n".
+Definition GroupPreparer__collectFastDecision: val :=
+  rec: "GroupPreparer__collectFastDecision" "gpp" "rid" "b" :=
+    MapInsert (struct.loadF GroupPreparer "frespm" "gpp") "rid" "b";;
+    #().
 
 Definition GroupPreparer__fquorum: val :=
   rec: "GroupPreparer__fquorum" "gpp" "n" :=
     (quorum.FastQuorum (struct.loadF GroupPreparer "nrps" "gpp")) ≤ "n".
 
-Definition GroupPreparer__tryBecomeAborted: val :=
-  rec: "GroupPreparer__tryBecomeAborted" "gpp" :=
-    let: "n" := countbm (struct.loadF GroupPreparer "fresps" "gpp") #false in
+Definition GroupPreparer__tryFastAbort: val :=
+  rec: "GroupPreparer__tryFastAbort" "gpp" :=
+    let: "n" := util.CountBoolMap (struct.loadF GroupPreparer "frespm" "gpp") #false in
     (if: GroupPreparer__fquorum "gpp" "n"
     then
       struct.storeF GroupPreparer "phase" "gpp" GPP_ABORTED;;
       #true
     else #false).
 
-Definition GroupPreparer__tryBecomePrepared: val :=
-  rec: "GroupPreparer__tryBecomePrepared" "gpp" :=
-    let: "n" := countbm (struct.loadF GroupPreparer "fresps" "gpp") #true in
+Definition GroupPreparer__cquorum: val :=
+  rec: "GroupPreparer__cquorum" "gpp" "n" :=
+    (quorum.ClassicQuorum (struct.loadF GroupPreparer "nrps" "gpp")) ≤ "n".
+
+Definition GroupPreparer__hcquorum: val :=
+  rec: "GroupPreparer__hcquorum" "gpp" "n" :=
+    (quorum.Half (quorum.ClassicQuorum (struct.loadF GroupPreparer "nrps" "gpp"))) ≤ "n".
+
+Definition GroupPreparer__tryBecomeUnpreparing: val :=
+  rec: "GroupPreparer__tryBecomeUnpreparing" "gpp" :=
+    let: "nresp" := MapLen (struct.loadF GroupPreparer "frespm" "gpp") in
+    (if: (~ (GroupPreparer__cquorum "gpp" "nresp"))
+    then #()
+    else
+      let: "nfu" := util.CountBoolMap (struct.loadF GroupPreparer "frespm" "gpp") #false in
+      (if: (~ (GroupPreparer__hcquorum "gpp" "nfu"))
+      then #()
+      else
+        struct.storeF GroupPreparer "srespm" "gpp" (NewMap uint64T boolT #());;
+        struct.storeF GroupPreparer "phase" "gpp" GPP_UNPREPARING;;
+        #())).
+
+Definition GroupPreparer__tryFastPrepare: val :=
+  rec: "GroupPreparer__tryFastPrepare" "gpp" :=
+    let: "n" := util.CountBoolMap (struct.loadF GroupPreparer "frespm" "gpp") #true in
     (if: GroupPreparer__fquorum "gpp" "n"
     then
       struct.storeF GroupPreparer "phase" "gpp" GPP_PREPARED;;
       #true
     else #false).
 
-Definition GroupPreparer__cquorum: val :=
-  rec: "GroupPreparer__cquorum" "gpp" "n" :=
-    (quorum.ClassicQuorum (struct.loadF GroupPreparer "nrps" "gpp")) ≤ "n".
+Definition GroupPreparer__collectValidation: val :=
+  rec: "GroupPreparer__collectValidation" "gpp" "rid" :=
+    MapInsert (struct.loadF GroupPreparer "vdm" "gpp") "rid" #true;;
+    #().
 
 Definition GroupPreparer__tryBecomePreparing: val :=
   rec: "GroupPreparer__tryBecomePreparing" "gpp" :=
-    let: "n" := MapLen (struct.loadF GroupPreparer "sresps" "gpp") in
-    (if: GroupPreparer__cquorum "gpp" "n"
-    then
-      struct.storeF GroupPreparer "phase" "gpp" GPP_PREPARING;;
-      struct.storeF GroupPreparer "sresps" "gpp" (NewMap uint64T boolT #());;
-      #()
-    else #()).
+    let: "nvd" := MapLen (struct.loadF GroupPreparer "vdm" "gpp") in
+    (if: (~ (GroupPreparer__cquorum "gpp" "nvd"))
+    then #()
+    else
+      let: "nresp" := MapLen (struct.loadF GroupPreparer "frespm" "gpp") in
+      (if: (~ (GroupPreparer__cquorum "gpp" "nresp"))
+      then #()
+      else
+        let: "nfp" := util.CountBoolMap (struct.loadF GroupPreparer "frespm" "gpp") #true in
+        (if: (~ (GroupPreparer__hcquorum "gpp" "nfp"))
+        then #()
+        else
+          struct.storeF GroupPreparer "srespm" "gpp" (NewMap uint64T boolT #());;
+          struct.storeF GroupPreparer "phase" "gpp" GPP_PREPARING;;
+          #()))).
 
 Definition GroupPreparer__processFastPrepareResult: val :=
   rec: "GroupPreparer__processFastPrepareResult" "gpp" "rid" "res" :=
@@ -546,18 +577,25 @@ Definition GroupPreparer__processFastPrepareResult: val :=
     else
       (if: "res" = tulip.REPLICA_FAILED_VALIDATION
       then
-        MapInsert (struct.loadF GroupPreparer "fresps" "gpp") "rid" #false;;
-        GroupPreparer__tryBecomeAborted "gpp";;
-        #()
+        GroupPreparer__collectFastDecision "gpp" "rid" #false;;
+        let: "aborted" := GroupPreparer__tryFastAbort "gpp" in
+        (if: "aborted"
+        then #()
+        else
+          (if: (~ (GroupPreparer__in "gpp" GPP_VALIDATING))
+          then #()
+          else
+            GroupPreparer__tryBecomeUnpreparing "gpp";;
+            #()))
       else
-        MapInsert (struct.loadF GroupPreparer "fresps" "gpp") "rid" #true;;
-        (if: GroupPreparer__tryBecomePrepared "gpp"
+        GroupPreparer__collectFastDecision "gpp" "rid" #true;;
+        (if: GroupPreparer__tryFastPrepare "gpp"
         then #()
         else
-          (if: (struct.loadF GroupPreparer "phase" "gpp") ≠ GPP_VALIDATING
+          (if: (~ (GroupPreparer__in "gpp" GPP_VALIDATING))
           then #()
           else
-            MapInsert (struct.loadF GroupPreparer "sresps" "gpp") "rid" #true;;
+            GroupPreparer__collectValidation "gpp" "rid";;
             GroupPreparer__tryBecomePreparing "gpp";;
             #())))).
 
@@ -566,13 +604,13 @@ Definition GroupPreparer__processValidateResult: val :=
     (if: GroupPreparer__tryResign "gpp" "res"
     then #()
     else
-      (if: (struct.loadF GroupPreparer "phase" "gpp") ≠ GPP_VALIDATING
+      (if: "res" = tulip.REPLICA_FAILED_VALIDATION
       then #()
       else
-        (if: "res" = tulip.REPLICA_FAILED_VALIDATION
+        (if: (~ (GroupPreparer__in "gpp" GPP_VALIDATING))
         then #()
         else
-          MapInsert (struct.loadF GroupPreparer "sresps" "gpp") "rid" #true;;
+          GroupPreparer__collectValidation "gpp" "rid";;
           GroupPreparer__tryBecomePreparing "gpp";;
           #()))).
 
@@ -581,26 +619,32 @@ Definition GroupPreparer__processPrepareResult: val :=
     (if: GroupPreparer__tryResign "gpp" "res"
     then #()
     else
-      MapInsert (struct.loadF GroupPreparer "sresps" "gpp") "rid" #true;;
-      let: "n" := MapLen (struct.loadF GroupPreparer "sresps" "gpp") in
-      (if: GroupPreparer__cquorum "gpp" "n"
-      then
-        struct.storeF GroupPreparer "phase" "gpp" GPP_PREPARED;;
-        #()
-      else #())).
+      (if: (~ (GroupPreparer__in "gpp" GPP_PREPARING))
+      then #()
+      else
+        MapInsert (struct.loadF GroupPreparer "srespm" "gpp") "rid" #true;;
+        let: "n" := MapLen (struct.loadF GroupPreparer "srespm" "gpp") in
+        (if: GroupPreparer__cquorum "gpp" "n"
+        then
+          struct.storeF GroupPreparer "phase" "gpp" GPP_PREPARED;;
+          #()
+        else #()))).
 
 Definition GroupPreparer__processUnprepareResult: val :=
   rec: "GroupPreparer__processUnprepareResult" "gpp" "rid" "res" :=
     (if: GroupPreparer__tryResign "gpp" "res"
     then #()
     else
-      MapInsert (struct.loadF GroupPreparer "sresps" "gpp") "rid" #true;;
-      let: "n" := MapLen (struct.loadF GroupPreparer "sresps" "gpp") in
-      (if: GroupPreparer__cquorum "gpp" "n"
-      then
-        struct.storeF GroupPreparer "phase" "gpp" GPP_ABORTED;;
-        #()
-      else #())).
+      (if: (~ (GroupPreparer__in "gpp" GPP_UNPREPARING))
+      then #()
+      else
+        MapInsert (struct.loadF GroupPreparer "srespm" "gpp") "rid" #true;;
+        let: "n" := MapLen (struct.loadF GroupPreparer "srespm" "gpp") in
+        (if: GroupPreparer__cquorum "gpp" "n"
+        then
+          struct.storeF GroupPreparer "phase" "gpp" GPP_ABORTED;;
+          #()
+        else #()))).
 
 Definition GroupPreparer__processQueryResult: val :=
   rec: "GroupPreparer__processQueryResult" "gpp" "rid" "res" :=

external/Goose/github_com/mit_pdos/tulip/quorum.v

@@ -6,7 +6,7 @@ Context `{ext_ty: ext_types}.
 
 Definition FastQuorum: val :=
   rec: "FastQuorum" "n" :=
-    (("n" + #1) * #3) `quot` #4.
+    ((#3 * "n") + #3) `quot` #4.
 
 Definition ClassicQuorum: val :=
   rec: "ClassicQuorum" "n" :=

external/Goose/github_com/mit_pdos/tulip/util.v

@@ -40,6 +40,15 @@ Definition Sort: val :=
       Continue);;
     #().
 
+Definition CountBoolMap: val :=
+  rec: "CountBoolMap" "m" "b" :=
+    let: "n" := ref_to uint64T #0 in
+    MapIter "m" (λ: <> "v",
+      (if: "v" = "b"
+      then "n" <-[uint64T] (std.SumAssumeNoOverflow (![uint64T] "n") #1)
+      else #()));;
+    ![uint64T] "n".
+
 Definition EncodeString: val :=
   rec: "EncodeString" "bs" "str" :=
     let: "data" := ref_to (slice.T byteT) "bs" in

src/program_proof/rsm/pure/quorum.v

@@ -23,6 +23,12 @@ Section def.
   Definition fquorum c q :=
     q ⊆ c ∧ fquorum_size c q.
 
+  Definition hcquorum_size c q :=
+    size c / 4 < size q.
+
+  Definition hcquorum c q :=
+    q ⊆ c ∧ hcquorum_size c q.
+
 End def.
 
 Section lemma.
@@ -80,6 +86,22 @@ Section lemma.
       (apply (quorums_overlapped_raw c); [done | done | lia]).
   Qed.
 
+  Lemma hcquorum_fquorum_overlapped c q1 q2 :
+    hcquorum c q1 ->
+    fquorum c q2 ->
+    ∃ x, x ∈ q1 ∧ x ∈ q2.
+  Proof.
+    intros Hq1 Hq2.
+    destruct Hq1 as [Hincl1 Hsize1].
+    destruct Hq2 as [Hincl2 Hsize2].
+    apply (quorums_overlapped_raw c).
+    { apply Hincl1. }
+    { apply Hincl2. }
+    rewrite /hcquorum_size in Hsize1.
+    rewrite /fquorum_size in Hsize2.
+    lia.
+  Qed.
+
   Lemma cquorums_overlapped c q1 q2 :
     cquorum c q1 ->
     cquorum c q2 ->

src/program_proof/tulip/inv_group.v

@@ -244,14 +244,21 @@ Section inv.
     Persistent (is_group_prepare_proposal_if_classic γ gid ts rk p).
   Proof. rewrite /is_group_prepare_proposal_if_classic. case_decide; apply _. Defined.
 
+  (* NB: [safe_proposal] seems unnecessarily strong in that it always requires a
+  classic quorum of responses, while sometimes a prepare proposal can be made
+  even without a classic quorum (e.g., in a 3-node cluster, a transaction client
+  should be able to choose to abort in the slow path immediately after receiving
+  the first unprepare). This would not be a liveness issue (since liveness
+  assumes a classic quorum of nodes to be alive), but might affect performance
+  in certain cases. *)
   Definition safe_proposal γ gid (ts : nat) (rk : nat) (p : bool) : iProp Σ :=
     ∃ bsqlb : gmap u64 ballot,
       let n := latest_before_quorum rk bsqlb in
       "#Hlbs"     ∷ ([∗ map] rid ↦ l ∈ bsqlb, is_replica_ballot_lb γ gid rid ts l) ∗
       "#Hlatestc" ∷ is_group_prepare_proposal_if_classic γ gid ts n p ∗
       "%Hquorum"  ∷ ⌜cquorum rids_all (dom bsqlb)⌝ ∗
       "%Hlen"     ∷ ⌜map_Forall (λ _ l, (rk ≤ length l)%nat) bsqlb⌝ ∗
-      "%Hlatestf" ∷ ⌜if decide (n = O) then nfast bsqlb (negb p) ≤ size bsqlb / 2 else True⌝.
+      "%Hlatestf" ∷ ⌜if decide (n = O) then size rids_all / 4 + 1 ≤ nfast bsqlb p else True⌝.
 
   Definition safe_proposals γ gid (ts : nat) (ps : gmap nat bool) : iProp Σ :=
     [∗ map] r ↦ p ∈ ps, safe_proposal γ gid ts r p.

src/program_proof/tulip/invariance/prepare.v

@@ -226,7 +226,7 @@ Section inv.
         rewrite dom_fmap_L Hdombmm.
         by destruct Hquorum as [? _].
       }
-      iAssert (⌜equal_latest_proposal_or_free bsq ps r d⌝)%I as %Heq.
+      iAssert (⌜equal_latest_proposal_or_free bs bsq ps r d⌝)%I as %Heq.
       { iAssert (⌜map_Forall2 (λ _ lb l, prefix lb l) bsqlb bsq⌝)%I as %Hprefix.
         { rewrite map_Forall2_forall.
           iSplit; last done.
@@ -244,9 +244,15 @@ Section inv.
           specialize (Hzunused _ _ Hpsm).
           by rewrite Hzunused in Hd.
         }
-        rewrite (equal_latest_proposal_or_free_eq _ _ _ _ _ Hnz Hlen Hprefix).
+        rewrite (equal_latest_proposal_or_free_eq _ _ _ _ _ _ Hnz Hlen Hprefix).
         rewrite /equal_latest_proposal_or_free /is_group_prepare_proposal_if_classic.
-        case_decide as Hr; first done.
+        case_decide as Hr.
+        { assert (size bs = size rids_all) as Heq.
+          { subst bs.
+            by rewrite /ballot_map_at_ts map_size_fmap -Hdombmm size_dom.
+          }
+          by rewrite Heq.
+        }
         iDestruct (group_prepare_proposal_lookup with "Hlatestc Hpsm")
           as %(ps' & Hps' & Hlookup).
         rewrite Hpsm in Hps'.