Library iris.locks.ticket_clh_triples
From iris.program_logic Require Export invariants ghost_ownership.
From iris.program_logic Require Import ownership auth sts saved_prop.
From iris.proofmode Require Import weakestpre invariants sts.
From iris.heap_lang Require Import heap proofmode notation refine_proofmode.
From iris.locks Require ticket clh.
Global Set Bullet Behavior "Strict Subproofs".
Section ticket_sts.
Local Open Scope nat_scope.
Inductive ticket_state :=
| ticket_pre: nat → ticket_state
| ticket_entered: nat → ticket_state.
Global Instance ticket_state_inhabited: Inhabited ticket_state :=
populate (ticket_pre O).
Definition owner (t: ticket_state) : nat :=
match t with
| ticket_pre n | ticket_entered n ⇒ n
end.
Inductive ticket_prim_step : relation ticket_state :=
| ticket_enter n: ticket_prim_step (ticket_pre n) (ticket_entered n)
| ticket_finish n: ticket_prim_step (ticket_entered n) (ticket_pre (S n)).
Inductive token := enter_tok (n: nat) | finish_tok (n: nat).
Definition tok (s: ticket_state) : set token :=
match s with
| ticket_pre n ⇒
{[ t | ∃ i, (t = enter_tok i ∧ i < n) ∨ (t = finish_tok i ∧ i < n) ]}
| ticket_entered n ⇒
{[ t | ∃ i, (t = enter_tok i ∧ i ≤ n) ∨ (t = finish_tok i ∧ i < n) ]}
end.
Global Arguments tok !_ /.
Canonical Structure sts := sts.STS ticket_prim_step tok.
Lemma enter_step0 n:
sts.step (ticket_pre n, {[enter_tok n]})
(ticket_entered n, ∅).
Proof.
constructor.
- constructor.
- set_unfold. intros ? (?&[(?&?)|(?&?)]) Heq; subst; inversion Heq; omega.
- set_unfold. intros ? (?&[(?&?)|(?&?)]) Heq; subst; inversion Heq; omega.
- set_unfold. split.
× intros [(?&[(?&?)|(?&?)])|?].
** subst. left. eexists. left. split; eauto; omega.
** subst. left. eexists. right. split; eauto; omega.
** subst. left. eexists. left. split; eauto; omega.
× intros [(n'&[(?&?)|(?&?)])|].
** assert (n' = n ∨ n' < n) as [-> | ] by omega.
*** naive_solver.
*** left. eexists. left. split; eauto.
** left. eexists. right. split; eauto; omega.
** intros; exfalso; auto.
Qed.
Lemma enter_step1 n:
sts.steps (ticket_pre n, {[enter_tok n]})
(ticket_entered n, ∅).
Proof. apply rtc_once, enter_step0. Qed.
Lemma enter_step2 n:
sts.steps (ticket_pre n, {[enter_tok n]} ∪ {[finish_tok n]})
(ticket_entered n, {[finish_tok n]}).
Proof.
apply rtc_once.
constructor.
- constructor.
- set_unfold. intros ? (?&[(?&?)|(?&?)]) [Heq|Heq]; subst; inversion Heq; omega.
- set_unfold. intros ? (?&[(?&?)|(?&?)]) Heq; subst; inversion Heq; omega.
- set_unfold. split.
× intros [(?&[(?&?)|(?&?)])|[?|?]].
** subst. left. eexists. left. split; eauto; omega.
** subst. left. eexists. right. split; eauto; omega.
** subst. left. eexists. left. split; eauto; omega.
** subst. right; done.
× intros [(n'&[(?&?)|(?&?)])| ->].
** assert (n' = n ∨ n' < n) as [-> | ] by omega.
*** naive_solver.
*** left. eexists. left. split; eauto.
** left. eexists. right. split; eauto; omega.
** auto.
Qed.
Lemma finish_step0 n:
sts.step (ticket_entered n, {[finish_tok n]})
(ticket_pre (S n), ∅).
Proof.
constructor.
- constructor.
- set_unfold. intros ? (?&[(?&?)|(?&?)]); subst; inversion 1. omega.
- set_unfold. intros ? (?&[(?&?)|(?&?)]) Heq; subst; inversion Heq; omega.
- set_unfold. split.
× intros [(?&[(?&?)|(?&?)])|?].
** subst. left. eexists. left. split; eauto; omega.
** subst. left. eexists. right. split; eauto; omega.
** subst. left. eexists. right. split; eauto; omega.
× intros [(n'&[(?&?)|(?&?)])|?]; last exfalso; auto.
** left. eexists. left. split; eauto. omega.
** assert (n' = n ∨ n' < n) as [-> | ] by omega.
*** naive_solver.
*** left. eexists. right. split; eauto.
Qed.
Lemma finish_step1 n:
sts.steps (ticket_entered n, {[finish_tok n]})
(ticket_pre (S n), ∅).
Proof. apply rtc_once, finish_step0. Qed.
Lemma pre_closed1 n:
sts.closed ({[ticket_pre n]}) ({[enter_tok n]}).
Proof.
split.
- set_unfold. intros n' →.
set_unfold. intros k (?&[(?&?)|(?&?)]) Heq; try congruence.
subst. inversion Heq; omega.
- set_unfold. intros ? s' →.
inversion 1 as [T1 T2 Hdisj Hstep].
inversion Hstep as [???? Hstep' ? Hdisj' Hconserve]; subst.
inversion Hstep'; subst.
exfalso.
eapply (Hdisj (enter_tok n)); set_unfold; eauto.
specialize (Hconserve (enter_tok n)). destruct Hconserve as [_ Hconserve].
destruct Hconserve as [(n'&[(Heq&?)|(Heq&?)]) |]; first by (left; naive_solver).
× inversion Heq. omega.
× inversion Heq.
× auto.
Qed.
Lemma pre_closed2 n:
sts.closed ({[ticket_pre n]}) ({[enter_tok n]} ∪ {[finish_tok n]}).
Proof.
split.
- set_unfold. intros n' →.
set_unfold. intros k (?&[(?&?)|(?&?)]) [Heq|Heq]; try congruence.
× subst. inversion Heq; omega.
× subst. inversion Heq; omega.
- set_unfold. intros ? s' →.
inversion 1 as [T1 T2 Hdisj Hstep].
inversion Hstep as [???? Hstep' ? Hdisj' Hconserve]; subst.
inversion Hstep'; subst.
exfalso.
eapply (Hdisj (enter_tok n)); set_unfold; eauto.
specialize (Hconserve (enter_tok n)). destruct Hconserve as [_ Hconserve].
destruct Hconserve as [(n'&[(Heq&?)|(Heq&?)]) |]; first by (left; naive_solver).
× inversion Heq. omega.
× inversion Heq.
× auto.
Qed.
Lemma finish_closed1 n:
sts.closed ({[ s | owner s ≤ n]}) ({[finish_tok n]}).
Proof.
split.
- set_unfold. intros x Hle n' Hin →.
move:Hin; destruct x; rewrite //=; set_unfold; intros (?&[(Heq&?)|(Heq&?)]).
× inversion Heq; congruence.
× inversion Heq; omega.
× inversion Heq; congruence.
× inversion Heq; omega.
- set_unfold. intros x x' Hle.
inversion 1 as [T1 T2 Hdisj Hstep].
inversion Hstep as [???? Hstep' ? Hdisj' Hconserve]; subst.
inversion Hstep'; subst; rewrite //= in Hle ×.
assert (S n0 ≤ n ∨ n < S n0) as [|] by omega; auto.
exfalso.
eapply (Hdisj (finish_tok n)); set_unfold; eauto.
specialize (Hconserve (finish_tok n)). destruct Hconserve as [_ Hconserve].
destruct Hconserve as [(n'&[(Heq&?)|(Heq&?)]) |]; first by (left; naive_solver).
× inversion Heq.
× inversion Heq. omega.
× auto.
Qed.
Lemma finish_upper_bound s x:
s ∈ sts.up (ticket_pre 0) {[finish_tok x]} → owner s ≤ x.
Proof.
intros Hin%(sts.up_subseteq (ticket_pre 0)); [ | eapply finish_closed1 | ];
set_unfold; (done || omega).
Qed.
Definition up_tok (k: nat) : set token :=
{[ t | ∃ n, (t = enter_tok n ∨ t = finish_tok n) ∧ n ≥ k]}.
Lemma up_tok_anti n:
up_tok (S n) ⊆ up_tok n.
Proof.
set_unfold. intros x (n'&[?|?]&?); ∃ n'; split; auto; omega.
Qed.
Lemma pre_init: sts.tok (ticket_pre O) ≡ ∅.
Proof.
set_unfold. intros ? (?&[(?&?)|(?&?)]); omega.
Qed.
Lemma up_tok_init: up_tok O ≡ ⊤.
Proof.
set_unfold; intros x. split; first done.
destruct x as [n|n]; ∃ n; split; eauto; omega.
Qed.
Lemma pre_subseteq_enter n:
tok (ticket_pre n) ⊆ tok (ticket_entered n).
Proof.
rewrite //=. set_unfold. intros t (x&[(?&?)|(?&?)]); subst.
- ∃ x. left. split; auto; omega.
- ∃ x. right. split; auto.
Qed.
Lemma enter_subseteq_pre n:
tok (ticket_entered n) ⊆ tok (ticket_pre (S n)).
Proof.
rewrite //=. set_unfold. intros t (x&[(?&?)|(?&?)]); subst.
- ∃ x. left. split; auto; omega.
- ∃ x. right. split; auto.
Qed.
Lemma frame_step_token_monotone T t1 t2:
rtc (sts.frame_step T) t1 t2 →
tok t1 ⊆ tok t2.
Proof.
induction 1 as [| ??? Hfstep ? IHrtc]; first done.
inversion Hfstep as [?? Hdisj Hstep]. inversion Hstep as [???? Hprim]; subst.
inversion Hprim; subst.
- etransitivity; last apply IHrtc. apply pre_subseteq_enter.
- etransitivity; last apply IHrtc. apply enter_subseteq_pre.
Qed.
Lemma frame_step_owner_monotone T t1 t2:
rtc (sts.frame_step T) t1 t2 →
owner t1 ≤ owner t2.
Proof.
induction 1 as [| ??? Hfstep ? IHrtc]; first done.
inversion Hfstep as [?? Hdisj Hstep]. inversion Hstep as [???? Hprim]; subst.
inversion Hprim; subst.
- etransitivity; last apply IHrtc. rewrite //=.
- etransitivity; last apply IHrtc. rewrite //=. omega.
Qed.
Lemma frame_step_owner_monotone' T n n':
rtc (sts.frame_step T) (ticket_entered n) (ticket_pre n') →
n < n'.
Proof.
remember (ticket_entered n) as te eqn:Heqn.
remember (ticket_pre n') as tp eqn:Heqn'.
intros Hrtc. revert n n' Heqn Heqn'.
induction Hrtc as [| ??? Hfstep ? IHrtc]; first (intros; congruence).
inversion Hfstep as [?? Hdisj Hstep]. inversion Hstep as [???? Hprim]; subst.
inversion Hprim; subst.
- intros. congruence.
- intros. inversion Heqn. subst.
apply frame_step_owner_monotone in Hrtc. simpl in ×. omega.
Qed.
Lemma pre_step_entered T n t:
(sts.frame_step T) (ticket_pre n) t →
t = ticket_entered n.
Proof.
inversion 1 as [?? Hdisj Hstep]. inversion Hstep as [???? Hprim]; subst.
inversion Hprim; subst. done.
Qed.
Lemma owner_contains_enter_lt t:
∀ n', n' < owner t → enter_tok n' ∈ tok t.
Proof.
intros n' Hlt. destruct t; set_unfold; ∃ n'.
- naive_solver.
- left. split; auto. omega.
Qed.
Lemma owner_contains_finish_lt t:
∀ n', n' < owner t → finish_tok n' ∈ tok t.
Proof.
intros n' Hlt. destruct t; set_unfold; ∃ n'.
- naive_solver.
- right. split; auto.
Qed.
Lemma rtc_ticket_pre_tok n t:
rtc (sts.frame_step ∅) (ticket_pre n) t →
t = ticket_pre n ∨ ∀ n', n' ≤ n → enter_tok n' ∈ tok t.
Proof.
intros Hrtc%frame_step_owner_monotone.
inversion Hrtc.
- destruct t.
× left. simpl in *; subst; done.
× right. simpl in ×. intros.
set_unfold. ∃ n'. left; naive_solver.
- right. intros. simpl in ×. apply owner_contains_enter_lt. omega.
Qed.
Lemma rtc_ticket_entered_tok n t:
rtc (sts.frame_step ∅) (ticket_entered n) t →
t = ticket_entered n ∨ ∀ n', n' ≤ n → finish_tok n' ∈ tok t.
Proof.
intros Hrtc.
destruct t.
- apply frame_step_owner_monotone' in Hrtc.
right. intros n' Hle. set_unfold. eexists. right. split; auto. omega.
- eapply frame_step_owner_monotone in Hrtc. simpl in ×.
inversion Hrtc.
× left. subst. auto.
× right. subst. intros. set_unfold. eexists. right. split; auto.
omega.
Qed.
Lemma pre_upper_bound n:
(sts.up (ticket_pre n) ∅ ∩ sts.up (ticket_pre 0) {[enter_tok n]})
⊆ {[ ticket_pre n]}.
Proof.
intros t (Hup1&Hup2)%elem_of_intersection.
apply sts.closed_up in Hup2; last (rewrite pre_init; set_solver).
set_unfold. apply rtc_ticket_pre_tok in Hup1 as [|]; first done.
exfalso; eapply (Hup2 (enter_tok n)); naive_solver.
Qed.
Lemma finish_upper_bound2 n:
(sts.up (ticket_entered n) ∅ ∩ sts.up (ticket_pre 0) {[finish_tok n]})
⊆ {[ ticket_entered n]}.
Proof.
intros t (Hup1&Hup2)%elem_of_intersection.
apply sts.closed_up in Hup2; last (rewrite pre_init; set_solver).
set_unfold. apply rtc_ticket_entered_tok in Hup1 as [|]; first done.
exfalso; eapply (Hup2 (finish_tok n)); auto.
Qed.
Lemma finish_upper_bound3 n:
ticket_entered n ∈ sts.up (ticket_pre 0) {[finish_tok n]}.
Proof.
cut (∀ k m, k ≤ m → ticket_entered k ∈ sts.up (ticket_pre 0) {[finish_tok m]});
first by eauto.
clear n. induction k; set_unfold⇒ m Hle.
- eapply rtc_once.
eapply (sts.Frame_step) with (T1 := {[enter_tok 0]}).
× set_unfold. intros ? → [(?&[?|(?&?)])|].
** omega.
** congruence.
** congruence.
× eapply enter_step0.
- eapply rtc_r; first eapply rtc_r; first (eapply IHk; omega).
× eapply (sts.Frame_step) with (T1 := {[finish_tok k]}).
** set_unfold. intros ??; subst.
intros [(n&[(Heq&?)|(Heq&?)])|Heq]; try congruence; inversion Heq; omega.
** eapply finish_step0.
× eapply (sts.Frame_step) with (T1 := {[enter_tok (S k)]}).
** set_unfold. intros ??; subst.
intros [(n&[(Heq&?)|(Heq&?)])|Heq]; try congruence; inversion Heq; omega.
** eapply enter_step0.
Qed.
Lemma finish_closed2 n:
sts.closed {[ ticket_entered n ]} ({[finish_tok n]}).
Proof.
split.
- set_unfold. intros x Heq0 n' Hin ->; subst.
move:Hin; rewrite //=; set_unfold; intros (?&[(Heq&?)|(Heq&?)]).
× inversion Heq; congruence.
× inversion Heq; omega.
- set_unfold. intros x x' Heq0; subst.
inversion 1 as [T1 T2 Hdisj Hstep].
inversion Hstep as [???? Hstep' ? Hdisj' Hconserve]; subst.
inversion Hstep'; subst.
exfalso.
eapply (Hdisj (finish_tok n)); set_unfold; eauto.
specialize (Hconserve (finish_tok n)). destruct Hconserve as [_ Hconserve].
destruct Hconserve as [(n'&[(Heq&?)|(Heq&?)]) |]; first by (left; naive_solver).
× inversion Heq.
× inversion Heq. omega.
× auto.
Qed.
End ticket_sts.
Class tlockG Σ := TicketG {
tlock_stsG :> stsG lang.heap_lang Σ sts;
}.
Definition tlockGF : gFunctorList := [stsGF sts].
Instance inGF_tlockG `{H : inGFs lang.heap_lang Σ tlockGF} : tlockG Σ.
Proof. destruct H as (?). split; apply _. Qed.
Section proof.
Context `{!heapG Σ, !sheapG heap_lang Σ, !tlockG Σ} (N : namespace).
Context `{!refineG heap_lang Σ (delayed_lang (heap_lang) Kd Fd) (S Kd × (Kd + 3))}.
Context (Hgt: 99 < Kd).
Local Notation iProp := (iPropG heap_lang Σ).
Definition sN : namespace := N .@ "sts".
Definition inN : namespace := N .@ "inv_next".
Definition isN : namespace := N .@ "inv_spin".
Definition sts_interp (lo lhd: loc) (R: iProp) (t: ticket_state) : iProp :=
(lo ↦s #(owner t) ★
match t with
| ticket_pre n ⇒ ⧆R ★ ∃ v, lhd ↦ v
| ticket_entered n ⇒ Emp
end)%I.
Definition owner_sts_ctx γ lo lhd R :=
(⧆■ (heapN ⊥ N) ★ ⧆■(sheapN ⊥ N) ★ ⧆■(heapN ⊥ sheapN)
★ heap_ctx ★ sheap_ctx ★ sts_ctx γ sN (sts_interp lo lhd R))%I.
Definition spin_inv (γ: gname) (lo lhd: loc) (o: nat) (l: loc) : iProp :=
((l ↦{1/2} #true ★ sts_ownS γ (sts.up (ticket_pre O) {[finish_tok o]}) {[finish_tok o]})
∨ (l ↦ #false ★ sts_ownS γ (sts.up (ticket_pre (S o)) ∅) ∅))%I.
Definition next_inv (γ: gname) (lo lhd: loc) (ln ltl: loc) : iProp :=
(∃ (n: nat) (l: loc),
ln ↦s #n ★ ltl ↦ #l ★
match n with
| O ⇒ l ↦ #false
| S n' ⇒ inv isN (spin_inv γ lo lhd n' l)
end ★
sts_ownS γ (sts.up (ticket_pre O) (up_tok n)) (up_tok n))%I.
Local Open Scope nat_scope.
Definition is_lock (γ : gname) (lks lk: val) (R: iProp) : iProp :=
(∃ lo ln lhd ltl : loc,
(⧆■ (heapN ⊥ N) ★ ⧆■(sheapN ⊥ N) ★ ⧆■(heapN ⊥ sheapN)
★ heap_ctx ★ sheap_ctx ★ sts_ctx γ sN (sts_interp lo lhd R) ★
inv inN (next_inv γ lo lhd ln ltl) ★
sts_ownS γ (sts.up (ticket_pre O) ∅) ∅ ★
⧆■(lks = (#lo, #ln)%V) ★
⧆■(lk = (#lhd, #ltl)%V)))%I.
Definition issued (γ : gname) (lks lk: val) (x : nat) (lpred lmine: loc) : iProp :=
(∃ lo ln lhd ltl : loc,
⧆■(lks = (#lo, #ln)%V) ★
⧆■(lk = (#lhd, #ltl)%V) ★
(sts_ownS γ (sts.up (ticket_pre O) {[enter_tok x]}) {[enter_tok x]} ★
match x with
| O ⇒ lpred ↦ #false
| S x' ⇒ inv isN (spin_inv γ lo lhd x' lpred)
end ★
lmine ↦{1/2} #true ★
inv isN (spin_inv γ lo lhd x lmine)))%I.
Definition locked (γ : gname) (lks lk: val) : iProp :=
(∃ (lo ln lhd ltl lmine : loc) (x: nat),
⧆■(lks = (#lo, #ln)%V) ★
⧆■(lk = (#lhd, #ltl)%V) ★
(sts_ownS γ (sts.up (ticket_entered x) ∅) ∅ ★
lhd ↦ #lmine ★
lmine ↦{1/2} #true ★
inv isN (spin_inv γ lo lhd x lmine)))%I.
Import uPred.
Lemma newlock_spec i K d d' R:
(d > 5 ∧ d ≤ Kd) →
(d' ≤ Kd)%nat →
heapN ⊥ N →
sheapN ⊥ N →
(heap_ctx ★ sheap_ctx ★ ownT i (ticket.newlock #()) K d ★ ⧆R
⊢ WP clh.newlock #() {{ lk, ∃ lks γ, is_lock γ lks lk R ★
ownT i (of_val lks) K d'}})%I.
Proof.
iIntros (Hd Hd' HN1 HN2) "(#?&#?&Hown&HR)".
rewrite /ticket.newlock /clh.newlock.
wp_let. refine_let d.
wp_alloc dummy as "Hd". refine_alloc d lo as "Ho".
wp_let. refine_delay (d-1).
wp_alloc lhd as "Hhd". refine_delay (d-2).
wp_alloc ltl as "Htl". refine_alloc d' ln as "Hn".
wp_value; iExists (#lo, #ln)%V; iFrame.
assert (nclose sN ⊆ ⊤) as Hdisj; eauto with ndisj.
iPoseProof (sts_alloc (sts_interp lo lhd R) ⊤ sN (ticket_pre O) Hdisj) as "Hsts".
iPvs ("Hsts" with "[HR Ho Hhd]") as (γ) "(Hsts&Htok)"; clear Hdisj.
{ rewrite /sts_interp //=. iIntros "@". iNext. iFrame. iExists #dummy; done. }
rewrite pre_init.
setoid_replace (⊤ ∖ ∅: sts.tokens sts) with (⊤: sts.tokens sts)
by (set_unfold; naive_solver).
rewrite /is_lock.
iPvs (sts_own_weaken _ γ _ ((sts.up (ticket_pre 0) ⊤) ∩ (sts.up (ticket_pre 0) ∅))
_ (⊤ ∪ ∅)
with "Htok") as "Htok"; eauto.
{ split; eauto using sts.elem_of_up. }
{ rewrite subseteq_intersection_1; last (eapply sts.up_preserving; set_solver).
rewrite comm subseteq_union_1; eauto.
eapply sts.closed_up. rewrite pre_init. set_solver. }
rewrite sts_ownS_op.
- iDestruct "Htok" as "(Htok1&Htok2)".
assert (nclose inN ⊆ ⊤) as Hdisj; eauto with ndisj.
iPoseProof (inv_alloc inN ⊤ (next_inv γ lo lhd ln ltl) Hdisj) as "Hinv".
iPvs ("Hinv" with "[Hn Hd Htl Htok1]") as "Hinv"; clear Hdisj.
{ rewrite /next_inv //=. iIntros "@". iNext. iExists O. iExists dummy.
iFrame. rewrite up_tok_init. done. }
iPvsIntro. iExists γ, lo, ln, lhd, ltl. iFrame.
rewrite ?pure_equiv //; first (rewrite -?emp_True ?left_id ?right_id; iSplit; auto).
eauto with ndisj.
- set_solver.
- eapply sts.closed_up. rewrite pre_init. set_solver.
- eapply sts.closed_up. rewrite pre_init. set_solver.
Qed.
Instance issued_affine: AffineP (issued γ lks lk x lpred lmine).
Proof.
rewrite /issued; intros; destruct x; apply _.
Qed.
Instance is_lock_affine: AffineP (is_lock γ lks lk R).
Proof.
rewrite /is_lock; intros; apply _.
Qed.
Instance locked_affine: AffineP (locked γ lks lk).
Proof.
rewrite /is_lock; intros; apply _.
Qed.
Instance sts_empty_relevant: RelevantP (sts_ownS γ (sts.up s ∅) ∅).
Proof.
rewrite /RelevantP /sts_ownS ⇒ γ n.
apply own_core_persistent.
rewrite /Persistent /pcore /cmra_pcore //=.
rewrite /dra.validity_pcore //=.
rewrite //=. econstructor.
rewrite /sts_frag //=. econstructor; rewrite //=.
intros. rewrite /core /dra.dra_core //=.
rewrite sts.up_closed //. apply sts.closed_up. set_solver.
Qed.
Lemma sts_up_dup γ s:
sts_ownS γ (sts.up s ∅) ∅ ⊢
(sts_ownS γ (sts.up s ∅) ∅ ★
sts_ownS γ (sts.up s ∅) ∅)%I.
Proof.
apply relevant_sep_dup, _.
Qed.
Instance is_lock_relevant: RelevantP (is_lock γ lks lk R).
Proof.
rewrite /is_lock; intros. apply _.
Qed.
Global Instance sts_ownS_timeless S T : ATimelessP (sts_ownS γ S T).
Proof. intros γ. rewrite /sts_ownS. apply _. Qed.
Instance affine_match_state:
AffineP (match s' with
| ticket_pre _ ⇒ ⧆R ★ ∃ v : val, lhd' ↦ v
| ticket_entered _ ⇒ Emp
end).
Proof. destruct s'; apply _. Qed.
Instance affine_match_nat:
AffineP (match n with
| O ⇒ l ↦ #false
| S n' ⇒ inv isN (spin_inv γ lo lhd n' l)
end).
Proof. destruct n; apply _. Qed.
Ltac do_prim_step :=
match goal with
| [ |- ?e1 = fill ?K ?e2 ] ⇒
auto; (try reshape_expr e1 ltac:(fun K' e' ⇒ unify K K'; done))
| [ |- prim_step_nofork heap_lang (?e, ?σ) _] ⇒
reshape_expr e ltac:(fun K' e' ⇒
eapply (Ectx_step _ _ _ _ _ K' e');
[ eauto | rewrite //= | do_head_step eauto ])
end.
Lemma wait_loop_spec i K (d d': nat) (γ: gname) (lks lk: val) (x: nat) (lpred lmine: loc) R:
(d > 5 ∧ d ≤ Kd) →
(d' < Kd - 1) →
(is_lock γ lks lk R ★ issued γ lks lk x lpred lmine ★
ownT i (ticket.wait_loop #x lks) K d
⊢ WP (clh.wait_loop #lmine #lpred lk) {{ v, ⧆■(v = #()) ★ locked γ lks lk ★
ownT i (#())%E K d' ★ ⧆R}})%I.
Proof.
iIntros (Hd Hd') "(?&?&Hown)".
iLob as "IH".
iIntros "@ ! ? ? Hown".
refine_focus (ticket.wait_loop #x%E).
rewrite {2}/is_lock. iDestruct "~" as (lo ln lhd ltl) "(%&%&%&#?&#?&#?&#?&?&%&%)".
wp_rec. refine_rec d.
wp_value; refine_unfocus; iPvsIntro.
wp_lam. refine_lam d.
wp_value; iPvsIntro.
rewrite /issued. iDestruct "~1" as (lo' ln' lhd' ltl') "(%&%&Hsts&Hx&Hmine&Hinv)".
subst. inversion H5; subst. inversion H4; subst.
wp_lam.
destruct x; refine_proj d.
- iClear "IH".
wp_focus (! #lpred)%E.
iSts γ as s Hin.
rewrite /sts_interp.
rewrite {1}sts.up_up_set in Hin ×.
rewrite sts.up_closed; last apply pre_closed1. inversion 1; subst.
iDestruct "Hsts" as "(Hlo&Hhd)".
assert (sN ⊥ heapN) as Hdisj1 by (rewrite /sN; eauto with ndisj).
assert (sN ⊥ sheapN) as Hdisj2 by (rewrite /sN; eauto with ndisj).
wp_load.
rewrite (affine_elim (lo' ↦s #0)). refine_load d.
iExists (ticket_entered 0). iExists ∅.
iSplitL "".
{ iPureIntro. apply enter_step1. }
iSplitL "Hlo".
{ iIntros "@". iNext. iFrame. done. }
iIntros "Hsts".
wp_let. refine_let d.
wp_if. refine_op d.
wp_proj. refine_delay (d-1).
iDestruct "Hhd" as "(HR&Hhd)".
iDestruct "Hhd" as (v0) "Hhd".
rewrite sts_own_weaken.
× iPvs "Hsts".
wp_store. refine_if_true d'.
iFrame. iSplitL ""; first done.
rewrite /locked. iExists lo', ln', lhd', ltl', lmine, 0.
iSplitL ""; first done.
iSplitL ""; first done.
iFrame. done.
× set_solver.
× apply sts.elem_of_up.
× apply sts.closed_up. set_solver.
- iDestruct "Hx" as "#Hx".
wp_focus (! #lpred)%E.
iInv "Hx" as "Hspin"; auto with fsaV.
rewrite /spin_inv //=.
rewrite {1}later_or.
rewrite affine_or.
iDestruct "Hspin" as "[?|?]".
×
iDestruct "Hspin" as "(Hpred&Hsts')".
iTimeless "Hpred". iTimeless "Hsts'".
iApply wp_pvs.
rewrite (affine_elim (sts_ownS _ _ _)).
iSts γ as s' Hin'.
assert (owner s' ≤ x) by (eauto using finish_upper_bound).
rewrite /sts_interp.
rewrite (affine_elim (lpred ↦{1/2} _)).
assert (sN ⊥ heapN) as Hdisj1 by (rewrite /sN; eauto with ndisj).
assert (sN ⊥ sheapN) as Hdisj2 by (rewrite /sN; eauto with ndisj).
assert (isN ⊥ sheapN) as ? by (rewrite /isN; eauto with ndisj).
assert (isN ⊥ heapN) as ? by (rewrite /isN; eauto with ndisj).
wp_load.
iDestruct "Hsts'" as "(Hlo&Hhd)".
refine_load d'.
iExists s', {[finish_tok x]}.
iSplitL "".
{ iPureIntro. done. }
iSplitL "Hlo Hhd".
{ iIntros "@". iNext. iFrame. done. }
iIntros "Hsts'".
iPvs (sts_own_weaken _ γ s' (sts.up (ticket_pre 0) {[finish_tok x]}) {[finish_tok x]}
{[finish_tok x]} with "Hsts'") as "Hweaken"; eauto.
{ apply sts.closed_up. set_unfold. intros ? (?&[(?&?)|(?&?)]). congruence.
omega. }
iPvsIntro.
iSplitL "Hweaken Hpred".
{ iIntros "@ >". iLeft; iFrame; done. }
wp_let. refine_let d.
wp_if.
assert (d ≤ Kd) as Hle by omega.
iPoseProof (refine_heap_pure_det_nofork d d Hle Hle _ K 2 _
(ticket.wait_loop #(S x) (#lo', #ln')%E)
with "[Hown]") as "Hown";
[ | | | | iFrame | ]; auto.
{ omega. }
{ intros.
eapply (nsteps_l _ _ _
((if: #false then #()
else (rec: "wait_loop" "x" "lk"
:= let: "o" := ! (Fst "lk")
in if: "x" = "o" then #() else ("wait_loop" "x") "lk")
#(Z.pos (Pos.of_succ_nat x)) (#lo', #ln'))%E, σ)).
{ eapply Ectx_step with (e1' := ((#(Z.pos (Pos.of_succ_nat x))%E = #(owner s'))%E))
(e2' := #false); simpl; try do_prim_step.
econstructor. rewrite //=; f_equal.
replace ((bool_decide (Z.pos (Pos.of_succ_nat x) = owner s'))) with false; auto.
symmetry; apply bool_decide_false. rewrite Zpos_P_of_succ_nat. omega. }
eapply nsteps_once; do_prim_step.
}
iPsvs "Hown". iPvsIntro.
iSpecialize ("IH" with "[~5]").
{ rewrite /is_lock.
iExists lo', ln', lhd', ltl'. iFrame.
repeat (iSplitL; auto). }
iSpecialize ("IH" with "[Hsts Hmine Hinv] Hown").
{
iExists lo', ln', lhd', ltl'. iFrame.
repeat (iSplitL; auto).
}
iAssumption.
×
iDestruct "Hspin" as "(Hpred&Hsts')".
iTimeless "Hpred". iTimeless "Hsts'".
iApply wp_pvs.
rewrite (affine_elim (sts_ownS _ _ _)).
iPoseProof (sts_up_dup γ (ticket_pre (S x)) with "Hsts'") as "Hsts'".
iDestruct "Hsts'" as "(Hsts1'&Hsts2')".
iCombine "Hsts1'" "Hsts" as "Hsts''".
rewrite -sts.sts_ownS_op; last 3 first.
{ set_solver. }
{ apply sts.closed_up. set_solver. }
{ apply sts.closed_up. rewrite pre_init. set_solver. }
iPvs (sts_ownS_weaken _ γ _ {[ticket_pre (S x)]} with "Hsts''") as "Hsts''".
{ rewrite left_id; reflexivity. }
{ apply pre_upper_bound. }
{ apply pre_closed1. }
iSts γ as s' Hin'.
inversion Hin'. subst.
rewrite /sts_interp.
rewrite (affine_elim (lpred ↦ _)).
assert (sN ⊥ heapN) as Hdisj1 by (rewrite /sN; eauto with ndisj).
assert (sN ⊥ sheapN) as Hdisj2 by (rewrite /sN; eauto with ndisj).
assert (isN ⊥ sheapN) as ? by (rewrite /isN; eauto with ndisj).
assert (isN ⊥ heapN) as ? by (rewrite /isN; eauto with ndisj).
wp_load.
iDestruct "Hsts''" as "(Hlo&Hhd)".
refine_load d.
iExists (ticket_entered (S x)), ∅.
iSplitL "".
{ iPureIntro. apply enter_step1. }
iSplitL "Hlo".
{ iIntros "@". iNext. iFrame. done. }
iIntros "HstsEntered".
iPvs (sts_own_weaken _ γ _ (sts.up (ticket_entered (S x)) ∅) ∅
∅ with "HstsEntered") as "Hweaken"; eauto.
{ apply sts.elem_of_up. }
{ apply sts.closed_up. set_solver. }
iPvsIntro.
iSplitL "Hpred Hsts2'".
{ iIntros "@ >". iRight. iFrame. done. }
wp_let. refine_let d.
wp_if. refine_op d.
replace ((bool_decide (Z.pos (Pos.of_succ_nat x) = _))) with true; last first.
{ symmetry; apply bool_decide_true; done. }
wp_proj. refine_if_true (d' + 1).
iDestruct "Hhd" as "(HR&Hhd)".
iDestruct "Hhd" as (v) "Hhd".
wp_store. refine_delay d'.
iFrame. iSplitL ""; first auto.
rewrite /locked.
iExists lo', ln', lhd', ltl', lmine, (S x).
iSplitL ""; first auto.
iSplitL ""; first auto.
iFrame. done.
Qed.
Lemma acquire_spec i K (d d': nat) (γ: gname) (lks lk: val) R:
(d > 5 ∧ d ≤ Kd) →
(d' < Kd - 1) →
(is_lock γ lks lk R ★ ownT i (ticket.acquire lks) K d
⊢ WP (clh.acquire lk) {{ v, ⧆■(v = #()) ★ locked γ lks lk ★
ownT i (#())%E K d' ★ ⧆R}})%I.
Proof.
iIntros (Hd Hd') "(?&Hown)".
rewrite /ticket.acquire /clh.acquire.
rewrite /is_lock. iDestruct "~" as (lo ln lhd ltl) "(%&%&%&#?&#?&#?&#Hnext&Hbase&%&%)".
subst.
wp_lam. refine_lam d.
wp_alloc me as "Hme". refine_proj d.
wp_let. refine_delay (d-1).
wp_proj. refine_delay (d-2).
wp_focus (Swap _ _)%E.
iInv "Hnext" as "HnextOpen"; auto with fsaV.
rewrite {2}/next_inv.
iDestruct "HnextOpen" as (n l) "(Hn&Htl&Hold&Htoks)".
iTimeless "Hn". iTimeless "Htl".
rewrite affine_elim.
rewrite affine_elim.
assert (sN ⊥ heapN) as Hdisj1 by (rewrite /sN; eauto with ndisj).
assert (sN ⊥ sheapN) as Hdisj2 by (rewrite /sN; eauto with ndisj).
assert (inN ⊥ sheapN) as ? by (rewrite /inN; eauto with ndisj).
assert (inN ⊥ heapN) as ? by (rewrite /inN; eauto with ndisj).
wp_swap. rewrite -psvs_pvs'. refine_fai d.
iDestruct "Hme" as "(Hme1&Hme2)".
rewrite (affine_elim (sts_ownS _ _ _)).
assert (up_tok n ≡ up_tok (S n) ∪ ({[enter_tok n]} ∪ {[finish_tok n]})) as Htok_split.
{ set_unfold; split.
- intros (n'&[?|?]&Hge).
× inversion Hge; subst.
** right; auto.
** left. eexists. split; auto. omega.
× inversion Hge; subst.
** right; auto.
** left. eexists. split; auto. omega.
- intros [(n'&?&?)|?].
× ∃ n'. split; auto with arith.
× ∃ n. split; auto.
}
assert (sts.up (ticket_pre 0) (up_tok n) ⊆
sts.up (ticket_pre 0) (up_tok (S n)) ∩
sts.up (ticket_pre 0) ({[enter_tok n]} ∪ {[finish_tok n]})) as Hstate_split.
{ apply intersection_greatest.
- eapply sts.up_preserving; auto. apply up_tok_anti.
- eapply sts.up_preserving; auto. rewrite Htok_split. set_solver.
}
iPvs (sts_ownS_weaken _ _ _ _ _ _ with "Htoks") as "Htoks".
{ rewrite Htok_split; reflexivity. }
{ apply Hstate_split. }
{
eapply sts.closed_op.
- apply sts.closed_up. rewrite pre_init. set_solver.
- apply sts.closed_up. rewrite pre_init. set_solver.
}
rewrite sts_ownS_op; last 3 first.
{ set_unfold. intros x (n'&[?|?]&?) [?|?]; subst; try congruence;
(assert (n = n'); first by congruence); omega. }
{ eapply sts.closed_up. rewrite pre_init. set_solver. }
{ eapply sts.closed_up. rewrite pre_init. set_solver. }
iDestruct "Htoks" as "(HtoksUp&Htoksn)".
assert (sts.up (ticket_pre 0) ({[enter_tok n]} ∪ {[finish_tok n]}) ⊆
sts.up (ticket_pre 0) ({[enter_tok n]}) ∩
sts.up (ticket_pre 0) ({[finish_tok n]})) as Hstate_split'.
{ apply intersection_greatest; eapply sts.up_preserving; auto; set_solver. }
iPvs (sts_ownS_weaken _ _ _ _ _ _ with "Htoksn") as "Htoksn'".
{ reflexivity. }
{ apply Hstate_split'. }
{
eapply sts.closed_op.
- apply sts.closed_up. rewrite pre_init. set_solver.
- apply sts.closed_up. rewrite pre_init. set_solver.
}
rewrite sts_ownS_op; last 3 first.
{ set_unfold. intros; congruence. }
{ eapply sts.closed_up. rewrite pre_init. set_solver. }
{ eapply sts.closed_up. rewrite pre_init. set_solver. }
iDestruct "Htoksn'" as "(Henter&Hfinish)".
iPvs (inv_alloc isN _ (spin_inv γ lo lhd n me) with "[Hme1 Hfinish]") as "#Hinv".
{ rewrite /isN /inN. eauto with ndisj. }
{ rewrite /spin_inv. iIntros "@ >". iLeft. iFrame. done. }
iPvsIntro.
iSplitL "Htl Hn HtoksUp".
{ rewrite /next_inv. iIntros "@ >". iExists (S n)%nat, me.
replace (n + 1) with (S n) by omega.
replace (n+1)%Z with (Z.pos (Pos.of_succ_nat n)); last first.
{ rewrite Zpos_P_of_succ_nat. omega. }
iFrame; done. }
wp_let. refine_let d.
iPoseProof (wait_loop_spec i K d d' γ (#lo, #ln)%V (#lhd, #ltl) n
with "[Hbase Hme2 Henter Hown Hold]"); try done.
{ rewrite /ticket.wait_loop. iFrame "Hown".
rewrite /issued. iSplitL "Hbase".
- rewrite /is_lock. iExists lo, ln, lhd, ltl. iFrame.
repeat iSplitL ""; auto.
- iExists lo, ln, lhd, ltl.
rewrite affine_elim; iFrame. repeat iSplitL ""; auto.
}
Qed.
Lemma release_spec i K (d d': nat) (γ: gname) (lks lk: val) R:
(d > 5 ∧ d ≤ Kd) →
(d' < Kd - 1) →
(is_lock γ lks lk R ★ locked γ lks lk ★ ownT i (ticket.release lks) K d ★ ⧆R
⊢ WP (clh.release lk) {{ v, ⧆■(v = #()) ★ ownT i (#())%E K d'}})%I.
Proof.
iIntros (Hd Hd') "(Hlock&Hlocked&Hown&HR)".
rewrite /ticket.release /clh.release /is_lock /locked.
iDestruct "Hlock" as (lo ln lhd ltl) "(%&%&%&#?&#?&#?&#Hnext&Hbase&%&%)"; subst.
iDestruct "Hlocked" as (lo' ln' lhd' ltl' lmine x) "(%&%&Hsts&Hhd&Hmine&Hinv)"; subst.
wp_let.
assert (d ≤ Kd) as Hle by omega.
iPoseProof (refine_heap_pure_det_nofork d d Hle Hle _ K 3 _
((#lo <- ! #lo + #1)%E)
with "[Hown]") as "Hown"; try omega;
[ | | | iFrame; done | ]; auto.
{ intros σ.
eapply (nsteps_l _ _ _ ((Fst (#lo, #ln) <- ! (Fst (#lo, #ln)) + #1)%E, σ));
first do_prim_step.
eapply (nsteps_l _ _ _ ((#lo <- ! (Fst (#lo, #ln)) + #1)%E, σ));
first do_prim_step.
eapply (nsteps_once _ ((#lo <- ! #lo + #1)%E, σ));
first do_prim_step.
}
iPsvs "Hown".
iPvsIntro.
rewrite (sts_up_dup γ (ticket_entered x)). iDestruct "Hsts" as "(Hsts0&Hsts)".
iApply wp_pvs. wp_proj.
iInv "Hinv" as "Hspin"; auto with fsaV.
rewrite /spin_inv.
rewrite {1}later_or. rewrite affine_or.
iDestruct "Hspin" as "[?|?]"; last first.
{
iDestruct "Hspin" as "(Hfalse&?)".
iTimeless "Hfalse". rewrite (affine_elim (lmine ↦ _)).
iCombine "Hfalse" "Hmine" as "Hfalse".
rewrite heap_mapsto_op.
iDestruct "Hfalse" as "(%&?)".
congruence.
}
iDestruct "Hspin" as "(Hmine'&Hsts')".
iTimeless "Hsts'".
rewrite (affine_elim (sts_ownS _ _ _ )).
iCombine "Hsts" "Hsts'" as "Hsts".
rewrite -sts_ownS_op; last 3 first.
{ set_solver. }
{ apply sts.closed_up. set_solver. }
{ apply sts.closed_up. rewrite pre_init. set_solver. }
iPvs (sts_ownS_weaken _ γ _ {[ticket_entered x]} with "Hsts") as "Ho".
{ rewrite left_id. reflexivity. }
{ apply finish_upper_bound2. }
{ apply finish_closed2. }
rewrite -psvs_pvs'.
iSts γ as s Hin.
inversion Hin; subst.
rewrite {2}/sts_interp.
rewrite right_id.
iTimeless "Ho".
rewrite (affine_elim (lo ↦s _)). rewrite //=.
assert (sN ⊥ heapN) as Hdisj1 by (rewrite /sN; eauto with ndisj).
assert (sN ⊥ sheapN) as Hdisj2 by (rewrite /sN; eauto with ndisj).
assert (isN ⊥ sheapN) as ? by (rewrite /isN; eauto with ndisj).
assert (isN ⊥ heapN) as ? by (rewrite /isN; eauto with ndisj).
inversion H3; subst.
refine_load d.
iExists (ticket_entered x), {[finish_tok x]}.
iSplitL ""; first auto.
iSplitL "Ho".
{ iIntros "@ >". rewrite /sts_interp //=. iFrame. done. }
iIntros "Hsts".
iPvs (sts_own_weaken _ γ _ (sts.up (ticket_pre 0) {[finish_tok x]}) with "Hsts") as "Hsts".
{ reflexivity. }
{ apply finish_upper_bound3. }
{ apply sts.closed_up. set_unfold. intros t (n&[(?&?)|(?&?)]) Heq.
- subst. congruence.
- subst. inversion Heq; omega.
}
iPvsIntro.
iSplitL "Hmine' Hsts".
{ iIntros "@ >". iLeft. rewrite (affine_elim (lmine ↦{1/2} _)).
iFrame. done. }
wp_load. refine_op d.
iInv "Hinv" as "Hspin"; auto with fsaV.
iApply wp_pvs.
rewrite /spin_inv.
rewrite {1}later_or. rewrite affine_or.
iDestruct "Hspin" as "[?|?]"; last first.
{
iDestruct "Hspin" as "(Hfalse&?)".
iTimeless "Hfalse". rewrite (affine_elim (lmine ↦ _)).
iCombine "Hfalse" "Hmine" as "Hfalse".
rewrite heap_mapsto_op.
iDestruct "Hfalse" as "(%&?)".
congruence.
}
iDestruct "Hspin" as "(Hmine'&Hsts')".
iTimeless "Hsts'".
rewrite (affine_elim (sts_ownS _ _ _ )).
iCombine "Hsts0" "Hsts'" as "Hsts".
rewrite -sts_ownS_op; last 3 first.
{ set_solver. }
{ apply sts.closed_up. set_solver. }
{ apply sts.closed_up. rewrite pre_init. set_solver. }
iPvs (sts_ownS_weaken _ γ _ {[ticket_entered x]} with "Hsts") as "Ho".
{ rewrite left_id. reflexivity. }
{ apply finish_upper_bound2. }
{ apply finish_closed2. }
iSts γ as s Hin'.
inversion Hin'; subst.
rewrite {2}/sts_interp.
rewrite right_id.
iTimeless "Hmine'". iTimeless "Ho".
rewrite (affine_elim (lmine ↦{1/2} _)).
rewrite (affine_elim (lo ↦s _)). rewrite //=.
iCombine "Hmine" "Hmine'" as "Hmine".
rewrite heap_mapsto_op_eq.
replace (1/2 + 1/2)%Qp with 1%Qp by (auto using Qp_div_2).
wp_store. refine_store d'.
iExists (ticket_pre (S x)), ∅.
iSplitL ""; first auto.
{ iPureIntro. eapply finish_step1. }
iSplitL "Ho HR Hhd".
{ iIntros "@ >". rewrite /sts_interp //=.
rewrite Zpos_P_of_succ_nat. iFrame.
iExists (#lmine)%V. done. }
iIntros "Hsts".
iPvs (sts_own_weaken _ γ _ (sts.up (ticket_pre (S x)) ∅) with "Hsts") as "Hsts".
{ reflexivity. }
{ apply sts.elem_of_up. }
{ apply sts.closed_up. set_solver. }
iSplitL "Hmine Hsts".
{ iPvsIntro. iIntros "@ >". iRight. iFrame. done. }
do 2 iPvsIntro. iFrame. iPureIntro. done.
Qed.
End proof.
From iris.program_logic Require Import ownership auth sts saved_prop.
From iris.proofmode Require Import weakestpre invariants sts.
From iris.heap_lang Require Import heap proofmode notation refine_proofmode.
From iris.locks Require ticket clh.
Global Set Bullet Behavior "Strict Subproofs".
Section ticket_sts.
Local Open Scope nat_scope.
Inductive ticket_state :=
| ticket_pre: nat → ticket_state
| ticket_entered: nat → ticket_state.
Global Instance ticket_state_inhabited: Inhabited ticket_state :=
populate (ticket_pre O).
Definition owner (t: ticket_state) : nat :=
match t with
| ticket_pre n | ticket_entered n ⇒ n
end.
Inductive ticket_prim_step : relation ticket_state :=
| ticket_enter n: ticket_prim_step (ticket_pre n) (ticket_entered n)
| ticket_finish n: ticket_prim_step (ticket_entered n) (ticket_pre (S n)).
Inductive token := enter_tok (n: nat) | finish_tok (n: nat).
Definition tok (s: ticket_state) : set token :=
match s with
| ticket_pre n ⇒
{[ t | ∃ i, (t = enter_tok i ∧ i < n) ∨ (t = finish_tok i ∧ i < n) ]}
| ticket_entered n ⇒
{[ t | ∃ i, (t = enter_tok i ∧ i ≤ n) ∨ (t = finish_tok i ∧ i < n) ]}
end.
Global Arguments tok !_ /.
Canonical Structure sts := sts.STS ticket_prim_step tok.
Lemma enter_step0 n:
sts.step (ticket_pre n, {[enter_tok n]})
(ticket_entered n, ∅).
Proof.
constructor.
- constructor.
- set_unfold. intros ? (?&[(?&?)|(?&?)]) Heq; subst; inversion Heq; omega.
- set_unfold. intros ? (?&[(?&?)|(?&?)]) Heq; subst; inversion Heq; omega.
- set_unfold. split.
× intros [(?&[(?&?)|(?&?)])|?].
** subst. left. eexists. left. split; eauto; omega.
** subst. left. eexists. right. split; eauto; omega.
** subst. left. eexists. left. split; eauto; omega.
× intros [(n'&[(?&?)|(?&?)])|].
** assert (n' = n ∨ n' < n) as [-> | ] by omega.
*** naive_solver.
*** left. eexists. left. split; eauto.
** left. eexists. right. split; eauto; omega.
** intros; exfalso; auto.
Qed.
Lemma enter_step1 n:
sts.steps (ticket_pre n, {[enter_tok n]})
(ticket_entered n, ∅).
Proof. apply rtc_once, enter_step0. Qed.
Lemma enter_step2 n:
sts.steps (ticket_pre n, {[enter_tok n]} ∪ {[finish_tok n]})
(ticket_entered n, {[finish_tok n]}).
Proof.
apply rtc_once.
constructor.
- constructor.
- set_unfold. intros ? (?&[(?&?)|(?&?)]) [Heq|Heq]; subst; inversion Heq; omega.
- set_unfold. intros ? (?&[(?&?)|(?&?)]) Heq; subst; inversion Heq; omega.
- set_unfold. split.
× intros [(?&[(?&?)|(?&?)])|[?|?]].
** subst. left. eexists. left. split; eauto; omega.
** subst. left. eexists. right. split; eauto; omega.
** subst. left. eexists. left. split; eauto; omega.
** subst. right; done.
× intros [(n'&[(?&?)|(?&?)])| ->].
** assert (n' = n ∨ n' < n) as [-> | ] by omega.
*** naive_solver.
*** left. eexists. left. split; eauto.
** left. eexists. right. split; eauto; omega.
** auto.
Qed.
Lemma finish_step0 n:
sts.step (ticket_entered n, {[finish_tok n]})
(ticket_pre (S n), ∅).
Proof.
constructor.
- constructor.
- set_unfold. intros ? (?&[(?&?)|(?&?)]); subst; inversion 1. omega.
- set_unfold. intros ? (?&[(?&?)|(?&?)]) Heq; subst; inversion Heq; omega.
- set_unfold. split.
× intros [(?&[(?&?)|(?&?)])|?].
** subst. left. eexists. left. split; eauto; omega.
** subst. left. eexists. right. split; eauto; omega.
** subst. left. eexists. right. split; eauto; omega.
× intros [(n'&[(?&?)|(?&?)])|?]; last exfalso; auto.
** left. eexists. left. split; eauto. omega.
** assert (n' = n ∨ n' < n) as [-> | ] by omega.
*** naive_solver.
*** left. eexists. right. split; eauto.
Qed.
Lemma finish_step1 n:
sts.steps (ticket_entered n, {[finish_tok n]})
(ticket_pre (S n), ∅).
Proof. apply rtc_once, finish_step0. Qed.
Lemma pre_closed1 n:
sts.closed ({[ticket_pre n]}) ({[enter_tok n]}).
Proof.
split.
- set_unfold. intros n' →.
set_unfold. intros k (?&[(?&?)|(?&?)]) Heq; try congruence.
subst. inversion Heq; omega.
- set_unfold. intros ? s' →.
inversion 1 as [T1 T2 Hdisj Hstep].
inversion Hstep as [???? Hstep' ? Hdisj' Hconserve]; subst.
inversion Hstep'; subst.
exfalso.
eapply (Hdisj (enter_tok n)); set_unfold; eauto.
specialize (Hconserve (enter_tok n)). destruct Hconserve as [_ Hconserve].
destruct Hconserve as [(n'&[(Heq&?)|(Heq&?)]) |]; first by (left; naive_solver).
× inversion Heq. omega.
× inversion Heq.
× auto.
Qed.
Lemma pre_closed2 n:
sts.closed ({[ticket_pre n]}) ({[enter_tok n]} ∪ {[finish_tok n]}).
Proof.
split.
- set_unfold. intros n' →.
set_unfold. intros k (?&[(?&?)|(?&?)]) [Heq|Heq]; try congruence.
× subst. inversion Heq; omega.
× subst. inversion Heq; omega.
- set_unfold. intros ? s' →.
inversion 1 as [T1 T2 Hdisj Hstep].
inversion Hstep as [???? Hstep' ? Hdisj' Hconserve]; subst.
inversion Hstep'; subst.
exfalso.
eapply (Hdisj (enter_tok n)); set_unfold; eauto.
specialize (Hconserve (enter_tok n)). destruct Hconserve as [_ Hconserve].
destruct Hconserve as [(n'&[(Heq&?)|(Heq&?)]) |]; first by (left; naive_solver).
× inversion Heq. omega.
× inversion Heq.
× auto.
Qed.
Lemma finish_closed1 n:
sts.closed ({[ s | owner s ≤ n]}) ({[finish_tok n]}).
Proof.
split.
- set_unfold. intros x Hle n' Hin →.
move:Hin; destruct x; rewrite //=; set_unfold; intros (?&[(Heq&?)|(Heq&?)]).
× inversion Heq; congruence.
× inversion Heq; omega.
× inversion Heq; congruence.
× inversion Heq; omega.
- set_unfold. intros x x' Hle.
inversion 1 as [T1 T2 Hdisj Hstep].
inversion Hstep as [???? Hstep' ? Hdisj' Hconserve]; subst.
inversion Hstep'; subst; rewrite //= in Hle ×.
assert (S n0 ≤ n ∨ n < S n0) as [|] by omega; auto.
exfalso.
eapply (Hdisj (finish_tok n)); set_unfold; eauto.
specialize (Hconserve (finish_tok n)). destruct Hconserve as [_ Hconserve].
destruct Hconserve as [(n'&[(Heq&?)|(Heq&?)]) |]; first by (left; naive_solver).
× inversion Heq.
× inversion Heq. omega.
× auto.
Qed.
Lemma finish_upper_bound s x:
s ∈ sts.up (ticket_pre 0) {[finish_tok x]} → owner s ≤ x.
Proof.
intros Hin%(sts.up_subseteq (ticket_pre 0)); [ | eapply finish_closed1 | ];
set_unfold; (done || omega).
Qed.
Definition up_tok (k: nat) : set token :=
{[ t | ∃ n, (t = enter_tok n ∨ t = finish_tok n) ∧ n ≥ k]}.
Lemma up_tok_anti n:
up_tok (S n) ⊆ up_tok n.
Proof.
set_unfold. intros x (n'&[?|?]&?); ∃ n'; split; auto; omega.
Qed.
Lemma pre_init: sts.tok (ticket_pre O) ≡ ∅.
Proof.
set_unfold. intros ? (?&[(?&?)|(?&?)]); omega.
Qed.
Lemma up_tok_init: up_tok O ≡ ⊤.
Proof.
set_unfold; intros x. split; first done.
destruct x as [n|n]; ∃ n; split; eauto; omega.
Qed.
Lemma pre_subseteq_enter n:
tok (ticket_pre n) ⊆ tok (ticket_entered n).
Proof.
rewrite //=. set_unfold. intros t (x&[(?&?)|(?&?)]); subst.
- ∃ x. left. split; auto; omega.
- ∃ x. right. split; auto.
Qed.
Lemma enter_subseteq_pre n:
tok (ticket_entered n) ⊆ tok (ticket_pre (S n)).
Proof.
rewrite //=. set_unfold. intros t (x&[(?&?)|(?&?)]); subst.
- ∃ x. left. split; auto; omega.
- ∃ x. right. split; auto.
Qed.
Lemma frame_step_token_monotone T t1 t2:
rtc (sts.frame_step T) t1 t2 →
tok t1 ⊆ tok t2.
Proof.
induction 1 as [| ??? Hfstep ? IHrtc]; first done.
inversion Hfstep as [?? Hdisj Hstep]. inversion Hstep as [???? Hprim]; subst.
inversion Hprim; subst.
- etransitivity; last apply IHrtc. apply pre_subseteq_enter.
- etransitivity; last apply IHrtc. apply enter_subseteq_pre.
Qed.
Lemma frame_step_owner_monotone T t1 t2:
rtc (sts.frame_step T) t1 t2 →
owner t1 ≤ owner t2.
Proof.
induction 1 as [| ??? Hfstep ? IHrtc]; first done.
inversion Hfstep as [?? Hdisj Hstep]. inversion Hstep as [???? Hprim]; subst.
inversion Hprim; subst.
- etransitivity; last apply IHrtc. rewrite //=.
- etransitivity; last apply IHrtc. rewrite //=. omega.
Qed.
Lemma frame_step_owner_monotone' T n n':
rtc (sts.frame_step T) (ticket_entered n) (ticket_pre n') →
n < n'.
Proof.
remember (ticket_entered n) as te eqn:Heqn.
remember (ticket_pre n') as tp eqn:Heqn'.
intros Hrtc. revert n n' Heqn Heqn'.
induction Hrtc as [| ??? Hfstep ? IHrtc]; first (intros; congruence).
inversion Hfstep as [?? Hdisj Hstep]. inversion Hstep as [???? Hprim]; subst.
inversion Hprim; subst.
- intros. congruence.
- intros. inversion Heqn. subst.
apply frame_step_owner_monotone in Hrtc. simpl in ×. omega.
Qed.
Lemma pre_step_entered T n t:
(sts.frame_step T) (ticket_pre n) t →
t = ticket_entered n.
Proof.
inversion 1 as [?? Hdisj Hstep]. inversion Hstep as [???? Hprim]; subst.
inversion Hprim; subst. done.
Qed.
Lemma owner_contains_enter_lt t:
∀ n', n' < owner t → enter_tok n' ∈ tok t.
Proof.
intros n' Hlt. destruct t; set_unfold; ∃ n'.
- naive_solver.
- left. split; auto. omega.
Qed.
Lemma owner_contains_finish_lt t:
∀ n', n' < owner t → finish_tok n' ∈ tok t.
Proof.
intros n' Hlt. destruct t; set_unfold; ∃ n'.
- naive_solver.
- right. split; auto.
Qed.
Lemma rtc_ticket_pre_tok n t:
rtc (sts.frame_step ∅) (ticket_pre n) t →
t = ticket_pre n ∨ ∀ n', n' ≤ n → enter_tok n' ∈ tok t.
Proof.
intros Hrtc%frame_step_owner_monotone.
inversion Hrtc.
- destruct t.
× left. simpl in *; subst; done.
× right. simpl in ×. intros.
set_unfold. ∃ n'. left; naive_solver.
- right. intros. simpl in ×. apply owner_contains_enter_lt. omega.
Qed.
Lemma rtc_ticket_entered_tok n t:
rtc (sts.frame_step ∅) (ticket_entered n) t →
t = ticket_entered n ∨ ∀ n', n' ≤ n → finish_tok n' ∈ tok t.
Proof.
intros Hrtc.
destruct t.
- apply frame_step_owner_monotone' in Hrtc.
right. intros n' Hle. set_unfold. eexists. right. split; auto. omega.
- eapply frame_step_owner_monotone in Hrtc. simpl in ×.
inversion Hrtc.
× left. subst. auto.
× right. subst. intros. set_unfold. eexists. right. split; auto.
omega.
Qed.
Lemma pre_upper_bound n:
(sts.up (ticket_pre n) ∅ ∩ sts.up (ticket_pre 0) {[enter_tok n]})
⊆ {[ ticket_pre n]}.
Proof.
intros t (Hup1&Hup2)%elem_of_intersection.
apply sts.closed_up in Hup2; last (rewrite pre_init; set_solver).
set_unfold. apply rtc_ticket_pre_tok in Hup1 as [|]; first done.
exfalso; eapply (Hup2 (enter_tok n)); naive_solver.
Qed.
Lemma finish_upper_bound2 n:
(sts.up (ticket_entered n) ∅ ∩ sts.up (ticket_pre 0) {[finish_tok n]})
⊆ {[ ticket_entered n]}.
Proof.
intros t (Hup1&Hup2)%elem_of_intersection.
apply sts.closed_up in Hup2; last (rewrite pre_init; set_solver).
set_unfold. apply rtc_ticket_entered_tok in Hup1 as [|]; first done.
exfalso; eapply (Hup2 (finish_tok n)); auto.
Qed.
Lemma finish_upper_bound3 n:
ticket_entered n ∈ sts.up (ticket_pre 0) {[finish_tok n]}.
Proof.
cut (∀ k m, k ≤ m → ticket_entered k ∈ sts.up (ticket_pre 0) {[finish_tok m]});
first by eauto.
clear n. induction k; set_unfold⇒ m Hle.
- eapply rtc_once.
eapply (sts.Frame_step) with (T1 := {[enter_tok 0]}).
× set_unfold. intros ? → [(?&[?|(?&?)])|].
** omega.
** congruence.
** congruence.
× eapply enter_step0.
- eapply rtc_r; first eapply rtc_r; first (eapply IHk; omega).
× eapply (sts.Frame_step) with (T1 := {[finish_tok k]}).
** set_unfold. intros ??; subst.
intros [(n&[(Heq&?)|(Heq&?)])|Heq]; try congruence; inversion Heq; omega.
** eapply finish_step0.
× eapply (sts.Frame_step) with (T1 := {[enter_tok (S k)]}).
** set_unfold. intros ??; subst.
intros [(n&[(Heq&?)|(Heq&?)])|Heq]; try congruence; inversion Heq; omega.
** eapply enter_step0.
Qed.
Lemma finish_closed2 n:
sts.closed {[ ticket_entered n ]} ({[finish_tok n]}).
Proof.
split.
- set_unfold. intros x Heq0 n' Hin ->; subst.
move:Hin; rewrite //=; set_unfold; intros (?&[(Heq&?)|(Heq&?)]).
× inversion Heq; congruence.
× inversion Heq; omega.
- set_unfold. intros x x' Heq0; subst.
inversion 1 as [T1 T2 Hdisj Hstep].
inversion Hstep as [???? Hstep' ? Hdisj' Hconserve]; subst.
inversion Hstep'; subst.
exfalso.
eapply (Hdisj (finish_tok n)); set_unfold; eauto.
specialize (Hconserve (finish_tok n)). destruct Hconserve as [_ Hconserve].
destruct Hconserve as [(n'&[(Heq&?)|(Heq&?)]) |]; first by (left; naive_solver).
× inversion Heq.
× inversion Heq. omega.
× auto.
Qed.
End ticket_sts.
Class tlockG Σ := TicketG {
tlock_stsG :> stsG lang.heap_lang Σ sts;
}.
Definition tlockGF : gFunctorList := [stsGF sts].
Instance inGF_tlockG `{H : inGFs lang.heap_lang Σ tlockGF} : tlockG Σ.
Proof. destruct H as (?). split; apply _. Qed.
Section proof.
Context `{!heapG Σ, !sheapG heap_lang Σ, !tlockG Σ} (N : namespace).
Context `{!refineG heap_lang Σ (delayed_lang (heap_lang) Kd Fd) (S Kd × (Kd + 3))}.
Context (Hgt: 99 < Kd).
Local Notation iProp := (iPropG heap_lang Σ).
Definition sN : namespace := N .@ "sts".
Definition inN : namespace := N .@ "inv_next".
Definition isN : namespace := N .@ "inv_spin".
Definition sts_interp (lo lhd: loc) (R: iProp) (t: ticket_state) : iProp :=
(lo ↦s #(owner t) ★
match t with
| ticket_pre n ⇒ ⧆R ★ ∃ v, lhd ↦ v
| ticket_entered n ⇒ Emp
end)%I.
Definition owner_sts_ctx γ lo lhd R :=
(⧆■ (heapN ⊥ N) ★ ⧆■(sheapN ⊥ N) ★ ⧆■(heapN ⊥ sheapN)
★ heap_ctx ★ sheap_ctx ★ sts_ctx γ sN (sts_interp lo lhd R))%I.
Definition spin_inv (γ: gname) (lo lhd: loc) (o: nat) (l: loc) : iProp :=
((l ↦{1/2} #true ★ sts_ownS γ (sts.up (ticket_pre O) {[finish_tok o]}) {[finish_tok o]})
∨ (l ↦ #false ★ sts_ownS γ (sts.up (ticket_pre (S o)) ∅) ∅))%I.
Definition next_inv (γ: gname) (lo lhd: loc) (ln ltl: loc) : iProp :=
(∃ (n: nat) (l: loc),
ln ↦s #n ★ ltl ↦ #l ★
match n with
| O ⇒ l ↦ #false
| S n' ⇒ inv isN (spin_inv γ lo lhd n' l)
end ★
sts_ownS γ (sts.up (ticket_pre O) (up_tok n)) (up_tok n))%I.
Local Open Scope nat_scope.
Definition is_lock (γ : gname) (lks lk: val) (R: iProp) : iProp :=
(∃ lo ln lhd ltl : loc,
(⧆■ (heapN ⊥ N) ★ ⧆■(sheapN ⊥ N) ★ ⧆■(heapN ⊥ sheapN)
★ heap_ctx ★ sheap_ctx ★ sts_ctx γ sN (sts_interp lo lhd R) ★
inv inN (next_inv γ lo lhd ln ltl) ★
sts_ownS γ (sts.up (ticket_pre O) ∅) ∅ ★
⧆■(lks = (#lo, #ln)%V) ★
⧆■(lk = (#lhd, #ltl)%V)))%I.
Definition issued (γ : gname) (lks lk: val) (x : nat) (lpred lmine: loc) : iProp :=
(∃ lo ln lhd ltl : loc,
⧆■(lks = (#lo, #ln)%V) ★
⧆■(lk = (#lhd, #ltl)%V) ★
(sts_ownS γ (sts.up (ticket_pre O) {[enter_tok x]}) {[enter_tok x]} ★
match x with
| O ⇒ lpred ↦ #false
| S x' ⇒ inv isN (spin_inv γ lo lhd x' lpred)
end ★
lmine ↦{1/2} #true ★
inv isN (spin_inv γ lo lhd x lmine)))%I.
Definition locked (γ : gname) (lks lk: val) : iProp :=
(∃ (lo ln lhd ltl lmine : loc) (x: nat),
⧆■(lks = (#lo, #ln)%V) ★
⧆■(lk = (#lhd, #ltl)%V) ★
(sts_ownS γ (sts.up (ticket_entered x) ∅) ∅ ★
lhd ↦ #lmine ★
lmine ↦{1/2} #true ★
inv isN (spin_inv γ lo lhd x lmine)))%I.
Import uPred.
Lemma newlock_spec i K d d' R:
(d > 5 ∧ d ≤ Kd) →
(d' ≤ Kd)%nat →
heapN ⊥ N →
sheapN ⊥ N →
(heap_ctx ★ sheap_ctx ★ ownT i (ticket.newlock #()) K d ★ ⧆R
⊢ WP clh.newlock #() {{ lk, ∃ lks γ, is_lock γ lks lk R ★
ownT i (of_val lks) K d'}})%I.
Proof.
iIntros (Hd Hd' HN1 HN2) "(#?&#?&Hown&HR)".
rewrite /ticket.newlock /clh.newlock.
wp_let. refine_let d.
wp_alloc dummy as "Hd". refine_alloc d lo as "Ho".
wp_let. refine_delay (d-1).
wp_alloc lhd as "Hhd". refine_delay (d-2).
wp_alloc ltl as "Htl". refine_alloc d' ln as "Hn".
wp_value; iExists (#lo, #ln)%V; iFrame.
assert (nclose sN ⊆ ⊤) as Hdisj; eauto with ndisj.
iPoseProof (sts_alloc (sts_interp lo lhd R) ⊤ sN (ticket_pre O) Hdisj) as "Hsts".
iPvs ("Hsts" with "[HR Ho Hhd]") as (γ) "(Hsts&Htok)"; clear Hdisj.
{ rewrite /sts_interp //=. iIntros "@". iNext. iFrame. iExists #dummy; done. }
rewrite pre_init.
setoid_replace (⊤ ∖ ∅: sts.tokens sts) with (⊤: sts.tokens sts)
by (set_unfold; naive_solver).
rewrite /is_lock.
iPvs (sts_own_weaken _ γ _ ((sts.up (ticket_pre 0) ⊤) ∩ (sts.up (ticket_pre 0) ∅))
_ (⊤ ∪ ∅)
with "Htok") as "Htok"; eauto.
{ split; eauto using sts.elem_of_up. }
{ rewrite subseteq_intersection_1; last (eapply sts.up_preserving; set_solver).
rewrite comm subseteq_union_1; eauto.
eapply sts.closed_up. rewrite pre_init. set_solver. }
rewrite sts_ownS_op.
- iDestruct "Htok" as "(Htok1&Htok2)".
assert (nclose inN ⊆ ⊤) as Hdisj; eauto with ndisj.
iPoseProof (inv_alloc inN ⊤ (next_inv γ lo lhd ln ltl) Hdisj) as "Hinv".
iPvs ("Hinv" with "[Hn Hd Htl Htok1]") as "Hinv"; clear Hdisj.
{ rewrite /next_inv //=. iIntros "@". iNext. iExists O. iExists dummy.
iFrame. rewrite up_tok_init. done. }
iPvsIntro. iExists γ, lo, ln, lhd, ltl. iFrame.
rewrite ?pure_equiv //; first (rewrite -?emp_True ?left_id ?right_id; iSplit; auto).
eauto with ndisj.
- set_solver.
- eapply sts.closed_up. rewrite pre_init. set_solver.
- eapply sts.closed_up. rewrite pre_init. set_solver.
Qed.
Instance issued_affine: AffineP (issued γ lks lk x lpred lmine).
Proof.
rewrite /issued; intros; destruct x; apply _.
Qed.
Instance is_lock_affine: AffineP (is_lock γ lks lk R).
Proof.
rewrite /is_lock; intros; apply _.
Qed.
Instance locked_affine: AffineP (locked γ lks lk).
Proof.
rewrite /is_lock; intros; apply _.
Qed.
Instance sts_empty_relevant: RelevantP (sts_ownS γ (sts.up s ∅) ∅).
Proof.
rewrite /RelevantP /sts_ownS ⇒ γ n.
apply own_core_persistent.
rewrite /Persistent /pcore /cmra_pcore //=.
rewrite /dra.validity_pcore //=.
rewrite //=. econstructor.
rewrite /sts_frag //=. econstructor; rewrite //=.
intros. rewrite /core /dra.dra_core //=.
rewrite sts.up_closed //. apply sts.closed_up. set_solver.
Qed.
Lemma sts_up_dup γ s:
sts_ownS γ (sts.up s ∅) ∅ ⊢
(sts_ownS γ (sts.up s ∅) ∅ ★
sts_ownS γ (sts.up s ∅) ∅)%I.
Proof.
apply relevant_sep_dup, _.
Qed.
Instance is_lock_relevant: RelevantP (is_lock γ lks lk R).
Proof.
rewrite /is_lock; intros. apply _.
Qed.
Global Instance sts_ownS_timeless S T : ATimelessP (sts_ownS γ S T).
Proof. intros γ. rewrite /sts_ownS. apply _. Qed.
Instance affine_match_state:
AffineP (match s' with
| ticket_pre _ ⇒ ⧆R ★ ∃ v : val, lhd' ↦ v
| ticket_entered _ ⇒ Emp
end).
Proof. destruct s'; apply _. Qed.
Instance affine_match_nat:
AffineP (match n with
| O ⇒ l ↦ #false
| S n' ⇒ inv isN (spin_inv γ lo lhd n' l)
end).
Proof. destruct n; apply _. Qed.
Ltac do_prim_step :=
match goal with
| [ |- ?e1 = fill ?K ?e2 ] ⇒
auto; (try reshape_expr e1 ltac:(fun K' e' ⇒ unify K K'; done))
| [ |- prim_step_nofork heap_lang (?e, ?σ) _] ⇒
reshape_expr e ltac:(fun K' e' ⇒
eapply (Ectx_step _ _ _ _ _ K' e');
[ eauto | rewrite //= | do_head_step eauto ])
end.
Lemma wait_loop_spec i K (d d': nat) (γ: gname) (lks lk: val) (x: nat) (lpred lmine: loc) R:
(d > 5 ∧ d ≤ Kd) →
(d' < Kd - 1) →
(is_lock γ lks lk R ★ issued γ lks lk x lpred lmine ★
ownT i (ticket.wait_loop #x lks) K d
⊢ WP (clh.wait_loop #lmine #lpred lk) {{ v, ⧆■(v = #()) ★ locked γ lks lk ★
ownT i (#())%E K d' ★ ⧆R}})%I.
Proof.
iIntros (Hd Hd') "(?&?&Hown)".
iLob as "IH".
iIntros "@ ! ? ? Hown".
refine_focus (ticket.wait_loop #x%E).
rewrite {2}/is_lock. iDestruct "~" as (lo ln lhd ltl) "(%&%&%&#?&#?&#?&#?&?&%&%)".
wp_rec. refine_rec d.
wp_value; refine_unfocus; iPvsIntro.
wp_lam. refine_lam d.
wp_value; iPvsIntro.
rewrite /issued. iDestruct "~1" as (lo' ln' lhd' ltl') "(%&%&Hsts&Hx&Hmine&Hinv)".
subst. inversion H5; subst. inversion H4; subst.
wp_lam.
destruct x; refine_proj d.
- iClear "IH".
wp_focus (! #lpred)%E.
iSts γ as s Hin.
rewrite /sts_interp.
rewrite {1}sts.up_up_set in Hin ×.
rewrite sts.up_closed; last apply pre_closed1. inversion 1; subst.
iDestruct "Hsts" as "(Hlo&Hhd)".
assert (sN ⊥ heapN) as Hdisj1 by (rewrite /sN; eauto with ndisj).
assert (sN ⊥ sheapN) as Hdisj2 by (rewrite /sN; eauto with ndisj).
wp_load.
rewrite (affine_elim (lo' ↦s #0)). refine_load d.
iExists (ticket_entered 0). iExists ∅.
iSplitL "".
{ iPureIntro. apply enter_step1. }
iSplitL "Hlo".
{ iIntros "@". iNext. iFrame. done. }
iIntros "Hsts".
wp_let. refine_let d.
wp_if. refine_op d.
wp_proj. refine_delay (d-1).
iDestruct "Hhd" as "(HR&Hhd)".
iDestruct "Hhd" as (v0) "Hhd".
rewrite sts_own_weaken.
× iPvs "Hsts".
wp_store. refine_if_true d'.
iFrame. iSplitL ""; first done.
rewrite /locked. iExists lo', ln', lhd', ltl', lmine, 0.
iSplitL ""; first done.
iSplitL ""; first done.
iFrame. done.
× set_solver.
× apply sts.elem_of_up.
× apply sts.closed_up. set_solver.
- iDestruct "Hx" as "#Hx".
wp_focus (! #lpred)%E.
iInv "Hx" as "Hspin"; auto with fsaV.
rewrite /spin_inv //=.
rewrite {1}later_or.
rewrite affine_or.
iDestruct "Hspin" as "[?|?]".
×
iDestruct "Hspin" as "(Hpred&Hsts')".
iTimeless "Hpred". iTimeless "Hsts'".
iApply wp_pvs.
rewrite (affine_elim (sts_ownS _ _ _)).
iSts γ as s' Hin'.
assert (owner s' ≤ x) by (eauto using finish_upper_bound).
rewrite /sts_interp.
rewrite (affine_elim (lpred ↦{1/2} _)).
assert (sN ⊥ heapN) as Hdisj1 by (rewrite /sN; eauto with ndisj).
assert (sN ⊥ sheapN) as Hdisj2 by (rewrite /sN; eauto with ndisj).
assert (isN ⊥ sheapN) as ? by (rewrite /isN; eauto with ndisj).
assert (isN ⊥ heapN) as ? by (rewrite /isN; eauto with ndisj).
wp_load.
iDestruct "Hsts'" as "(Hlo&Hhd)".
refine_load d'.
iExists s', {[finish_tok x]}.
iSplitL "".
{ iPureIntro. done. }
iSplitL "Hlo Hhd".
{ iIntros "@". iNext. iFrame. done. }
iIntros "Hsts'".
iPvs (sts_own_weaken _ γ s' (sts.up (ticket_pre 0) {[finish_tok x]}) {[finish_tok x]}
{[finish_tok x]} with "Hsts'") as "Hweaken"; eauto.
{ apply sts.closed_up. set_unfold. intros ? (?&[(?&?)|(?&?)]). congruence.
omega. }
iPvsIntro.
iSplitL "Hweaken Hpred".
{ iIntros "@ >". iLeft; iFrame; done. }
wp_let. refine_let d.
wp_if.
assert (d ≤ Kd) as Hle by omega.
iPoseProof (refine_heap_pure_det_nofork d d Hle Hle _ K 2 _
(ticket.wait_loop #(S x) (#lo', #ln')%E)
with "[Hown]") as "Hown";
[ | | | | iFrame | ]; auto.
{ omega. }
{ intros.
eapply (nsteps_l _ _ _
((if: #false then #()
else (rec: "wait_loop" "x" "lk"
:= let: "o" := ! (Fst "lk")
in if: "x" = "o" then #() else ("wait_loop" "x") "lk")
#(Z.pos (Pos.of_succ_nat x)) (#lo', #ln'))%E, σ)).
{ eapply Ectx_step with (e1' := ((#(Z.pos (Pos.of_succ_nat x))%E = #(owner s'))%E))
(e2' := #false); simpl; try do_prim_step.
econstructor. rewrite //=; f_equal.
replace ((bool_decide (Z.pos (Pos.of_succ_nat x) = owner s'))) with false; auto.
symmetry; apply bool_decide_false. rewrite Zpos_P_of_succ_nat. omega. }
eapply nsteps_once; do_prim_step.
}
iPsvs "Hown". iPvsIntro.
iSpecialize ("IH" with "[~5]").
{ rewrite /is_lock.
iExists lo', ln', lhd', ltl'. iFrame.
repeat (iSplitL; auto). }
iSpecialize ("IH" with "[Hsts Hmine Hinv] Hown").
{
iExists lo', ln', lhd', ltl'. iFrame.
repeat (iSplitL; auto).
}
iAssumption.
×
iDestruct "Hspin" as "(Hpred&Hsts')".
iTimeless "Hpred". iTimeless "Hsts'".
iApply wp_pvs.
rewrite (affine_elim (sts_ownS _ _ _)).
iPoseProof (sts_up_dup γ (ticket_pre (S x)) with "Hsts'") as "Hsts'".
iDestruct "Hsts'" as "(Hsts1'&Hsts2')".
iCombine "Hsts1'" "Hsts" as "Hsts''".
rewrite -sts.sts_ownS_op; last 3 first.
{ set_solver. }
{ apply sts.closed_up. set_solver. }
{ apply sts.closed_up. rewrite pre_init. set_solver. }
iPvs (sts_ownS_weaken _ γ _ {[ticket_pre (S x)]} with "Hsts''") as "Hsts''".
{ rewrite left_id; reflexivity. }
{ apply pre_upper_bound. }
{ apply pre_closed1. }
iSts γ as s' Hin'.
inversion Hin'. subst.
rewrite /sts_interp.
rewrite (affine_elim (lpred ↦ _)).
assert (sN ⊥ heapN) as Hdisj1 by (rewrite /sN; eauto with ndisj).
assert (sN ⊥ sheapN) as Hdisj2 by (rewrite /sN; eauto with ndisj).
assert (isN ⊥ sheapN) as ? by (rewrite /isN; eauto with ndisj).
assert (isN ⊥ heapN) as ? by (rewrite /isN; eauto with ndisj).
wp_load.
iDestruct "Hsts''" as "(Hlo&Hhd)".
refine_load d.
iExists (ticket_entered (S x)), ∅.
iSplitL "".
{ iPureIntro. apply enter_step1. }
iSplitL "Hlo".
{ iIntros "@". iNext. iFrame. done. }
iIntros "HstsEntered".
iPvs (sts_own_weaken _ γ _ (sts.up (ticket_entered (S x)) ∅) ∅
∅ with "HstsEntered") as "Hweaken"; eauto.
{ apply sts.elem_of_up. }
{ apply sts.closed_up. set_solver. }
iPvsIntro.
iSplitL "Hpred Hsts2'".
{ iIntros "@ >". iRight. iFrame. done. }
wp_let. refine_let d.
wp_if. refine_op d.
replace ((bool_decide (Z.pos (Pos.of_succ_nat x) = _))) with true; last first.
{ symmetry; apply bool_decide_true; done. }
wp_proj. refine_if_true (d' + 1).
iDestruct "Hhd" as "(HR&Hhd)".
iDestruct "Hhd" as (v) "Hhd".
wp_store. refine_delay d'.
iFrame. iSplitL ""; first auto.
rewrite /locked.
iExists lo', ln', lhd', ltl', lmine, (S x).
iSplitL ""; first auto.
iSplitL ""; first auto.
iFrame. done.
Qed.
Lemma acquire_spec i K (d d': nat) (γ: gname) (lks lk: val) R:
(d > 5 ∧ d ≤ Kd) →
(d' < Kd - 1) →
(is_lock γ lks lk R ★ ownT i (ticket.acquire lks) K d
⊢ WP (clh.acquire lk) {{ v, ⧆■(v = #()) ★ locked γ lks lk ★
ownT i (#())%E K d' ★ ⧆R}})%I.
Proof.
iIntros (Hd Hd') "(?&Hown)".
rewrite /ticket.acquire /clh.acquire.
rewrite /is_lock. iDestruct "~" as (lo ln lhd ltl) "(%&%&%&#?&#?&#?&#Hnext&Hbase&%&%)".
subst.
wp_lam. refine_lam d.
wp_alloc me as "Hme". refine_proj d.
wp_let. refine_delay (d-1).
wp_proj. refine_delay (d-2).
wp_focus (Swap _ _)%E.
iInv "Hnext" as "HnextOpen"; auto with fsaV.
rewrite {2}/next_inv.
iDestruct "HnextOpen" as (n l) "(Hn&Htl&Hold&Htoks)".
iTimeless "Hn". iTimeless "Htl".
rewrite affine_elim.
rewrite affine_elim.
assert (sN ⊥ heapN) as Hdisj1 by (rewrite /sN; eauto with ndisj).
assert (sN ⊥ sheapN) as Hdisj2 by (rewrite /sN; eauto with ndisj).
assert (inN ⊥ sheapN) as ? by (rewrite /inN; eauto with ndisj).
assert (inN ⊥ heapN) as ? by (rewrite /inN; eauto with ndisj).
wp_swap. rewrite -psvs_pvs'. refine_fai d.
iDestruct "Hme" as "(Hme1&Hme2)".
rewrite (affine_elim (sts_ownS _ _ _)).
assert (up_tok n ≡ up_tok (S n) ∪ ({[enter_tok n]} ∪ {[finish_tok n]})) as Htok_split.
{ set_unfold; split.
- intros (n'&[?|?]&Hge).
× inversion Hge; subst.
** right; auto.
** left. eexists. split; auto. omega.
× inversion Hge; subst.
** right; auto.
** left. eexists. split; auto. omega.
- intros [(n'&?&?)|?].
× ∃ n'. split; auto with arith.
× ∃ n. split; auto.
}
assert (sts.up (ticket_pre 0) (up_tok n) ⊆
sts.up (ticket_pre 0) (up_tok (S n)) ∩
sts.up (ticket_pre 0) ({[enter_tok n]} ∪ {[finish_tok n]})) as Hstate_split.
{ apply intersection_greatest.
- eapply sts.up_preserving; auto. apply up_tok_anti.
- eapply sts.up_preserving; auto. rewrite Htok_split. set_solver.
}
iPvs (sts_ownS_weaken _ _ _ _ _ _ with "Htoks") as "Htoks".
{ rewrite Htok_split; reflexivity. }
{ apply Hstate_split. }
{
eapply sts.closed_op.
- apply sts.closed_up. rewrite pre_init. set_solver.
- apply sts.closed_up. rewrite pre_init. set_solver.
}
rewrite sts_ownS_op; last 3 first.
{ set_unfold. intros x (n'&[?|?]&?) [?|?]; subst; try congruence;
(assert (n = n'); first by congruence); omega. }
{ eapply sts.closed_up. rewrite pre_init. set_solver. }
{ eapply sts.closed_up. rewrite pre_init. set_solver. }
iDestruct "Htoks" as "(HtoksUp&Htoksn)".
assert (sts.up (ticket_pre 0) ({[enter_tok n]} ∪ {[finish_tok n]}) ⊆
sts.up (ticket_pre 0) ({[enter_tok n]}) ∩
sts.up (ticket_pre 0) ({[finish_tok n]})) as Hstate_split'.
{ apply intersection_greatest; eapply sts.up_preserving; auto; set_solver. }
iPvs (sts_ownS_weaken _ _ _ _ _ _ with "Htoksn") as "Htoksn'".
{ reflexivity. }
{ apply Hstate_split'. }
{
eapply sts.closed_op.
- apply sts.closed_up. rewrite pre_init. set_solver.
- apply sts.closed_up. rewrite pre_init. set_solver.
}
rewrite sts_ownS_op; last 3 first.
{ set_unfold. intros; congruence. }
{ eapply sts.closed_up. rewrite pre_init. set_solver. }
{ eapply sts.closed_up. rewrite pre_init. set_solver. }
iDestruct "Htoksn'" as "(Henter&Hfinish)".
iPvs (inv_alloc isN _ (spin_inv γ lo lhd n me) with "[Hme1 Hfinish]") as "#Hinv".
{ rewrite /isN /inN. eauto with ndisj. }
{ rewrite /spin_inv. iIntros "@ >". iLeft. iFrame. done. }
iPvsIntro.
iSplitL "Htl Hn HtoksUp".
{ rewrite /next_inv. iIntros "@ >". iExists (S n)%nat, me.
replace (n + 1) with (S n) by omega.
replace (n+1)%Z with (Z.pos (Pos.of_succ_nat n)); last first.
{ rewrite Zpos_P_of_succ_nat. omega. }
iFrame; done. }
wp_let. refine_let d.
iPoseProof (wait_loop_spec i K d d' γ (#lo, #ln)%V (#lhd, #ltl) n
with "[Hbase Hme2 Henter Hown Hold]"); try done.
{ rewrite /ticket.wait_loop. iFrame "Hown".
rewrite /issued. iSplitL "Hbase".
- rewrite /is_lock. iExists lo, ln, lhd, ltl. iFrame.
repeat iSplitL ""; auto.
- iExists lo, ln, lhd, ltl.
rewrite affine_elim; iFrame. repeat iSplitL ""; auto.
}
Qed.
Lemma release_spec i K (d d': nat) (γ: gname) (lks lk: val) R:
(d > 5 ∧ d ≤ Kd) →
(d' < Kd - 1) →
(is_lock γ lks lk R ★ locked γ lks lk ★ ownT i (ticket.release lks) K d ★ ⧆R
⊢ WP (clh.release lk) {{ v, ⧆■(v = #()) ★ ownT i (#())%E K d'}})%I.
Proof.
iIntros (Hd Hd') "(Hlock&Hlocked&Hown&HR)".
rewrite /ticket.release /clh.release /is_lock /locked.
iDestruct "Hlock" as (lo ln lhd ltl) "(%&%&%&#?&#?&#?&#Hnext&Hbase&%&%)"; subst.
iDestruct "Hlocked" as (lo' ln' lhd' ltl' lmine x) "(%&%&Hsts&Hhd&Hmine&Hinv)"; subst.
wp_let.
assert (d ≤ Kd) as Hle by omega.
iPoseProof (refine_heap_pure_det_nofork d d Hle Hle _ K 3 _
((#lo <- ! #lo + #1)%E)
with "[Hown]") as "Hown"; try omega;
[ | | | iFrame; done | ]; auto.
{ intros σ.
eapply (nsteps_l _ _ _ ((Fst (#lo, #ln) <- ! (Fst (#lo, #ln)) + #1)%E, σ));
first do_prim_step.
eapply (nsteps_l _ _ _ ((#lo <- ! (Fst (#lo, #ln)) + #1)%E, σ));
first do_prim_step.
eapply (nsteps_once _ ((#lo <- ! #lo + #1)%E, σ));
first do_prim_step.
}
iPsvs "Hown".
iPvsIntro.
rewrite (sts_up_dup γ (ticket_entered x)). iDestruct "Hsts" as "(Hsts0&Hsts)".
iApply wp_pvs. wp_proj.
iInv "Hinv" as "Hspin"; auto with fsaV.
rewrite /spin_inv.
rewrite {1}later_or. rewrite affine_or.
iDestruct "Hspin" as "[?|?]"; last first.
{
iDestruct "Hspin" as "(Hfalse&?)".
iTimeless "Hfalse". rewrite (affine_elim (lmine ↦ _)).
iCombine "Hfalse" "Hmine" as "Hfalse".
rewrite heap_mapsto_op.
iDestruct "Hfalse" as "(%&?)".
congruence.
}
iDestruct "Hspin" as "(Hmine'&Hsts')".
iTimeless "Hsts'".
rewrite (affine_elim (sts_ownS _ _ _ )).
iCombine "Hsts" "Hsts'" as "Hsts".
rewrite -sts_ownS_op; last 3 first.
{ set_solver. }
{ apply sts.closed_up. set_solver. }
{ apply sts.closed_up. rewrite pre_init. set_solver. }
iPvs (sts_ownS_weaken _ γ _ {[ticket_entered x]} with "Hsts") as "Ho".
{ rewrite left_id. reflexivity. }
{ apply finish_upper_bound2. }
{ apply finish_closed2. }
rewrite -psvs_pvs'.
iSts γ as s Hin.
inversion Hin; subst.
rewrite {2}/sts_interp.
rewrite right_id.
iTimeless "Ho".
rewrite (affine_elim (lo ↦s _)). rewrite //=.
assert (sN ⊥ heapN) as Hdisj1 by (rewrite /sN; eauto with ndisj).
assert (sN ⊥ sheapN) as Hdisj2 by (rewrite /sN; eauto with ndisj).
assert (isN ⊥ sheapN) as ? by (rewrite /isN; eauto with ndisj).
assert (isN ⊥ heapN) as ? by (rewrite /isN; eauto with ndisj).
inversion H3; subst.
refine_load d.
iExists (ticket_entered x), {[finish_tok x]}.
iSplitL ""; first auto.
iSplitL "Ho".
{ iIntros "@ >". rewrite /sts_interp //=. iFrame. done. }
iIntros "Hsts".
iPvs (sts_own_weaken _ γ _ (sts.up (ticket_pre 0) {[finish_tok x]}) with "Hsts") as "Hsts".
{ reflexivity. }
{ apply finish_upper_bound3. }
{ apply sts.closed_up. set_unfold. intros t (n&[(?&?)|(?&?)]) Heq.
- subst. congruence.
- subst. inversion Heq; omega.
}
iPvsIntro.
iSplitL "Hmine' Hsts".
{ iIntros "@ >". iLeft. rewrite (affine_elim (lmine ↦{1/2} _)).
iFrame. done. }
wp_load. refine_op d.
iInv "Hinv" as "Hspin"; auto with fsaV.
iApply wp_pvs.
rewrite /spin_inv.
rewrite {1}later_or. rewrite affine_or.
iDestruct "Hspin" as "[?|?]"; last first.
{
iDestruct "Hspin" as "(Hfalse&?)".
iTimeless "Hfalse". rewrite (affine_elim (lmine ↦ _)).
iCombine "Hfalse" "Hmine" as "Hfalse".
rewrite heap_mapsto_op.
iDestruct "Hfalse" as "(%&?)".
congruence.
}
iDestruct "Hspin" as "(Hmine'&Hsts')".
iTimeless "Hsts'".
rewrite (affine_elim (sts_ownS _ _ _ )).
iCombine "Hsts0" "Hsts'" as "Hsts".
rewrite -sts_ownS_op; last 3 first.
{ set_solver. }
{ apply sts.closed_up. set_solver. }
{ apply sts.closed_up. rewrite pre_init. set_solver. }
iPvs (sts_ownS_weaken _ γ _ {[ticket_entered x]} with "Hsts") as "Ho".
{ rewrite left_id. reflexivity. }
{ apply finish_upper_bound2. }
{ apply finish_closed2. }
iSts γ as s Hin'.
inversion Hin'; subst.
rewrite {2}/sts_interp.
rewrite right_id.
iTimeless "Hmine'". iTimeless "Ho".
rewrite (affine_elim (lmine ↦{1/2} _)).
rewrite (affine_elim (lo ↦s _)). rewrite //=.
iCombine "Hmine" "Hmine'" as "Hmine".
rewrite heap_mapsto_op_eq.
replace (1/2 + 1/2)%Qp with 1%Qp by (auto using Qp_div_2).
wp_store. refine_store d'.
iExists (ticket_pre (S x)), ∅.
iSplitL ""; first auto.
{ iPureIntro. eapply finish_step1. }
iSplitL "Ho HR Hhd".
{ iIntros "@ >". rewrite /sts_interp //=.
rewrite Zpos_P_of_succ_nat. iFrame.
iExists (#lmine)%V. done. }
iIntros "Hsts".
iPvs (sts_own_weaken _ γ _ (sts.up (ticket_pre (S x)) ∅) with "Hsts") as "Hsts".
{ reflexivity. }
{ apply sts.elem_of_up. }
{ apply sts.closed_up. set_solver. }
iSplitL "Hmine Hsts".
{ iPvsIntro. iIntros "@ >". iRight. iFrame. done. }
do 2 iPvsIntro. iFrame. iPureIntro. done.
Qed.
End proof.