Skip to content
Snippets Groups Projects
Commit 6edb53e7 authored by Robbert Krebbers's avatar Robbert Krebbers
Browse files

Some clean up/tweaks of locks.

parent 86672bca
No related branches found
No related tags found
No related merge requests found
Hide whitespace changes
Inline Side-by-side
heap_lang/lib/lock.v
+ 24
− 27
View file @ 6edb53e7
(** Abstract Lock Interface **)
From iris.heap_lang Require Import heap notation.
Structure lock Σ `{!heapG Σ} :=
Lock {
(* -- operations -- *)
newlock : val;
acquire : val;
release : val;
(* -- predicates -- *)
(* name is used to associate locked with is_lock *)
name: Type;
is_lock (N: namespace) (γ: name) (lock: val) (R: iProp Σ) : iProp Σ;
locked (γ: name) : iProp Σ;
(* -- general properties -- *)
is_lock_ne N γ lk n: Proper (dist n ==> dist n) (is_lock N γ lk);
is_lock_persistent N γ lk R : PersistentP (is_lock N γ lk R);
locked_timeless γ : TimelessP (locked γ);
locked_exclusive γ : locked γ ★ locked γ ⊢ False;
(* -- operation specs -- *)
newlock_spec N (R : iProp Σ) Φ :
heapN ⊥ N →
heap_ctx ★ R ★ (∀ l γ, is_lock N γ l R -★ Φ l) ⊢ WP newlock #() {{ Φ }};
acquire_spec N γ lk R (Φ : val → iProp Σ) :
is_lock N γ lk R ★ (locked γ -★ R -★ Φ #()) ⊢ WP acquire lk {{ Φ }};
release_spec N γ lk R (Φ : val → iProp Σ) :
is_lock N γ lk R ★ locked γ ★ R ★ Φ #() ⊢ WP release lk {{ Φ }}
}.
Structure lock Σ `{!heapG Σ} := Lock {
(* -- operations -- *)
newlock : val;
acquire : val;
release : val;
(* -- predicates -- *)
(* name is used to associate locked with is_lock *)
name : Type;
is_lock (N: namespace) (γ: name) (lock: val) (R: iProp Σ) : iProp Σ;
locked (γ: name) : iProp Σ;
(* -- general properties -- *)
is_lock_ne N γ lk n: Proper (dist n ==> dist n) (is_lock N γ lk);
is_lock_persistent N γ lk R : PersistentP (is_lock N γ lk R);
locked_timeless γ : TimelessP (locked γ);
locked_exclusive γ : locked γ ★ locked γ ⊢ False;
(* -- operation specs -- *)
newlock_spec N (R : iProp Σ) Φ :
heapN ⊥ N →
heap_ctx ★ R ★ (∀ l γ, is_lock N γ l R -★ Φ l) ⊢ WP newlock #() {{ Φ }};
acquire_spec N γ lk R (Φ : val → iProp Σ) :
is_lock N γ lk R ★ (locked γ -★ R -★ Φ #()) ⊢ WP acquire lk {{ Φ }};
release_spec N γ lk R (Φ : val → iProp Σ) :
is_lock N γ lk R ★ locked γ ★ R ★ Φ #() ⊢ WP release lk {{ Φ }}
}.
Arguments newlock {_ _} _.
Arguments acquire {_ _} _.
......
heap_lang/lib/spin_lock.v
+ 60
− 66
View file @ 6edb53e7
......@@ -21,71 +21,65 @@ Instance subG_lockΣ {Σ} : subG lockΣ Σ → lockG Σ.
Proof. intros [?%subG_inG _]%subG_inv. split; apply _. Qed.
Section proof.
Context `{!heapG Σ, !lockG Σ} (N : namespace).
Definition lock_inv (γ : gname) (l : loc) (R : iProp Σ) : iProp Σ :=
(∃ b : bool, l ↦ #b ★ if b then True else own γ (Excl ()) ★ R)%I.
Definition is_lock (γ: gname) (lk : val) (R : iProp Σ) : iProp Σ :=
(∃ (l: loc), heapN ⊥ N ∧ heap_ctx ∧ lk = #l ∧ inv N (lock_inv γ l R))%I.
Definition locked (γ: gname): iProp Σ := own γ (Excl ())%I.
Lemma locked_exclusive (γ: gname): (locked γ ★ locked γ ⊢ False)%I.
Proof.
iIntros "[Hl Hl']". iCombine "Hl" "Hl'" as "Hl". by iDestruct (own_valid with "Hl") as %[].
Qed.
Global Instance lock_inv_ne n γ l : Proper (dist n ==> dist n) (lock_inv γ l).
Proof. solve_proper. Qed.
Global Instance is_lock_ne n l : Proper (dist n ==> dist n) (is_lock γ l).
Proof. solve_proper. Qed.
(* Global Instance locked_ne n γ : Proper (dist n ==> dist n) (locked γ). *)
(* Proof. solve_proper. Qed. *)
(** The main proofs. *)
Global Instance is_lock_persistent γ l R : PersistentP (is_lock γ l R).
Proof. apply _. Qed.
(* Lemma locked_is_lock lk R : locked lk R ⊢ is_lock lk R. *)
(* Proof. rewrite /is_lock. iDestruct 1 as (γ l) "(?&?&?&?&_)". iExists γ, l. auto. Qed. *)
Global Instance locked_timeless γ : TimelessP (locked γ).
Proof. apply _. Qed.
Lemma newlock_spec (R : iProp Σ) Φ :
heapN ⊥ N →
heap_ctx ★ R ★ (∀ lk γ, is_lock γ lk R -★ Φ lk) ⊢ WP newlock #() {{ Φ }}.
Proof.
iIntros (?) "(#Hh & HR & HΦ)". rewrite /newlock.
wp_seq. wp_alloc l as "Hl".
iVs (own_alloc (Excl ())) as (γ) "Hγ"; first done.
iVs (inv_alloc N _ (lock_inv γ l R) with "[-HΦ]") as "#?".
{ iIntros "!>". iExists false. by iFrame. }
iVsIntro. iApply "HΦ". iExists l. eauto.
Qed.
Lemma acquire_spec γ lk R (Φ : val → iProp Σ) :
is_lock γ lk R ★ (locked γ -★ R -★ Φ #()) ⊢ WP acquire lk {{ Φ }}.
Proof.
iIntros "[Hl HΦ]". iDestruct "Hl" as (l) "(% & #? & % & #?)". subst.
iLöb as "IH". wp_rec. wp_bind (CAS _ _ _)%E.
iInv N as ([]) "[Hl HR]" "Hclose".
- wp_cas_fail. iVs ("Hclose" with "[Hl]"); first (iNext; iExists true; eauto).
iVsIntro. wp_if. by iApply "IH".
- wp_cas_suc. iDestruct "HR" as "[Hγ HR]".
iVs ("Hclose" with "[Hl]"); first (iNext; iExists true; eauto).
iVsIntro. wp_if. iApply ("HΦ" with "[-HR] HR"). by iFrame.
Qed.
Lemma release_spec γ lk R (Φ : val → iProp Σ) :
is_lock γ lk R ★ locked γ ★ R ★ Φ #() ⊢ WP release lk {{ Φ }}.
Proof.
iIntros "(Hlock & Hlocked & HR & HΦ)". iDestruct "Hlock" as (l) "(% & #? & % & #?)". subst.
rewrite /release. wp_let. iInv N as (b) "[Hl _]" "Hclose".
wp_store. iFrame "HΦ". iApply "Hclose". iNext. iExists false. by iFrame.
Qed.
Context `{!heapG Σ, !lockG Σ} (N : namespace).
Definition lock_inv (γ : gname) (l : loc) (R : iProp Σ) : iProp Σ :=
(∃ b : bool, l ↦ #b ★ if b then True else own γ (Excl ()) ★ R)%I.
Definition is_lock (γ : gname) (lk : val) (R : iProp Σ) : iProp Σ :=
(∃ l: loc, heapN ⊥ N ∧ heap_ctx ∧ lk = #l ∧ inv N (lock_inv γ l R))%I.
Definition locked (γ : gname): iProp Σ := own γ (Excl ()).
Lemma locked_exclusive (γ : gname) : locked γ ★ locked γ ⊢ False.
Proof. rewrite /locked -own_op own_valid. by iIntros (?). Qed.
Global Instance lock_inv_ne n γ l : Proper (dist n ==> dist n) (lock_inv γ l).
Proof. solve_proper. Qed.
Global Instance is_lock_ne n l : Proper (dist n ==> dist n) (is_lock γ l).
Proof. solve_proper. Qed.
(** The main proofs. *)
Global Instance is_lock_persistent γ l R : PersistentP (is_lock γ l R).
Proof. apply _. Qed.
Global Instance locked_timeless γ : TimelessP (locked γ).
Proof. apply _. Qed.
Lemma newlock_spec (R : iProp Σ) Φ :
heapN ⊥ N →
heap_ctx ★ R ★ (∀ lk γ, is_lock γ lk R -★ Φ lk) ⊢ WP newlock #() {{ Φ }}.
Proof.
iIntros (?) "(#Hh & HR & HΦ)". rewrite /newlock /=.
wp_seq. wp_alloc l as "Hl".
iVs (own_alloc (Excl ())) as (γ) "Hγ"; first done.
iVs (inv_alloc N _ (lock_inv γ l R) with "[-HΦ]") as "#?".
{ iIntros "!>". iExists false. by iFrame. }
iVsIntro. iApply "HΦ". iExists l. eauto.
Qed.
Lemma acquire_spec γ lk R (Φ : val → iProp Σ) :
is_lock γ lk R ★ (locked γ -★ R -★ Φ #()) ⊢ WP acquire lk {{ Φ }}.
Proof.
iIntros "[Hl HΦ]". iDestruct "Hl" as (l) "(% & #? & % & #?)". subst.
iLöb as "IH". wp_rec. wp_bind (CAS _ _ _)%E.
iInv N as ([]) "[Hl HR]" "Hclose".
- wp_cas_fail. iVs ("Hclose" with "[Hl]"); first (iNext; iExists true; eauto).
iVsIntro. wp_if. by iApply "IH".
- wp_cas_suc. iDestruct "HR" as "[Hγ HR]".
iVs ("Hclose" with "[Hl]"); first (iNext; iExists true; eauto).
iVsIntro. wp_if. iApply ("HΦ" with "[-HR] HR"). by iFrame.
Qed.
Lemma release_spec γ lk R (Φ : val → iProp Σ) :
is_lock γ lk R ★ locked γ ★ R ★ Φ #() ⊢ WP release lk {{ Φ }}.
Proof.
iIntros "(Hlock & Hlocked & HR & HΦ)".
iDestruct "Hlock" as (l) "(% & #? & % & #?)". subst.
rewrite /release /=. wp_let. iInv N as (b) "[Hl _]" "Hclose".
wp_store. iFrame "HΦ". iApply "Hclose". iNext. iExists false. by iFrame.
Qed.
End proof.
Definition spin_lock `{!heapG Σ, !lockG Σ} :=
Lock _ _ newlock acquire release gname is_lock locked _ _ _ locked_exclusive newlock_spec acquire_spec release_spec.
Definition spin_lock `{!heapG Σ, !lockG Σ} : lock Σ :=
{| lock.locked_exclusive := locked_exclusive; lock.newlock_spec := newlock_spec;
lock.acquire_spec := acquire_spec; lock.release_spec := release_spec |}.
heap_lang/lib/ticket_lock.v
+ 92
− 91
View file @ 6edb53e7
......@@ -4,7 +4,7 @@ From iris.program_logic Require Import auth.
From iris.proofmode Require Import invariants.
From iris.heap_lang Require Import proofmode notation.
From iris.algebra Require Import gset.
From iris.heap_lang.lib Require Import lock.
From iris.heap_lang.lib Require Export lock.
Import uPred.
Definition wait_loop: val :=
......@@ -53,7 +53,7 @@ Section proof.
(∃ (o n: nat),
lo ↦ #o ★ ln ↦ #n ★
auth_inv γ1 (tickets_inv n) ★
((own γ2 (Excl ()) ★ R) ∨ auth_own γ1 (GSet {[ o ]})))%I.
((own γ2 (Excl ()) ★ R) ∨ auth_own γ1 (GSet {[ o ]})))%I.
Definition is_lock (γs: gname * gname) (l: val) (R: iProp Σ) : iProp Σ :=
(∃ (lo ln: loc),
......@@ -68,7 +68,8 @@ Section proof.
Definition locked (γs: gname * gname) : iProp Σ := own (snd γs) (Excl ())%I.
Global Instance lock_inv_ne n γ1 γ2 lo ln : Proper (dist n ==> dist n) (lock_inv γ1 γ2 lo ln).
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 γs n l : Proper (dist n ==> dist n) (is_lock γs l).
Proof. solve_proper. Qed.
......@@ -78,14 +79,13 @@ Section proof.
Proof. apply _. Qed.
Lemma locked_exclusive (γs: gname * gname) : (locked γs ★ locked γs ⊢ False)%I.
Proof.
iIntros "[Hl Hl']". iCombine "Hl" "Hl'" as "Hl". by iDestruct (own_valid with "Hl") as %[].
Qed.
Proof. rewrite /locked -own_op own_valid. by iIntros (?). Qed.
Lemma newlock_spec (R : iProp Σ) Φ :
heapN ⊥ N → heap_ctx ★ R ★ (∀ lk γs, is_lock γs lk R -★ Φ lk) ⊢ WP newlock #() {{ Φ }}.
heapN ⊥ N →
heap_ctx ★ R ★ (∀ lk γs, is_lock γs lk R -★ Φ lk) ⊢ WP newlock #() {{ Φ }}.
Proof.
iIntros (HN) "(#Hh & HR & HΦ)". rewrite /newlock.
iIntros (HN) "(#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.
......@@ -99,95 +99,96 @@ Section proof.
by iFrame.
+ iLeft. by iFrame.
- iVsIntro.
iSpecialize ("HΦ" $! (#lo, #ln)%V (γ1, γ2)). iApply "HΦ".
iApply ("HΦ" $! (#lo, #ln)%V (γ1, γ2)).
iExists lo, ln.
iSplit; by eauto.
Qed.
Lemma wait_loop_spec γs l x R (Φ : val → iProp Σ) :
issued γs l x R ★ (locked γs -★ R -★ Φ #()) ⊢ WP wait_loop #x l {{ Φ }}.
Proof.
iIntros "[Hl HΦ]". iDestruct "Hl" as (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 "[Hlo Hln Hainv Ht]").
{ iNext. iExists o, n. iFrame. eauto. }
iVsIntro. wp_let. wp_op=>[_|[]] //.
wp_if. iVsIntro.
iApply ("HΦ" with "[-HR] HR"). eauto.
+ iExFalso. iCombine "Ht" "Haown" as "Haown".
iDestruct (auth_own_valid with "Haown") as % ?%gset_disj_valid_op.
set_solver.
- iVs ("Hclose" with "[Hlo Hln Ha]").
Lemma wait_loop_spec γs l x R (Φ : val → iProp Σ) :
issued γs l x R ★ (locked γs -★ R -★ Φ #()) ⊢ WP wait_loop #x l {{ Φ }}.
Proof.
iIntros "[Hl HΦ]". iDestruct "Hl" as (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 "[Hlo Hln Hainv Ht]").
{ iNext. iExists o, n. iFrame. eauto. }
iVsIntro. wp_let. wp_op=>[_|[]] //.
wp_if. iVsIntro.
iApply ("HΦ" with "[-HR] HR"). eauto.
+ iExFalso. iCombine "Ht" "Haown" as "Haown".
iDestruct (auth_own_valid with "Haown") as % ?%gset_disj_valid_op.
set_solver.
- iVs ("Hclose" with "[Hlo Hln Ha]").
{ iNext. iExists o, n. by iFrame. }
iVsIntro. wp_let. wp_op=>[[/Nat2Z.inj //]|?].
wp_if. iApply ("IH" with "Ht"). by iExact "HΦ".
Qed.
Lemma acquire_spec γs l R (Φ : val → iProp Σ) :
is_lock γs l R ★ (locked γs -★ R -★ Φ #()) ⊢ WP acquire l {{ Φ }}.
Proof.
iIntros "[Hl HΦ]". iDestruct "Hl" as (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_op=>[[/Nat2Z.inj //]|?].
wp_if. iApply ("IH" with "Ht"). by iExact "HΦ".
Qed.
Lemma acquire_spec γs l R (Φ : val → iProp Σ) :
is_lock γs l R ★ (locked γs -★ R -★ Φ #()) ⊢ WP acquire l {{ Φ }}.
Proof.
iIntros "[Hl HΦ]". iDestruct "Hl" as (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_op.
wp_bind (CAS _ _ _).
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 "[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.
rewrite Nat2Z.inj_succ -Z.add_1_r.
iFrame. iExists (GSet (seq_set 0 (S n))). by iFrame. }
iVsIntro. wp_if.
iApply (wait_loop_spec γs (#lo, #ln)).
iSplitR "HΦ"; last by auto.
rewrite /issued /auth_own; eauto 10.
- wp_cas_fail.
iVs ("Hclose" with "[Hlo' Hln' Hainv Haown]").
{ iNext. iExists o', n'. by iFrame. }
iVsIntro. wp_if. by iApply "IH".
Qed.
Lemma release_spec γs l R (Φ : val → iProp Σ):
is_lock γs l R ★ locked γs ★ R ★ Φ #() ⊢ WP release l {{ Φ }}.
Proof.
iIntros "(Hl & Hγ & HR & HΦ)". iDestruct "Hl" as (lo ln) "(% & #? & % & #?)".
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.
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 "[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 "[Hlo' Hln' Hr]").
{ iNext. iExists o', n'. by iFrame. }
iVsIntro. wp_if. by iApply ("IH" with "Hγ HR").
Qed.
iVsIntro. wp_let. wp_proj. wp_op.
wp_bind (CAS _ _ _).
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 "[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.
rewrite Nat2Z.inj_succ -Z.add_1_r.
iFrame. iExists (GSet (seq_set 0 (S n))). by iFrame. }
iVsIntro. wp_if.
iApply (wait_loop_spec γs (#lo, #ln)).
iSplitR "HΦ"; last by auto.
rewrite /issued /auth_own; eauto 10.
- wp_cas_fail.
iVs ("Hclose" with "[Hlo' Hln' Hainv Haown]").
{ iNext. iExists o', n'. by iFrame. }
iVsIntro. wp_if. by iApply "IH".
Qed.
Lemma release_spec γs l R (Φ : val → iProp Σ):
is_lock γs l R ★ locked γs ★ R ★ Φ #() ⊢ WP release l {{ Φ }}.
Proof.
iIntros "(Hl & Hγ & HR & HΦ)". iDestruct "Hl" as (lo ln) "(% & #? & % & #?)".
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.
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 "[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 "[Hlo' Hln' Hr]").
{ iNext. iExists o', n'. by iFrame. }
iVsIntro. wp_if. by iApply ("IH" with "Hγ HR").
Qed.
End proof.
Typeclasses Opaque is_lock issued locked.
Definition ticket_lock `{!heapG Σ, !tlockG Σ} :=
Lock _ _ newlock acquire release (gname * gname) is_lock locked _ _ _ locked_exclusive newlock_spec acquire_spec release_spec.
Definition ticket_lock `{!heapG Σ, !tlockG Σ} : lock Σ :=
{| lock.locked_exclusive := locked_exclusive; lock.newlock_spec := newlock_spec;
lock.acquire_spec := acquire_spec; lock.release_spec := release_spec |}.
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment