Skip to content
GitLab
Commit 6ff38476 authored by Ike Mulder's avatar Ike Mulder
Browse files

Added rough alternative proof for rwlock_linux. Slight improvements for pure_solver.

parent ed7e189c
Show whitespace changes
Inline Side-by-side
theories/biabd/biabd_local_updates.v
View file @ 6ff38476
......@@ -289,6 +289,10 @@ Section biabds.
FindLocalUpdate x x' y y' φ →
BiAbd (TTl := [tele]) (TTr := [tele]) p (own γ $ ● x) (own γ $ ● x') (fupd E E)
(own γ (◯ y) ∗ ⌜φ⌝)%I (own γ $ ◯ y') | 150.
(* these must currently be after CmraSubtract, while they should have higher priority.
The biabd search greedily chooses a modality, and if that is not compatible with the goal,
the search just fails.
*)
Proof.
rewrite /FindLocalUpdate /BiAbd /= => Hφ.
rewrite assoc.
......@@ -479,7 +483,8 @@ Section validity.
IsValidOp a a ε Σ True%I.
Proof. apply from_isop. rewrite /IsOp right_id //. Qed.
Global Instance ucmra_subtract_all (a : A) : UcmraSubtract a a True ε.
Global Instance ucmra_subtract_all (a : A) : UcmraSubtract a a True ε | 100.
(* this one may glance over pcore like info we can actually keep *)
Proof. by rewrite /UcmraSubtract /CmraSubtract /= right_id => _. Qed.
Global Instance ucmra_subtract_unit (a : A) : UcmraSubtract a ε True a.
......@@ -1584,6 +1589,17 @@ Section validity.
rewrite /CmraSubtract => Hφq /=.
case => /Hφq {Hφq} /= <- -> //.
Qed.
(*
Global Instance auth_auth_subtract_all {A : ucmra} (a1 a2 : A) φ c :
UcmraSubtract a2 a1 φ c →
UcmraSubtract (● a1) (● a2) (φ) (◯ c).
(* this is not true; they are not equivalent, since the equivalence drops down to projections on ● and ◯ *)
Proof.
rewrite /UcmraSubtract /CmraSubtract /= => Hφ /= /Hφ <-.
rewrite /equiv /= /ofe_equiv /=.
rewrite /viewUR /=.
case => /Hφq {Hφq} /= <- -> //.
Qed. *)
End recursive.
......@@ -1735,7 +1751,7 @@ Section generic_instances.
Global Instance biabd_cmra_subtract {A : cmra} `{!inG Σ A} (a b : A) γ φ mc p :
CmraSubtract a b φ mc →
BiAbd (TTl := [tele]) (TTr := [tele]) p (own γ a) (own γ b) id
⌜φ⌝%I (match mc with | Some c => own γ c | None => emp%I end).
⌜φ⌝%I (match mc with | Some c => own γ c | None => emp%I end) (* | 41*).
Proof.
rewrite /CmraSubtract /BiAbd => Hφ /=.
apply bi.wand_elim_r', bi.pure_elim' => /Hφ <-.
......
theories/examples/rwlock_linux.v
View file @ 6ff38476
......@@ -7,7 +7,7 @@ From iris.bi Require Import fractional.
From iris_automation.examples.comparison Require Import ticket_lock.
Definition BOUND : nat := 100.
Definition BOUND : positive := 100.
Definition new_rwlock : val :=
......@@ -19,7 +19,8 @@ Definition new_rwlock : val :=
Definition acquire_reader_int : val :=
rec: "acq_reader" "readers" :=
if: ! "readers" < #BOUND then
if: ! "readers" < #(Z.pos BOUND) then
(* verification would be simpler if we do a conditional CAS loop here. but that is less racy *)
FAA "readers" #1
else
"acq_reader" "readers".
......@@ -146,21 +147,7 @@ Section countertiedfrac.
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 ;
......@@ -370,6 +357,247 @@ Section proof.
Proof. iStepsS. Qed.
End proof.
*)
Definition rwlock2R := authUR $ prodUR max_natUR $ optionUR $ exclR natO.
Class rwlock2G Σ := {
rwlock2_G :> inG Σ rwlock2R ;
rwtlock2_G :> tlockG Σ ;
rwlock2_pos_G :> inG Σ $ authUR $ optionUR $ positiveR;
rwlock2_excl_G : > inG Σ $ exclR unitO
}.
Definition rwlock2Σ : gFunctors := #[ GFunctor rwlock2R; tlockΣ; GFunctor $ authUR $ optionUR $ positiveR; GFunctor $ exclR unitO ].
Instance subG_rwlock2Σ {Σ} : subG rwlock2Σ Σ → rwlock2G Σ.
Proof. solve_inG. Qed.
Section proof2.
Context `{!heapG Σ, !rwlock2G Σ} (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".
Let bsucc := Pos.succ BOUND.
Definition readers_inv' (γi γl γp γP : gname) (readers : loc) : iProp Σ :=
∃ (i d : nat),
readers ↦ #(i - d) ∗ own γi (● (MaxNat d, Excl' i)) ∗
((∃ (p : positive), ⌜(Z.pos p + d)%Z = i⌝ ∗ ⌜p ≤ BOUND⌝%positive ∗ own γP (Excl ()) ∗
own γp (● (Some p)) ∗ P ((pos_to_Qp (bsucc - p)%positive) / pos_to_Qp bsucc)%Qp) ∨
(⌜i = d⌝%Z ∗ own γp (● None) ∗ (P 1 ∗ own γP (Excl ()) ∨ own γl (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' (γi γl : gname) : iProp Σ :=
∃ (i : nat), own γl (Excl ()) ∗ own γi (◯ (ε, Excl' i)).
Definition is_rwlock' (γi γl γp γP γt : gname) (rwlk : val) : iProp Σ :=
∃ (tlk : val) (rdrs : loc),
⌜rwlk = (tlk, #rdrs)%V⌝ ∗ inv N (readers_inv' γi γl γp γP rdrs) ∗ is_lock γt tlk (tlock_inv' γi γl).
Hint Extern 4 (✓ (● ?a)) =>
by apply auth_auth_valid : core.
Ltac biabd_instances_heaplang.trySolvePureEqAdd2 ::=
match goal with
| |- #(LitInt Z0) = #(LitInt $ (Z.of_nat ?l) - (Z.of_nat ?r)) =>
is_evar l; is_evar r; unify l O; unify r O; done
| |- #(LitInt $ Z.of_nat ?l1 - Z.of_nat ?r1 + 1) =
#(LitInt $ Z.of_nat ?l - Z.of_nat ?r) =>
is_evar l; is_evar r;
unify l (S l1); unify r r1; pure_solver.trySolvePure
| |- #(LitInt $ Z.of_nat ?l1 - Z.of_nat ?r1 + -1) =
#(LitInt $ Z.of_nat ?l - Z.of_nat ?r) =>
is_evar l; is_evar r;
unify l (l1); unify r (S r1); pure_solver.trySolvePure
end.
Transparent is_lock.
Lemma new_rwlock_spec' :
{{{ P 1 }}} new_rwlock #() {{{ rwlk γi γl γp γP γt, RET rwlk; is_rwlock' γi γl γp γP γt rwlk }}}.
Proof.
do 2 (iMod (own_alloc (Excl ())) as (?) "?"; 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.
Transparent is_lock.
Global Instance is_lock_persistent' γ lk R : Persistent (is_lock γ lk R).
Proof. unfold is_lock. iSolveTC. Qed.
Global Instance auth_keep_maxnat γ i d E :
BiAbd (TTl := [tele]) (TTr := [tele]) false (own γ (● (MaxNat d, Excl' i))) (own γ (● (MaxNat d, Excl' i))) (fupd E E)
emp%I (own γ (◯ (MaxNat d, None))).
Proof.
rewrite /BiAbd /=.
iStepS.
iMod (own_update with "H1") as "[H1 H1']".
{ eapply auth_update_alloc.
eapply prod_local_update_1.
by eapply (max_nat_local_update _ _ (MaxNat d)). }
iStepsS.
Qed.
Global Instance give_P_part p i d:
BiAbd (TTl := [tele]) (TTr := [tele]) false
(P (pos_to_Qp (101 - p) / pos_to_Qp 101))
(P (pos_to_Qp (101 - Z.to_pos (S i - d)) / pos_to_Qp 101)) id
(⌜(Z.pos p + d)%Z = i⌝ ∗ ⌜p < BOUND⌝%positive)%I (P (/ pos_to_Qp 101)).
Proof.
rewrite /BiAbd /=; iStepS.
rewrite -HP.
replace (S i - d)%Z with (Z.pos p + 1)%Z; [ | lia].
enough ((pos_to_Qp (101 - Z.to_pos (Z.pos p + 1)) / pos_to_Qp 101 + / pos_to_Qp 101)%Qp =
(pos_to_Qp (101 - p) / pos_to_Qp 101))%Qp as -> => //.
replace (/ pos_to_Qp 101)%Qp with (1 / pos_to_Qp 101)%Qp.
rewrite -Qp_div_add_distr.
f_equal.
rewrite pos_to_Qp_add.
f_equal. unfold BOUND in H0. lia.
unfold Qp_div.
by rewrite Qp_mul_1_l.
Qed.
Global Instance give_P_first_part i:
BiAbd (TTl := [tele]) (TTr := [tele]) false
(P 1)
(P (pos_to_Qp (101 - Z.to_pos (S i - i)) / pos_to_Qp 101)) id
(emp)%I (P (/ pos_to_Qp 101)).
Proof.
rewrite /BiAbd /=; iStepS.
rewrite -HP.
replace (S i - i)%Z with (1)%Z; [ | lia].
enough ((pos_to_Qp (101 - Z.to_pos 1) / pos_to_Qp 101 + / pos_to_Qp 101)%Qp =
1)%Qp as -> => //.
replace (/ pos_to_Qp 101)%Qp with (1 / pos_to_Qp 101)%Qp.
rewrite -Qp_div_add_distr.
rewrite pos_to_Qp_add.
replace ((101 - Z.to_pos 1) + 1)%positive with 101%positive by lia.
by rewrite Qp_div_diag.
unfold Qp_div.
by rewrite Qp_mul_1_l.
Qed.
End rwlock_autom.
Opaque locked.
Global Instance acquire_reader_int_step (γi γl γp γP : gname) (readers : loc) i :
ReductionStep (wp_red_cond, [tele_arg ⊤; NotStuck]) (acquire_reader_int #readers) ⊣ ⟨fupd ⊤ ⊤⟩
inv N (readers_inv' γi γl γp γP readers) ∗ (own γl $ Excl ()) ∗ own γi (◯ (ε, Excl' i)) ; empty_hyp_first =[▷^1]=>
∃ (z : Z), ⟨fupd ⊤ ⊤⟩ #z ⊣ own γl (Excl ()) ∗ own γp (◯ (Some 1%positive)) ∗ P (/ pos_to_Qp bsucc) ∗ own γi (◯ (ε, Excl' (S i))).
Proof.
apply: texan_to_red_cond => //=.
iStepS.
iStepS.
iStepS.
iLöb as "IH".
wp_lam.
do 4 iStepS.
- do 3 iStepS.
do 5 iStepS.
* iStepsS.
* iStepsS.
- iRight. iStepS. iLeft. iStepS.
do 3 iStepS.
do 5 iStepS.
* iStepsS.
* lia.
Qed.
Lemma acquire_reader_spec rwlk γi γl γp γP γt :
{{{ is_rwlock' γi γl γp γP γt rwlk }}} acquire_reader rwlk {{{ RET #(); own γp (◯ (Some 1%positive)) ∗ P (/ pos_to_Qp bsucc) }}}.
Proof. iStepsS. Qed.
Ltac pure_solver.trySolvePureAdd1 ::=
match goal with
| |- ¬ (_ < _)%Z => lia
end.
Lemma release_reader_spec rwlk γi γl γp γP γt :
{{{ is_rwlock' γi γl γp γP γt rwlk ∗ own γp (◯ (Some 1%positive)) ∗ P (/ pos_to_Qp bsucc) }}}
release_reader rwlk
{{{ (z : Z), RET #z; True }}}.
Proof.
iStepsS.
destruct (decide (x7 = 1%positive)) as [-> | Hneq].
- iRight. iStepS. iLeft.
iCombine "H4 H10" as "HP".
rewrite -(Qp_mul_1_l (/ pos_to_Qp bsucc)%Qp).
change (bsucc) with (101%positive).
change (1 * / pos_to_Qp 101)%Qp with (1/ pos_to_Qp 101)%Qp.
rewrite -Qp_div_add_distr.
rewrite pos_to_Qp_add.
change (1 + (101 - 1))%positive with 101%positive.
rewrite Qp_div_diag.
iStepsS.
- iLeft. iStepS.
iCombine "H4 H10" as "HP".
rewrite -(Qp_mul_1_l (/ pos_to_Qp bsucc)%Qp).
change (bsucc) with (101%positive).
change (1 * / pos_to_Qp 101)%Qp with (1/ pos_to_Qp 101)%Qp.
rewrite -Qp_div_add_distr.
rewrite pos_to_Qp_add.
enough ((1 + (101 - x7))%positive = (101 - Z.to_pos (x4 - S x5))%positive) as <-.
iStepsS.
unfold BOUND in H0. lia.
Qed.
Global Instance wait_for_readers_step (γi γl γp γP : gname) (readers : loc) i :
ReductionStep (wp_red_cond, [tele_arg ⊤; NotStuck]) (wait_for_readers #readers) ⊣ ⟨fupd ⊤ ⊤⟩
inv N (readers_inv' γi γl γp γP readers) ∗ (own γl $ Excl ()) ∗ own γi (◯ (ε, Excl' i)); empty_hyp_first =[▷^1]=>
⟨fupd ⊤ ⊤⟩ #() ⊣ P 1 ∗ own γi (◯ (MaxNat i, Excl' i)) ∗ own γP (Excl ()).
Proof.
apply: texan_to_red_cond => //=.
iStepsS.
iLöb as "IH".
wp_lam.
iStepsS. lia.
iRight.
iStepS. iRight.
iStepsS. contradict H1. pure_solver.trySolvePure.
Unshelve. apply inhabitant.
Qed.
Lemma acquire_writer_spec rwlk γi γl γp γP γt :
{{{ is_rwlock' γi γl γp γP γt rwlk }}}
acquire_writer rwlk
{{{ (i : nat), RET #(); P 1 ∗ own γi (◯ (MaxNat i, Excl' i)) ∗ locked γt ∗ own γP (Excl ()) }}}.
Proof. iStepsS. Qed.
Lemma release_writer_spec rwlk γi γl γp γP γt i :
{{{ is_rwlock' γi γl γp γP γt rwlk ∗ P 1 ∗ own γi (◯ (MaxNat i, Excl' i)) ∗ locked γt ∗ own γP (Excl ()) }}}
release_writer rwlk
{{{ RET #(); True }}}.
Proof.
iStepsS.
rewrite {1}/SolveSep /=.
iInv N as "HN"; iRevert "HN"; iStepsS.
iRight. iStepS. iLeft. iStepS.
iIntros "!>". iStepS.
iIntros "!>". iStepsS.
Qed.
End proof.
......
theories/steps/pure_solver.v
View file @ 6ff38476
......@@ -4,6 +4,21 @@ From stdpp Require Import namespaces.
From iris_automation Require Import util_classes.
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.
(* missing from std library. TODO: Coq PR ? *)
Lemma z_of_nat_equality (z : Z) (n : nat) :
(0 ≤ z)%Z →
......@@ -11,6 +26,12 @@ Lemma z_of_nat_equality (z : Z) (n : nat) :
(Z.of_nat n = z).
Proof. lia. Qed.
Lemma z_pos_equality (z : Z) (n : positive) :
(0 < z)%Z →
(Z.to_pos z = n) →
(Z.pos n = z).
Proof. lia. Qed.
Lemma z_plus_eq_remove_r (a b z : Z) :
(a = z - b)%Z →
(a + b = z)%Z.
......@@ -30,6 +51,7 @@ Ltac solveZEq :=
|has_evar l;
lazymatch l with
| Z.of_nat ?n => is_evar n; refine (z_of_nat_equality _ _ _ _); [lia | reflexivity]
| Z.pos ?p => is_evar p; refine (z_pos_equality _ _ _ _); [lia | reflexivity]
| (?a + ?b)%Z =>
first
[has_evar a; has_evar b; fail 3 "Cannot solve Z equation"l"="r": contains multiple evars"
......
theories/steps/small_steps.v
View file @ 6ff38476
......@@ -37,7 +37,8 @@ Ltac trySolvePurePreSplit φ R :=
| has_evar φ;
(split; first by trySolvePure ||
(* if there is an evar, we need to solve it now *)
fail 1 "Pure condition"φ"needs to be proved now!")
(* somehow prepending idtac changes the semantics and makes it work like intentioned...?*)
idtac; fail 1 "Pure condition"φ"needs to be proved now!")
(* final option: solve it now, and if unsuccesful, shelve it *)
| split; [first [by trySolvePure | shelve] | ] ].
......
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment