Skip to content
Snippets Groups Projects
Commit 8de85872 authored by Robbert Krebbers's avatar Robbert Krebbers
Browse files

Style tweaks to rwlocks. 

- Remove unneeded imports
- Remove double spaces and insert space before colons
- Shorten long lines
- Favor `(.. & .. & ..)` over nesting `[.. [.. ..]]`
- Use `injection` intro patterns
- Favor `%H` over `"%H"`
- Use `first by eauto` instead of `first eauto` since the latter does not fail if `eauto` fails
parent 12e75edb
No related branches found
No related tags found
No related merge requests found
Hide whitespace changes
Inline Side-by-side
iris_heap_lang/lib/rw_spin_lock.v
+ 73
− 92
View file @ 8de85872
From stdpp Require Import numbers.
From iris.algebra Require Import gmultiset.
From iris.base_logic Require Import invariants.
From iris.bi.lib Require Export fractional.
From iris.proofmode Require Import proofmode.
From iris.program_logic Require Export weakestpre.
From iris.heap_lang Require Export lang.
From iris.heap_lang Require Import proofmode notation.
......@@ -46,17 +44,17 @@ Section proof.
Local Definition rw_state_inv (γ : gname) (l : loc) (Φ : Qp → iProp Σ) : iProp Σ :=
∃ z : Z, l ↦ #z ∗
(* We need *some* ghost state that allows us to establish a contradiction in
the left disjunct (where the lock is write-locked) when proving [release_reader_spec],
so we use a fraction of the empty authoritative reader set (the rest goes to [writer_locked].)
Any fraction would do, but the benefit of giving over half to [writer_locked]
(and keeping less than half here) is that we can prove [writer_locked_exclusive].
*)
(* We need *some* ghost state that allows us to establish a contradiction
in the left disjunct (where the lock is write-locked) when proving
[release_reader_spec], so we use a fraction of the empty authoritative
reader set (the rest goes to [writer_locked].) Any fraction would do, but
the benefit of giving over half to [writer_locked] (and keeping less than
half here) is that we can prove [writer_locked_exclusive]. *)
(⌜(z = -1)%Z⌝ ∗ own γ (●{# 1/4} ∅)
∨ ⌜(0 ≤ z)%Z⌝ ∗ ∃ (q : Qp) (g : gmultiset Qp),
own γ (● g) ∗
⌜size g = Z.to_nat z⌝ ∗
⌜(set_fold Qp.add q g = 1)%Qp⌝ ∗
⌜set_fold Qp.add q g = 1%Qp⌝ ∗
Φ q
).
Local Hint Extern 0 (environments.envs_entails _ (rw_state_inv _ _ _)) =>
......@@ -76,20 +74,21 @@ Section proof.
Local Definition reader_locked (γ : gname) (q : Qp) : iProp Σ := own γ (◯ {[+ q +]}).
Local Definition writer_locked (γ : gname) : iProp Σ := own γ (● {# 3/4} ∅).
Local Lemma writer_locked_exclusive γ : writer_locked γ -∗ writer_locked γ -∗ False.
Local Lemma writer_locked_exclusive γ :
writer_locked γ -∗ writer_locked γ -∗ False.
Proof.
iIntros "H1 H2". iCombine "H1 H2" gives "%Hvalid". exfalso.
iIntros "H1 H2". iCombine "H1 H2" gives %Hvalid. exfalso.
rewrite
auth_auth_dfrac_op_valid
dfrac_op_own
dfrac_valid_own in Hvalid.
destruct Hvalid as [Htoomuch _].
contradict Htoomuch.
auto.
by destruct Hvalid as [? _].
Qed.
Local Lemma writer_locked_not_reader_locked γ q : writer_locked γ -∗ reader_locked γ q -∗ False.
Local Lemma writer_locked_not_reader_locked γ q :
writer_locked γ -∗ reader_locked γ q -∗ False.
Proof.
iIntros "H1 H2". iCombine "H1 H2" gives "%Hvalid". exfalso.
iIntros "H1 H2". iCombine "H1 H2" gives %Hvalid. exfalso.
apply auth_both_dfrac_valid in Hvalid as (_ & Hvalid & _).
generalize (Hvalid 0)=> /cmra_discrete_included_r /gmultiset_included /(_ q).
rewrite multiplicity_empty multiplicity_singleton. by lia.
......@@ -99,24 +98,23 @@ Section proof.
is_rw_lock γ lk Φ -∗ ▷ □ (∀ q, Φ q ∗-∗ Ψ q) -∗ is_rw_lock γ lk Ψ.
Proof.
iIntros "[#HΦdup [%l [-> #Hlockinv]]] #Hiff".
unfold is_rw_lock.
iSplitR.
{ iApply (internal_fractional_iff with "Hiff HΦdup"). }
{ iApply (internal_fractional_iff with "Hiff HΦdup"). }
iExists l; iSplitR; first done.
iApply (inv_iff with "[Hlockinv Hiff //]"); iIntros "!> !>".
iDestruct "Hiff" as "#Hiff".
iClear "HΦdup Hlockinv".
iSplit.
- iIntros "[%z [? Hstate]]". iExists z. iFrame.
iDestruct "Hstate" as "[?|[? [% [% (? & ? & ? & ?)]]]]".
- iIntros "(%z & ? & Hstate)". iExists z. iFrame.
iDestruct "Hstate" as "[?|(? & % & % & ? & ? & ? & ?)]".
+ iFrame.
+ iRight.
iFrame.
iExists _, _.
iFrame.
by iApply "Hiff".
- iIntros "[%z [? Hstate]]". iExists z. iFrame.
iDestruct "Hstate" as "[?|[? [% [% (? & ? & ? & ?)]]]]".
- iIntros "(%z & ? & Hstate)". iExists z. iFrame.
iDestruct "Hstate" as "[?|(? & % & % & ? & ? & ? & ?)]".
+ iFrame.
+ iRight.
iFrame.
......@@ -139,12 +137,12 @@ Section proof.
own γ (● { dq } g) ∗ own γ (◯ ({[+ v +]})) ⊢ ⌜v ∈ g⌝.
Proof.
iIntros "[Hauth Hfrag]".
iCombine "Hauth Hfrag" gives "%Hvalid".
iCombine "Hauth Hfrag" gives %Hvalid.
iPureIntro.
apply (auth_valid_gmultiset_singleton _ _ _ Hvalid).
Qed.
Local Lemma newlock_spec (Φ : Qp → iProp Σ) `{!AsFractional P Φ 1}:
Local Lemma newlock_spec (Φ : Qp → iProp Σ) `{!AsFractional P Φ 1} :
{{{ P }}}
newlock #()
{{{ lk γ, RET lk; is_rw_lock γ lk Φ }}}.
......@@ -152,89 +150,82 @@ Section proof.
iIntros (φ) "HΦ Hφ".
wp_lam.
iMod (own_alloc (● ∅)) as (γ) "Hγ".
{ apply auth_auth_valid; done. }
{ apply auth_auth_valid; done. }
wp_alloc l as "Hl".
iMod (inv_alloc N _ (rw_state_inv γ l Φ) with "[-Hφ]") as "#?".
{ rewrite [P]as_fractional.
eauto 10 with iFrame.
}
eauto 10 with iFrame. }
iApply "Hφ".
iSplitR.
{ iApply fractional_internal_fractional.
apply (as_fractional_fractional (P:=P)).
}
apply (as_fractional_fractional (P:=P)). }
eauto 10.
Qed.
Local Lemma try_acquire_reader_spec γ lk Φ:
Local Lemma try_acquire_reader_spec γ lk Φ :
{{{ is_rw_lock γ lk Φ }}}
try_acquire_reader lk
{{{ b, RET #b; if b is true then ∃ q, reader_locked γ q ∗ Φ q else True }}}.
{{{ (b : bool), RET #b; if b then ∃ q, reader_locked γ q ∗ Φ q else True }}}.
Proof.
iIntros (φ) "[#HΦdup [%l [-> #Hlockinv]]] Hφ".
iIntros (φ) "[#HΦdup (%l & -> & #Hlockinv)] Hφ".
wp_lam.
wp_bind (!_)%E.
iInv "Hlockinv" as (z) "[> Hl Hz]".
wp_load.
iSplitL "Hl Hz"; first eauto with iFrame.
iSplitL "Hl Hz"; first by eauto with iFrame.
iModIntro.
wp_pures.
destruct (Z.le_dec 0%Z z) as [Hle|?]; last first.
{ rewrite bool_decide_false //.
wp_pures.
iApply "Hφ".
done.
}
done. }
rewrite bool_decide_true //.
wp_pures.
wp_bind (CmpXchg _ _ _).
iInv "Hlockinv" as (z') "[> Hl Hz]".
wp_cmpxchg as Heq|?; last first.
wp_cmpxchg as [= ->]|?; last first.
{ iSplitR "Hφ".
{ eauto with iFrame. }
{ eauto with iFrame. }
iModIntro.
wp_pures.
by iApply "Hφ".
}
injection Heq as ->.
iDestruct "Hz" as "[[-> _]|[Hz_ge_0 [%q [%g Hg]]]]"; first contradiction.
by iApply "Hφ". }
iDestruct "Hz" as "[[-> _]|(Hz_ge_0 & %q & %g & Hg)]"; first done.
iDestruct "Hg" as "(Hauth & %Hsize & %Hfold & HΦ)".
rewrite -[q in Φ q]Qp.div_2.
iDestruct ("HΦdup" $! (q / 2)%Qp (q / 2)%Qp with "HΦ") as "[HΦ HΦgive]".
iMod (own_update _ _ (●(g ⊎ {[+ (q / 2)%Qp+]}) ⋅ ◯({[+ (q / 2)%Qp +]})) with "Hauth") as "[Hauth Hview]".
iMod (own_update _ _ (●(g ⊎ {[+ (q / 2)%Qp+]}) ⋅
◯({[+ (q / 2)%Qp +]})) with "Hauth") as "[Hauth Hview]".
{ apply auth_update_alloc.
rewrite -{2}[({[+ (q / 2)%Qp+]})]gmultiset_disj_union_left_id.
apply gmultiset_local_update_alloc.
}
apply gmultiset_local_update_alloc. }
iSplitR "HΦgive Hview Hφ".
{ iExists (z + 1)%Z.
iModIntro.
iModIntro.
iFrame.
iRight.
iSplitL "Hz_ge_0"; first eauto with lia.
iSplitL "Hz_ge_0"; first by eauto with lia.
iExists _, _.
iFrame.
iSplit.
{ iPureIntro.
rewrite gmultiset_size_disj_union gmultiset_size_singleton.
lia.
}
lia. }
iPureIntro.
rewrite
gmultiset_set_fold_disj_union
gmultiset_set_fold_singleton
-gmultiset_set_fold_comm_acc.
{ rewrite Qp.div_2 //. }
intros. rewrite 2!Qp.add_assoc [(_ + q/2)%Qp]Qp.add_comm //.
}
intros. rewrite 2!Qp.add_assoc [(_ + q/2)%Qp]Qp.add_comm //. }
iModIntro.
wp_pures.
iApply "Hφ".
eauto with iFrame.
Qed.
Local Lemma acquire_reader_spec γ lk Φ:
Local Lemma acquire_reader_spec γ lk Φ :
{{{ is_rw_lock γ lk Φ }}}
acquire_reader lk
{{{ q, RET #(); reader_locked γ q ∗ Φ q }}}.
......@@ -253,101 +244,94 @@ Section proof.
eauto.
Qed.
Local Lemma release_reader_spec γ lk Φ q:
Local Lemma release_reader_spec γ lk Φ q :
{{{ is_rw_lock γ lk Φ ∗ reader_locked γ q ∗ Φ q }}}
release_reader lk
{{{ RET #(); True }}}.
Proof.
iIntros (φ) "([#HΦdup [%l [-> Hlockinv]]] & Hlocked & HΦ) Hφ".
iIntros (φ) "((#HΦdup & %l & -> & Hlockinv) & Hlocked & HΦ) Hφ".
wp_lam.
wp_bind (FAA _ _).
iInv "Hlockinv" as (z) "[> Hl Hz]".
wp_faa.
unfold reader_locked.
iDestruct "Hz" as "[[_ Hempty]|[%Hz_ge_0 [%q' [%g (Hg & %Hsize & %Hsum & HΦq')]]]]".
iDestruct "Hz" as "[[_ Hempty]|(%Hz_ge_0 & %q' & %g & Hg & %Hsize & %Hsum & HΦq')]".
{ iExFalso.
iDestruct (own_auth_gmultiset_singleton_2 with "[$]") as "%".
multiset_solver.
}
iAssert (⌜(0 < z)%Z ∧ q ∈ g⌝)%I as "%".
{ iDestruct (own_auth_gmultiset_singleton_2 with "[$]") as "%".
iDestruct (own_auth_gmultiset_singleton_2 with "[$]") as %?.
multiset_solver. }
iAssert (⌜(0 < z)%Z ∧ q ∈ g⌝)%I as %?.
{ iDestruct (own_auth_gmultiset_singleton_2 with "[$]") as %?.
iPureIntro.
split; last assumption.
apply Z2Nat.neq_0_pos.
rewrite -Hsize gmultiset_size_empty_iff.
multiset_solver.
}
multiset_solver. }
iCombine "Hg Hlocked" as "Hown".
iMod (own_update _ _ (●(g ∖ {[+ q +]})) with "Hown") as "Hown".
{ apply auth_update_dealloc.
replace ε with ({[+ q +]} ∖ {[+ q +]} : gmultiset Qp); last first.
{ rewrite gmultiset_difference_diag //. }
{ rewrite gmultiset_difference_diag //. }
apply gmultiset_local_update_dealloc.
multiset_solver.
}
multiset_solver. }
iModIntro.
iSplitR "Hφ".
{ iExists (z + -1)%Z.
iFrame.
iRight.
iSplit.
{ eauto with lia. }
{ eauto with lia. }
iExists _, _.
iDestruct ("HΦdup" $! q q' with "[HΦ HΦq']") as "HΦ"; first iFrame.
iDestruct ("HΦdup" $! q q' with "[$HΦ $HΦq']") as "HΦ".
iModIntro.
iFrame.
iSplit.
{ iPureIntro.
rewrite gmultiset_size_difference; last multiset_solver.
rewrite gmultiset_size_singleton.
lia.
}
lia. }
iPureIntro.
rewrite -Hsum gmultiset_set_fold_comm_acc; last first.
{ intros. rewrite 2!Qp.add_assoc [(_ + q)%Qp]Qp.add_comm //. }
{ intros. rewrite 2!Qp.add_assoc [(_ + q)%Qp]Qp.add_comm //. }
rewrite
-gmultiset_set_fold_singleton
-gmultiset_set_fold_disj_union
gmultiset_disj_union_comm
-gmultiset_disj_union_difference //.
multiset_solver.
}
multiset_solver. }
wp_pures.
by iApply "Hφ".
Qed.
Local Lemma try_acquire_writer_spec γ lk Φ:
Local Lemma try_acquire_writer_spec γ lk Φ :
{{{ is_rw_lock γ lk Φ }}}
try_acquire_writer lk
{{{ b, RET #b; if b is true then writer_locked γ ∗ Φ 1%Qp else True }}}.
{{{ (b : bool), RET #b; if b then writer_locked γ ∗ Φ 1%Qp else True }}}.
Proof.
iIntros (φ) "[#HΦdup [%l [-> #Hlockinv]]] Hφ".
iIntros (φ) "(#HΦdup & %l & -> & #Hlockinv) Hφ".
wp_lam.
wp_bind (CmpXchg _ _ _).
iInv ("Hlockinv") as (z) "[> Hl Hz]".
wp_cmpxchg as Heq|?; last first.
wp_cmpxchg as [= ->]|?; last first.
{ iModIntro.
iSplitL "Hl Hz".
{ eauto with iFrame. }
{ eauto with iFrame. }
wp_pures.
by iApply "Hφ".
}
injection Heq as ->.
iDestruct "Hz" as "[[%H0_eq_1 ?]|[_ [%q [%g (Hg & %Hsize & %Hfold & HΦ)]]]]".
{ iExFalso. by contradict H0_eq_1. }
apply gmultiset_size_empty_inv in Hsize. subst g.
by iApply "Hφ". }
iDestruct "Hz" as "[[%H0_eq_1 ?]|(_ & %q & %g & Hg & %Hsize & %Hfold & HΦ)]".
{ done. }
apply gmultiset_size_empty_inv in Hsize as ->.
rewrite gmultiset_set_fold_empty in Hfold. subst q.
rewrite -[in (●{# 1} _)]Qp.quarter_three_quarter.
iDestruct "Hg" as "[Hg Hg_give]".
iModIntro.
iSplitL "Hl Hg".
{ eauto 10 with iFrame. }
{ eauto 10 with iFrame. }
wp_pures.
iApply "Hφ".
by iFrame.
Qed.
Local Lemma acquire_writer_spec γ lk Φ:
Local Lemma acquire_writer_spec γ lk Φ :
{{{ is_rw_lock γ lk Φ }}}
acquire_writer lk
{{{ RET #(); writer_locked γ ∗ Φ 1%Qp }}}.
......@@ -366,29 +350,26 @@ Section proof.
eauto.
Qed.
Local Lemma release_writer_spec γ lk Φ:
Local Lemma release_writer_spec γ lk Φ :
{{{ is_rw_lock γ lk Φ ∗ writer_locked γ ∗ Φ 1%Qp }}}
release_writer lk
{{{ RET #(); True }}}.
Proof.
iIntros (φ) "([#HΦdup [%l [-> #Hlockinv]]] & Hlocked & HΦ) Hφ".
iIntros (φ) "((#HΦdup & %l & -> & #Hlockinv) & Hlocked & HΦ) Hφ".
wp_lam.
iInv ("Hlockinv") as (z) "[> Hl Hz]".
wp_store.
iDestruct "Hz" as "[[? Hg]|[_ [% [% [Hg_owned _]]]]]"; last first.
iDestruct "Hz" as "[[? Hg]|(_ & % & % & Hg_owned & _)]"; last first.
{ iExFalso.
iCombine "Hg_owned Hlocked" gives "%Hvalid".
iCombine "Hg_owned Hlocked" gives %Hvalid.
rewrite
auth_auth_dfrac_op_valid
dfrac_op_own
dfrac_valid_own in Hvalid.
destruct Hvalid as [Htoomuch _].
contradict Htoomuch.
auto.
}
by destruct Hvalid as [? _]. }
iCombine "Hg Hlocked" as "Hown".
rewrite Qp.quarter_three_quarter.
iSplitR "Hφ"; first eauto 15 with iFrame.
iSplitR "Hφ"; first by eauto 15 with iFrame.
by iApply "Hφ".
Qed.
End proof.
......
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment