Commit 6a6fe26f by Dan Frumin

### Don't use subnamespaces in the ticket lock refinement

parent 4c60831d
 ... @@ -117,21 +117,15 @@ Section refinement. ... @@ -117,21 +117,15 @@ Section refinement. Program Definition lockInt := λne vv, Program Definition lockInt := λne vv, (∃ (lo ln : loc) (γ : gname) (l' : loc), (∃ (lo ln : loc) (γ : gname) (l' : loc), ⌜vv.1 = (#lo, #ln)%V⌝ ∗ ⌜vv.2 = #l'⌝ ⌜vv.1 = (#lo, #ln)%V⌝ ∗ ⌜vv.2 = #l'⌝ ∗ inv (N.@(lo,ln,l')) (lockInv lo ln γ l'))%I. ∗ inv N (lockInv lo ln γ l'))%I. Next Obligation. solve_proper. Qed. Next Obligation. solve_proper. Qed. (* Program Definition lockInt (γp : gname) := λne vv, *) (* (∃ (lo ln : loc) (γ : gname) (l' : loc), *) (* ⌜vv.1 = (#lo, #ln)%V⌝ ∗ ⌜vv.2 = #l'⌝ *) (* ∗ inPool γp lo ln γ l')%I. *) (* Next Obligation. solve_proper. Qed. *) Instance lockInt_persistent ww : Persistent (lockInt ww). Instance lockInt_persistent ww : Persistent (lockInt ww). Proof. apply _. Qed. Proof. apply _. Qed. (** * Refinement proofs *) (** * Refinement proofs *) Local Ltac openI N := Local Ltac openI := iInv N as (o n b) ">(Hlo & Hln & Hissued & Hl' & Hbticket)" "Hcl". iInv N as (o n b) ">(Hlo & Hln & Hissued & Hl' & Hbticket)" "Hcl". Local Ltac closeI := iMod ("Hcl" with "[-]") as "_"; Local Ltac closeI := iMod ("Hcl" with "[-]") as "_"; first by (iNext; iExists _,_,_; iFrame). first by (iNext; iExists _,_,_; iFrame). ... @@ -154,7 +148,7 @@ Section refinement. ... @@ -154,7 +148,7 @@ Section refinement. iIntros (l') "Hl'". iIntros (l') "Hl'". (* Establishing the invariant *) (* Establishing the invariant *) iMod newIssuedTickets as (γ) "Hγ". iMod newIssuedTickets as (γ) "Hγ". iMod (inv_alloc (N.@(lo,ln,l')) _ (lockInv lo ln γ l') with "[-]") as "#Hinv". iMod (inv_alloc N _ (lockInv lo ln γ l') with "[-]") as "#Hinv". { iNext. iExists _,_,_. iFrame. } { iNext. iExists _,_,_. iFrame. } rel_vals. iModIntro. iAlways. rel_vals. iModIntro. iAlways. iExists _,_,_,_. iFrame "Hinv". eauto. iExists _,_,_,_. iFrame "Hinv". eauto. ... @@ -163,7 +157,7 @@ Section refinement. ... @@ -163,7 +157,7 @@ Section refinement. (* Acquiring a lock *) (* Acquiring a lock *) (* helper lemma *) (* helper lemma *) Lemma wait_loop_refinement Δ Γ (lo ln : loc) γ (l' : loc) (m : nat) : Lemma wait_loop_refinement Δ Γ (lo ln : loc) γ (l' : loc) (m : nat) : inv (N.@(lo,ln,l')) (lockInv lo ln γ l') -∗ inv N (lockInv lo ln γ l') -∗ ticket γ m -∗ ticket γ m -∗ {(lockInt :: Δ); ⤉Γ} ⊨ {(lockInt :: Δ); ⤉Γ} ⊨ wait_loop #m (#lo, #ln) ≤log≤ lock.acquire #l' : TUnit. wait_loop #m (#lo, #ln) ≤log≤ lock.acquire #l' : TUnit. ... @@ -174,7 +168,7 @@ Section refinement. ... @@ -174,7 +168,7 @@ Section refinement. unlock {2}wait_loop. simpl. unlock {2}wait_loop. simpl. rel_let_l. rel_proj_l. rel_let_l. rel_proj_l. rel_load_l_atomic. rel_load_l_atomic. openI (N.@(lo, ln, l')). openI. iModIntro. iExists _; iFrame; iNext. iModIntro. iExists _; iFrame; iNext. iIntros "Hlo". iIntros "Hlo". rel_op_l. rel_op_l. ... @@ -263,7 +257,7 @@ Section refinement. ... @@ -263,7 +257,7 @@ Section refinement. if b then ticket γ o else True)%I if b then ticket γ o else True)%I True%I γ); first done. True%I γ); first done. iAlways. iAlways. openI (N.@(lo, ln, l')). openI. iModIntro. iExists _,_; iFrame. iModIntro. iExists _,_; iFrame. iSplitL "Hbticket Hl'". iSplitL "Hbticket Hl'". { iExists _. iFrame. } { iExists _. iFrame. } ... @@ -296,7 +290,7 @@ Section refinement. ... @@ -296,7 +290,7 @@ Section refinement. rel_let_l. repeat rel_proj_l. rel_let_l. repeat rel_proj_l. rel_apply_l (bin_log_FG_increment_logatomic _ (issuedTickets γ)%I True%I); first done. rel_apply_l (bin_log_FG_increment_logatomic _ (issuedTickets γ)%I True%I); first done. iAlways. iAlways. openI (N.@(lo, ln, l')). openI. iModIntro. iExists _; iFrame. iModIntro. iExists _; iFrame. iSplit. iSplit. - iDestruct 1 as (m) "[Hln ?]". - iDestruct 1 as (m) "[Hln ?]". ... @@ -368,7 +362,7 @@ Section refinement. ... @@ -368,7 +362,7 @@ Section refinement. ∗ if b then ticket γ o else True)%I). ∗ if b then ticket γ o else True)%I). rel_apply_l (wkincr_atomic_l R True%I); first done. rel_apply_l (wkincr_atomic_l R True%I); first done. iAlways. iAlways. openI (N.@(lo, ln, l')). openI. iModIntro. iExists _; iFrame. iModIntro. iExists _; iFrame. rewrite {1}/R. iSplitR "Hcl". rewrite {1}/R. iSplitR "Hcl". { iExists _,_; by iFrame. } clear o n b. { iExists _,_; by iFrame. } clear o n b. ... ...
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!