Skip to content
Snippets Groups Projects
Commit 548a5de9 authored by Zhen Zhang's avatar Zhen Zhang
Browse files

use pair of ref in ticket lock

parent 59a8f5bf
No related branches found
No related tags found
No related merge requests found
......@@ -7,26 +7,27 @@ From iris.algebra Require Import gset.
Import uPred.
Definition wait_loop: val :=
rec: "wait_loop" "x" "l" :=
let: "o" := Fst !"l" in
rec: "wait_loop" "x" "lock" :=
let: "o" := !(Fst "lock") in
if: "x" = "o"
then #() (* my turn *)
else "wait_loop" "x" "l".
else "wait_loop" "x" "lock".
Definition newlock : val := λ: <>, ((* owner *) ref #0, (* next *) ref #0).
Definition newlock : val := λ: <>, ref((* owner *) #0, (* next *) #0).
Definition acquire : val :=
rec: "acquire" "l" :=
let: "oldl" := !"l" in
if: CAS "l" "oldl" (Fst "oldl", Snd "oldl" + #1)
then wait_loop (Snd "oldl") "l"
else "acquire" "l".
rec: "acquire" "lock" :=
let: "n" := !(Snd "lock") in
if: CAS (Snd "lock") "n" ("n" + #1)
then wait_loop "n" "lock"
else "acquire" "lock".
Definition release : val :=
rec: "release" "l" :=
let: "oldl" := !"l" in
if: CAS "l" "oldl" (Fst "oldl" + #1, Snd "oldl")
rec: "release" "lock" :=
let: "o" := !(Fst "lock") in
if: CAS (Fst "lock") "o" ("o" + #1)
then #()
else "release" "l".
else "release" "lock".
Global Opaque newlock acquire release wait_loop.
......@@ -42,28 +43,29 @@ Instance subG_tlockΣ {Σ} : subG tlockΣ Σ → tlockG Σ.
Proof. intros [? [?%subG_inG _]%subG_inv]%subG_inv. split; apply _. Qed.
Section proof.
Context `{!heapG Σ, !tlockG Σ} (N : namespace).
Context `{!heapG Σ, !tlockG Σ} (N : namespace) (HN: heapN N).
Definition tickets_inv (n: nat) (gs: gset_disjUR nat) : iProp Σ :=
(gs = GSet (seq_set 0 n))%I.
Definition lock_inv (γ1 γ2: gname) (l : loc) (R : iProp Σ) : iProp Σ :=
( o n: nat, l (#o, #n)
auth_inv γ1 (tickets_inv n)
((own γ2 (Excl ()) R) auth_own γ1 (GSet {[ o ]})))%I.
Definition lock_inv (γ1 γ2: gname) (lo ln: loc) (R : iProp Σ) : iProp Σ :=
( (o n: nat),
lo #o ln #n
auth_inv γ1 (tickets_inv n)
((own γ2 (Excl ()) R) auth_own γ1 (GSet {[ o ]})))%I.
Definition is_lock (l: loc) (R: iProp Σ) : iProp Σ :=
( γ1 γ2, heapN N heap_ctx inv N (lock_inv γ1 γ2 l R))%I.
Definition is_lock (l: val) (R: iProp Σ) : iProp Σ :=
( γ1 γ2 (lo ln: loc), heap_ctx l = (#lo, #ln)%V inv N (lock_inv γ1 γ2 lo ln R))%I.
Definition issued (l : loc) (x: nat) (R : iProp Σ) : iProp Σ :=
( γ1 γ2, heapN N heap_ctx inv N (lock_inv γ1 γ2 l R)
auth_own γ1 (GSet {[ x ]}))%I.
Definition issued (l : val) (x: nat) (R : iProp Σ) : iProp Σ :=
( γ1 γ2 (lo ln: loc), heap_ctx l = (#lo, #ln)%V inv N (lock_inv γ1 γ2 lo ln R)
auth_own γ1 (GSet {[ x ]}))%I.
Definition locked (l : loc) (R : iProp Σ) : iProp Σ :=
( γ1 γ2, heapN N heap_ctx inv N (lock_inv γ1 γ2 l R)
own γ2 (Excl ()))%I.
Definition locked (l : val) (R : iProp Σ) : iProp Σ :=
( γ1 γ2 (lo ln: loc), heap_ctx l = (#lo, #ln)%V inv N (lock_inv γ1 γ2 lo ln R)
own γ2 (Excl ()))%I.
Global Instance lock_inv_ne n γ1 γ2 l : Proper (dist n ==> dist n) (lock_inv γ1 γ2 l).
Global Instance lock_inv_ne n γ1 γ2 lo ln: Proper (dist n ==> dist n) (lock_inv γ1 γ2 lo ln).
Proof. solve_proper. Qed.
Global Instance is_lock_ne n l: Proper (dist n ==> dist n) (is_lock l).
Proof. solve_proper. Qed.
......@@ -74,14 +76,13 @@ Global Instance is_lock_persistent l R : PersistentP (is_lock l R).
Proof. apply _. Qed.
Lemma newlock_spec (R : iProp Σ) Φ :
heapN N
heap_ctx R ( l, is_lock l R -★ Φ #l) WP newlock #() {{ Φ }}.
heap_ctx R ( l, is_lock l R -★ Φ l) WP newlock #() {{ Φ }}.
Proof.
iIntros (?) "(#Hh & HR & HΦ)". rewrite /newlock.
wp_seq. wp_alloc l as "Hl".
iIntros "(#Hh & HR & HΦ)". rewrite /newlock.
wp_seq. wp_alloc lo as "Hlo". wp_alloc ln as "Hln".
iVs (own_alloc (Excl ())) as (γ2) "Hγ2"; first done.
iVs (own_alloc_strong (Auth (Excl' ) ) {[ γ2 ]}) as (γ1) "[% Hγ1]"; first done.
iVs (inv_alloc N _ (lock_inv γ1 γ2 l R) with "[-HΦ]").
iVs (inv_alloc N _ (lock_inv γ1 γ2 lo ln R) with "[-HΦ]").
{ iNext. rewrite /lock_inv.
iExists 0%nat, 0%nat.
iFrame.
......@@ -93,90 +94,90 @@ Proof.
by iFrame. }
iVsIntro.
iApply "HΦ".
iExists γ1, γ2.
iExists γ1, γ2, lo, ln.
iSplit; by auto.
Qed.
Lemma wait_loop_spec l x R (Φ : val iProp Σ) :
issued l x R ( l, locked l R -★ R -★ Φ #()) WP wait_loop #x #l {{ Φ }}.
issued l x R ( l, locked l R -★ R -★ Φ #()) WP wait_loop #x l {{ Φ }}.
Proof.
iIntros "[Hl HΦ]". iDestruct "Hl" as (γ1 γ2) "(% & #? & #? & Ht)".
iLöb as "IH". wp_rec. wp_let. wp_bind (! _)%E.
iInv N as (o n) "[Hl Ha]" "Hclose".
iIntros "[Hl HΦ]". iDestruct "Hl" as (γ1 γ2 lo ln) "(#? & % & #? & Ht)".
iLöb as "IH". wp_rec. subst. wp_let. wp_proj. wp_bind (! _)%E.
iInv N as (o n) "[Hlo [Hln Ha]]" "Hclose".
wp_load. destruct (decide (x = o)) as [->|Hneq].
- iDestruct "Ha" as "[Hainv [[Ho HR] | Haown]]".
+ iVs ("Hclose" with "[Hl Hainv Ht]").
+ iVs ("Hclose" with "[Hlo Hln Hainv Ht]").
{ iNext. iExists o, n. iFrame. eauto. }
iVsIntro. wp_proj. wp_let. wp_op=>[_|[]] //.
iVsIntro. wp_let. wp_op=>[_|[]] //.
wp_if. iVsIntro.
iApply ("HΦ" with "[-HR] HR"). iExists γ1, γ2; eauto.
iApply ("HΦ" with "[-HR] HR"). iExists γ1, γ2, lo, ln; eauto.
+ iExFalso. iCombine "Ht" "Haown" as "Haown".
iDestruct (auth_own_valid with "Haown") as % ?%gset_disj_valid_op.
set_solver.
- iVs ("Hclose" with "[Hl Ha]").
- iVs ("Hclose" with "[Hlo Hln Ha]").
{ iNext. iExists o, n. by iFrame. }
iVsIntro. wp_proj. wp_let. wp_op=>?; first omega.
iVsIntro. wp_let. wp_op=>?; first omega.
wp_if. by iApply ("IH" with "Ht").
Qed.
Lemma acquire_spec l R (Φ : val iProp Σ) :
is_lock l R ( l, locked l R -★ R -★ Φ #()) WP acquire #l {{ Φ }}.
is_lock l R ( l, locked l R -★ R -★ Φ #()) WP acquire l {{ Φ }}.
Proof.
iIntros "[Hl HΦ]". iDestruct "Hl" as (γ1 γ2) "(% & #? & #?)".
iLöb as "IH". wp_rec. wp_bind (! _)%E.
iInv N as (o n) "[Hl Ha]" "Hclose".
wp_load. iVs ("Hclose" with "[Hl Ha]").
iIntros "[Hl HΦ]". iDestruct "Hl" as (γ1 γ2 lo ln) "(#? & % & #?)".
iLöb as "IH". wp_rec. wp_bind (! _)%E. subst. wp_proj.
iInv N as (o n) "[Hlo [Hln Ha]]" "Hclose".
wp_load. iVs ("Hclose" with "[Hlo Hln Ha]").
{ iNext. iExists o, n. by iFrame. }
iVsIntro. wp_let. wp_proj. wp_proj. wp_op.
iVsIntro. wp_let. wp_proj. wp_op.
wp_bind (CAS _ _ _).
iInv N as (o' n') "[Hl [Hainv Haown]]" "Hclose".
destruct (decide ((#o', #n') = (#o, #n)))%V
as [[= ->%Nat2Z.inj ->%Nat2Z.inj] | Hneq].
iInv N as (o' n') "[Hlo' [Hln' [Hainv Haown]]]" "Hclose".
destruct (decide (#n' = #n))%V
as [[= ->%Nat2Z.inj] | Hneq].
- wp_cas_suc.
iDestruct "Hainv" as (s) "[Ho %]"; subst.
iVs (own_update with "Ho") as "Ho".
{ eapply auth_update_no_frag, (gset_alloc_empty_local_update n).
rewrite elem_of_seq_set; omega. }
iDestruct "Ho" as "[Hofull Hofrag]".
iVs ("Hclose" with "[Hl Haown Hofull]").
iVs ("Hclose" with "[Hlo' Hln' Haown Hofull]").
{ rewrite gset_disj_union; last by apply (seq_set_S_disjoint 0).
rewrite -(seq_set_S_union_L 0).
iNext. iExists o, (S n)%nat.
iNext. iExists o', (S n)%nat.
rewrite Nat2Z.inj_succ -Z.add_1_r.
iFrame. iExists (GSet (seq_set 0 (S n))). by iFrame. }
iVsIntro. wp_if. wp_proj.
iApply wait_loop_spec.
iVsIntro. wp_if.
iApply (wait_loop_spec (#lo, #ln)).
iSplitR "HΦ"; last by done.
rewrite /issued /auth_own; eauto 10.
- wp_cas_fail.
iVs ("Hclose" with "[Hl Hainv Haown]").
iVs ("Hclose" with "[Hlo' Hln' Hainv Haown]").
{ iNext. iExists o', n'. by iFrame. }
iVsIntro. wp_if. by iApply "IH".
Qed.
Lemma release_spec R l (Φ : val iProp Σ):
locked l R R Φ #() WP release #l {{ Φ }}.
locked l R R Φ #() WP release l {{ Φ }}.
Proof.
iIntros "(Hl & HR & HΦ)"; iDestruct "Hl" as (γ1 γ2) "(% & #? & #? & Hγ)".
iLöb as "IH". wp_rec. wp_bind (! _)%E.
iInv N as (o n) "[Hl Hr]" "Hclose".
wp_load. iVs ("Hclose" with "[Hl Hr]").
iIntros "(Hl & HR & HΦ)"; iDestruct "Hl" as (γ1 γ2 lo ln) "(#? & % & #? & Hγ)".
iLöb as "IH". wp_rec. subst. wp_proj. wp_bind (! _)%E.
iInv N as (o n) "[Hlo [Hln Hr]]" "Hclose".
wp_load. iVs ("Hclose" with "[Hlo Hln Hr]").
{ iNext. iExists o, n. by iFrame. }
iVsIntro. wp_let. wp_bind (CAS _ _ _ ).
wp_proj. wp_op. wp_proj.
iInv N as (o' n') "[Hl Hr]" "Hclose".
destruct (decide ((#o', #n') = (#o, #n)))%V
as [[= ->%Nat2Z.inj ->%Nat2Z.inj] | Hneq].
wp_proj. wp_op.
iInv N as (o' n') "[Hlo' [Hln' Hr]]" "Hclose".
destruct (decide (#o' = #o))%V
as [[= ->%Nat2Z.inj ] | Hneq].
- wp_cas_suc.
iDestruct "Hr" as "[Hainv [[Ho _] | Hown]]".
+ iExFalso. iCombine "Hγ" "Ho" as "Ho".
iDestruct (own_valid with "#Ho") as %[].
+ iVs ("Hclose" with "[Hl HR Hγ Hainv]").
{ iNext. iExists (o + 1)%nat, n%nat.
+ iVs ("Hclose" with "[Hlo' Hln' HR Hγ Hainv]").
{ iNext. iExists (o + 1)%nat, n'%nat.
iFrame. rewrite Nat2Z.inj_add.
iFrame. iLeft; by iFrame. }
iVsIntro. by wp_if.
- wp_cas_fail. iVs ("Hclose" with "[Hl Hr]").
- wp_cas_fail. iVs ("Hclose" with "[Hlo' Hln' Hr]").
{ iNext. iExists o', n'. by iFrame. }
iVsIntro. wp_if. by iApply ("IH" with "Hγ HR").
Qed.
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment