Commit eacc4197 authored by Zhen Zhang's avatar Zhen Zhang

Abstract lock interface

parent a1171d02
......@@ -97,6 +97,7 @@ heap_lang/lib/spawn.v
heap_lang/lib/par.v
heap_lang/lib/assert.v
heap_lang/lib/lock.v
heap_lang/lib/spin_lock.v
heap_lang/lib/ticket_lock.v
heap_lang/lib/counter.v
heap_lang/lib/barrier/barrier.v
......
From iris.program_logic Require Export weakestpre.
From iris.heap_lang Require Export lang.
From iris.proofmode Require Import invariants tactics.
From iris.heap_lang Require Import proofmode notation.
From iris.algebra Require Import excl.
(** 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 {{ Φ }}
}.
Arguments newlock {_ _} _.
Arguments acquire {_ _} _.
Arguments release {_ _} _.
Arguments is_lock {_ _} _ _ _ _ _.
Arguments locked {_ _} _ _.
Existing Instances is_lock_ne is_lock_persistent locked_timeless.
Instance is_lock_proper Σ `{!heapG Σ} (L: lock Σ) N lk R:
Proper (() ==> ()) (is_lock L N lk R) := ne_proper _.
Definition newlock : val := λ: <>, ref #false.
Definition acquire : val :=
rec: "acquire" "l" :=
if: CAS "l" #false #true then #() else "acquire" "l".
Definition release : val := λ: "l", "l" <- #false.
Global Opaque newlock acquire release.
(** The CMRA we need. *)
(* Not bundling heapG, as it may be shared with other users. *)
Class lockG Σ := LockG { lock_tokG :> inG Σ (exclR unitC) }.
Definition lockΣ : gFunctors := #[GFunctor (constRF (exclR unitC))].
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 (l : loc) (R : iProp Σ) : iProp Σ :=
( γ, heapN N heap_ctx inv N (lock_inv γ l R))%I.
Definition locked (l : loc) (R : iProp Σ) : iProp Σ :=
( γ, heapN N heap_ctx
inv N (lock_inv γ l R) own γ (Excl ()))%I.
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 l : Proper (dist n ==> dist n) (locked l).
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 l R : locked l R is_lock l R.
Proof. rewrite /is_lock. iDestruct 1 as (γ) "(?&?&?&_)"; eauto. Qed.
Lemma newlock_spec (R : iProp Σ) Φ :
heapN N
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".
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 γ; eauto.
Qed.
Lemma acquire_spec l R (Φ : val iProp Σ) :
is_lock l R (locked l R - R - Φ #()) WP acquire #l {{ Φ }}.
Proof.
iIntros "[Hl HΦ]". iDestruct "Hl" as (γ) "(%&#?&#?)".
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"). iExists γ; eauto.
Qed.
Lemma release_spec R l (Φ : val iProp Σ) :
locked l R R Φ #() WP release #l {{ Φ }}.
Proof.
iIntros "(Hl&HR&HΦ)"; iDestruct "Hl" as (γ) "(% & #? & #? & Hγ)".
rewrite /release /=. wp_let. iInv N as (b) "[Hl _]" "Hclose".
wp_store. iFrame "HΦ". iApply "Hclose". iNext. iExists false. by iFrame.
Qed.
End proof.
From iris.program_logic Require Export weakestpre.
From iris.heap_lang Require Export lang.
From iris.proofmode Require Import invariants tactics.
From iris.heap_lang Require Import proofmode notation.
From iris.algebra Require Import excl.
From iris.heap_lang.lib Require Import lock.
Definition newlock : val := λ: <>, ref #false.
Definition acquire : val :=
rec: "acquire" "l" :=
if: CAS "l" #false #true then #() else "acquire" "l".
Definition release : val := λ: "l", "l" <- #false.
Global Opaque newlock acquire release.
(** The CMRA we need. *)
(* Not bundling heapG, as it may be shared with other users. *)
Class lockG Σ := LockG { lock_tokG :> inG Σ (exclR unitC) }.
Definition lockΣ : gFunctors := #[GFunctor (constRF (exclR unitC))].
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.
End proof.
Definition spin_lock `{!heapG Σ, !lockG Σ} :=
Lock _ _ newlock acquire release gname is_lock locked _ _ _ locked_exclusive newlock_spec acquire_spec release_spec.
......@@ -4,6 +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.
Import uPred.
Definition wait_loop: val :=
......@@ -43,65 +44,70 @@ Instance subG_tlockΣ {Σ} : subG tlockΣ Σ → tlockG Σ.
Proof. intros [? [?%subG_inG _]%subG_inv]%subG_inv. split; apply _. Qed.
Section proof.
Context `{!heapG Σ, !tlockG Σ} (N : namespace) (HN: heapN N).
Context `{!heapG Σ, !tlockG Σ} (N : namespace).
Definition tickets_inv (n: nat) (gs: gset_disjUR nat) : iProp Σ :=
(gs = GSet (seq_set 0 n))%I.
Definition tickets_inv (n: nat) (gs: gset_disjUR nat) : iProp Σ :=
(gs = GSet (seq_set 0 n))%I.
Definition lock_inv (γ1 γ2: gname) (lo ln: loc) (R : iProp Σ) : iProp Σ :=
( (o n: nat),
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: 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 : 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 : 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 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.
Global Instance locked_ne n l: Proper (dist n ==> dist n) (locked l).
Proof. solve_proper. Qed.
Global Instance is_lock_persistent l R : PersistentP (is_lock l R).
Proof. apply _. Qed.
Lemma newlock_spec (R : iProp Σ) Φ :
heap_ctx R ( l, is_lock l R - Φ l) WP newlock #() {{ Φ }}.
Definition is_lock (γs: gname * gname) (l: val) (R: iProp Σ) : iProp Σ :=
( (lo ln: loc),
heapN N heap_ctx
l = (#lo, #ln)%V inv N (lock_inv (fst γs) (snd γs) lo ln R))%I.
Definition issued (γs: gname * gname) (l : val) (x: nat) (R : iProp Σ) : iProp Σ :=
( (lo ln: loc),
heapN N heap_ctx
l = (#lo, #ln)%V inv N (lock_inv (fst γs) (snd γs) lo ln R)
auth_own (fst γs) (GSet {[ x ]}))%I.
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).
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.
Global Instance is_lock_persistent γs l R : PersistentP (is_lock γs l R).
Proof. apply _. Qed.
Global Instance locked_timeless γs : TimelessP (locked γs).
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.
Lemma newlock_spec (R : iProp Σ) Φ :
heapN N heap_ctx R ( lk γs, is_lock γs lk R - Φ lk) WP newlock #() {{ Φ }}.
Proof.
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.
iVs (inv_alloc N _ (lock_inv γ1 γ2 lo ln R) with "[-HΦ]").
- iNext. rewrite /lock_inv.
iExists 0%nat, 0%nat.
iFrame.
iSplitL "Hγ1".
+ rewrite /auth_inv.
iExists (GSet ).
by iFrame.
+ iLeft. by iFrame.
- iVsIntro.
iSpecialize ("HΦ" $! (#lo, #ln)%V (γ1, γ2)). iApply "HΦ".
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 "(#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 lo ln R) with "[-HΦ]").
{ iNext. rewrite /lock_inv.
iExists 0%nat, 0%nat.
iFrame.
iSplitL "Hγ1".
{ rewrite /auth_inv.
iExists (GSet ).
by iFrame. }
iLeft.
by iFrame. }
iVsIntro.
iApply "HΦ".
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 {{ Φ }}.
Proof.
iIntros "[Hl HΦ]". iDestruct "Hl" as (γ1 γ2 lo ln) "(#? & % & #? & Ht)".
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].
......@@ -110,7 +116,7 @@ Proof.
{ iNext. iExists o, n. iFrame. eauto. }
iVsIntro. wp_let. wp_op=>[_|[]] //.
wp_if. iVsIntro.
iApply ("HΦ" with "[-HR] HR"). iExists γ1, γ2, lo, ln; eauto.
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.
......@@ -120,10 +126,10 @@ Proof.
wp_if. iApply ("IH" with "Ht"). by iExact "HΦ".
Qed.
Lemma acquire_spec l R (Φ : val iProp Σ) :
is_lock l R ( l, locked l R - R - Φ #()) WP acquire l {{ Φ }}.
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 (γ1 γ2 lo ln) "(#? & % & #?)".
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]").
......@@ -145,8 +151,8 @@ Proof.
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 (#lo, #ln)).
iSplitR "HΦ"; last by done.
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]").
......@@ -154,10 +160,10 @@ Proof.
iVsIntro. wp_if. by iApply "IH".
Qed.
Lemma release_spec R l (Φ : val iProp Σ):
locked l R R Φ #() WP release l {{ Φ }}.
Lemma release_spec γs l R (Φ : val iProp Σ):
is_lock γs l R locked γs R Φ #() WP release l {{ Φ }}.
Proof.
iIntros "(Hl & HR & HΦ)"; iDestruct "Hl" as (γ1 γ2 lo ln) "(#? & % & #? & Hγ)".
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]").
......@@ -182,3 +188,6 @@ 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.
Markdown is supported
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