Commit ed7e189c authored by Ike Mulder's avatar Ike Mulder
Browse files

Added rwlock linux-style, like starling. Removed faulty 'by' in find_biabd.

parent c2fb75fd
......@@ -412,6 +412,12 @@ Section validity.
Global Instance cmra_subtract_None (a : A) : CmraSubtract a a True None | 50.
Proof. by rewrite /CmraSubtract /=. Qed.
Global Instance cmra_subtract_explicit_l (a b : A) : CmraSubtract (a b) a True (Some b) | 500.
Proof. by rewrite /CmraSubtract /=. Qed.
Global Instance cmra_subtract_explicit_r (a b : A) : CmraSubtract (a b) b True (Some a) | 500.
Proof. by rewrite /CmraSubtract /= comm. Qed.
Global Instance exclusive_none_coallocate (a : A) :
Exclusive a
CoAllocate a None | 60.
......
......@@ -291,44 +291,8 @@ Section stages.
Qed.
End goal_steps.
End stages. (*
Ltac biabd_rec_step_goal_opt :=
(simple eapply biabd_mod_intro_r; [iSolveTC | iSolveTC | | ]) ||
((lazymatch goal with
| |- @BiAbd _ ?TTl (@TeleS ?A ?TTr) _ _ ?Q _ _ _ =>
simple notypeclasses refine (biabd_witness_postpone _ _ _ _ _ _ _ _ _ _ _ _ ); [shelve|shelve|shelve|
intros ?; simpl;
simple notypeclasses refine (@biabd_evar_cut_witness _ A _ TTr _ _ Q _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _);
[ shelve | shelve | shelve | shelve | shelve | shelve | simpl | idtac..]
|idtac..]
end)).
Ltac biabd_wand_backtrack :=
lazymatch goal with
| |- BiAbd ?p ?P _ _ _ _ =>
assert (∃ R V, IntoWand2 p P R V) as _ by (eexists; eexists; iSolveTC);
(notypeclasses refine (biabd_wand _ _ _ _ _ _ _ _ _ _); [iSolveTC| ]) +
(* not too happy about this :( *)
(biabd_rec_step_goal_opt)
end.
End stages.
Ltac biabd_rec_step_hyp_opt :=
(notypeclasses refine (biabd_later_mono _ _ _ _ _ _ _ _ _ _ _ _); [iSolveTC..| ]) ||
((notypeclasses refine (biabd_sepl _ _ _ _ _ _ _ _)) + (notypeclasses refine (biabd_sepr _ _ _ _ _ _ _ _))) ||
(simple eapply biabd_exist; [iSolveTC |
cbn [tforall tele_fold tele_bind tele_app tele_appd_dep]; intros | idtac..]) ||
(lazymatch goal with
| |- @BiAbd ?PROP ?TTl ?TTr _ _ ?Q _ _ _ =>
let A := open_constr:((_ : Type)) in
let R := open_constr:((_ : A → PROP)) in
notypeclasses refine (biabd_forall_postpone _ _ R _ _ _ _ _ _ _ _ _); [ iSolveTC |
intros ?; simpl;
simple notypeclasses refine (@biabd_evar_cut_forall _ A _ TTr _ R Q _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _);
[shelve|shelve|shelve|shelve|shelve|shelve|simpl|..] | ]
end) ||
(simple eapply biabd_mod_intro_l; [iSolveTC| iSolveTC| | ]) ||
(notypeclasses refine (biabd_wand _ _ _ _ _ _ _ _ _ _); [iSolveTC| ]). *)
Ltac biabd_step_hyp p P :=
(notypeclasses refine (biabdhyp_later_mono _ _ _ _ _ _ _ _ _ _ _ _); [iSolveTC..| ]) ||
......@@ -350,22 +314,6 @@ Ltac biabd_step_goal :=
(simple eapply biabdgoal_mod_intro_r; [iSolveTC | iSolveTC | | ]) ||
(notypeclasses refine (biabdgoal_witness_both _ _ _ _ _ _ _ _ _ _ _ _ _ _);
[ intros; do 4 (notypeclasses refine (ex_intro _ _ _)); split; [ | simple notypeclasses refine (ex_intro _ _ _); last cbn beta ] | idtac..]).
(*
Ltac find_biabd_decompose_goal_steps :=
iSolveTC || (biabd_rec_step_goal_opt;
lazymatch goal with
| |- BiAbd _ _ _ _ _ _ => find_biabd_decompose_goal_steps
| |- _ => iSolveTC
end).
Ltac find_biabd_decompose :=
(biabd_rec_step_hyp_opt;
lazymatch goal with
| |- BiAbd _ _ _ _ _ _ => find_biabd_decompose
| |- _ => iSolveTC
end
) || find_biabd_decompose_goal_steps. *)
Ltac find_biabd_step :=
lazymatch goal with
......@@ -374,21 +322,8 @@ Ltac find_biabd_step :=
| |- _ => iSolveTC
end.
(*Ltac find_biabd_direct_goal_steps :=
(biabd_rec_step_goal_opt;
lazymatch goal with
| |- BiAbd _ _ _ _ _ _ => find_biabd_direct_goal_steps
| |- _ => iSolveTC
end
) || (eapply bi_abd_from_assumption; iSolveTC) || (eapply bi_abd_from_assumption_intuit).
Ltac find_biabd_direct :=
(try (notypeclasses refine (biabd_later_mono _ _ _ _ _ _ _ _ _ _ _ _); [iSolveTC..| ]));
find_biabd_direct_goal_steps.
Ltac find_biabd_old := find_biabd_direct || find_biabd_decompose. *)
Ltac find_biabd := simple eapply biabd_from_unfold_hyp; by repeat find_biabd_step.
(* fail succeeds only on empty goals :) *)
Ltac find_biabd := simple eapply biabd_from_unfold_hyp; repeat find_biabd_step; fail.
Global Hint Extern 4 (BiAbdMod _ ?P _ ?M _ _ _ _) =>
(* we need to prevent reopening invariants; it is sound to do it, but unwanted *)
......
......@@ -134,11 +134,12 @@ Section actris_test.
par_map_worker vmap lk c
{{{ RET #(); True }}}.
Proof.
iIntros "#Hmap !>" (Φ) "[#Hlk Hγ] HΦ". iLöb as "IH".
iStepsS. iIntros "!>".
iStepsS. iLöb as "IH".
wp_lam.
iStepsS.
{ destruct x1; eauto. right. fold_leibniz. by apply H1. }
destruct x; iStepsS; multiset_solver.
{ destruct x2; eauto. right. fold_leibniz. by apply H1. }
destruct x0; iStepsS; multiset_solver.
Qed.
Lemma par_map_workers_spec2 γl γ n vmap lk c :
......
......@@ -170,7 +170,7 @@ Section spec.
SolveSepSideCondition (1 < Z.to_pos p)%positive
BiAbd (TTl := [tele_pair Qp; Qp]) (TTr := [tele_pair Qp]) false (own γ ( (Some (q, Z.to_pos p)))) (λ q', own γ ( (Some (q', Z.to_pos (p - 1))))) (fupd E E)
(λ qPo qPd, (q + qPo = 1)%Qp P qPo (own γ ( (Some (qPd, 1%positive)))) P qPd)%I
(λ qPo qPd q', r, (q = r + qPd)%Qp q' = r P (qPo + qPd) (r + (qPo + qPd) = 1)%Qp)%I.
(λ qPo qPd q', (q = q' + qPd)%Qp P (qPo + qPd) (q' + (qPo + qPd) = 1)%Qp)%I.
Proof using HP.
rewrite /SolveSepSideCondition /BiAbd /= => Hlt qPo qPd.
iStepS; [|lia].
......
......@@ -35,7 +35,7 @@ Proof. solve_inG. Qed.
Section tlock_instances.
Global Instance set_seq_local_update n n' :
SolveSepSideCondition (n' = S n)
FindLocalUpdate (GSet $ set_seq 0 n) (GSet $ set_seq 0 n') (GSet $ ) (GSet {[n]}) True | 100.
FindLocalUpdate (GSet $ set_seq 0 n) (GSet $ set_seq 0 n') (GSet ) (GSet {[n]}) True | 100.
Proof.
rewrite /FindLocalUpdate /SolveSepSideCondition => -> _.
apply set_local_update.
......
From iris.algebra Require Import auth csum excl frac numbers.
From iris_automation.heap_lang Require Import stepping_tacs.
From iris_automation.biabd Require Import biabd_local_updates.
From iris.heap_lang Require Import proofmode.
From iris.bi Require Import fractional.
From iris_automation.examples.comparison Require Import ticket_lock.
Definition BOUND : nat := 100.
Definition new_rwlock : val :=
λ: "_",
let: "rdrs" := ref #0 in
let: "tlk" := newlock #() in
("tlk", "rdrs").
Definition acquire_reader_int : val :=
rec: "acq_reader" "readers" :=
if: ! "readers" < #BOUND then
FAA "readers" #1
else
"acq_reader" "readers".
Definition acquire_reader : val :=
λ: "rwlk",
acquire (Fst "rwlk") ;;
acquire_reader_int (Snd "rwlk") ;;
release (Fst "rwlk").
Definition release_reader : val :=
λ: "rwlk",
FAA (Snd "rwlk") #-1.
Definition wait_for_readers : val :=
rec: "wait" "readers" :=
if: ! "readers" = #0 then
#()
else
"wait" "readers".
Definition acquire_writer : val :=
λ: "rwlk",
acquire (Fst "rwlk") ;;
wait_for_readers (Snd "rwlk").
Definition release_writer : val :=
λ: "rwlk",
release (Fst "rwlk").
Class TCUnfoldBeta (A : Prop) :=
tc_unfolded_beta : A.
Global Hint Extern 4 (TCUnfoldBeta ?A) => rewrite /TCUnfoldBeta; cbn beta; iSolveTC : typeclass_instances.
Section countertiedfrac.
Context {PROP : bi} `{!CmraDiscrete A} `{BiFUpd PROP}.
Class CounterFracTie (Pa Pf : Qp A PROP) := {
countertiedfrac_increase q1 a1 q2 a2 E : (q1 + q2)%Qp (Pa q1 a1 |={E}=> Pa (q1 + q2)%Qp (a1 a2) Pf q2 a2) ;
countertiedfrac_decrease q1 a1 q2 a2 E : Pa (q1 + q2)%Qp (a1 a2) Pf q2 a2 |={E}=> Pa q1 a1 ;
countertiedfrac_valid1 q a : Pa q a ⌜✓ q;
countertiedfrac_valid q1 a1 q2 a2 : Pa q1 a1 Pf q2 a2 (q2 < q1)%Qp a2 a1 q1 = q2 a1 a2
}.
Class CounterTiedFractional (Pa Pf : Qp A PROP) (P : Qp PROP) (φi φd : A A A Prop) := {
countertiedfrac_fractional : Fractional P ;
countertiedfrac_counterfractie : CounterFracTie Pa Pf ;
countertiedfrac_increase_cond a_f a_t a_i : φi a_f a_t a_i a_t = a_f a_i ;
countertiedfrac_decrease_cond a_f a_t a_i : φd a_f a_t a_i a_f = a_t a_i ¬ a_f a_i;
}.
Class AsCounterTiedFractional (P : PROP) (Pa : Qp A PROP) (q : Qp) (a : A) :=
as_counter_tied_fractional : P @{PROP} Pa q a.
Global Instance increase_counter_tied_frac Pa Pf P φi φd qh ah ag ai Ph Pg E :
AsCounterTiedFractional Ph Pa qh ah
( (q : Qp), AsCounterTiedFractional (Pg q) Pa q ag)
CounterTiedFractional Pa Pf P φi φd
TCUnfoldBeta (φi ah ag ai)
BiAbd (TTl := [tele_pair Qp]) (TTr := [tele_pair Qp]) false Ph Pg (fupd E E)
(λ qP, P qP (qh + qP = 1)%Qp)%I
(λ qP q', (q' = qh + qP / 2)%Qp Pf (qP /2)%Qp ai P (qP /2)%Qp P (qP / 2)%Qp)%I.
Proof.
rewrite /AsCounterTiedFractional => -> HPg.
case => HP [HPaPf _ _ _ ] Hφ _.
rewrite /TCUnfoldBeta => /Hφ Hag.
rewrite /BiAbd /=.
do 2 iStepS.
iExists (qh + x/2)%Qp.
iRevert "H1 H2"; iStopProof.
apply bi.pure_elim' => Hqx.
do 3 iStepS.
rewrite HPg (HPaPf _ _ (x /2)%Qp ai); last first.
{ apply frac_valid. rewrite -Hqx. apply Qp_add_le_mono_l. by apply Qp_lt_le_incl, Qp_div_lt. }
iMod "H2" as "[$ $]".
rewrite -{1}(Qp_div_2 x).
rewrite HP.
iFrame "H3".
by iIntros "!>".
Qed.
Global Instance decrease_counter_tied_frac Pa Pf P φi φd qh ah ag ai Ph Pg E :
AsCounterTiedFractional Ph Pa qh ah
( (q : Qp), AsCounterTiedFractional (Pg q) Pa q ag)
CounterTiedFractional Pa Pf P φi φd
TCUnfoldBeta (φd ah ag ai)
BiAbd (TTl := [tele_pair Qp; Qp]) (TTr := [tele_pair Qp]) false Ph Pg (fupd E E)
(λ qPo qPd, (qh + qPo = 1)%Qp P qPo Pf qPd ai P qPd)%I
(λ qPo qPd q', (qh = q' + qPd)%Qp P (qPo + qPd)%Qp (q' + (qPo + qPd) = 1)%Qp)%I.
Proof.
rewrite /AsCounterTiedFractional => -> HPg.
case => HP [_ HPaPf1 _ HPaPf2] _ Hφ.
rewrite /TCUnfoldBeta => /Hφ Hag.
rewrite /BiAbd /=.
do 3 iStepS.
iAssert ( (x0 < qh)%Qp ai ah qh = x0 ah ai)%I as "#[[% %]|[% %]]".
{ iPoseProof (HPaPf2 with "[H1 H4]") as "[%|%]"; first by iFrame.
- iLeft. rewrite (bi.pure_True _ H0). eauto.
- iRight. rewrite (bi.pure_True _ H0). eauto. }
2:{ contradict H1. apply Hag. }
iCombine "H1 H4" as "H1".
destruct Hag; subst.
apply Qp_lt_sum in H0.
destruct H0 as [r Hr].
rewrite (Qp_add_comm) in Hr. subst.
iExists (r)%Qp.
rewrite HPg.
rewrite (HPaPf1).
iMod "H1" as "$".
rewrite HP.
iFrame.
iIntros "!>".
iDestruct "H2" as %<-.
rewrite bi.pure_True => //.
iSplitR =>//.
iPureIntro.
by rewrite (Qp_add_comm x x0) assoc.
Qed.
End countertiedfrac.
Require Import ZifyClasses.
Lemma of_pos_to_pos_eq : forall z, Zpos (Z.to_pos z) = Z.max 1 z.
Proof.
intros x; destruct x.
- reflexivity.
- apply eq_sym, Zpos_max_1.
- reflexivity.
Qed.
Global Instance Op_Z_to_pos : UnOp Z.to_pos := { TUOp := (λ z, 1 `max` z)%Z ; TUOpInj := of_pos_to_pos_eq }.
Add Zify UnOp Op_Z_to_pos.
Definition rwlockR := authUR $ optionUR $ csumR (exclR unitO) (prodR fracR positiveR).
Class rwlockG Σ := {
rwlock_G :> inG Σ rwlockR ;
rwlock_excl_G :> inG Σ $ exclR unitO;
rwtlock_G :> tlockG Σ
}.
Definition rwlockΣ : gFunctors := #[ GFunctor rwlockR; tlockΣ; GFunctor $ exclR unitO ].
Instance subG_rwlockΣ {Σ} : subG rwlockΣ Σ rwlockG Σ.
Proof. solve_inG. Qed.
Section proof.
Context `{!heapG Σ, !rwlockG Σ} (P : Qp iProp Σ) {HP : Fractional P}.
Instance P_AsFractional q : AsFractional (P q) P q.
Proof using HP. done. Qed.
Let N := nroot .@ "rw_lock".
Definition readers_inv (γ γ' : gname) (readers : loc) : iProp Σ :=
(z : Z),
readers #z
((0 < z%Z (q q' : Qp), own γ ( (Some $ Cinr (q, Z.to_pos z))) (q + q' = 1)%Qp P q')
(z = 0%Z own γ ( (Some $ Cinl $ Excl ())) (P 1 own γ ( (Some $ Cinl $ Excl ())) own γ' (Excl ())))).
(* because of the (z + 1), an own γ (◯ (Some $ Cinr (q, 1%positive))) token is no longer enough to guarantee that ⌜0 < z⌝%Z.
that means releasing a reader does not necessarily leave the reader greater or equal zero.. *)
Definition tlock_inv (γ' : gname) : iProp Σ :=
own γ' (Excl ()).
Definition is_rwlock (γ1 γ2 γ3 : gname) (rwlk : val) : iProp Σ :=
(tlk : val) (rdrs : loc),
rwlk = (tlk, #rdrs)%V inv N (readers_inv γ1 γ3 rdrs) is_lock γ2 tlk (tlock_inv γ3).
Hint Extern 4 ( ( ?a)) =>
by apply auth_auth_valid : core.
Ltac biabd_instances_heaplang.trySolvePureEqAdd2 ::=
match goal with
| H: (?ql + ?qr = 1)%Qp |- (?ql + ?qr / 2 + ?qr2 = 1)%Qp =>
let ql' := fresh in
set (ql' := ql);
rewrite -H -assoc;
unfold ql';
apply Qp_add_eq_mono_l, Qp_div_2
| |- (1 / 2 + ?x = 1)%Qp => is_evar x; apply Qp_div_2
end.
Lemma new_rwlock_spec :
{{{ P 1 }}} new_rwlock #() {{{ rwlk γ1 γ2 γ3, RET rwlk; is_rwlock γ1 γ2 γ3 rwlk }}}.
Proof.
iMod (own_alloc (( (Some $ Cinl $ Excl ())
(Some $ Cinl $ Excl ()))))
as (γ) "[H● H◯]"; first by apply auth_both_valid_discrete.
iMod (own_alloc (Excl ())) as (γ') "Hγ"; first done.
iHammer.
Qed.
Section rwlock_autom.
Global Instance acquire_step (γ : gname) (lk : val) R :
ReductionStep (wp_red_cond, [tele_arg ⊤; NotStuck]) (acquire lk) fupd is_lock γ lk R; empty_hyp_first =[^1]=>
fupd #() locked γ R | 50.
Proof.
apply: texan_to_red_cond => //=.
exact: acquire_spec.
Qed.
Global Instance release_step (γ : gname) (lk : val) R :
ReductionStep (wp_red_cond, [tele_arg ⊤; NotStuck]) (release lk) fupd is_lock γ lk R locked γ R; empty_hyp_first =[^1]=>
fupd #() True | 50.
Proof.
apply: texan_to_red_cond => //=.
exact: release_spec.
Qed.
Global Instance is_lock_persistent γ lk R : Persistent (is_lock γ lk R).
Proof. iSolveTC. Qed.
Global Opaque is_lock.
Global Instance own_countertied_fractional γ :
CounterTiedFractional (A := positiveR) (λ q p, own γ ( (Some $ Cinr (q, p))))
(λ q p, own γ ( (Some $ Cinr (q, p)))) P
(λ p1 p2 p3, TCAnd (SolveSepSideCondition (p1 + 1 = p2)%positive) (TCEq p3 1%positive))
(λ p1 p2 p3, TCAnd (SolveSepSideCondition (p1 = p2 + 1)%positive) (TCEq p3 1%positive)).
Proof.
split; try iSolveTC.
- split; [iStepsS..| | iStepsS].
* do 3 iStepS.
iDestruct (own_valid with "H1") as %?.
revert H.
rewrite auth_auth_valid => /Some_valid /Cinr_valid /pair_valid [Hx _].
iStepsS.
* left. split => //. by apply pos_included.
- rewrite /SolveSepSideCondition; intros. change (a_f a_i) with (a_f + a_i)%positive. destruct H as [H ->]. lia.
- rewrite /SolveSepSideCondition; intros. change (a_t a_i) with (a_t + a_i)%positive. destruct H as [H ->]. split => //.
fold_leibniz. lia.
Qed.
Global Instance as_own_countertied_fractional γ q p :
AsCounterTiedFractional (own γ ( (Some $ Cinr (q, p)))) (λ q p, own γ ( (Some $ Cinr (q, p)))) q p.
Proof. done. Qed.
(* this one breaks own_countertied_fractional! *)
Global Instance find_local_update_incomparable {A : ucmra} (x x' : A) :
Cancelable x
(* TODO: make typeclasses to simplify ✓ x *)
(* This one has highest priority; it is to find things like
(Some (Cinl x), Some (Cinl x)) ~l~> (Some (Cinr x'), Some (Cinr x'))
i.e. for ucmra's with incomparable elements
what we ACTUALLY want is BiAbd for cmra's :)
-> for given p and q, find minimal r and maximal s, such that
p ⋅? r ≡[{n}?] q ⋅? s
*)
FindLocalUpdate x x' x x' ( x') | 999.
Proof.
rewrite /FindLocalUpdate => Hx Hx'.
etrans.
rewrite -[x in (x, _)]right_id.
by apply cancel_local_update_unit.
apply local_update_unital => n z Heps.
rewrite left_id => <-.
rewrite right_id.
split => //.
by apply cmra_valid_validN.
Qed.
Global Instance add_first_reader γ E :
BiAbd (TTl := [tele]) (TTr := [tele_pair Qp]) false (own γ ( (Some $ Cinl $ Excl ()))) (λ q, own γ ( (Some $ Cinr (q, xH)))) (fupd E E)
(own γ ( (Some $ Cinl $ Excl ()))) (λ q, own γ ( (Some $ Cinr (q, xH))) q = 1/2%Qp)%I.
Proof.
rewrite /BiAbd /=.
iStepS.
iExists (1/2)%Qp.
iStepsS.
Qed.
Global Instance release_writer_biabd γ1 γ3 E rdrs :
BiAbd (TTl := [tele]) (TTr := [tele]) true (inv N (readers_inv γ1 γ3 rdrs)) (own γ3 (Excl ())) (fupd E E)
(own γ1 ( (Some $ Cinl $ Excl ())) P 1 ⌜↑N E)%I True%I.
Proof.
rewrite /BiAbd /=.
iStepS.
iInv N as "HN"; iRevert "HN"; iStepsS.
iLeft. iStepS. by iFrame.
Qed.
End rwlock_autom.
Opaque locked.
Global Instance acquire_reader_int_step (γ γ' : gname) (readers : loc) :
ReductionStep (wp_red_cond, [tele_arg ⊤; NotStuck]) (acquire_reader_int #readers) fupd
inv N (readers_inv γ γ' readers) (own γ' $ Excl ()) ; empty_hyp_first =[^1]=>
(z : Z), fupd #z q, own γ' (Excl ()) own γ ( (Some $ Cinr (q, 1%positive))) P q.
Proof.
apply: texan_to_red_cond => //=.
iStepsS.
iLöb as "IH".
wp_lam.
iHammer.
Qed.
Lemma acquire_reader_spec rwlk γ1 γ2 γ3 :
{{{ is_rwlock γ1 γ2 γ3 rwlk }}} acquire_reader rwlk {{{ (q : Qp), RET #(); own γ1 ( (Some $ Cinr (q, 1%positive))) P q}}}.
Proof. iStepsS. Qed.
Ltac pure_solver.trySolvePureAdd1 ::=
match goal with
| |- ¬ (_ < _)%Z => lia
end.
Lemma release_reader_spec rwlk γ1 γ2 γ3 q :
{{{ is_rwlock γ1 γ2 γ3 rwlk own γ1 ( (Some $ Cinr (q, 1%positive))) P q }}}
release_reader rwlk
{{{ (z : Z), RET #z; True }}}.
Proof.
iStepsS.
iLeft.
iCombine "H4 H8" as "HP".
rewrite H0.
iStepsS.
Qed.
Global Instance wait_for_readers_step (γ γ' : gname) (readers : loc) :
ReductionStep (wp_red_cond, [tele_arg ⊤; NotStuck]) (wait_for_readers #readers) fupd
inv N (readers_inv γ γ' readers) (own γ' $ Excl ()) ; empty_hyp_first =[^1]=>
fupd #() own γ ( (Some $ Cinl $ Excl ())) P 1.
Proof.
apply: texan_to_red_cond => //=.
iStepsS.
iLöb as "IH".
wp_lam.
iHammer using lia.
Qed.
Lemma acquire_writer_spec rwlk γ1 γ2 γ3 :
{{{ is_rwlock γ1 γ2 γ3 rwlk }}}
acquire_writer rwlk
{{{ RET #(); own γ1 ( (Some $ Cinl $ Excl ())) P 1 locked γ2 }}}.
Proof. iStepsS. Qed.
Lemma release_writer_spec rwlk γ1 γ2 γ3 :
{{{ is_rwlock γ1 γ2 γ3 rwlk own γ1 ( (Some $ Cinl $ Excl ())) P 1 locked γ2 }}}
release_writer rwlk
{{{ RET #(); True }}}.
Proof. iStepsS. Qed.
End proof.
......@@ -58,6 +58,7 @@ Ltac trySolvePureEq :=
match constr:((T, l)) with
| (Z, _) => solveZEq
| (nat, _) => lia