Sync tulip proof

Note that right now the "debug/moderation" procedures (i.e., dumping states and
forcing re-election to control the leader location) is invoked through an
out-of-band interface (i.e., not through the verified client). This means the
proof does not enforce their correctness. The plan is to add an verified
moderator to make operations outside the transaction protocol. All the
moderation methods (on the moderator and the server sides) should have trivial
specification, but proving against them would still be useful by ensuring no UBs
appear in the implementation.

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

@@ -799,19 +799,19 @@ Definition GroupCoordinator__GetLeader: val :=
     Mutex__Unlock (struct.loadF GroupCoordinator "mu" "gcoord");;
     SliceGet uint64T (struct.loadF GroupCoordinator "rps" "gcoord") "idxleader".
 
+Definition GroupCoordinator__SendCommit: val :=
+  rec: "GroupCoordinator__SendCommit" "gcoord" "rid" "ts" "pwrs" :=
+    let: "data" := message.EncodeTxnCommitRequest "ts" "pwrs" in
+    GroupCoordinator__Send "gcoord" "rid" "data";;
+    #().
+
 Definition GroupCoordinator__Finalized: val :=
   rec: "GroupCoordinator__Finalized" "gcoord" "ts" :=
     Mutex__Lock (struct.loadF GroupCoordinator "mu" "gcoord");;
     let: (<>, "ok") := MapGet (struct.loadF GroupCoordinator "tsfinals" "gcoord") "ts" in
     Mutex__Unlock (struct.loadF GroupCoordinator "mu" "gcoord");;
     (~ "ok").
 
-Definition GroupCoordinator__SendCommit: val :=
-  rec: "GroupCoordinator__SendCommit" "gcoord" "rid" "ts" "pwrs" :=
-    let: "data" := message.EncodeTxnCommitRequest "ts" "pwrs" in
-    GroupCoordinator__Send "gcoord" "rid" "data";;
-    #().
-
 Definition GroupCoordinator__ChangeLeader: val :=
   rec: "GroupCoordinator__ChangeLeader" "gcoord" :=
     Mutex__Lock (struct.loadF GroupCoordinator "mu" "gcoord");;
@@ -824,11 +824,13 @@ Definition GroupCoordinator__Commit: val :=
   rec: "GroupCoordinator__Commit" "gcoord" "ts" "pwrs" :=
     GroupCoordinator__RegisterFinalization "gcoord" "ts";;
     let: "leader" := ref_to uint64T (GroupCoordinator__GetLeader "gcoord") in
+    GroupCoordinator__SendCommit "gcoord" (![uint64T] "leader") "ts" "pwrs";;
+    time.Sleep params.NS_RESEND_COMMIT;;
     Skip;;
     (for: (λ: <>, (~ (GroupCoordinator__Finalized "gcoord" "ts"))); (λ: <>, Skip) := λ: <>,
+      "leader" <-[uint64T] (GroupCoordinator__ChangeLeader "gcoord");;
       GroupCoordinator__SendCommit "gcoord" (![uint64T] "leader") "ts" "pwrs";;
       time.Sleep params.NS_RESEND_COMMIT;;
-      "leader" <-[uint64T] (GroupCoordinator__ChangeLeader "gcoord");;
       Continue);;
     #().
 
@@ -842,10 +844,12 @@ Definition GroupCoordinator__Abort: val :=
   rec: "GroupCoordinator__Abort" "gcoord" "ts" :=
     GroupCoordinator__RegisterFinalization "gcoord" "ts";;
     let: "leader" := ref_to uint64T (GroupCoordinator__GetLeader "gcoord") in
+    GroupCoordinator__SendAbort "gcoord" (![uint64T] "leader") "ts";;
+    time.Sleep params.NS_RESEND_ABORT;;
     Skip;;
     (for: (λ: <>, (~ (GroupCoordinator__Finalized "gcoord" "ts"))); (λ: <>, Skip) := λ: <>,
+      "leader" <-[uint64T] (GroupCoordinator__ChangeLeader "gcoord");;
       GroupCoordinator__SendAbort "gcoord" (![uint64T] "leader") "ts";;
       time.Sleep params.NS_RESEND_ABORT;;
-      "leader" <-[uint64T] (GroupCoordinator__ChangeLeader "gcoord");;
       Continue);;
     #().

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

@@ -50,6 +50,10 @@ Definition MSG_TXN_COMMIT : expr := #300.
 
 Definition MSG_TXN_ABORT : expr := #301.
 
+Definition MSG_DUMP_STATE : expr := #10000.
+
+Definition MSG_FORCE_ELECTION : expr := #10001.
+
 Definition EncodeTxnReadRequest: val :=
   rec: "EncodeTxnReadRequest" "ts" "key" :=
     let: "bs" := NewSliceWithCap byteT #0 #32 in
@@ -332,6 +336,33 @@ Definition DecodeTxnCommitRequest: val :=
       "PartialWrites" ::= "pwrs"
     ].
 
+Definition EncodeDumpStateRequest: val :=
+  rec: "EncodeDumpStateRequest" "gid" :=
+    let: "bs" := NewSliceWithCap byteT #0 #16 in
+    let: "bs1" := marshal.WriteInt "bs" MSG_DUMP_STATE in
+    let: "data" := marshal.WriteInt "bs1" "gid" in
+    "data".
+
+Definition DecodeDumpStateRequest: val :=
+  rec: "DecodeDumpStateRequest" "bs" :=
+    let: ("gid", <>) := marshal.ReadInt "bs" in
+    struct.mk TxnRequest [
+      "Kind" ::= MSG_DUMP_STATE;
+      "Timestamp" ::= "gid"
+    ].
+
+Definition EncodeForceElectionRequest: val :=
+  rec: "EncodeForceElectionRequest" <> :=
+    let: "bs" := NewSliceWithCap byteT #0 #8 in
+    let: "data" := marshal.WriteInt "bs" MSG_FORCE_ELECTION in
+    "data".
+
+Definition DecodeForceElectionRequest: val :=
+  rec: "DecodeForceElectionRequest" <> :=
+    struct.mk TxnRequest [
+      "Kind" ::= MSG_FORCE_ELECTION
+    ].
+
 Definition EncodeTxnCommitResponse: val :=
   rec: "EncodeTxnCommitResponse" "ts" "res" :=
     let: "bs" := NewSliceWithCap byteT #0 #24 in
@@ -413,8 +444,14 @@ Definition DecodeTxnRequest: val :=
                     (if: "kind" = MSG_TXN_ABORT
                     then DecodeTxnAbortRequest "bs1"
                     else
-                      struct.mk TxnRequest [
-                      ]))))))))).
+                      (if: "kind" = MSG_DUMP_STATE
+                      then DecodeDumpStateRequest "bs1"
+                      else
+                        (if: "kind" = MSG_FORCE_ELECTION
+                        then DecodeForceElectionRequest #()
+                        else
+                          struct.mk TxnRequest [
+                          ]))))))))))).
 
 Definition DecodeTxnResponse: val :=
   rec: "DecodeTxnResponse" "bs" :=

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

@@ -6,15 +6,15 @@ Context `{ext_ty: ext_types}.
 
 Definition N_SHARDS : expr := #2.
 
-Definition NS_RECONNECT : expr := #10000000.
+Definition NS_RECONNECT : expr := #100000000.
 
 Definition NS_RESEND_PREPARE : expr := #500000000.
 
-Definition NS_RESEND_READ : expr := #20000000.
+Definition NS_RESEND_READ : expr := #400000000.
 
-Definition NS_RESEND_COMMIT : expr := #40000000.
+Definition NS_RESEND_COMMIT : expr := #400000000.
 
-Definition NS_RESEND_ABORT : expr := #40000000.
+Definition NS_RESEND_ABORT : expr := #400000000.
 
 Definition NS_SPAWN_BACKUP_BASE : expr := #5000000000.
 
@@ -30,10 +30,10 @@ Definition NS_ELECTION_TIMEOUT_BASE : expr := #2000000000.
 
 Definition NS_ELECTION_TIMEOUT_DELTA : expr := #1000000000.
 
-Definition N_RETRY_REPLICATED : expr := #10.
+Definition N_RETRY_REPLICATED : expr := #500.
 
-Definition NS_REPLICATED_INTERVAL : expr := #1000000.
+Definition NS_REPLICATED_INTERVAL : expr := #10000.
 
-Definition N_TXN_SITES : expr := #64.
+Definition N_TXN_SITES : expr := #1024.
 
 End code.

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

@@ -750,6 +750,44 @@ Definition Paxos__ConnectAll: val :=
       (Paxos__Connect "px" "nid");;
     #().
 
+Definition Paxos__DumpState: val :=
+  rec: "Paxos__DumpState" "px" :=
+    Mutex__Lock (struct.loadF Paxos "mu" "px");;
+    (* fmt.Printf("Current term: %d\n", px.termc) *)
+    (* fmt.Printf("Ledger term: %d\n", px.terml) *)
+    (* fmt.Printf("Number of log entries: %d\n", uint64(len(px.log))) *)
+    (* fmt.Printf("Committed LSN: %d\n", px.lsnc) *)
+    (* fmt.Printf("Is candidate / leader: %t / %t\n", px.iscand, px.isleader) *)
+    (if: struct.loadF Paxos "iscand" "px"
+    then
+      (* fmt.Printf("Candidate state:\n") *)
+      (* fmt.Printf("Largest term seen in prepare: %d\n", px.termp) *)
+      (* fmt.Printf("Longest log after committed LSN in prepare: %d\n", px.termp) *)
+      (* fmt.Printf("Number of votes granted: %d\n", uint64(len(px.respp))) *)
+      #()
+    else #());;
+    (if: struct.loadF Paxos "isleader" "px"
+    then
+      (* fmt.Printf("Leader state:\n") *)
+      (* fmt.Printf("Match LSN for each peer:\n") *)
+      MapIter (struct.loadF Paxos "lsnpeers" "px") (λ: "nid" "lsnpeer",
+        (* fmt.Printf("Peer %d -> %d\n", nid, lsnpeer) *)
+        #())
+    else #());;
+    Mutex__Unlock (struct.loadF Paxos "mu" "px");;
+    #().
+
+Definition Paxos__ForceElection: val :=
+  rec: "Paxos__ForceElection" "px" :=
+    Mutex__Lock (struct.loadF Paxos "mu" "px");;
+    let: ("termc", "lsnc") := Paxos__nominate "px" in
+    Mutex__Unlock (struct.loadF Paxos "mu" "px");;
+    ForSlice uint64T <> "nidloop" (struct.loadF Paxos "peers" "px")
+      (let: "nid" := "nidloop" in
+      Fork (let: "data" := EncodePrepareRequest "termc" "lsnc" in
+            Paxos__Send "px" "nid" "data"));;
+    #().
+
 Definition mkPaxos: val :=
   rec: "mkPaxos" "nidme" "termc" "terml" "lsnc" "log" "addrm" "fname" :=
     let: "sc" := MapLen "addrm" in

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

@@ -64,7 +64,7 @@ Definition Replica__Commit: val :=
     then #true
     else
       let: ("lsn", "term") := txnlog.TxnLog__SubmitCommit (struct.loadF Replica "txnlog" "rp") "ts" "pwrs" in
-      (if: "lsn" = #0
+      (if: "term" = #0
       then #false
       else
         let: "safe" := txnlog.TxnLog__WaitUntilSafe (struct.loadF Replica "txnlog" "rp") "lsn" "term" in
@@ -84,7 +84,7 @@ Definition Replica__Abort: val :=
     then #true
     else
       let: ("lsn", "term") := txnlog.TxnLog__SubmitAbort (struct.loadF Replica "txnlog" "rp") "ts" in
-      (if: "lsn" = #0
+      (if: "term" = #0
       then #false
       else
         let: "safe" := txnlog.TxnLog__WaitUntilSafe (struct.loadF Replica "txnlog" "rp") "lsn" "term" in
@@ -547,6 +547,29 @@ Definition Replica__StartBackupTxnCoordinator: val :=
     backup.BackupTxnCoordinator__Finalize "tcoord";;
     #().
 
+(* For debugging and evaluation purpose. *)
+Definition Replica__DumpState: val :=
+  rec: "Replica__DumpState" "rp" "gid" :=
+    Mutex__Lock (struct.loadF Replica "mu" "rp");;
+    (* fmt.Printf("@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@\n") *)
+    (* fmt.Printf("[G %d / R %d] Dumping replica state:\n", gid, rp.rid) *)
+    (* fmt.Printf("-------------------------------------------------------------\n") *)
+    (* fmt.Printf("Number of finalized txns: %d\n", uint64(len(rp.txntbl))) *)
+    (* fmt.Printf("Number of prepared txns: %d\n", uint64(len(rp.prepm))) *)
+    (* fmt.Printf("Number of acquired keys: %d\n", uint64(len(rp.ptsm))) *)
+    (* fmt.Printf("Applied LSN: %d\n\n", rp.lsna) *)
+    (* fmt.Printf("[G %d / R %d] Dumping paxos state:\n", gid, rp.rid) *)
+    (* fmt.Printf("-------------------------------------------------------------\n") *)
+    txnlog.TxnLog__DumpState (struct.loadF Replica "txnlog" "rp");;
+    (* fmt.Printf("@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@\n") *)
+    Mutex__Unlock (struct.loadF Replica "mu" "rp");;
+    #().
+
+Definition Replica__ForceElection: val :=
+  rec: "Replica__ForceElection" "rp" :=
+    txnlog.TxnLog__ForceElection (struct.loadF Replica "txnlog" "rp");;
+    #().
+
 Definition Replica__RequestSession: val :=
   rec: "Replica__RequestSession" "rp" "conn" :=
     Skip;;
@@ -636,7 +659,18 @@ Definition Replica__RequestSession: val :=
                           let: "data" := message.EncodeTxnAbortResponse "ts" tulip.REPLICA_WRONG_LEADER in
                           grove_ffi.Send "conn" "data";;
                           Continue)
-                      else Continue))))))))));;
+                      else
+                        (if: "kind" = message.MSG_DUMP_STATE
+                        then
+                          let: "gid" := struct.get message.TxnRequest "Timestamp" "req" in
+                          Replica__DumpState "rp" "gid";;
+                          Continue
+                        else
+                          (if: "kind" = message.MSG_FORCE_ELECTION
+                          then
+                            Replica__ForceElection "rp";;
+                            Continue
+                          else Continue))))))))))));;
     #().
 
 Definition Replica__Serve: val :=

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

@@ -43,7 +43,7 @@ Definition TXNLOG_COMMIT : expr := #1.
    be done in a general way, without relying on the content. *)
 Definition TxnLog__SubmitCommit: val :=
   rec: "TxnLog__SubmitCommit" "log" "ts" "pwrs" :=
-    let: "bs" := NewSliceWithCap byteT #0 #32 in
+    let: "bs" := NewSliceWithCap byteT #0 #64 in
     let: "bs1" := marshal.WriteInt "bs" TXNLOG_COMMIT in
     let: "bs2" := marshal.WriteInt "bs1" "ts" in
     let: "data" := util.EncodeKVMapFromSlice "bs2" "pwrs" in
@@ -110,6 +110,16 @@ Definition TxnLog__Lookup: val :=
           (struct.mk Cmd [
            ], #false)))).
 
+Definition TxnLog__DumpState: val :=
+  rec: "TxnLog__DumpState" "log" :=
+    paxos.Paxos__DumpState (struct.loadF TxnLog "px" "log");;
+    #().
+
+Definition TxnLog__ForceElection: val :=
+  rec: "TxnLog__ForceElection" "log" :=
+    paxos.Paxos__ForceElection (struct.loadF TxnLog "px" "log");;
+    #().
+
 Definition Start: val :=
   rec: "Start" "nidme" "addrm" "fname" :=
     let: "px" := paxos.Start "nidme" "addrm" "fname" in

src/program_proof/tulip/inv_txnsys.v

@@ -388,7 +388,7 @@ Section tidinv.
   Context `{!heapGS Σ}.
   Context `{!tulip_ghostG Σ}.
 
-  Definition zN_TXN_SITES : Z := 64.
+  Definition zN_TXN_SITES : Z := 1024.
 
   Definition sid_of (ts: u64) : u64 := word.modu ts (W64 zN_TXN_SITES).
 

src/program_proof/tulip/program/gcoord/gcoord_abort.v

@@ -23,13 +23,29 @@ Section program.
     (*@                                                                         @*)
     wp_apply (wp_GroupCoordinator__RegisterFinalization with "Hgcoord").
     iNamed "Hgcoord".
+
+    (*@     var leader = gcoord.GetLeader()                                     @*)
+    (*@     gcoord.SendAbort(leader, ts)                                        @*)
+    (*@     primitive.Sleep(params.NS_RESEND_ABORT)                             @*)
+    (*@                                                                         @*)
     wp_apply (wp_GroupCoordinator__GetLeader with "Hgcoord").
     iIntros (leader Hleader).
     wp_apply wp_ref_to; first by auto.
     iIntros (leaderP) "HleaderP".
-    wp_pures.
+    wp_load.
+    wp_apply (wp_GroupCoordinator__SendAbort with "Habted Hgcoord").
+    { apply Hleader. }
+    wp_apply wp_Sleep.
+
+    (*@     for !gcoord.Finalized(ts) {                                         @*)
+    (*@         // Retry with different leaders until success.                  @*)
+    (*@         leader = gcoord.ChangeLeader()                                  @*)
+    (*@         gcoord.SendAbort(leader, ts)                                    @*)
+    (*@         primitive.Sleep(params.NS_RESEND_ABORT)                         @*)
+    (*@     }                                                                   @*)
+    (*@ }                                                                       @*)
+
 
-    (*@     var leader = gcoord.GetLeader()                                     @*)
     (*@     for !gcoord.Finalized(ts) {                                         @*)
     (*@         gcoord.SendAbort(leader, ts)                                    @*)
     (*@         primitive.Sleep(params.NS_RESEND_ABORT)                         @*)
@@ -49,15 +65,14 @@ Section program.
       destruct finalized; wp_pures.
       { by iApply "HΦ". }
       iDestruct "HP" as (leader') "[HleaderP %Hin]".
-      wp_load.
-      wp_apply (wp_GroupCoordinator__SendAbort with "Habted").
-      { apply Hin. }
-      { iFrame "Hgcoord". }
-      wp_apply wp_Sleep.
-      wp_apply (wp_GroupCoordinator__ChangeLeader).
-      { iFrame "Hgcoord". }
+      wp_apply (wp_GroupCoordinator__ChangeLeader with "Hgcoord").
       iIntros (leadernew Hleadernew).
       wp_store.
+      wp_load.
+      wp_apply (wp_GroupCoordinator__SendAbort with "Habted Hgcoord").
+      { apply Hleadernew. }
+      wp_apply wp_Sleep.
+      wp_pures.
       iApply "HΦ".
       by iFrame.
     }