### Massively simplify the ticket lock refinement

`Thanks to Robbert`
parent 299978e2
 ... @@ -70,10 +70,6 @@ Section refinement. ... @@ -70,10 +70,6 @@ Section refinement. Definition ticket (γ : gname) (n : nat) := own γ (◯ GSet {[ n ]}). Definition ticket (γ : gname) (n : nat) := own γ (◯ GSet {[ n ]}). (** total number of issued tickets is `n` *) (** total number of issued tickets is `n` *) Definition issuedTickets (γ : gname) (n : nat) := own γ (● GSet (seq_set 0 n)). Definition issuedTickets (γ : gname) (n : nat) := own γ (● GSet (seq_set 0 n)). (** the locks `(ln, lo)` and `l'` are linked together in the pool `γP` *) Definition inPool (γP : gname) (lo ln : loc) (γ : gname) (l' : loc) := own γP (◯ {[(lo, ln, γ), l']}). (** the set `P` is in fact the lock pool associated with `γP` *) Definition isPool (γP : gname) (P : lockPool) := own γP (● P). Lemma ticket_nondup γ n : ticket γ n -∗ ticket γ n -∗ False. Lemma ticket_nondup γ n : ticket γ n -∗ ticket γ n -∗ False. Proof. Proof. ... @@ -98,52 +94,12 @@ Section refinement. ... @@ -98,52 +94,12 @@ Section refinement. by iFrame. by iFrame. Qed. Qed. Instance inPool_persistent γP lo ln γ l' : Persistent (inPool γP lo ln γ l'). Proof. apply _. Qed. Lemma inPool_lookup γP lo ln γ l' P : inPool γP lo ln γ l' -∗ isPool γP P -∗ ⌜(lo, ln, γ, l') ∈ P⌝. Proof. iIntros "Hrs Ho". iDestruct (own_valid_2 with "Ho Hrs") as %Hfoo. iPureIntro. apply auth_valid_discrete in Hfoo. simpl in Hfoo. destruct Hfoo as [Hfoo _]. revert Hfoo. rewrite left_id. by rewrite gset_included elem_of_subseteq_singleton. Qed. Lemma isPool_insert γP lo ln γ l' P : isPool γP P ==∗ inPool γP lo ln γ l' ∗ isPool γP ({[(lo, ln, γ, l')]} ∪ P). Proof. iIntros "HP". iMod (own_update with "HP") as "[HP Hls]". { eapply auth_update_alloc. eapply (gset_local_update _ _ ({[(lo, ln, γ, l')]} ∪ P)). apply union_subseteq_r. } iFrame "HP". rewrite -gset_op_union. by iDestruct "Hls" as "[#Hls _]". Qed. Lemma newIsPool (P : lockPool) : (|==> ∃ γP, isPool γP P)%I. Proof. apply (own_alloc (● (P : lockPoolR))). by apply auth_auth_valid. Qed. Instance isPool_timeless γP P : Timeless (isPool γP P). Proof. apply _. Qed. Instance inPool_timeless γP lo ln γ l' : Timeless (inPool γP lo ln γ l'). Proof. apply _. Qed. Instance ticket_timeless γ n : Timeless (ticket γ n). Instance ticket_timeless γ n : Timeless (ticket γ n). Proof. apply _. Qed. Proof. apply _. Qed. Instance issuedTickets_timeless γ n : Timeless (issuedTickets γ n). Instance issuedTickets_timeless γ n : Timeless (issuedTickets γ n). Proof. apply _. Qed. Proof. apply _. Qed. Opaque ticket issuedTickets inPool isPool. Opaque ticket issuedTickets. (** * Invariants and abstracts for them *) (** * Invariants and abstracts for them *) Definition lockInv (lo ln : loc) (γ : gname) (l' : loc) : iProp Σ := Definition lockInv (lo ln : loc) (γ : gname) (l' : loc) : iProp Σ := ... @@ -156,84 +112,34 @@ Section refinement. ... @@ -156,84 +112,34 @@ Section refinement. Instance lockInv_timeless lo ln γ l' : Timeless (lockInv lo ln γ l'). Instance lockInv_timeless lo ln γ l' : Timeless (lockInv lo ln γ l'). Proof. apply _. Qed. Proof. apply _. Qed. Definition lockPoolInv (P : lockPool) : iProp Σ := Definition N := logrelN.@"locked". ([∗ set] rs ∈ P, match rs with | ((lo, ln, γ), l') => lockInv lo ln γ l' end)%I. Instance lockPoolInv_timeless P : Timeless (lockPoolInv P). Proof. apply big_sepS_timeless. intros [[[? ?] ?] ?]. apply _. Qed. Lemma lockPoolInv_empty : lockPoolInv ∅. Proof. by rewrite /lockPoolInv big_sepS_empty. Qed. Lemma lockPool_open γP (P : lockPool) (lo ln : loc) (γ : gname) (l' : loc) : isPool γP P -∗ inPool γP lo ln γ l' -∗ lockPoolInv P -∗ isPool γP P ∗ (lockInv lo ln γ l') ∗ (lockInv lo ln γ l' -∗ lockPoolInv P). Proof. iIntros "HP #Hin HPinv". iDestruct (inPool_lookup with "Hin HP") as %Hin. rewrite /lockPoolInv. iDestruct (big_sepS_elem_of_acc _ P _ with "HPinv") as "[Hrs Hreg]"; first apply Hin. by iFrame. Qed. Lemma lockPool_insert γP (P : lockPool) (lo ln : loc) γ l' : isPool γP P -∗ lockPoolInv P -∗ lockInv lo ln γ l' ==∗ isPool γP ({[(lo, ln, γ, l')]} ∪ P) ∗ lockPoolInv ({[(lo, ln, γ, l')]} ∪ P) ∗ inPool γP lo ln γ l'. Proof. iIntros "HP HPinv". iDestruct 1 as (n o b) "(Hlo & Hln & Hissued & Hl' & Hticket)". iMod (isPool_insert γP lo ln γ l' P with "HP") as "[\$ \$]". rewrite /lockInv. iAssert (⌜(lo, ln, γ, l') ∈ P⌝ → False)%I as %Hbaz. { iIntros (HP). rewrite /lockPoolInv. rewrite (big_sepS_elem_of _ P _ HP). iDestruct "HPinv" as (? ? ?) "(Hlo' & Hln' & ?)". iDestruct (mapsto_valid_2 with "Hlo' Hlo") as %Hfoo. compute in Hfoo; contradiction. } rewrite /lockPoolInv. rewrite big_sepS_insert; last assumption. iFrame. iExists _,_,_. by iFrame. Qed. Opaque lockPoolInv. Definition moduleInv γp : iProp Σ := (∃ (P : lockPool), isPool γp P ∗ lockPoolInv P)%I. Program Definition lockInt (γp : gname) := λ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'⌝ ∗ inPool γp lo ln γ l')%I. ∗ inv (N.@(lo,ln,l')) (lockInv lo ln γ l'))%I. Next Obligation. solve_proper. Qed. Next Obligation. solve_proper. Qed. Instance lockInt_persistent γp ww : Persistent (lockInt γp ww). (* 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). Proof. apply _. Qed. Proof. apply _. Qed. (** * Refinement proofs *) (** * Refinement proofs *) Definition N := logrelN.@"locked". Local Ltac openI N := iInv N as (P) ">[HP HPinv]" "Hcl". Local Ltac openI N := 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). (* Allocating a new lock *) (* Allocating a new lock *) Lemma newlock_refinement Δ Γ γp: Lemma newlock_refinement Δ Γ: inv N (moduleInv γp) -∗ {(lockInt:: Δ); ⤉Γ} ⊨ newlock ≤log≤ lock.newlock : (Unit → TVar 0). {(lockInt γp :: Δ); ⤉Γ} ⊨ newlock ≤log≤ lock.newlock : (Unit → TVar 0). Proof. Proof. iIntros "#Hinv". unlock newlock. unlock newlock. iApply bin_log_related_arrow_val; eauto. iApply bin_log_related_arrow_val; eauto. { by unlock lock.newlock. } { by unlock lock.newlock. } ... @@ -247,61 +153,52 @@ Section refinement. ... @@ -247,61 +153,52 @@ Section refinement. { solve_ndisj. } { solve_ndisj. } iIntros (l') "Hl'". iIntros (l') "Hl'". (* Establishing the invariant *) (* Establishing the invariant *) openI N. iMod newIssuedTickets as (γ) "Hγ". iMod newIssuedTickets as (γ) "Hγ". iMod (lockPool_insert _ _ lo ln with "HP HPinv [Hlo Hln Hl' Hγ]") as "(HP & HPinv & #Hin)". iMod (inv_alloc (N.@(lo,ln,l')) _ (lockInv lo ln γ l') with "[-]") as "#Hinv". { iExists _,_,_; by iFrame. } { iNext. iExists _,_,_. iFrame. } closeI. rel_vals. iModIntro. iAlways. rel_vals; iModIntro; iAlways. iExists _,_,_,_. iFrame "Hinv". eauto. iExists _,_,_,_. by iFrame "Hin". Qed. Qed. (* Acquiring a lock *) (* Acquiring a lock *) (* helper lemma *) (* helper lemma *) Lemma wait_loop_refinement Δ Γ γp (lo ln : loc) γ (l' : loc) (m : nat) : Lemma wait_loop_refinement Δ Γ (lo ln : loc) γ (l' : loc) (m : nat) : inv N (moduleInv γp) -∗ inv (N.@(lo,ln,l')) (lockInv lo ln γ l') -∗ inPool γp lo ln γ l' -∗ (* two locks are linked *) ticket γ m -∗ ticket γ m -∗ {(lockInt γp :: Δ); ⤉Γ} ⊨ {(lockInt :: Δ); ⤉Γ} ⊨ wait_loop #m (#lo, #ln) ≤log≤ lock.acquire #l' : TUnit. wait_loop #m (#lo, #ln) ≤log≤ lock.acquire #l' : TUnit. Proof. Proof. iIntros "#Hinv #Hin Hticket". iIntros "#Hinv Hticket". rel_rec_l. rel_rec_l. iLöb as "IH". iLöb as "IH". 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. openI (N.@(lo, ln, l')). iDestruct (lockPool_open with "HP Hin HPinv") as "(HP & Hls & HPinv)". rewrite {1}/lockInv. iDestruct "Hls" as (o n b) "(Hlo & Hln & Hissued & Hl' & Hrest)". iModIntro. iExists _; iFrame; iNext. iModIntro. iExists _; iFrame; iNext. iIntros "Hlo". iIntros "Hlo". rel_op_l. rel_op_l. case_decide; subst; rel_if_l. case_decide; subst; rel_if_l. (* Whether the ticket is called out *) (* Whether the ticket is called out *) - destruct b. - destruct b. { iDestruct (ticket_nondup with "Hticket Hrest") as %[]. } { iDestruct (ticket_nondup with "Hticket Hbticket") as %[]. } rel_apply_r (bin_log_related_acquire_r with "Hl'"). rel_apply_r (bin_log_related_acquire_r with "Hl'"). { solve_ndisj. } { solve_ndisj. } iIntros "Hl'". iIntros "Hl'". iSpecialize ("HPinv" with "[Hlo Hln Hl' Hissued Hticket]"). { iExists _,_,_. by iFrame. } closeI. closeI. iApply bin_log_related_unit. iApply bin_log_related_unit. - iMod ("Hcl" with "[-Hticket]") as "_". - iMod ("Hcl" with "[-Hticket]") as "_". { iNext. iExists P; iFrame. { iNext. iExists _,_,_; by iFrame. } iApply "HPinv". iExists _,_,_; by iFrame. } rel_rec_l. rel_rec_l. unlock wait_loop. simpl_subst/=. by iApply "IH". unlock wait_loop. simpl_subst/=. by iApply "IH". Qed. Qed. (** Logically atomic spec for `acquire`. (** Logically atomic spec for `acquire`. *) Parameter type: nat (* Parameter type: nat *) Precondition: (* Precondition: *) λo, ∃ n, lo ↦ᵢ o ∗ ln ↦ᵢ n ∗ issuedTickets γ n (* λo, ∃ n, lo ↦ᵢ o ∗ ln ↦ᵢ n ∗ issuedTickets γ n *) Postcondition: (* Postcondition: *) λo, ∃ n, lo ↦ᵢ o ∗ ln ↦ᵢ n ∗ issuedTickets γ n ∗ ticket γ o *) (* λo, ∃ n, lo ↦ᵢ o ∗ ln ↦ᵢ n ∗ issuedTickets γ n ∗ ticket γ o *) Lemma acquire_l_logatomic R P γ Δ Γ E1 E2 K lo ln t τ : Lemma acquire_l_logatomic R P γ Δ Γ E1 E2 K lo ln t τ : P -∗ P -∗ □ (|={E1,E2}=> ∃ o n : nat, lo ↦ᵢ #o ∗ ln ↦ᵢ #n ∗ issuedTickets γ n ∗ R o ∗ □ (|={E1,E2}=> ∃ o n : nat, lo ↦ᵢ #o ∗ ln ↦ᵢ #n ∗ issuedTickets γ n ∗ R o ∗ ... @@ -352,11 +249,9 @@ Section refinement. ... @@ -352,11 +249,9 @@ Section refinement. rel_rec_l. iApply ("IH" with "HP Hm"). rel_rec_l. iApply ("IH" with "HP Hm"). Qed. Qed. Lemma acquire_refinement Δ Γ γp : Lemma acquire_refinement Δ Γ : inv N (moduleInv γp) -∗ {lockInt :: Δ; ⤉Γ} ⊨ acquire ≤log≤ lock.acquire : (TVar 0 → Unit). {(lockInt γp :: Δ); ⤉Γ} ⊨ acquire ≤log≤ lock.acquire : (TVar 0 → Unit). Proof. Proof. iIntros "#Hinv". iApply bin_log_related_arrow_val; eauto. iApply bin_log_related_arrow_val; eauto. { by unlock acquire. } { by unlock acquire. } { by unlock lock.acquire. } { by unlock lock.acquire. } ... @@ -368,20 +263,16 @@ Section refinement. ... @@ -368,20 +263,16 @@ 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. openI (N.@(lo, ln, l')). iDestruct (lockPool_open with "HP Hin HPinv") as "(HP & Hls & HPinv)". rewrite {1}/lockInv. iDestruct "Hls" as (o n b) "(Hlo & Hln & Hissued & Hl' & Hticket)". iModIntro. iExists _,_; iFrame. iModIntro. iExists _,_; iFrame. iSplitL "Hticket Hl'". iSplitL "Hbticket Hl'". { iExists _. iFrame. } { iExists _. iFrame. } clear b o n. clear b o n. iSplit. iSplit. - iDestruct 1 as (o' n') "(Hlo & Hln & Hissued & Hrest)". - iDestruct 1 as (o' n') "(Hlo & Hln & Hissued & Hrest)". iDestruct "Hrest" as (b) "[Hl' Ht]". iDestruct "Hrest" as (b) "[Hl' Ht]". iApply ("Hcl" with "[-]"). iApply ("Hcl" with "[-]"). iNext. iExists P; iFrame. iNext. iExists _,_,_. by iFrame. iApply "HPinv". iExists _,_,_. by iFrame. - iIntros (o n) "(Hlo & Hln & Hissued & Ht & Hrest) _". - iIntros (o n) "(Hlo & Hln & Hissued & Ht & Hrest) _". iDestruct "Hrest" as (b) "[Hl' Ht']". iDestruct "Hrest" as (b) "[Hl' Ht']". destruct b. destruct b. ... @@ -390,40 +281,31 @@ Section refinement. ... @@ -390,40 +281,31 @@ Section refinement. { solve_ndisj. } { solve_ndisj. } iIntros "Hl'". iIntros "Hl'". iMod ("Hcl" with "[-]") as "_". iMod ("Hcl" with "[-]") as "_". { iNext. iExists P; iFrame. { iNext. iExists _,_,_; by iFrame. } iApply "HPinv". iExists _,_,_; by iFrame. } iApply bin_log_related_unit. iApply bin_log_related_unit. Qed. Qed. Lemma acquire_refinement_direct Δ Γ γp : Lemma acquire_refinement_direct Δ Γ : inv N (moduleInv γp) -∗ {(lockInt :: Δ); ⤉Γ} ⊨ acquire ≤log≤ lock.acquire : (TVar 0 → Unit). {(lockInt γp :: Δ); ⤉Γ} ⊨ acquire ≤log≤ lock.acquire : (TVar 0 → Unit). Proof. Proof. iIntros "#Hinv". unlock acquire; simpl. unlock acquire; simpl. iApply bin_log_related_arrow_val; eauto. iApply bin_log_related_arrow_val; eauto. { by unlock lock.acquire. } { by unlock lock.acquire. } iAlways. iIntros (? ?) "/= #Hl". iAlways. iIntros (? ?) "/= #Hl". iDestruct "Hl" as (lo ln γ l') "(% & % & Hin)". simplify_eq. iDestruct "Hl" as (lo ln γ l') "(% & % & Hin)". simplify_eq. rel_let_l. repeat rel_proj_l. rel_let_l. repeat rel_proj_l. (* rel_rec_l. (* TODO: cannot find the reduct *) *) 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. openI (N.@(lo, ln, l')). iDestruct (lockPool_open with "HP Hin HPinv") as "(HP & Hls & HPinv)". rewrite {1}/lockInv. iDestruct "Hls" as (o n b) "(Hlo & Hln & Hissued & Hl' & Hticket)". iModIntro. iExists _; iFrame. iModIntro. iExists _; iFrame. iSplit. iSplit. - iDestruct 1 as (m) "[Hln ?]". - iDestruct 1 as (m) "[Hln ?]". iApply ("Hcl" with "[-]"). iApply ("Hcl" with "[-]"). iNext. iExists P; iFrame. iNext. iExists _,_,_; by iFrame. iApply "HPinv". iExists _,_,_; by iFrame. - iIntros (m) "[Hln Hissued] _". - iIntros (m) "[Hln Hissued] _". iMod (issueNewTicket with "Hissued") as "[Hissued Hm]". iMod (issueNewTicket with "Hissued") as "[Hissued Hm]". iMod ("Hcl" with "[-Hm]") as "_". iMod ("Hcl" with "[-Hm]") as "_". { iNext. iExists P; iFrame. { iNext. iExists _,_,_; by iFrame. } iApply "HPinv". iExists _,_,_; by iFrame. } rel_let_l. rel_let_l. by iApply wait_loop_refinement. by iApply wait_loop_refinement. Qed. Qed. ... @@ -471,11 +353,9 @@ Section refinement. ... @@ -471,11 +353,9 @@ Section refinement. iExists _; iFrame. iExists _; iFrame. Qed. Qed. Lemma release_refinement Δ Γ γp : Lemma release_refinement Δ Γ : inv N (moduleInv γp) -∗ {(lockInt :: Δ); ⤉Γ} ⊨ release ≤log≤ lock.release : (TVar 0 → Unit). {(lockInt γp :: Δ); ⤉Γ} ⊨ release ≤log≤ lock.release : (TVar 0 → Unit). Proof. Proof. iIntros "#Hinv". unlock release. unlock release. iApply bin_log_related_arrow_val; eauto. iApply bin_log_related_arrow_val; eauto. { by unlock lock.release. } { by unlock lock.release. } ... @@ -488,19 +368,15 @@ Section refinement. ... @@ -488,19 +368,15 @@ 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. openI (N.@(lo, ln, l')). iDestruct (lockPool_open with "HP Hin HPinv") as "(HP & Hls & HPinv)". rewrite {1}/lockInv. iDestruct "Hls" as (o n b) "(Hlo & Hrest)". iModIntro. iExists _; iFrame. iModIntro. iExists _; iFrame. rewrite {1}/R. iSplitL "Hrest". rewrite {1}/R. iSplitR "Hcl". { iExists _,_; iFrame. } clear o n b. { iExists _,_; by iFrame. } clear o n b. iSplit. iSplit. - iDestruct 1 as (o) "[Hlo HR]". - iDestruct 1 as (o) "[Hlo HR]". unfold R. iDestruct "HR" as (n b) "HR". unfold R. iDestruct "HR" as (n b) "HR". iApply "Hcl". iApply "Hcl". iNext. iExists P; iFrame. iNext. iExists _,_,_; by iFrame. iApply "HPinv". iExists _,_,_; by iFrame. - iIntros (?) "[Hlo HR] _". - iIntros (?) "[Hlo HR] _". iDestruct "Hlo" as (o) "Hlo". iDestruct "Hlo" as (o) "Hlo". unfold R. iDestruct "HR" as (n b) "(Hln & Hissued & Hl' & Hticket)". unfold R. iDestruct "HR" as (n b) "(Hln & Hissued & Hl' & Hticket)". ... @@ -508,8 +384,7 @@ Section refinement. ... @@ -508,8 +384,7 @@ Section refinement. { solve_ndisj. } { solve_ndisj. } iIntros "Hl'". iIntros "Hl'". iMod ("Hcl" with "[-]") as "_". iMod ("Hcl" with "[-]") as "_". { iNext. iExists P; iFrame. { iNext. iExists _,_,_. by iFrame. } iApply "HPinv". iExists _,_,_. by iFrame. } iApply bin_log_related_unit. iApply bin_log_related_unit. Qed. Qed. ... @@ -519,13 +394,10 @@ Section refinement. ... @@ -519,13 +394,10 @@ Section refinement. Pack (lock.newlock, lock.acquire, lock.release) : lockT. Pack (lock.newlock, lock.acquire, lock.release) : lockT. Proof. Proof. iIntros (Δ). iIntros (Δ). iMod (newIsPool ∅) as (γp) "HP". iApply (bin_log_related_pack _ lockInt). iMod (inv_alloc N _ (moduleInv γp) with "[HP]") as "#Hinv". { iNext. iExists _; iFrame. iApply lockPoolInv_empty. } iApply (bin_log_related_pack _ (lockInt γp)). repeat iApply bin_log_related_pair. repeat iApply bin_log_related_pair. - by iApply newlock_refinement. - by iApply newlock_refinement. - by iApply acquire_refinement. - by iApply acquire_refinement_direct. - by iApply release_refinement. - by iApply release_refinement. Qed. Qed. ... ...
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!