Prove replica prepare

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

@@ -13,19 +13,15 @@ Definition PrepareProposal := struct.decl [
   "dec" :: boolT
 ].
 
-Definition PrepareStatusEntry := struct.decl [
-  "rankl" :: uint64T;
-  "prep" :: struct.t PrepareProposal
-].
-
 Definition Replica := struct.decl [
   "mu" :: ptrT;
   "rid" :: uint64T;
   "txnlog" :: ptrT;
   "lsna" :: uint64T;
   "prepm" :: mapT (slice.T (struct.t tulip.WriteEntry));
   "ptgsm" :: mapT (slice.T uint64T);
-  "pstbl" :: mapT (struct.t PrepareStatusEntry);
+  "pstbl" :: mapT (struct.t PrepareProposal);
+  "rktbl" :: mapT uint64T;
   "txntbl" :: mapT boolT;
   "ptsm" :: mapT uint64T;
   "sptsm" :: mapT uint64T;
@@ -199,6 +195,16 @@ Definition Replica__acquire: val :=
         (Replica__acquireKey "rp" "ts" (struct.get tulip.WriteEntry "Key" "ent"));;
       #true).
 
+Definition Replica__finalized: val :=
+  rec: "Replica__finalized" "rp" "ts" :=
+    let: ("cmted", "done") := MapGet (struct.loadF Replica "txntbl" "rp") "ts" in
+    (if: "done"
+    then
+      (if: "cmted"
+      then (tulip.REPLICA_COMMITTED_TXN, #true)
+      else (tulip.REPLICA_ABORTED_TXN, #true))
+    else (tulip.REPLICA_OK, #false)).
+
 Definition Replica__logValidate: val :=
   rec: "Replica__logValidate" "rp" "ts" "pwrs" "ptgs" :=
     #().
@@ -212,12 +218,9 @@ Definition Replica__logValidate: val :=
    @error: Error code. *)
 Definition Replica__validate: val :=
   rec: "Replica__validate" "rp" "ts" "pwrs" "ptgs" :=
-    let: ("cmted", "done") := MapGet (struct.loadF Replica "txntbl" "rp") "ts" in
-    (if: "done"
-    then
-      (if: "cmted"
-      then tulip.REPLICA_COMMITTED_TXN
-      else tulip.REPLICA_ABORTED_TXN)
+    let: ("res", "final") := Replica__finalized "rp" "ts" in
+    (if: "final"
+    then "res"
     else
       let: (<>, "validated") := MapGet (struct.loadF Replica "prepm" "rp") "ts" in
       (if: "validated"
@@ -244,23 +247,27 @@ Definition Replica__Validate: val :=
     Mutex__Unlock (struct.loadF Replica "mu" "rp");;
     "res".
 
-Definition Replica__probe: val :=
-  rec: "Replica__probe" "rp" "ts" :=
+Definition Replica__logFastPrepare: val :=
+  rec: "Replica__logFastPrepare" "rp" "ts" "pwrs" "ptgs" :=
+    #().
+
+Definition Replica__lastProposal: val :=
+  rec: "Replica__lastProposal" "rp" "ts" :=
     let: ("ps", "ok") := MapGet (struct.loadF Replica "pstbl" "rp") "ts" in
-    let: "pp" := struct.get PrepareStatusEntry "prep" "ps" in
-    (struct.get PrepareStatusEntry "rankl" "ps", struct.get PrepareProposal "rank" "pp", struct.get PrepareProposal "dec" "pp", "ok").
+    (struct.get PrepareProposal "rank" "ps", struct.get PrepareProposal "dec" "ps", "ok").
 
 Definition Replica__accept: val :=
   rec: "Replica__accept" "rp" "ts" "rank" "dec" :=
     let: "pp" := struct.mk PrepareProposal [
       "rank" ::= "rank";
       "dec" ::= "dec"
     ] in
-    let: "psnew" := struct.mk PrepareStatusEntry [
-      "rankl" ::= "rank" + #1;
-      "prep" ::= "pp"
-    ] in
-    MapInsert (struct.loadF Replica "pstbl" "rp") "ts" "psnew";;
+    MapInsert (struct.loadF Replica "pstbl" "rp") "ts" "pp";;
+    MapInsert (struct.loadF Replica "rktbl" "rp") "ts" (std.SumAssumeNoOverflow "rank" #1);;
+    #().
+
+Definition Replica__logAccept: val :=
+  rec: "Replica__logAccept" "rp" "ts" "rank" "dec" :=
     #().
 
 (* Arguments:
@@ -273,14 +280,11 @@ Definition Replica__accept: val :=
    @error: Error code. *)
 Definition Replica__fastPrepare: val :=
   rec: "Replica__fastPrepare" "rp" "ts" "pwrs" "ptgs" :=
-    let: ("cmted", "done") := MapGet (struct.loadF Replica "txntbl" "rp") "ts" in
-    (if: "done"
-    then
-      (if: "cmted"
-      then tulip.REPLICA_COMMITTED_TXN
-      else tulip.REPLICA_ABORTED_TXN)
+    let: ("res", "final") := Replica__finalized "rp" "ts" in
+    (if: "final"
+    then "res"
     else
-      let: (((<>, "rank"), "dec"), "ok") := Replica__probe "rp" "ts" in
+      let: (("rank", "dec"), "ok") := Replica__lastProposal "rp" "ts" in
       (if: "ok"
       then
         (if: #0 < "rank"
@@ -297,9 +301,12 @@ Definition Replica__fastPrepare: val :=
           let: "acquired" := Replica__acquire "rp" "ts" "pwrs" in
           Replica__accept "rp" "ts" #0 "acquired";;
           (if: (~ "acquired")
-          then tulip.REPLICA_FAILED_VALIDATION
+          then
+            Replica__logAccept "rp" "ts" #0 #false;;
+            tulip.REPLICA_FAILED_VALIDATION
           else
             MapInsert (struct.loadF Replica "prepm" "rp") "ts" "pwrs";;
+            Replica__logFastPrepare "rp" "ts" "pwrs" "ptgs";;
             tulip.REPLICA_OK)))).
 
 Definition Replica__FastPrepare: val :=
@@ -310,6 +317,11 @@ Definition Replica__FastPrepare: val :=
     Mutex__Unlock (struct.loadF Replica "mu" "rp");;
     "res".
 
+Definition Replica__lowestRank: val :=
+  rec: "Replica__lowestRank" "rp" "ts" :=
+    let: ("rank", "ok") := MapGet (struct.loadF Replica "rktbl" "rp") "ts" in
+    ("rank", "ok").
+
 (* Accept the prepare decision for @ts at @rank, if @rank is most recent.
 
    Arguments:
@@ -321,18 +333,16 @@ Definition Replica__FastPrepare: val :=
    @error: Error code. *)
 Definition Replica__tryAccept: val :=
   rec: "Replica__tryAccept" "rp" "ts" "rank" "dec" :=
-    let: ("cmted", "done") := MapGet (struct.loadF Replica "txntbl" "rp") "ts" in
-    (if: "done"
-    then
-      (if: "cmted"
-      then tulip.REPLICA_COMMITTED_TXN
-      else tulip.REPLICA_ABORTED_TXN)
+    let: ("res", "final") := Replica__finalized "rp" "ts" in
+    (if: "final"
+    then "res"
     else
-      let: ((("rankl", <>), <>), "ok") := Replica__probe "rp" "ts" in
+      let: ("rankl", "ok") := Replica__lowestRank "rp" "ts" in
       (if: "ok" && ("rank" < "rankl")
       then tulip.REPLICA_STALE_COORDINATOR
       else
         Replica__accept "rp" "ts" "rank" "dec";;
+        Replica__logAccept "rp" "ts" "rank" "dec";;
         tulip.REPLICA_OK)).
 
 Definition Replica__Prepare: val :=
@@ -364,18 +374,14 @@ Definition Replica__inquire: val :=
         (struct.mk PrepareProposal [
          ], #false, slice.nil, tulip.REPLICA_ABORTED_TXN))
     else
-      let: ("ps", "ok") := MapGet (struct.loadF Replica "pstbl" "rp") "ts" in
-      (if: "ok" && ("rank" ≤ (struct.get PrepareStatusEntry "rankl" "ps"))
+      let: ("rankl", "ok") := MapGet (struct.loadF Replica "rktbl" "rp") "ts" in
+      (if: "ok" && ("rank" ≤ "rankl")
       then
         (struct.mk PrepareProposal [
          ], #false, slice.nil, tulip.REPLICA_INVALID_RANK)
       else
-        let: "pp" := struct.get PrepareStatusEntry "prep" "ps" in
-        let: "psnew" := struct.mk PrepareStatusEntry [
-          "rankl" ::= "rank";
-          "prep" ::= "pp"
-        ] in
-        MapInsert (struct.loadF Replica "pstbl" "rp") "ts" "psnew";;
+        let: "pp" := Fst (MapGet (struct.loadF Replica "pstbl" "rp") "ts") in
+        MapInsert (struct.loadF Replica "rktbl" "rp") "ts" "rank";;
         let: ("pwrs", "vd") := MapGet (struct.loadF Replica "prepm" "rp") "ts" in
         ("pp", "vd", "pwrs", tulip.REPLICA_OK))).
 
@@ -389,14 +395,11 @@ Definition Replica__Inquire: val :=
 
 Definition Replica__query: val :=
   rec: "Replica__query" "rp" "ts" "rank" :=
-    let: ("cmted", "done") := MapGet (struct.loadF Replica "txntbl" "rp") "ts" in
-    (if: "done"
-    then
-      (if: "cmted"
-      then tulip.REPLICA_COMMITTED_TXN
-      else tulip.REPLICA_ABORTED_TXN)
+    let: ("res", "final") := Replica__finalized "rp" "ts" in
+    (if: "final"
+    then "res"
     else
-      let: ((("rankl", <>), <>), "ok") := Replica__probe "rp" "ts" in
+      let: ("rankl", "ok") := Replica__lowestRank "rp" "ts" in
       (if: "ok" && ("rank" < "rankl")
       then tulip.REPLICA_STALE_COORDINATOR
       else tulip.REPLICA_OK)).
@@ -505,8 +508,7 @@ Definition Replica__Start: val :=
 Definition Replica__StartBackupTxnCoordinator: val :=
   rec: "Replica__StartBackupTxnCoordinator" "rp" "ts" :=
     Mutex__Lock (struct.loadF Replica "mu" "rp");;
-    let: "ps" := Fst (MapGet (struct.loadF Replica "pstbl" "rp") "ts") in
-    let: "rank" := (struct.get PrepareStatusEntry "rankl" "ps") + #1 in
+    let: "rank" := (Fst (MapGet (struct.loadF Replica "rktbl" "rp") "ts")) + #1 in
     let: "ptgs" := Fst (MapGet (struct.loadF Replica "ptgsm" "rp") "ts") in
     let: "tcoord" := backup.MkBackupTxnCoordinator "ts" "rank" "ptgs" (struct.loadF Replica "rps" "rp") (struct.loadF Replica "leader" "rp") in
     backup.BackupTxnCoordinator__ConnectAll "tcoord";;

src/program_proof/tulip/base.v

@@ -8,6 +8,7 @@ Definition dbmod := (dbkey * dbval)%type.
 Definition dbmap := gmap dbkey dbval.
 Definition dbkmod := gmap nat dbval.
 Definition coordid := (u64 * u64)%type.
+Definition ppsl := (u64 * bool)%type.
 
 (** Transaction result. *)
 Inductive txnres :=
@@ -66,6 +67,26 @@ Proof.
   by destruct v.
 Defined.
 
+Definition ppsl_to_val (v : ppsl) : val := (#v.1, (#v.2, #())).
+
+Definition ppsl_from_val (v : val) : option ppsl :=
+  match v with
+  | (#(LitInt n), (#(LitBool b), #()))%V => Some (n, b)
+  | _ => None
+  end.
+
+#[global]
+Instance ppsl_into_val : IntoVal ppsl.
+Proof.
+  refine {|
+      to_val := ppsl_to_val;
+      from_val := ppsl_from_val;
+      IntoVal_def := (W64 0, false);
+    |}.
+  intros v.
+  by destruct v.
+Defined.
+
 Definition fstring := {k : string | (String.length k < 2 ^ 64)%nat}.
 
 #[local]

src/program_proof/tulip/cmd.v

@@ -385,87 +385,81 @@ Section execute_cmds.
   | LocalState
       (cm : gmap nat bool) (hists : gmap dbkey dbhist) (cpm : gmap nat dbmap)
       (ptgsm : gmap nat (gset u64)) (sptsm ptsm : gmap dbkey nat)
-      (bm : gmap nat ballot) (laim : gmap nat nat)
+      (psm : gmap nat (nat * bool)) (rkm : gmap nat nat)
   | LocalStuck.
 
   Definition not_local_stuck st := st ≠ LocalStuck.
 
   Definition execute_commit st (tid : nat) (pwrs : dbmap) :=
     match st with
-    | LocalState cm hists cpm ptgsm sptsm ptsm bm laim =>
+    | LocalState cm hists cpm ptgsm sptsm ptsm psm rkm =>
         match cm !! tid with
         | Some true => st
         | Some false => LocalStuck
         | None => match cpm !! tid with
                  | Some _ => LocalState
                               (<[tid := true]> cm) (multiwrite tid pwrs hists)
                               (delete tid cpm) (delete tid ptgsm) sptsm (release pwrs ptsm)
-                              bm laim
+                              psm rkm
                  | None => LocalState
                             (<[tid := true]> cm) (multiwrite tid pwrs hists)
-                            cpm ptgsm sptsm ptsm bm laim
+                            cpm ptgsm sptsm ptsm psm rkm
                  end
         end
     | LocalStuck => LocalStuck
     end.
 
   Definition execute_abort st (tid : nat) :=
     match st with
-    | LocalState cm hists cpm ptgsm sptsm ptsm bm laim =>
+    | LocalState cm hists cpm ptgsm sptsm ptsm psm rkm =>
         match cm !! tid with
         | Some true => LocalStuck
         | Some false => st
         | None => match cpm !! tid with
                  | Some pwrs => LocalState
                                  (<[tid := false]> cm) hists (delete tid cpm)
-                                 (delete tid ptgsm) sptsm (release pwrs ptsm) bm laim
-                 | None => LocalState (<[tid := false]> cm) hists cpm ptgsm sptsm ptsm bm laim
+                                 (delete tid ptgsm) sptsm (release pwrs ptsm) psm rkm
+                 | None => LocalState (<[tid := false]> cm) hists cpm ptgsm sptsm ptsm psm rkm
                  end
         end
     | LocalStuck => LocalStuck
     end.
 
   Definition execute_acquire st (tid : nat) (pwrs : dbmap) (ptgs : gset u64) :=
     match st with
-    | LocalState cm hists cpm ptgsm sptsm ptsm bm laim =>
+    | LocalState cm hists cpm ptgsm sptsm ptsm psm rkm =>
         LocalState
           cm hists (<[tid := pwrs]> cpm) (<[tid := ptgs]> ptgsm)
-          (setts tid pwrs sptsm) (acquire tid pwrs ptsm) bm laim
+          (setts tid pwrs sptsm) (acquire tid pwrs ptsm) psm rkm
     | LocalStuck => LocalStuck
     end.
 
   Definition execute_read st (tid : nat) (key : dbkey) :=
     match st with
-    | LocalState cm hists cpm ptgsm sptsm ptsm bm laim =>
+    | LocalState cm hists cpm ptgsm sptsm ptsm psm rkm =>
         LocalState
-          cm hists cpm ptgsm (alter (λ spts, (spts `max` pred tid)%nat) key sptsm) ptsm bm laim
+          cm hists cpm ptgsm (alter (λ spts, (spts `max` pred tid)%nat) key sptsm) ptsm psm rkm
     | LocalStuck => LocalStuck
     end.
 
+  Definition init_psm (tid : nat) (psm : gmap nat (nat * bool)) :=
+    match psm !! tid with
+    | Some _ => psm
+    | None => <[tid := (O, false)]> psm
+    end.
+
   Definition execute_advance st (tid : nat) (rank : nat) :=
     match st with
-    | LocalState cm hists cpm ptgsm sptsm ptsm bm laim =>
-        let blt := extend rank Reject (match bm !! tid with
-                                       | Some l => l
-                                       | None => [Accept false]
-                                       end) in
-        let laim' := match laim !! tid with
-                     | Some _ => laim
-                     | _ => <[tid := O]> laim
-                     end in
-        LocalState cm hists cpm ptgsm sptsm ptsm (<[tid := blt]> bm) laim'
+    | LocalState cm hists cpm ptgsm sptsm ptsm psm rkm =>
+        LocalState cm hists cpm ptgsm sptsm ptsm (init_psm tid psm) (<[tid := rank]> rkm)
     | LocalStuck => LocalStuck
     end.
 
   Definition execute_accept st (tid : nat) (rank : nat) (pdec : bool) :=
     match st with
-    | LocalState cm hists cpm ptgsm sptsm ptsm bm laim =>
-        let blt := match bm !! tid with
-                   | Some l => extend rank Reject l
-                   | None => replicate rank Reject
-                   end ++ [Accept pdec] in
+    | LocalState cm hists cpm ptgsm sptsm ptsm psm rkm =>
         LocalState
-          cm hists cpm ptgsm sptsm ptsm (<[tid := blt]> bm) (<[tid := rank]> laim)
+          cm hists cpm ptgsm sptsm ptsm (<[tid := (rank, pdec)]> psm) (<[tid := S rank]> rkm)
     | LocalStuck => LocalStuck
     end.
 
@@ -499,14 +493,14 @@ Section execute_cmds.
     execute_cmds (cmds ++ [cmd]) = execute_cmd (execute_cmds cmds) cmd.
   Proof. by rewrite /execute_cmds foldl_snoc. Qed.
 
-  Lemma execute_cmds_dom_histm {log cm histm cpm ptgsm sptsm ptsm bm laim} :
-    execute_cmds log = LocalState cm histm cpm ptgsm sptsm ptsm bm laim ->
+  Lemma execute_cmds_dom_histm {log cm histm cpm ptgsm sptsm ptsm psm rkm} :
+    execute_cmds log = LocalState cm histm cpm ptgsm sptsm ptsm psm rkm ->
     dom histm = keys_all.
   Proof.
   Admitted.
 
-  Lemma execute_cmds_hist_not_nil {log cm histm cpm ptgsm sptsm ptsm bm laim} :
-    execute_cmds log = LocalState cm histm cpm ptgsm sptsm ptsm bm laim ->
+  Lemma execute_cmds_hist_not_nil {log cm histm cpm ptgsm sptsm ptsm psm rkm} :
+    execute_cmds log = LocalState cm histm cpm ptgsm sptsm ptsm psm rkm ->
     map_Forall (λ _ h, h ≠ []) histm.
   Admitted.
 
@@ -534,8 +528,8 @@ Section merge_clog_ilog.
 
   Lemma execute_cmds_apply_cmds clog ilog cm histm :
     let log := merge_clog_ilog clog ilog in
-    (∃ cpm ptgsm sptsm ptsm bm laim,
-        execute_cmds log = LocalState cm histm cpm ptgsm sptsm ptsm bm laim) ->
+    (∃ cpm ptgsm sptsm ptsm psm rkm,
+        execute_cmds log = LocalState cm histm cpm ptgsm sptsm ptsm psm rkm) ->
     apply_cmds clog = State cm histm.
   Admitted.