Use own_crash_ex for durable states in paxos

mit-pdos · Feb 15, 2025 · d11cd6d · d11cd6d
1 parent d7fb49a
commit d11cd6d
Show file tree

Hide file tree

Showing 18 changed files with 161 additions and 132 deletions.
diff --git a/external/Goose/github_com/mit_pdos/tulip/paxos.v b/external/Goose/github_com/mit_pdos/tulip/paxos.v
diff --git a/src/program_proof/tulip/paxos/base.v b/src/program_proof/tulip/paxos/base.v
@@ -435,7 +435,8 @@ Instance subG_paxos_ghostG {Σ} :
   subG paxos_ghostΣ Σ → paxos_ghostG Σ.
 Proof. solve_inG. Qed.
 
-(* Instance stagedG_paxos_ghostG Σ : paxos_ghostG Σ → stagedG Σ. *)
+Instance stagedG_paxos_ghostG Σ : paxos_ghostG Σ → stagedG Σ.
+Admitted.
 
 Record paxos_names := {
     consensus_log : gname;

diff --git a/src/program_proof/tulip/paxos/inv.v b/src/program_proof/tulip/paxos/inv.v
@@ -518,6 +518,23 @@ Section inv_file.
   Context `{!heapGS Σ, !paxos_ghostG Σ}.
 
   Definition paxosfileNS := paxosNS .@ "file".
+  (* TODO: make name consistent, also think about the right NS structure *)
+  Definition pxcrashNS := nroot .@ "pxcrash".
+
+  (* TODO: using nat (rather than u64) here would be more consistent with the
+  principle that in the protocol world types are perfect. *)
+  Inductive pxdur :=
+  | PaxosDurable (termc terml : u64) (log : list byte_string) (lsn : u64).
+
+  Definition own_paxos_durable
+    γ (nidme : u64) (dst : pxdur) : iProp Σ :=
+    match dst with
+    | PaxosDurable termc terml log lsnc =>
+        "Htermc" ∷ own_current_term_half γ nidme (uint.nat termc) ∗
+        "Hterml" ∷ own_ledger_term_half γ nidme (uint.nat terml) ∗
+        "Hlogn"  ∷ own_node_ledger_half γ nidme log ∗
+        "Hlsnc"  ∷ own_committed_lsn_half γ nidme (uint.nat lsnc)
+    end.
 
   (* Required during recovery. *)
   Definition valid_wal_entry (cmd : pxcmd) :=

diff --git a/src/program_proof/tulip/paxos/prelude.v b/src/program_proof/tulip/paxos/prelude.v
@@ -1,5 +1,6 @@
 From Perennial.program_proof Require Export grove_prelude.
 From Perennial.program_logic Require Export atomic. (* prefer the ncfupd atomics *)
+From Perennial.program_logic Require Export own_crash_inv. (* import [own_crash_ex] *)
 From Perennial.program_proof.rsm Require Export big_sep.
 From Perennial.program_proof.rsm.pure Require Export
   extend fin_maps fin_sets list misc nat sets word quorum.

diff --git a/src/program_proof/tulip/paxos/program/mk_paxos.v b/src/program_proof/tulip/paxos/program/mk_paxos.v
@@ -7,7 +7,8 @@ Section mk_paxos.
 
   Theorem wp_mkPaxos
     (nidme : u64) (termc : u64) (terml : u64) (lsnc : u64)
-    (logP : Slice.t) (log : list byte_string) (addrmP : loc) (addrm : gmap u64 chan) (fname : byte_string) γ :
+    (logP : Slice.t) (log : list byte_string) (addrmP : loc) (addrm : gmap u64 chan)
+    (fname : byte_string) γ :
     (1 < size addrm)%nat ->
     nidme ∈ dom addrm ->
     0 ≤ uint.Z nidme < max_nodes ->
@@ -17,18 +18,14 @@ Section mk_paxos.
     know_paxos_network_inv γ addrm -∗
     {{{ own_slice logP stringT (DfracOwn 1) log ∗
         own_map addrmP (DfracOwn 1) addrm ∗
-        (* own_crash_ex paxoscrashNS (own_current_term_half γ nidme) (uint.nat termc) ∗ *)
-        own_current_term_half γ nidme (uint.nat termc) ∗
-        own_ledger_term_half γ nidme (uint.nat terml) ∗
-        own_committed_lsn_half γ nidme (uint.nat lsnc) ∗
-        own_node_ledger_half γ nidme log
+        own_crash_ex pxcrashNS (own_paxos_durable γ nidme) (PaxosDurable termc terml log lsnc)
     }}}
       mkPaxos #nidme #termc #terml #lsnc (to_val logP) #addrmP #(LitString fname)
     {{{ (px : loc), RET #px; is_paxos_with_addrm px nidme addrm γ }}}.
   Proof.
     iIntros (Hmulti Hnidme Hltmax) "#Hfname #Hinv #Hinvfile #Hinvnet".
     (* avoid naming collision when opening invariant. *)
-    iIntros (Φ) "!> (Hlog & Haddrm & HtermcX & HtermlX & HlsncX & HlognX) HΦ".
+    iIntros (Φ) "!> (Hlog & Haddrm & Hdurable) HΦ".
     wp_rec.
 
     (*@ func mkPaxos(nidme, termc, terml, lsnc uint64, log []string, addrm map[uint64]grove_ffi.Address) *Paxos { @*)
@@ -140,6 +137,9 @@ Section mk_paxos.
       { clear -Hmulti Hszaddrm. word. }
       { rewrite size_dom. clear -Hmulti Hszaddrm. word. }
     }
+    iMod (own_crash_ex_open with "Hdurable") as "[> Hdurable HdurableC]".
+    { solve_ndisj. }
+    iNamedSuffix "Hdurable" "X".
     (* Obtain persistent/pure resources that for convenience are also kept in lock inv. *)
     iInv "Hinv" as "> HinvO" "HinvC".
     iAssert (prefix_base_ledger γ (uint.nat terml) log)%I as "#Hgebase".
@@ -150,8 +150,6 @@ Section mk_paxos.
       iDestruct (accepted_proposal_lookup with "Hacpt Hpsa") as %Hlogn.
       by iApply (big_sepM_lookup with "Hpsalbs").
     }
-    (* iMod (own_crash_ex_open with "HtermcX") as "(>HtermcX&Hclose_termcX)". *)
-    (* { solve_ndisj. } *)
     iAssert (if decide (termc = terml)
              then True
              else past_nodedecs_latest_before γ nidme (uint.nat termc) (uint.nat terml) log)%I
@@ -217,8 +215,9 @@ Section mk_paxos.
       iPureIntro.
       clear -Hltlog. word.
     }
-    (* iMod ("Hclose_termcX" with "HtermcX"). *)
     iMod ("HinvC" with "HinvO") as "_".
+    set dst := PaxosDurable termc terml log lsnc.
+    iMod ("HdurableC" $! dst with "[$HtermcX $HtermlX $HlognX $HlsncX]") as "Hdurable".
     iAssert (own_paxos px nidme nids γ ∗ own_paxos_comm px addrm γ)%I
       with "[-HΦ Hfree]" as "(Hpx & Hcomm)".
     { iFrame "Hcand Hleader Hsc ∗ # %". }

diff --git a/src/program_proof/tulip/paxos/program/paxos_accept.v b/src/program_proof/tulip/paxos/program/paxos_accept.v
@@ -98,12 +98,14 @@ Section accept.
       iNamed "Hfname".
       wp_loadField.
       wp_apply (wp_logAdvance with "Hents").
+      iMod (own_crash_ex_open with "Hdurable") as "[> Hdurable HdurableC]".
+      { solve_ndisj. }
+      iNamed "Hdurable".
       iInv "Hinv" as "> HinvO" "HinvC".
       iInv "Hinvfile" as "> HinvfileO" "HinvfileC".
       iDestruct (big_sepS_elem_of_acc with "HinvfileO") as "[Hnodefile HinvfileO]".
       { apply Hnidme. }
       iNamed "Hnodefile".
-      (* iMod (own_crash_ex_open with "Htermc") as "(>Htermc&Hclose_termc)"; first solve_ndisj. *)
       iApply ncfupd_mask_intro; first solve_ndisj.
       iIntros "Hmask".
       iDestruct (node_wal_fname_agree with "Hfnameme Hwalfname") as %->.
@@ -116,6 +118,8 @@ Section accept.
         { iFrame "∗ # %". }
         iMod ("HinvfileC" with "HinvfileO") as "_".
         iMod ("HinvC" with "HinvO") as "_".
+        set dst := PaxosDurable term terml log lsn.
+        iMod ("HdurableC" $! dst with "[$Htermc $Hterml $Hlogn $Hlsnc]") as "Hdurable".
         by iIntros "!> [_ %Hcontra]".
       }
       (* Case: Write succeeded. *)
@@ -141,16 +145,16 @@ Section accept.
         word.
       }
       iMod "Hmask" as "_".
-      (* iMod ("Hclose_termc" with "Htermc") as "Htermc". *)
       iMod ("HinvfileC" with "HinvfileO") as "_".
       iMod ("HinvC" with "HinvO") as "_".
+      set dst := PaxosDurable term term logleader lsn.
+      iMod ("HdurableC" $! dst with "[$Htermc $Hterml $Hlogn $Hlsnc]") as "Hdurable".
       iIntros "!> Hents".
       wp_pures.
 
       (*@         return lsna                                                     @*)
       (*@     }                                                                   @*)
       (*@                                                                         @*)
-      iApply "HΦ".
       set log' := logc ++ _.
       set logc' := take (uint.nat lsn) log'.
       iInv "Hinv" as "> HinvO" "HinvC".
@@ -176,19 +180,22 @@ Section accept.
         by rewrite take_idemp.
       }
       iClear "Hcmted".
+      iApply "HΦ".
       iModIntro.
-      rewrite Heq.
       iSplit.
       { iFrame "Hcand Hleader HlogP HtermlP".
         iClear "Hpreped".
         case_decide; last done.
+        iFrame "∗".
+        rewrite Heq.
         iFrame "∗ # %".
         iPureIntro.
         split; first done.
         rewrite -Heq.
         word.
       }
       iFrame "Hacpted'".
+      rewrite Heq.
       iApply (own_slice_sz with "Hlog").
     }
 
@@ -262,16 +269,17 @@ Section accept.
     iNamed "Hfname".
     wp_loadField.
     wp_apply (wp_logAccept with "Hents").
+    iMod (own_crash_ex_open with "Hdurable") as "[> Hdurable HdurableC]".
+    { solve_ndisj. }
+    iNamed "Hdurable".
     iInv "Hinv" as "> HinvO" "HinvC".
     iInv "Hinvfile" as "> HinvfileO" "HinvfileC".
     iDestruct (big_sepS_elem_of_acc with "HinvfileO") as "[Hnodefile HinvfileO]".
     { apply Hnidme. }
     iNamed "Hnodefile".
-    (* iMod (own_crash_ex_open with "Htermc") as "(>Htermc&Hclose_termc)"; first solve_ndisj. *)
     iApply ncfupd_mask_intro; first solve_ndisj.
     iIntros "Hmask".
     iDestruct (node_wal_fname_agree with "Hfnameme Hwalfname") as %->.
-
     iFrame "Hfile %".
     iIntros (bs' failed) "Hfile".
     destruct failed.
@@ -281,6 +289,8 @@ Section accept.
       { iFrame "∗ # %". }
       iMod ("HinvfileC" with "HinvfileO") as "_".
       iMod ("HinvC" with "HinvO") as "_".
+      set dst := PaxosDurable terml terml log lsnc.
+      iMod ("HdurableC" $! dst with "[$Htermc $Hterml $Hlogn $Hlsnc]") as "Hdurable".
       by iIntros "!> [_ %Hcontra]".
     }
     (* Case: Write succeeded. *)
@@ -299,9 +309,10 @@ Section accept.
       word.
     }
     iMod "Hmask" as "_".
-    (* iMod ("Hclose_termc" with "Htermc") as "Htermc". *)
     iMod ("HinvfileC" with "HinvfileO") as "_".
     iMod ("HinvC" with "HinvO") as "_".
+    set dst := PaxosDurable terml terml logleader lsnc.
+    iMod ("HdurableC" $! dst with "[$Htermc $Hterml $Hlogn $Hlsnc]") as "Hdurable".
     iIntros "!> Hents".
     wp_pures.
 

diff --git a/src/program_proof/tulip/paxos/program/paxos_ascend.v b/src/program_proof/tulip/paxos/program/paxos_ascend.v
@@ -74,12 +74,14 @@ Section ascend.
     iNamed "Hfname".
     do 4 wp_loadField.
     wp_apply (wp_logAdvance with "Hentsp").
+    iMod (own_crash_ex_open with "Hdurable") as "[> Hdurable HdurableC]".
+    { solve_ndisj. }
+    iNamed "Hdurable".
     iInv "Hinv" as "> HinvO" "HinvC".
     iInv "Hinvfile" as "> HinvfileO" "HinvfileC".
     iDestruct (big_sepS_elem_of_acc with "HinvfileO") as "[Hnodefile HinvfileO]".
     { apply Hnidme. }
     iNamed "Hnodefile".
-    (* iMod (own_crash_ex_open with "Htermc") as "(>Htermc&Hclose_termc)"; first solve_ndisj. *)
     iApply ncfupd_mask_intro; first solve_ndisj.
     iIntros "Hmask".
     iDestruct (node_wal_fname_agree with "Hfnameme Hwalfname") as %->.
@@ -92,6 +94,8 @@ Section ascend.
       { iFrame "∗ # %". }
       iMod ("HinvfileC" with "HinvfileO") as "_".
       iMod ("HinvC" with "HinvO") as "_".
+      set dst := PaxosDurable termc terml log lsnc.
+      iMod ("HdurableC" $! dst with "[$Htermc $Hterml $Hlogn $Hlsnc]") as "Hdurable".
       by iIntros "!> [_ %Hcontra]".
     }
     (* Case: Write succeeded. *)
@@ -125,9 +129,10 @@ Section ascend.
       word.
     }
     iMod "Hmask" as "_".
-    (* iMod ("Hclose_termc" with "Htermc") as "Htermc". *)
     iMod ("HinvfileC" with "HinvfileO") as "_".
     iMod ("HinvC" with "HinvO") as "_".
+    set dst := PaxosDurable termc termc log' lsnc.
+    iMod ("HdurableC" $! dst with "[$Htermc $Hterml $Hlogn $Hlsnc]") as "Hdurable".
     iIntros "!> Hents".
     wp_pures.
 

diff --git a/src/program_proof/tulip/paxos/program/paxos_commit.v b/src/program_proof/tulip/paxos/program/paxos_commit.v
@@ -82,6 +82,9 @@ Section commit.
       iNamed "Hfname".
       do 2 wp_loadField.
       wp_apply wp_logExpand.
+      iMod (own_crash_ex_open with "Hdurable") as "[> Hdurable HdurableC]".
+      { solve_ndisj. }
+      iNamed "Hdurable".
       iInv "Hinv" as "> HinvO" "HinvC".
       iInv "Hinvfile" as "> HinvfileO" "HinvfileC".
       iDestruct (big_sepS_elem_of_acc with "HinvfileO") as "[Hnodefile HinvfileO]".
@@ -99,6 +102,8 @@ Section commit.
         { iFrame "∗ # %". }
         iMod ("HinvfileC" with "HinvfileO") as "_".
         iMod ("HinvC" with "HinvO") as "_".
+        set dst := PaxosDurable term term log lsnc.
+        iMod ("HdurableC" $! dst with "[$Htermc $Hterml $Hlogn $Hlsnc]") as "Hdurable".
         by iIntros "!> %Hcontra".
       }
       (* Case: Write succeeded. *)
@@ -120,6 +125,9 @@ Section commit.
       iMod "Hmask" as "_".
       iMod ("HinvfileC" with "HinvfileO") as "_".
       iMod ("HinvC" with "HinvO") as "_".
+      set dst := PaxosDurable term term log logP.(Slice.sz).
+      iMod ("HdurableC" $! dst with "[$Htermc $Hterml $Hlogn Hlsnc]") as "Hdurable".
+      { by rewrite Hszlog. }
       iIntros "!> _".
       wp_pures.
 
@@ -129,7 +137,6 @@ Section commit.
       iApply "HΦ".
       iFrame "Hcand Hleader".
       iFrame "Hsafe'".
-      rewrite -Hszlog.
       iFrame "∗ # %".
       iPureIntro.
       clear -Hszlog. word.
@@ -146,6 +153,9 @@ Section commit.
     iNamed "Hfname".
     wp_loadField.
     wp_apply wp_logExpand.
+    iMod (own_crash_ex_open with "Hdurable") as "[> Hdurable HdurableC]".
+    { solve_ndisj. }
+    iNamed "Hdurable".
     iInv "Hinv" as "> HinvO" "HinvC".
     iInv "Hinvfile" as "> HinvfileO" "HinvfileC".
     iDestruct (big_sepS_elem_of_acc with "HinvfileO") as "[Hnodefile HinvfileO]".
@@ -163,6 +173,8 @@ Section commit.
       { iFrame "∗ # %". }
       iMod ("HinvfileC" with "HinvfileO") as "_".
       iMod ("HinvC" with "HinvO") as "_".
+      set dst := PaxosDurable term term log lsnc.
+      iMod ("HdurableC" $! dst with "[$Htermc $Hterml $Hlogn $Hlsnc]") as "Hdurable".
       by iIntros "!> %Hcontra".
     }
     (* Case: Write succeeded. *)
@@ -190,6 +202,8 @@ Section commit.
     iMod "Hmask" as "_".
     iMod ("HinvfileC" with "HinvfileO") as "_".
     iMod ("HinvC" with "HinvO") as "_".
+    set dst := PaxosDurable term term log lsn.
+    iMod ("HdurableC" $! dst with "[$Htermc $Hterml $Hlogn $Hlsnc]") as "Hdurable".
     iIntros "!> _".
     wp_pures.
     iApply "HΦ".