From d0a6e8d0a58419594191ce1c4aaac5f875fa4ade Mon Sep 17 00:00:00 2001 From: Dan Frumin Date: Mon, 15 Jan 2018 11:43:28 +0100 Subject: [PATCH] Use the most general rule for FAI in the ticket lock proof --- theories/tests/relatomic.v | 26 ++++++++++++-------------- 1 file changed, 12 insertions(+), 14 deletions(-) diff --git a/theories/tests/relatomic.v b/theories/tests/relatomic.v index 89eaf1c..2ba7d93 100644 --- a/theories/tests/relatomic.v +++ b/theories/tests/relatomic.v @@ -71,9 +71,9 @@ Section contents. Lemma FAI_atomic R1 R2 Γ E1 E2 K x t τ Δ : R2 -∗ □ (|={E1,E2}=> ∃ n : nat, x ↦ᵢ #n ∗ R1 n ∗ - (x ↦ᵢ #n ∗ R1 n ={E2,E1}=∗ True) ∧ - (x ↦ᵢ #(S n) ∗ R1 n -∗ R2 -∗ - {E2,E1;Δ;Γ} ⊨ fill K #n ≤log≤ t : τ)) + ((∃ (m: nat), x ↦ᵢ #m ∗ R1 m) ={E2,E1}=∗ True) ∧ + (∀ m, x ↦ᵢ #(S m) ∗ R1 m -∗ R2 -∗ + {E2,E1;Δ;Γ} ⊨ fill K #m ≤log≤ t : τ)) -∗ ({E1;Δ;Γ} ⊨ fill K (FAI #x) ≤log≤ t : τ). Proof. iIntros "HR2 #H". @@ -87,7 +87,7 @@ Section contents. iExists #n. iFrame. iNext. iIntros "Hx". iDestruct "Hrev" as "[Hrev _]". iMod ("Hrev" with "[HR Hx]") as "_". - { by iFrame. } + { iExists _. by iFrame. } rel_rec_l. rel_op_l. rel_cas_l_atomic. iMod "H" as (n') "[Hx [HR HQ]]". iModIntro. @@ -104,7 +104,7 @@ Section contents. rel_if_l. iDestruct "HQ" as "[HQ _]". iMod ("HQ" with "[Hx HR]") as "_". - { by iFrame. } + { iExists _. by iFrame. } unlock FAI. by iApply "IH". Qed. @@ -225,7 +225,7 @@ Section contents. rel_let_l. repeat rel_proj_l. (* rel_apply_l (FAI_atomic). *) rel_bind_l (FAI #ln). - iApply (FAI_atomic (fun _ => True)%I True%I); first done. + iApply (FAI_atomic (fun n => own γ (● GSet (seq_set 0 n)))%I True%I); first done. iAlways. iInv N as (P) "[>HP Hpool]" "Hcl". iDestruct (lockPool_lookup with "HP Hls") as %Hls. @@ -233,17 +233,15 @@ Section contents. rewrite {1}/lockInv. iDestruct "Hlk" as (o n b) "(>Hlo & >Hln & >Hseq & Hl' & Hrest)". iModIntro. iExists _; iFrame. - iSplitR; first done. iSplit. - - iIntros "[Hln ?]". - iMod ("Hcl" with "[-]") as "_". - { iNext. iExists P; iFrame. - iApply "Hpool". iExists _,_,_; iFrame. iFrame "Hrest". } - done. - - iIntros "[Hln ?] _". + - iDestruct 1 as (m) "[Hln ?]". + iApply ("Hcl" with "[-]"). + iNext. iExists P; iFrame. + iApply "Hpool". iExists _,_,_; by iFrame. + - iIntros (m) "[Hln Hseq] _". iMod (own_update with "Hseq") as "[Hseq Hticket]". { eapply auth_update_alloc. - eapply (gset_disj_alloc_empty_local_update _ {[ n ]}). + eapply (gset_disj_alloc_empty_local_update _ {[ m ]}). apply (seq_set_S_disjoint 0). } rewrite -(seq_set_S_union_L 0). iMod ("Hcl" with "[-Hticket]") as "_". -- 2.22.0