Commit ee272509 authored by Dan Frumin's avatar Dan Frumin

Ticket lock refinement using the log.atomic rule for counter incr

parent be63cb7e
From iris.proofmode Require Import tactics.
From iris.algebra Require Export auth gset excl.
From iris.base_logic Require Import auth.
From iris_logrel Require Export logrel examples.lock.
From iris_logrel Require Export logrel examples.lock examples.counter.
Definition wait_loop: val :=
rec: "wait_loop" "x" "lk" :=
......@@ -12,12 +12,9 @@ Definition wait_loop: val :=
Definition newlock : val :=
λ: <>, ((* owner *) ref #0, (* next *) ref #0).
Definition acquire : val :=
rec: "acquire" "lk" :=
let: "n" := !(Snd "lk") in
if: CAS (Snd "lk") "n" ("n" + #1)
then wait_loop "n" "lk"
else "acquire" "lk".
Definition acquire : val := λ: "lk",
let: "n" := FG_increment (Snd "lk") #() in
wait_loop "n" "lk".
Definition release : val :=
λ: "lk", (Fst "lk") <- !(Fst "lk") + #1.
......@@ -32,7 +29,13 @@ Proof. solve_typed. Qed.
Hint Resolve newlock_type : typeable.
Lemma acquire_type Γ : typed Γ acquire (LockType TUnit).
Proof. unlock acquire wait_loop. solve_typed. Qed.
Proof.
unlock acquire wait_loop.
econstructor; cbn; solve_typed.
econstructor; cbn; solve_typed.
econstructor; cbn; solve_typed.
econstructor; cbn; solve_typed.
Qed.
Hint Resolve acquire_type : typeable.
......@@ -41,8 +44,8 @@ Proof. solve_typed. Qed.
Hint Resolve release_type : typeable.
Definition lockτ : type := : (Unit TVar 0) × (TVar 0 Unit) × (TVar 0 Unit).
Lemma ticket_lock_typed Γ : typed Γ (Pack (newlock, acquire, release)) lockτ.
Definition lockT : type := : (Unit TVar 0) × (TVar 0 Unit) × (TVar 0 Unit).
Lemma ticket_lock_typed Γ : typed Γ (Pack (newlock, acquire, release)) lockT.
Proof.
apply TPack with LockType.
asimpl. solve_typed.
......@@ -124,151 +127,181 @@ Section refinement.
iPureIntro. eauto.
Qed.
Definition N := logrelN.@"locked".
(* Allocating a new lock *)
Lemma newlock_refinement Δ Γ γp:
inv N (moduleInv γp) -
{(lockInt γp :: Δ); ⤉Γ} newlock log lock.newlock : (Unit TVar 0).
Proof.
iIntros "#Hinv".
unlock newlock.
iApply bin_log_related_arrow_val; eauto.
{ by unlock lock.newlock. }
iAlways. iIntros (? ?) "/= [% %]"; simplify_eq.
rel_let_l.
rel_alloc_l as lo "Hlo".
rel_apply_r bin_log_related_newlock_r.
{ solve_ndisj. }
iIntros (l') "Hl'".
rel_alloc_l_atomic.
iInv N as (P) "[>HP Hpool]" "Hcl".
iModIntro. iNext.
iIntros (ln) "Hln".
iMod (own_alloc ( (GSet ) (GSet ))) as (γ) "[Hγ Hγ']".
{ by rewrite -auth_both_op. }
iMod (own_update with "HP") as "[HP Hls]".
{ eapply auth_update_alloc.
eapply (gset_local_update _ _ ({[(lo, ln, γ, l')]} P)).
apply union_subseteq_r. }
iDestruct (lockPool_excl _ lo ln γ l' with "Hpool Hlo") as %Hnew.
iMod ("Hcl" with "[-Hls]") as "_".
{ iNext. iExists _; iFrame.
rewrite /lockPoolInv.
rewrite big_sepS_insert; last assumption.
iFrame. iExists _,_,_. iFrame. simpl. iFrame. }
rel_vals. iModIntro.
rewrite -gset_op_union.
iDestruct "Hls" as "[#Hls _]".
iAlways. iExists _,_,_,_. iFrame "Hls". eauto.
Qed.
(* Acquiring a lock *)
Lemma wait_loop_refinement Δ Γ γp (lo ln : loc) γ (l' : loc) (m : nat) :
inv N (moduleInv γp) -
own γp ( {[(lo, ln), γ, l']}) - (* two locks are linked *)
own γ ( GSet {[m]}) - (* the ticket *)
{(lockInt γp :: Δ); ⤉Γ}
wait_loop #m (#lo, #ln) log lock.acquire #l' : TUnit.
Proof.
iIntros "#Hinv #Hls Hticket".
unlock wait_loop.
rel_rec_l.
iLöb as "IH".
rel_let_l. rel_proj_l.
rel_load_l_atomic.
iInv N as (P) "[>HP Hpool]" "Hcl".
iDestruct (lockPool_lookup with "HP Hls") as %Hls.
iDestruct (lockPool_open_later with "Hpool") as "[Hlk Hpool]"; first apply Hls.
rewrite {1}/lockInv.
iDestruct "Hlk" as (o n' b) "(>Hlo & >Hln & Hseq & Hl' & Hrest)".
iModIntro. iExists _; iFrame; iNext.
iIntros "Hlo".
rel_op_l.
case_decide; subst; rel_if_l.
(* Whether the ticket is called out *)
- destruct b.
{ iDestruct (own_valid_2 with "Hticket Hrest") as %?%gset_disj_valid_op.
set_solver. }
rel_apply_r (bin_log_related_acquire_r with "Hl'").
{ solve_ndisj. }
iIntros "Hl'".
iMod ("Hcl" with "[-]") as "_".
{ iNext. iExists P; iFrame.
iApply "Hpool". iExists _,_,_; iFrame. }
iApply bin_log_related_unit.
- iMod ("Hcl" with "[-Hticket]") as "_".
{ iNext. iExists P; iFrame.
iApply "Hpool". iExists _,_,_; by iFrame. }
rel_rec_l.
by iApply "IH".
Qed.
Lemma acquire_refinement Δ Γ γp :
inv N (moduleInv γp) -
{(lockInt γp :: Δ); ⤉Γ} acquire log lock.acquire : (TVar 0 Unit).
Proof.
iIntros "#Hinv".
unlock acquire; simpl.
iApply bin_log_related_arrow_val; eauto.
{ by unlock lock.acquire. }
iAlways. iIntros (? ?) "/= #Hl".
iDestruct "Hl" as (lo ln γ l') "(% & % & Hls)". simplify_eq.
rel_let_l. repeat rel_proj_l.
(* rel_rec_l. (* TODO: cannot find the reduct *) *)
rel_bind_l (FG_increment _ #()).
rel_rec_l.
rel_apply_l (bin_log_FG_increment_logatomic _ (fun n => own γ ( GSet (seq_set 0 n)))%I True%I); first done.
iAlways.
iInv N as (P) "[>HP Hpool]" "Hcl".
iDestruct (lockPool_lookup with "HP Hls") as %Hls.
iDestruct (lockPool_open_later with "Hpool") as "[Hlk Hpool]"; first apply Hls.
rewrite {1}/lockInv.
iDestruct "Hlk" as (o n b) "(>Hlo & >Hln & >Hseq & Hl' & Hrest)".
iModIntro. iExists _; iFrame.
iSplit.
- iDestruct 1 as (m) "[Hln ?]".
iApply ("Hcl" with "[-]").
iNext. iExists P; iFrame.
iApply "Hpool". iExists _,_,_; by iFrame.
- iIntros (m) "[Hln Hseq] _".
iMod (own_update with "Hseq") as "[Hseq Hticket]".
{ eapply auth_update_alloc.
eapply (gset_disj_alloc_empty_local_update _ {[ m ]}).
apply (seq_set_S_disjoint 0). }
rewrite -(seq_set_S_union_L 0).
iMod ("Hcl" with "[-Hticket]") as "_".
{ iNext. iExists P; iFrame.
iApply "Hpool". iExists _,_,_; by iFrame. }
simpl. rel_let_l.
by iApply wait_loop_refinement.
Qed.
(* Releasing the lock *)
Lemma release_refinement Δ Γ γp :
inv N (moduleInv γp) -
{(lockInt γp :: Δ); ⤉Γ} release log lock.release : (TVar 0 Unit).
Proof.
iIntros "#Hinv".
unlock release.
iApply bin_log_related_arrow_val; eauto.
{ by unlock lock.release. }
iAlways. iIntros (? ?) "/= #Hl".
iDestruct "Hl" as (lo ln γ l') "(% & % & Hls)". simplify_eq.
rel_let_l. repeat rel_proj_l.
rel_load_l_atomic.
iInv N as (P) "[>HP Hpool]" "Hcl".
iDestruct (lockPool_lookup with "HP Hls") as %Hls.
iDestruct (lockPool_open_later with "Hpool") as "[Hlk Hpool]"; first apply Hls.
rewrite {1}/lockInv.
iDestruct "Hlk" as (o n b) "(>Hlo & >Hln & ?)".
iModIntro. iExists _; iFrame; iNext.
iIntros "Hlo".
iMod ("Hcl" with "[-]") as "_".
{ iNext. iExists P; iFrame.
iApply "Hpool". iExists _,_,_; iFrame. }
rel_op_l.
rel_store_l_atomic. clear Hls n b P.
iInv N as (P) "[>HP Hpool]" "Hcl".
iDestruct (lockPool_lookup with "HP Hls") as %Hls.
iDestruct (lockPool_open_later with "Hpool") as "[Hlk Hpool]"; first apply Hls.
rewrite {1}/lockInv.
iDestruct "Hlk" as (o' n b) "(>Hlo & >Hln & Hseq & Hl' & Hrest)".
iModIntro. iExists _; iFrame; iNext.
iIntros "Hlo".
rel_apply_r (bin_log_related_release_r with "Hl'").
{ solve_ndisj. }
iIntros "Hl'".
iMod ("Hcl" with "[-]") as "_".
{ iNext. iExists P; iFrame.
iApply "Hpool". iExists _,_,_. by iFrame. }
iApply bin_log_related_unit.
Qed.
Lemma ticket_lock_refinement Γ :
Γ Pack (newlock, acquire, release)
log
Pack (lock.newlock, lock.acquire, lock.release) : lockτ.
Pack (lock.newlock, lock.acquire, lock.release) : lockT.
Proof.
iIntros (Δ).
pose (N:=logrelN.@"locked").
iMod (own_alloc ( ( : lockPoolR))) as (γp) "HP"; first done.
iMod (inv_alloc N _ (moduleInv γp) with "[HP]") as "#Hinv".
{ iNext. iExists . iFrame. by rewrite /lockPoolInv big_sepS_empty. }
iApply (bin_log_related_pack _ (lockInt γp)).
repeat iApply bin_log_related_pair.
- (* Allocating a new lock *)
unlock newlock lock.newlock.
iApply bin_log_related_arrow_val; eauto.
iAlways. iIntros (? ?) "/= [% %]"; simplify_eq.
rel_let_l. rel_let_r.
rel_alloc_r as l' "Hl'".
rel_alloc_l as lo "Hlo".
rel_alloc_l_atomic.
iInv N as (P) "[>HP Hpool]" "Hcl".
iModIntro. iNext.
iIntros (ln) "Hln".
iMod (own_alloc ( (GSet ) (GSet ))) as (γ) "[Hγ Hγ']".
{ by rewrite -auth_both_op. }
iMod (own_update with "HP") as "[HP Hls]".
{ eapply auth_update_alloc.
eapply (gset_local_update _ _ ({[(lo, ln, γ, l')]} P)).
apply union_subseteq_r. }
iDestruct (lockPool_excl _ lo ln γ l' with "Hpool Hlo") as %Hnew.
iMod ("Hcl" with "[-Hls]") as "_".
{ iNext. iExists _; iFrame.
rewrite /lockPoolInv.
rewrite big_sepS_insert; last assumption.
iFrame. iExists _,_,_. iFrame. simpl. iFrame. }
rel_vals. iModIntro.
rewrite -gset_op_union.
iDestruct "Hls" as "[#Hls _]".
iAlways. iExists _,_,_,_. iFrame "Hls". eauto.
- (* Acquire *)
unlock acquire.
iApply bin_log_related_arrow_val; eauto.
{ by unlock lock.acquire. }
iAlways. iIntros (? ?) "/= #Hl".
iDestruct "Hl" as (lo ln γ l') "(% & % & Hls)". simplify_eq.
iLöb as "IH".
rel_let_l. repeat rel_proj_l.
rel_load_l_atomic.
iInv N as (P) "[>HP Hpool]" "Hcl".
iDestruct (lockPool_lookup with "HP Hls") as %Hls.
iDestruct (lockPool_open_later with "Hpool") as "[Hlk Hpool]"; first apply Hls.
rewrite {1}/lockInv.
iDestruct "Hlk" as (o n b) "(>Hlo & >Hln & ?)".
iModIntro. iExists _; iFrame; iNext.
iIntros "Hln".
iMod ("Hcl" with "[-]") as "_".
{ iNext. iExists P; iFrame.
iApply "Hpool". iExists _,_,_; iFrame. }
rel_let_l. rel_proj_l. rel_op_l.
clear Hls o b P.
rel_cas_l_atomic.
iInv N as (P) "[>HP Hpool]" "Hcl".
iDestruct (lockPool_lookup with "HP Hls") as %Hls.
iDestruct (lockPool_open_later with "Hpool") as "[Hlk Hpool]"; first apply Hls.
rewrite {1}/lockInv.
iDestruct "Hlk" as (o n' b) "(>Hlo & >Hln & Hseq & Hl' & Hrest)".
iModIntro. iExists _; iFrame.
iSplit; iIntros (?); iNext; iIntros "Hln"; rel_if_l.
+ iMod ("Hcl" with "[-]") as "_".
{ iNext. iExists P; iFrame.
iApply "Hpool". iExists _,_,_; by iFrame. }
iApply "IH".
+ simplify_eq.
iMod (own_update with "Hseq") as "[Hseq Hticket]".
{ eapply auth_update_alloc.
eapply (gset_disj_alloc_empty_local_update _ {[ n ]}).
apply (seq_set_S_disjoint 0). }
rewrite -(seq_set_S_union_L 0).
rewrite Nat.add_1_r.
iMod ("Hcl" with "[-Hticket]") as "_".
{ iNext. iExists P; iFrame.
iApply "Hpool". iExists _,_,_; by iFrame. }
iClear "IH".
unlock wait_loop.
rel_rec_l.
iLöb as "IH".
rel_let_l. rel_proj_l.
rel_load_l_atomic. clear Hls P o b.
iInv N as (P) "[>HP Hpool]" "Hcl".
iDestruct (lockPool_lookup with "HP Hls") as %Hls.
iDestruct (lockPool_open_later with "Hpool") as "[Hlk Hpool]"; first apply Hls.
rewrite {1}/lockInv.
iDestruct "Hlk" as (o n' b) "(>Hlo & >Hln & Hseq & Hl' & Hrest)".
iModIntro. iExists _; iFrame; iNext.
iIntros "Hlo".
rel_op_l.
case_decide; subst; rel_if_l.
(* The ticket is called out *)
* unlock lock.acquire.
rel_rec_r.
destruct b.
{ iDestruct (own_valid_2 with "Hticket Hrest") as %?%gset_disj_valid_op.
set_solver. }
rel_cas_suc_r. rel_if_r.
iMod ("Hcl" with "[-]") as "_".
{ iNext. iExists P; iFrame.
iApply "Hpool". iExists _,_,_; by iFrame. }
iApply bin_log_related_unit.
* iMod ("Hcl" with "[-Hticket]") as "_".
{ iNext. iExists P; iFrame.
iApply "Hpool". iExists _,_,_; by iFrame. }
rel_rec_l.
by iApply "IH".
- (* Release *)
unlock release lock.release.
iApply bin_log_related_arrow_val; eauto.
iAlways. iIntros (? ?) "/= #Hl".
iDestruct "Hl" as (lo ln γ l') "(% & % & Hls)". simplify_eq.
rel_let_l. repeat rel_proj_l.
rel_load_l_atomic.
iInv N as (P) "[>HP Hpool]" "Hcl".
iDestruct (lockPool_lookup with "HP Hls") as %Hls.
iDestruct (lockPool_open_later with "Hpool") as "[Hlk Hpool]"; first apply Hls.
rewrite {1}/lockInv.
iDestruct "Hlk" as (o n b) "(>Hlo & >Hln & ?)".
iModIntro. iExists _; iFrame; iNext.
iIntros "Hlo".
iMod ("Hcl" with "[-]") as "_".
{ iNext. iExists P; iFrame.
iApply "Hpool". iExists _,_,_; iFrame. }
rel_op_l.
rel_store_l_atomic. clear Hls n b P.
iInv N as (P) "[>HP Hpool]" "Hcl".
iDestruct (lockPool_lookup with "HP Hls") as %Hls.
iDestruct (lockPool_open_later with "Hpool") as "[Hlk Hpool]"; first apply Hls.
rewrite {1}/lockInv.
iDestruct "Hlk" as (o' n b) "(>Hlo & >Hln & Hseq & Hl' & Hrest)".
iModIntro. iExists _; iFrame; iNext.
iIntros "Hlo".
rel_let_r. rel_store_r.
iMod ("Hcl" with "[-]") as "_".
{ iNext. iExists P; iFrame.
iApply "Hpool". iExists _,_,_; iFrame. }
iApply bin_log_related_unit.
- by iApply newlock_refinement.
- by iApply acquire_refinement.
- by iApply release_refinement.
Qed.
End refinement.
From iris.proofmode Require Import tactics.
From iris_logrel Require Import logrel.
From iris.program_logic Require Import hoare.
From iris.algebra Require Export auth gset excl.
From iris.base_logic Require Import auth.
From iris_logrel Require Import examples.lock.
Definition read : val := λ: "x", !"x".
Definition FAI : val := rec: "inc" "x" :=
let: "c" := !"x" in
......@@ -13,60 +8,8 @@ Definition FAI : val := rec: "inc" "x" :=
then "c"
else "inc" "x".
Definition makeCounter : val := λ: <>, ref #0.
Definition FG_counter : val := λ: <>,
let: "x" := makeCounter in
(λ: <>, FAI "x", λ: <>, read "x").
(* Definition makeLock : val := λ: <>, *)
(* let: "next" := makeCounter #() in *)
(* let: "owner" := makeCounter #() in *)
(* ref ("owner", "next"). *)
(* Definition release : val := λ: "x", *)
(* FAI (Fst (!"x")). *)
(* Definition wait_loop: val := *)
(* rec: "wait_loop" "x" "lk" := *)
(* if: "x" = !(Fst "lk") (* read the owner of the lock *) *)
(* then #() (* it's my turn *) *)
(* else "wait_loop" "x" "lk". (* otherwise spin on dat *) *)
(* Definition acquire : val := λ: "x", *)
(* let: "t" := FAI (Snd (!"x")) in *)
(* wait_loop "t" "x". *)
Definition lockT : type :=
: (Unit TVar 0) × (TVar 0 Unit) × (TVar 0 Unit).
Definition newlock : val :=
λ: <>, ((* owner *) ref #0, (* next *) ref #0).
Definition wait_loop: val :=
rec: "wait_loop" "x" "lk" :=
if: "x" = !(Fst "lk")
then #() (* my turn *)
else "wait_loop" "x" "lk".
Definition acquire : val :=
rec: "acquire" "lk" :=
let: "n" := FAI (Snd "lk") in
wait_loop "n" "lk".
Definition release : val :=
λ: "lk", (Fst "lk") <- !(Fst "lk") + #1.
Class tlockG Σ :=
tlock_G :> authG Σ (gset_disjUR nat).
Definition tlockΣ : gFunctors :=
#[ authΣ (gset_disjUR nat) ].
Definition lockPool := gset ((loc * loc * gname) * loc).
Definition lockPoolR := gsetUR ((loc * loc * gname) * loc).
Class lockPoolG Σ :=
lockPool_inG :> authG Σ lockPoolR.
Section contents.
Context `{logrelG Σ, tlockG Σ, lockPoolG Σ}.
Context `{logrelG Σ}.
Lemma FAI_atomic R1 R2 Γ E1 E2 K x t τ Δ :
R2 -
......@@ -109,232 +52,4 @@ Section contents.
by iApply "IH".
Qed.
Definition lockInv (lo ln : loc) (γ : gname) (l' : loc) : iProp Σ :=
( (o n : nat) (b : bool), lo ↦ᵢ #o ln ↦ᵢ #n
own γ ( GSet (seq_set 0 n)) l' ↦ₛ #b
if b then own γ ( GSet {[ o ]}) else True)%I.
Definition lockPoolInv (P : lockPool) : iProp Σ :=
([ set] rs P, match rs with
| ((lo, ln, γ), l') => lockInv lo ln γ l'
end)%I.
Definition moduleInv γp : iProp Σ :=
( (P : lockPool), own γp ( P) lockPoolInv P)%I.
Program Definition lockInt (γp : gname) := λne vv,
( (lo ln : loc) (γ : gname) (l' : loc),
vv.1 = (#lo, #ln)%V vv.2 = #l'⌝
own γp ( {[(lo, ln, γ), l']}))%I.
Next Obligation. solve_proper. Qed.
Instance lockInt_persistent γp ww : Persistent (lockInt γp ww).
Proof. apply _. Qed.
Lemma lockPool_open_later (P : lockPool) (lo ln : loc) (γ : gname) (l' : loc) :
(lo, ln, γ, l') P
lockPoolInv P -
( lockInv lo ln γ l') (lockInv lo ln γ l' - lockPoolInv P).
Proof.
iIntros (Hrin) "Hreg".
rewrite /lockPoolInv.
iDestruct (big_sepS_elem_of_acc _ P _ with "Hreg") as "[Hrs Hreg]"; first apply Hrin.
by iFrame.
Qed.
Lemma lockPool_lookup γp (P : lockPool) x :
own γp ( P) -
own γp ( {[ x ]}) -
x P.
Proof.
iIntros "Ho Hrs".
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 lockPool_excl (P : lockPool) (lo ln : loc) γ l' (v : val) :
lockPoolInv P - lo ↦ᵢ v - (lo, ln, γ, l') P.
Proof.
rewrite /lockPoolInv.
iIntros "HP Hlo".
iAssert ((lo, ln, γ, l') P False)%I as %Hbaz.
{
iIntros (HP).
rewrite (big_sepS_elem_of _ P _ HP).
iDestruct "HP" as (a b c) "(Hlo' & Hln & ?)".
iDestruct (mapsto_valid_2 with "Hlo' Hlo") as %Hfoo;
compute in Hfoo; contradiction.
}
iPureIntro. eauto.
Qed.
Definition N := logrelN.@"locked".
(* Allocating a new lock *)
Lemma newlock_refinement Δ Γ γp:
inv N (moduleInv γp) -
{(lockInt γp :: Δ); ⤉Γ} newlock log lock.newlock : (Unit TVar 0).
Proof.
iIntros "#Hinv".
unlock newlock.
iApply bin_log_related_arrow_val; eauto.
{ by unlock lock.newlock. }
iAlways. iIntros (? ?) "/= [% %]"; simplify_eq.
rel_let_l.
rel_alloc_l as lo "Hlo".
rel_apply_r bin_log_related_newlock_r.
{ solve_ndisj. }
iIntros (l') "Hl'".
rel_alloc_l_atomic.
iInv N as (P) "[>HP Hpool]" "Hcl".
iModIntro. iNext.
iIntros (ln) "Hln".
iMod (own_alloc ( (GSet ) (GSet ))) as (γ) "[Hγ Hγ']".
{ by rewrite -auth_both_op. }
iMod (own_update with "HP") as "[HP Hls]".
{ eapply auth_update_alloc.
eapply (gset_local_update _ _ ({[(lo, ln, γ, l')]} P)).
apply union_subseteq_r. }
iDestruct (lockPool_excl _ lo ln γ l' with "Hpool Hlo") as %Hnew.
iMod ("Hcl" with "[-Hls]") as "_".
{ iNext. iExists _; iFrame.
rewrite /lockPoolInv.
rewrite big_sepS_insert; last assumption.
iFrame. iExists _,_,_. iFrame. simpl. iFrame. }
rel_vals. iModIntro.
rewrite -gset_op_union.
iDestruct "Hls" as "[#Hls _]".
iAlways. iExists _,_,_,_. iFrame "Hls". eauto.
Qed.
(* Acquiring a lock *)
Lemma acquire_refinement Δ Γ γp :
inv N (moduleInv γp) -
{(lockInt γp :: Δ); ⤉Γ} acquire log lock.acquire : (TVar 0 Unit).
Proof.
iIntros "#Hinv".
unlock acquire; simpl.
iApply bin_log_related_arrow_val; eauto.
{ by unlock lock.acquire. }
iAlways. iIntros (? ?) "/= #Hl".
iDestruct "Hl" as (lo ln γ l') "(% & % & Hls)". simplify_eq.
rel_let_l. repeat rel_proj_l.
(* rel_apply_l (FAI_atomic). *)
rel_bind_l (FAI #ln).
iApply (FAI_atomic (fun n => own γ ( GSet (seq_set 0 n)))%I True%I); first done.
iAlways.
iInv N as (P) "[>HP Hpool]" "Hcl".
iDestruct (lockPool_lookup with "HP Hls") as %Hls.
iDestruct (lockPool_open_later with "Hpool") as "[Hlk Hpool]"; first apply Hls.
rewrite {1}/lockInv.
iDestruct "Hlk" as (o n b) "(>Hlo & >Hln & >Hseq & Hl' & Hrest)".
iModIntro. iExists _; iFrame.
iSplit.
- iDestruct 1 as (m) "[Hln ?]".
iApply ("Hcl" with "[-]").
iNext. iExists P; iFrame.
iApply "Hpool". iExists _,_,_; by iFrame.
- iIntros (m) "[Hln Hseq] _".
iMod (own_update with "Hseq") as "[Hseq Hticket]".
{ eapply auth_update_alloc.
eapply (gset_disj_alloc_empty_local_update _ {[ m ]}).
apply (seq_set_S_disjoint 0). }
rewrite -(seq_set_S_union_L 0).
iMod ("Hcl" with "[-Hticket]") as "_".
{ iNext. iExists P; iFrame.
iApply "Hpool". iExists _,_,_; by iFrame. }
simpl. rel_let_l.
unlock wait_loop.
rel_rec_l.
iLöb as "IH".
rel_let_l. rel_proj_l.
rel_load_l_atomic. clear Hls P o b.
iInv N as (P) "[>HP Hpool]" "Hcl".
iDestruct (lockPool_lookup with "HP Hls") as %Hls.
iDestruct (lockPool_open_later with "Hpool") as "[Hlk Hpool]"; first apply Hls.
rewrite {1}/lockInv.
iDestruct "Hlk" as (o n' b) "(>Hlo & >Hln & Hseq & Hl' & Hrest)".
iModIntro. iExists _; iFrame; iNext.
iIntros "Hlo".
rel_op_l.
case_decide; subst; rel_if_l.
(* The ticket is called out *)
+ destruct b.
{ iDestruct (own_valid_2 with "Hticket Hrest") as %?%gset_disj_valid_op.
set_solver. }
rel_apply_r (bin_log_related_acquire_r with "Hl'").
{ solve_ndisj. }
iIntros "Hl'".
iMod ("Hcl" with "[-]") as "_".
{ iNext. iExists P; iFrame.
iApply "Hpool". iExists _,_,_; iFrame. }
iApply bin_log_related_unit.
+ iMod ("Hcl" with "[-Hticket]") as "_".
{ iNext. iExists P; iFrame.
iApply "Hpool". iExists _,_,_; by iFrame. }
rel_rec_l.
by iApply "IH".
Qed.
(* Releasing the lock *)
Lemma release_refinement Δ Γ γp :
inv N (moduleInv γp) -
{(lockInt γp :: Δ); ⤉Γ} release log lock.release : (TVar 0 Unit).
Proof.
iIntros "#Hinv".
unlock release.
iApply bin_log_related_arrow_val; eauto.
{ by unlock lock.release. }
iAlways. iIntros (? ?) "/= #Hl".
iDestruct "Hl" as (lo ln γ l') "(% & % & Hls)". simplify_eq.
rel_let_l. repeat rel_proj_l.
rel_load_l_atomic.
iInv N as (P) "[>HP Hpool]" "Hcl".
iDestruct (lockPool_lookup with "HP Hls") as %Hls.
iDestruct (lockPool_open_later with "Hpool") as "[Hlk Hpool]"; first apply Hls.
rewrite {1}/lockInv.
iDestruct "Hlk" as (o n b) "(>Hlo & >Hln & ?)".
iModIntro. iExists _; iFrame; iNext.
iIntros "Hlo".
iMod ("Hcl" with "[-]") as "_".
{ iNext. iExists P; iFrame.
iApply "Hpool". iExists _,_,_; iFrame. }
rel_op_l.
rel_store_l_atomic. clear Hls n b P.
iInv N as (P) "[>HP Hpool]" "Hcl".
iDestruct (lockPool_lookup with "HP Hls") as %Hls.
iDestruct (lockPool_open_later with "Hpool") as "[Hlk Hpool]"; first apply Hls.
rewrite {1}/lockInv.
iDestruct "Hlk" as (o' n b) "(>Hlo & >Hln & Hseq & Hl' & Hrest)".
iModIntro. iExists _; iFrame; iNext.
iIntros "Hlo".
rel_apply_r (bin_log_related_release_r with "Hl'").
{ solve_ndisj. }
iIntros "Hl'".
iMod ("Hcl" with "[-]") as "_".
{ iNext. iExists P; iFrame.
iApply "Hpool". iExists _,_,_; iFrame. }
iApply bin_log_related_unit.
Qed.
Lemma ticket_lock_refinement Γ :
Γ Pack (newlock, acquire, release)
log
Pack (lock.newlock, lock.acquire, lock.release) : lockT.
Proof.
iIntros (Δ).
iMod (own_alloc ( ( : lockPoolR))) as (γp) "HP"; first done.
iMod (inv_alloc N _ (moduleInv γp) with "[HP]") as "#Hinv".
{ iNext. iExists . iFrame. by rewrite /lockPoolInv big_sepS_empty. }
iApply (bin_log_related_pack _ (lockInt γp)).
repeat iApply bin_log_related_pair.
- by iApply newlock_refinement.
- by iApply acquire_refinement.
- by iApply release_refinement.
Qed.
End contents.