Commit c5ec5ddf authored by Dan Frumin's avatar Dan Frumin
Browse files

FLOCK FLOCK FLOCK ?!?!?!?

parent 7e1f9e05
From iris.heap_lang Require Export proofmode notation.
(* From iris.heap_lang Require Import spin_lock. *)
From iris_c.lib Require Export spin_lock.
From iris.heap_lang Require Import spin_lock.
(* From iris_c.lib Require Export spin_lock. *)
From iris.base_logic.lib Require Import cancelable_invariants auth saved_prop.
From iris.algebra Require Import auth agree excl frac gmap gset.
From iris.bi.lib Require Import fractional.
......@@ -12,255 +12,344 @@ Canonical Structure lockstateC := leibnizC lockstate.
Instance lockstate_inhabited : Inhabited lockstate := populate Unlocked.
(** We need to be able to allocate resources into the lock even when
it is in use -- for that we need to have /active/ and /pending/
propositions. If the lock is unlocked (not acquired), then all the
propositions are active (can be acquired); if the lock is locked
(acquired), then some thread has the ownership of the active
propositions, but any other thread can add a pending proposition.
Pending propositions are thus always held by the lock.
When a thread acquires the lock, it gets all the active
propositions. For the whole construction to make sense, the thread
should return exactly the same propositions once it releases the
lock. For this to work we need to ensure that the set of active
proposition has not changed since the lock has been acquired.
Thus, we use ghost state to track the exact content of the set of
active propositions.
If we have a full access to the resource (with fraction 1), we may
want to cancel it and get the proposition back. In order to do
that we need to make sure that if we have the full fraction for
accessing the resource, then this resource cannot be active. For
that purpose we also need to store the information about the
fractional permissions for the active propositions.
Finally, the actual propositional content of the resources is
shared via cancellable invariants. Each proposition (active or
pending) is stored in a cancellable invariant associated with it:
C(X) = X.prop ∗ X.token₁ ∨ X.token₂
The exclusive tokens allow the thread to take out the proposition
for the whole duration of the critical section. *)
Record flock_name := {
(** ghost name for the actual spin lock invariant *)
flock_lock_name : gname;
(** -//- for keeping the track of the state of the flock *)
flock_state_name : gname;
(** -//- for keeping track of all propositions in the flock *)
flock_props_name : gname;
(** -//- for keeping track of the "active" propositions,
once you relase the lock you need to know that the set of the active propositions
has not changed since you have acquired it *)
flock_props_active_name : gname
}.
(* positive so that we have a `Fresh` instance for `gset positive` *)
(* Defined as `positive` so that we have a `Fresh` instance for `gset positive`.
Doubles as an invariant name. *)
Definition prop_id := positive.
Canonical Structure gnameC := leibnizC gname.
Record PropPerm := {
prop_perm : frac;
prop_saved_name : gname;
prop_perm_name : gname
(** The trick here is to store only ghost names associated with a 'flock resource' in the flock invariant.
If we start storing propositions, then we end up in the LATER HELL *)
Record lock_res_name := {
flock_cinv_name : gname;
flock_token1_name : gname;
flock_token2_name : gname;
}.
Canonical Structure PropPermC := leibnizC PropPerm.
Canonical Structure lock_res_nameC := leibnizC lock_res_name.
Class flockG Σ :=
FlockG {
flock_stateG :> inG Σ (authR (optionUR (exclR lockstateC)));
flock_lockG :> lockG Σ;
flock_savedProp :> savedPropG Σ;
flock_tokens :> inG Σ fracR;
flock_props_active :> inG Σ (authR (optionUR (exclR (gmapC prop_id PropPermC))));
flock_props :> inG Σ (authR (gmapUR prop_id (prodR fracR (agreeR (prodC gnameC gnameC)))))
flock_cinvG :> cinvG Σ;
(* note the difference between the two RAs here ! *)
flock_props_active :> inG Σ (authR (optionUR (exclR (gmapC prop_id (prodC fracC lock_res_nameC)))));
flock_props :> inG Σ (authR (gmapUR prop_id (prodR fracR (agreeR lock_res_nameC))));
flock_tokens :> inG Σ (exclR unitC);
}.
Definition flockΣ : gFunctors :=
#[GFunctor (authR (optionUR (exclR lockstateC)))
;lockΣ
;savedPropΣ
;GFunctor fracR
;GFunctor (authR (optionUR (exclR (gmapC prop_id PropPermC))))
;GFunctor (authR (gmapUR prop_id (prodR fracR (agreeR (prodC gnameC gnameC)))))%CF].
Record lock_res `{flockG Σ} := {
res_prop : iProp Σ;
res_frac : frac;
res_name : lock_res_name;
}.
Definition LockRes `{flockG Σ} (R : iProp Σ) (π : frac) (ρ : lock_res_name) :=
{| res_prop := R; res_frac := π; res_name := ρ |}.
Instance subG_flockΣ Σ : subG flockΣ Σ flockG Σ.
Proof. solve_inG. Qed.
(* TODO: DF, finish this *)
(* Definition flockΣ : gFunctors := *)
(* #[GFunctor (authR (optionUR (exclR lockstateC))) *)
(* ;lockΣ *)
(* ;savedPropΣ *)
(* ;GFunctor fracR *)
(* ;GFunctor (authR (optionUR (exclR (gmapC prop_id PropPermC)))) *)
(* ;GFunctor (authR (gmapUR prop_id (prodR fracR (agreeR (prodC gnameC gnameC)))))%CF]. *)
(* Instance subG_flockΣ Σ : subG flockΣ Σ → flockG Σ. *)
(* Proof. solve_inG. Qed. *)
Section flock.
Context `{heapG Σ, flockG Σ}.
Variable N : namespace.
Definition flockN := N.@"flock".
Definition invN := N.@"flock_inv".
Definition lockN := N.@"flock_lock".
Definition resN := N.@"flock_res".
Definition to_props_map (f : gmap prop_id (gname * gname))
: gmapUR prop_id (prodR fracR (agreeR (prodC gnameC gnameC))) :=
(λ x, (1%Qp, to_agree (x.1, x.2))) <$> f.
(** * Definitions **)
Definition token (ρ : lock_res_name) : iProp Σ :=
own (flock_token1_name ρ) (Excl ()).
Definition token (ρ : lock_res_name) : iProp Σ :=
own (flock_token2_name ρ) (Excl ()).
Definition to_props_map_ (f : gmap prop_id PropPerm)
: gmapUR prop_id (prodR fracR (agreeR (prodC gnameC gnameC))) :=
(λ x, (prop_perm x, to_agree (prop_saved_name x, prop_perm_name x))) <$> f.
(* Definition C' (X : lock_res) : iProp Σ := *)
(* (res_prop X ∗ token₁ (res_name X) ∨ token₂ (res_name X))%I. *)
Lemma to_props_map_singleton_included fp i q ρ:
{[i := (q, to_agree ρ)]} to_props_map fp fp !! i = Some ρ.
Proof.
rewrite singleton_included=> -[[q' av] []].
rewrite /to_props_map lookup_fmap fmap_Some_equiv => -[v' [Hi [/= -> ->]]].
move=> /Some_pair_included_total_2 [_] /to_agree_included /leibniz_equiv_iff -> //.
rewrite Hi. by destruct v'.
Qed.
Definition from_active (f : gmap prop_id PropPerm)
: gmap prop_id (gname * gname) :=
(λ x, (prop_saved_name x, prop_perm_name x)) <$> f.
Definition C (R : iProp Σ) (ρ : lock_res_name) : iProp Σ :=
(R token ρ token ρ)%I.
Lemma from_active_empty : from_active = .
Proof. by rewrite /from_active fmap_empty. Qed.
(* Tokens that allow you to get all the propositions from `A` out of the invariants *)
Definition all_tokens (P : gmap prop_id lock_res_name) : iProp Σ :=
([ map] i X P, token X)%I.
Definition all_props (f : gmap prop_id (gname*gname)) : iProp Σ :=
([ map] i ρ f, R, saved_prop_own ρ.1 R R)%I.
(** For active propositions we also need to know the fraction which was used to access it *)
Definition from_active (A : gmap prop_id (frac * lock_res_name))
:= fmap snd A.
Lemma all_props_to_props_map_ f f1 f2 :
to_props_map f = to_props_map_ f1 to_props_map_ f2
all_props f all_props (from_active f1) all_props (from_active f2).
Proof. Admitted.
Definition flock_res (γ : flock_name) (s : prop_id) (X : lock_res) : iProp Σ :=
(own (flock_props_name γ) ( {[s := (res_frac X, to_agree (res_name X))]})
cinv (resN.@s) (flock_cinv_name (res_name X)) (C (res_prop X) (res_name X))
cinv_own (flock_cinv_name (res_name X)) (res_frac X))%I.
Definition all_tokens (f : gmap prop_id PropPerm) : iProp Σ :=
([ map] i ρ f, own (prop_perm_name ρ) (prop_perm ρ))%I.
Definition flocked
(γ : flock_name) (A : gmap prop_id lock_res) : iProp Σ :=
( fa : gmap prop_id (frac * lock_res_name),
fa = fmap (λ X, (res_frac X, res_name X)) A
(* Information we retain: the flock is locked .. *)
own (flock_state_name γ) ( (Excl' Locked))
(* What are the exact propositions that we have activated.. *)
own (flock_props_active_name γ) ( (Excl' fa))
(* Tokens and permissions for closing the active propositions .. *)
([ map] i X A, token (res_name X)
cinv (resN.@i) (flock_cinv_name (res_name X)) (C (res_prop X) (res_name X))
cinv_own (flock_cinv_name (res_name X)) (res_frac X)))%I.
Definition to_props_map (f : gmap prop_id lock_res_name)
: gmapUR prop_id (prodR fracR (agreeR lock_res_nameC)) :=
fmap (λ X, (1%Qp, to_agree X)) f.
Definition flock_inv (γ : flock_name) : iProp Σ :=
( (s : lockstate)
(fp : gmap prop_id (gname * gname))
(fa : gmap prop_id PropPerm),
(** fa -- active propositions, fp -- pending propositions *)
(fa : gmap prop_id (frac * lock_res_name))
(fp : gmap prop_id lock_res_name),
fp ## from_active fa
own (flock_state_name γ) ( (Excl' s))
own (flock_props_name γ) ( to_props_map (fp from_active fa))
own (flock_props_active_name γ) ( Excl' fa)
all_props fp
own (flock_props_active_name γ) ( Excl' fa)
all_tokens fp
match s with
| Locked =>
locked (flock_lock_name γ)
all_tokens fa
| Unlocked => own (flock_props_active_name γ) ( Excl' )
([ map] i πX fa, own (flock_props_name γ) ( {[i:=(πX.1,to_agree πX.2)]}))
| Unlocked =>
(* there are no active proposition *)
own (flock_props_active_name γ) ( Excl' )
end)%I.
Definition is_flock (γ : flock_name) (lk : val) : iProp Σ :=
(inv (flockN .@ "inv") (flock_inv γ)
is_lock (flockN .@ "lock") (flock_lock_name γ) lk
(inv invN (flock_inv γ)
is_lock lockN (flock_lock_name γ) lk
(own (flock_state_name γ) ( (Excl' Unlocked))))%I.
Definition flocked
(γ : flock_name) (f : gmap prop_id PropPerm) : iProp Σ :=
(own (flock_state_name γ) ( (Excl' Locked))
own (flock_props_active_name γ) ( Excl' f)
all_props (from_active f))%I.
Definition flock_res (γ : flock_name) (s : prop_id) (R : iProp Σ) (π : Qp) : iProp Σ :=
( ρ, saved_prop_own ρ.1 R own ρ.2 π
own (flock_props_name γ) ( {[s := (π, to_agree ρ)]}))%I.
(** * Lemmata **)
(** ** Basic properties of the CAPs *)
(* Lemma flock_res_op (γ : flock_name) (s : prop_id) (R : iProp Σ) (π1 π2 : frac) : *)
(* flock_res γ s R (π1+π2) ⊣⊢ flock_res γ s R π1 ∗ flock_res γ s R π2. *)
(* Proof. *)
(* rewrite /flock_res. iSplit. *)
(* - iDestruct 1 as (ρ) "(Hs & #Hinv & Hρ)". *)
(* iDestruct "Hρ" as "[Hρ1 Hρ2]". *)
(* iDestruct "Hs" as "[Hs1 Hs2]". *)
(* iSplitL "Hρ1 Hs1"; iExists _; by iFrame. *)
(* - iIntros "[H1 H2]". *)
(* iDestruct "H1" as (ρ) "(Hs1 & #Hinv1 & Hρ1)". *)
(* iDestruct "H2" as (ρ') "(Hs2 & #Hinv2 & Hρ2)". *)
(* iCombine "Hs1 Hs2" as "Hs". *)
(* iDestruct (own_valid with "Hs") *)
(* as %Hfoo%auth_valid_discrete. *)
(* simpl in Hfoo. apply singleton_valid in Hfoo. *)
(* destruct Hfoo as [_ Hfoo%agree_op_inv']. *)
(* fold_leibniz. rewrite -!Hfoo. *)
(* iCombine "Hρ1 Hρ2" as "Hρ". *)
(* rewrite !frac_op' agree_idemp. *)
(* iExists ρ. by iFrame. *)
(* Qed. *)
(* Global Instance flock_res_fractional γ s R : Fractional (flock_res γ s R). *)
(* Proof. intros p q. apply flock_res_op. Qed. *)
(* Global Instance flock_res_as_fractional γ s R π : *)
(* AsFractional (flock_res γ s R π) (flock_res γ s R) π. *)
(* Proof. split. done. apply _. Qed. *)
Lemma flock_res_op (γ : flock_name) (s : prop_id) (R : iProp Σ) (π1 π2 : frac) :
flock_res γ s R (π1+π2) flock_res γ s R π1 flock_res γ s R π2.
Lemma to_props_map_singleton_included fp i q ρ:
{[i := (q, to_agree ρ)]} to_props_map fp fp !! i = Some ρ.
Proof.
rewrite /flock_res. iSplit.
- iDestruct 1 as (ρ) "(#Hsaved & Hρ & Hs)".
iDestruct "Hρ" as "[Hρ1 Hρ2]".
iDestruct "Hs" as "[Hs1 Hs2]".
iSplitL "Hρ1 Hs1"; iExists _; by iFrame.
- iIntros "[H1 H2]".
iDestruct "H1" as (ρ) "(#Hsaved & Hρ1 & Hs1)".
iDestruct "H2" as (ρ') "(_ & Hρ2 & Hs2)".
iCombine "Hs1 Hs2" as "Hs".
iDestruct (own_valid with "Hs")
as %Hfoo%auth_valid_discrete.
simpl in Hfoo. apply singleton_valid in Hfoo.
destruct Hfoo as [_ Hfoo%agree_op_inv'].
fold_leibniz. rewrite -!Hfoo.
iCombine "Hρ1 Hρ2" as "Hρ".
rewrite !frac_op' agree_idemp.
iExists ρ. by iFrame.
rewrite singleton_included=> -[[q' av] []].
rewrite /to_props_map lookup_fmap fmap_Some_equiv => -[v' [Hi [/= -> ->]]].
move=> /Some_pair_included_total_2 [_] /to_agree_included /leibniz_equiv_iff -> //.
Qed.
Global Instance flock_res_fractional γ s R : Fractional (flock_res γ s R).
Proof. intros p q. apply flock_res_op. Qed.
Global Instance flock_res_as_fractional γ s R π :
AsFractional (flock_res γ s R π) (flock_res γ s R) π.
Proof. split. done. apply _. Qed.
Lemma to_props_map_delete fp i:
delete i (to_props_map fp) = to_props_map (delete i fp).
Proof.
by rewrite /to_props_map fmap_delete.
Qed.
Lemma flock_res_single_alloc (X : gset prop_id) γ lk R E :
flockN E
is_flock γ lk - R
={E}= s, s X flock_res γ s R 1.
(** ** Spectral and physical operations *)
Lemma flock_res_alloc_strong (X : gset prop_id) γ lk R E :
N E
is_flock γ lk -
R ={E}= s ρ, s X flock_res γ s (LockRes R 1 ρ).
Proof.
iIntros (?) "Hl HR". rewrite /is_flock. iDestruct "Hl" as "(#Hcinv & #Hlk)".
iMod (saved_prop_alloc R) as (ρ1) "#Hρ1".
iMod (own_alloc 1%Qp) as (ρ2) "Hρ2"; first done.
iInv (flockN.@"inv") as (s fp fa) "(>% & >Hstate & >Hauth & >Hfactive & Hfp & Hrest)" "Hcl".
iIntros (?) "Hl HR". rewrite /is_flock.
iDestruct "Hl" as "(#Hfl & #Hlk)".
(* Pick a fresh name *)
iInv invN as (s fa fp)
"(>% & >Hstate & >Haprops & >Haactive & >Htokens & Hst)" "Hcl".
pose (i := (fresh ((dom (gset prop_id) (fp from_active fa)) X))).
assert (i (dom (gset prop_id) (fp from_active fa)) X) as Hs.
{ apply is_fresh. }
apply not_elem_of_union in Hs. destruct Hs as [Hi1 Hi2].
iMod (own_update with "Hauth") as "Hauth".
{ apply (auth_update_alloc _ (to_props_map (<[i := (ρ1,ρ2)]> fp from_active fa))
{[ i := (1%Qp, to_agree (ρ1, ρ2)) ]}).
(* Alloc all the data for the resource *)
iMod (own_alloc (Excl ())) as (γt) "T1"; first done.
iMod (own_alloc (Excl ())) as (γt) "T2"; first done.
iMod (cinv_alloc _ (resN.@i) (R own γt (Excl ()) own γt (Excl ()))%I with "[HR T1]") as (γc) "[#HR Hρ]".
{ iNext. iLeft. by iFrame. }
pose (ρ :=
{| flock_cinv_name := γc;
flock_token1_name := γt;
flock_token2_name := γt |}).
(* Put it in the map of flock resources *)
iMod (own_update with "Haprops") as "Haprops".
{ apply (auth_update_alloc _ (to_props_map (<[i := ρ]> fp from_active fa))
{[ i := (1%Qp, to_agree ρ) ]}).
rewrite -insert_union_l.
rewrite /to_props_map /= fmap_insert.
apply alloc_local_update; last done.
apply (not_elem_of_dom (to_props_map (fp from_active fa)) i (D:=gset prop_id)).
by rewrite /to_props_map dom_fmap. }
iDestruct "Hauth" as "[Hauth Hres]".
iExists i. iMod ("Hcl" with "[-Hres Hρ1 Hρ2]") as "_".
{ iNext. iExists _,_,_. iFrame. iFrame "Hrest".
rewrite /all_props big_sepM_insert; last first.
+ apply (not_elem_of_dom _ i (D:=gset prop_id)).
revert Hi1. rewrite dom_union_L not_elem_of_union. set_solver.
+ iFrame "Hfp". iSplitR; last by eauto.
iPureIntro. apply map_disjoint_insert_l_2; eauto.
iDestruct "Haprops" as "[Haprops Hi]".
iMod ("Hcl" with "[-Hi Hρ]") as "_".
{ iNext. iExists s, fa,(<[i:=ρ]>fp).
iFrame. rewrite /all_tokens big_sepM_insert; last first.
{ apply (not_elem_of_dom _ i (D:=gset prop_id)).
revert Hi1. rewrite dom_union_L not_elem_of_union.
set_solver. }
iFrame. iPureIntro.
apply map_disjoint_insert_l_2; eauto.
eapply (not_elem_of_dom (D:=gset prop_id)).
intros Hi; apply Hi1. rewrite dom_union_L elem_of_union.
eauto. }
iModIntro; iSplit; eauto.
iExists (ρ1,ρ2). iFrame "Hres Hρ1 Hρ2".
intros Hi; apply Hi1. rewrite dom_union_L elem_of_union. eauto.
}
iModIntro; iExists i, ρ; iSplit; eauto.
by iFrame.
Qed.
Lemma flock_res_single_dealloc γ lk i R E :
flockN E
is_flock γ lk - flock_res γ i R 1
={E}= R', R' (R R').
Lemma flock_res_dealloc γ lk i X E :
N E
res_frac X = 1%Qp
is_flock γ lk -
flock_res γ i X ={E}= (res_prop X).
Proof.
iIntros (?) "Hl HR". rewrite /is_flock. iDestruct "Hl" as "(#Hcinv & #Hlk)".
iInv (flockN.@"inv") as ([|] fp fa) "(>% & >Hstate & >Hauth & >Hfactive & Hfp & Hrest)" "Hcl".
- iDestruct "Hrest" as ">[Hlocked Htokens]".
iDestruct "HR" as ([ρ1 ρ2]) "(#Hρ1 & Hρ2 & HR)". simpl.
iDestruct (own_valid_2 with "Hauth HR")
iIntros (? HX) "Hl HR". rewrite /is_flock.
iDestruct "Hl" as "(#Hfl & #Hlk)".
destruct X as [R ? ρ]. simpl in HX. rewrite HX; clear HX.
iDestruct "HR" as "(Hi & #Hiinv & Hρ)".
iInv invN as ([|] fa fp)
"(>% & >Hstate & >Haprops & >Haactive & >Htokens & Hst)" "Hcl".
(* Locked *)
- iDestruct "Hst" as ">[Hlocked Hactives]".
(* We can now show that the proposition `i` is *not* active *)
iDestruct (own_valid_2 with "Haprops Hi")
as %[Hfoo%to_props_map_singleton_included _]%auth_valid_discrete_2.
iAssert (fa !! i = None)%I with "[-]" as %Hbar.
{ remember (fa !! i) as fai. destruct fai as [[π ρ'1 ρ'2]|]; last done.
iExFalso.
assert (fp !! i = None) as Hbar.
{ apply lookup_union_Some_raw in Hfoo.
destruct Hfoo as [Hfoo | [? ?]]; last done.
specialize (H2 i). revert H2. rewrite Hfoo.
rewrite /from_active lookup_fmap -Heqfai /=. done. }
apply lookup_union_Some in Hfoo; last done.
destruct Hfoo as [Hfoo | Hfa].
- exfalso. rewrite Hfoo in Hbar. inversion Hbar.
- revert Hfa. rewrite /from_active lookup_fmap -Heqfai /= =>Hfa.
rewrite /all_tokens (big_sepM_lookup _ fa i); last done.
simplify_eq/=.
iDestruct (own_valid with "Htokens") as %Hbaz1%frac_valid'.
iDestruct (own_valid_2 with "Hρ2 Htokens") as %Hbaz2.
rewrite frac_op' in Hbaz2. exfalso.
eapply Qp_not_plus_q_ge_1. apply Hbaz2. }
assert (fp !! i = Some (ρ1, ρ2)) as Hbaz.
{ remember (fa !! i) as fai. destruct fai as [[π ρ']|]; last done.
symmetry in Heqfai.
rewrite (big_sepM_lookup _ fa i (π, ρ')) //.
iDestruct (own_valid_2 with "Hi Hactives") as %Hbaz.
exfalso. revert Hbaz. rewrite -auth_frag_op /=.
admit. }
assert (fp !! i = Some ρ) as Hbaz.
{ apply lookup_union_Some in Hfoo; last done.
destruct Hfoo as [? | Hfoo]; first done.
exfalso. revert Hfoo. rewrite /from_active lookup_fmap Hbar. done. }
exfalso. revert Hfoo. by rewrite /from_active lookup_fmap Hbar.
}
iMod (own_update_2 with "Hauth HR") as "Hauth".
iMod (own_update_2 with "Haprops Hi") as "Haprops".
{ apply auth_update_dealloc, (delete_singleton_local_update _ i _). }
rewrite /all_props (big_sepM_delete _ fp i (ρ1,ρ2)); last done.
iDestruct "Hfp" as "[HR' Hfp]".
iDestruct "HR'" as (R') "[Hsaved HR']".
iDestruct (saved_prop_agree with "Hρ1 Hsaved") as "Hfoo".
iMod ("Hcl" with "[-HR' Hfoo Hρ2]") as "_".
{ iNext. iExists Locked, (delete i fp),fa. iFrame.
rewrite /all_tokens (big_sepM_delete _ fp i ρ) //.
iDestruct "Htokens" as "[T2 Htokens]".
iMod (cinv_cancel with "Hiinv Hρ") as "HC". solve_ndisj.
rewrite /C /=. iDestruct "HC" as "[[HR >T1] | >T2']"; last first.
{ iDestruct (own_valid_2 with "T2 T2'") as %?. done. }
iFrame "HR".
(* Now that the resource is cancelled we close the flock invariant *)
iApply "Hcl". iNext.
iExists Locked,fa,(delete i fp). iFrame.
iSplit.
{ iPureIntro. by apply map_disjoint_delete_l. }
rewrite /to_props_map -fmap_delete.
rewrite delete_union (delete_notin (from_active fa)); first iFrame.
by rewrite /from_active lookup_fmap Hbar. }
iModIntro. iExists R'. iFrame.
- iDestruct "Hrest" as ">Haactive".
+ iPureIntro. by apply map_disjoint_delete_l.
+ rewrite to_props_map_delete delete_union.
rewrite (delete_notin (from_active fa)) //.
rewrite /from_active lookup_fmap Hbar //.
(* Unlocked *)
- iDestruct "Hst" as ">Hfactive".
iAssert (fa = ∅⌝)%I with "[-]" as %->.
{ iDestruct (own_valid_2 with "Haactive Hfactive")
as %[Hfoo%Excl_included _]%auth_valid_discrete_2.
iPureIntro. by unfold_leibniz. }
rewrite from_active_empty right_id.
iDestruct "HR" as ([ρ1 ρ2]) "(#Hρ1 & Hρ2 & HR)". simpl.
iDestruct (own_valid_2 with "Hauth HR")
rewrite /from_active fmap_empty /= right_id.
iDestruct (own_valid_2 with "Haprops Hi")
as %[Hfoo%to_props_map_singleton_included _]%auth_valid_discrete_2.
iMod (own_update_2 with "Hauth HR") as "Hauth".
iMod (own_update_2 with "Haprops Hi") as "Haprops".
{ apply auth_update_dealloc, (delete_singleton_local_update _ i _). }
rewrite /all_props (big_sepM_delete _ fp i (ρ1,ρ2)); last done.
iDestruct "Hfp" as "[HR' Hfp]".
iDestruct "HR'" as (R') "[Hsaved HR']".
iDestruct (saved_prop_agree with "Hρ1 Hsaved") as "Hfoo".
iMod ("Hcl" with "[-HR' Hfoo Hρ2]") as "_".
{ iNext. iExists Unlocked, (delete i fp),. iFrame.
rewrite !from_active_empty right_id.
rewrite /to_props_map fmap_delete. iFrame "Hauth".
iPureIntro. apply map_disjoint_empty_r. }
iModIntro. iExists R'. iFrame.
Qed.
rewrite /all_tokens (big_sepM_delete _ fp i ρ) //.
iDestruct "Htokens" as "[T2 Htokens]".
iMod (cinv_cancel with "Hiinv Hρ") as "HC". solve_ndisj.
rewrite /C /=. iDestruct "HC" as "[[HR >T1] | >T2']"; last first.
{ iDestruct (own_valid_2 with "T2 T2'") as %?. done. }
iFrame "HR".
(* Now that the resource is cancelled we close the flock invariant *)
iApply "Hcl". iNext.
iExists Unlocked,,(delete i fp). iFrame.
iSplit.
+ iPureIntro. by apply map_disjoint_delete_l.
+ rewrite /from_active fmap_empty /= right_id.
by rewrite to_props_map_delete.
Admitted.
Lemma newlock_cancel_spec :
Lemma newflock_spec :
{{{ True }}} newlock #() {{{ lk γ, RET lk; is_flock γ lk }}}.
Proof.
iIntros (Φ) "_ HΦ". rewrite -wp_fupd.
......@@ -272,239 +361,38 @@ Section flock.
iMod (own_alloc (( Excl' ) ( Excl' ))) as (γ_ac_props) "[Hacprops1 Hacprops2]".
{ apply auth_valid_discrete. simpl.
split; last done. by rewrite left_id. }
iApply (newlock_spec (flockN.@"lock") (own γ_state ( (Excl' Unlocked))) with "Hfrag").
iApply (newlock_spec lockN (own γ_state ( (Excl' Unlocked))) with "Hfrag").
iNext. iIntros (lk γ_lock) "#Hlock".
pose (γ := (Build_flock_name γ_lock γ_state γ_props γ_ac_props)).
iMod (inv_alloc (flockN.@"inv") _ (flock_inv γ) with "[-HΦ]") as "#Hinv".
{ iNext. iExists Unlocked, , . rewrite from_active_empty right_id. iFrame.
iSplit; eauto. by rewrite /all_props big_sepM_empty. }
iMod (inv_alloc invN _ (flock_inv γ) with "[-HΦ]") as "#Hinv".
{ iNext. iExists Unlocked, , . rewrite /from_active fmap_empty right_id. iFrame.
iSplit; eauto. by rewrite /all_tokens big_sepM_empty. }
iModIntro. iApply ("HΦ" $! lk γ with "[-]").
rewrite /is_flock. by iFrame "Hlock".
Qed.
(* {{{ is_flock γ lk ∗ *)
(* ([∗ list] (i, R, π) ∈ I, flock_res γ i R π) }}} *)
(* acquire lk *)
(* {{{ RET #(); *)