Commit 0b438db2 authored by Robbert Krebbers's avatar Robbert Krebbers

Bump Iris (make use of `excl_auth`).

parent aa3aca77
Pipeline #21906 passed with stage
in 19 minutes and 35 seconds
......@@ -9,5 +9,5 @@ build: [make "-j%{jobs}%"]
install: [make "install"]
remove: [ "sh" "-c" "rm -rf '%{lib}%/coq/user-contrib/iris-c" ]
depends: [
"coq-iris" { (= "dev.2019-10-25.0.bbd38120") | (= "dev") }
"coq-iris" { (= "dev.2019-11-21.4.d1787db2") | (= "dev") }
]
From iris.bi.lib Require Import fractional.
From iris.algebra Require Import auth agree excl frac gmap gset.
From iris.algebra Require Import auth agree lib.excl_auth frac gmap gset.
From iris.base_logic.lib Require Import cancelable_invariants auth saved_prop.
From iris.heap_lang Require Export proofmode notation.
From iris.heap_lang Require Import spin_lock.
......@@ -97,22 +97,21 @@ Defined.
*)
Class flockG Σ :=
FlockG {
flock_stateG :> inG Σ (authR (optionUR (exclR lockstateO)));
flock_stateG :> inG Σ (excl_authR lockstateO);
flock_lockG :> lockG Σ;
flock_cinvG :> cinvG Σ;
(* note the difference between the two RAs here ! *)
flock_props_active :> inG Σ (authR
(optionUR (exclR (gmapO lock_res_gname fracR))));
flock_props_active :> inG Σ (excl_authR (gmapO lock_res_gname fracR));
flock_props :> inG Σ (authR
(gmapUR lock_res_gname fracR));
flock_tokens :> inG Σ (exclR unitO);
}.
Definition flockΣ : gFunctors :=
#[GFunctor (authR (optionUR (exclR lockstateO)))
#[GFunctor (excl_authR lockstateO)
;lockΣ
;cinvΣ
;GFunctor (authR (optionUR (exclR (gmapO lock_res_gname fracO))))
;GFunctor (excl_authR (gmapO lock_res_gname fracO))
;GFunctor (authR (gmapUR lock_res_gname fracR))%OF].
Instance subG_flockΣ Σ : subG flockΣ Σ flockG Σ.
......@@ -170,9 +169,9 @@ Section flock.
(γ : flock_name) (A : gmap lock_res_gname (frac*iProp Σ)) : iProp Σ :=
(let fa := fmap fst A : gmap lock_res_gname frac in
(* Information we retain: the flock is locked .. *)
own (flock_state_name γ) ( (Excl' Locked))
own (flock_state_name γ) (E Locked)
(* What are the exact propositions that we have activated.. *)
own (flock_props_active_name γ) ( (Excl' fa))
own (flock_props_active_name γ) (E fa)
(* Tokens and permissions for closing the active propositions .. *)
([ map] ρ πR A, token ρ
cinv (resN.@(N_of_ρ ρ)) (flock_cinv_name ρ) (C πR.2 ρ)
......@@ -189,11 +188,11 @@ Section flock.
(fp : gmap lock_res_gname unit), (** aka mapset lock_res_name *)
(** ... and those sets are disjoint *)
fp ## from_active fa
own (flock_state_name γ) ( (Excl' s))
own (flock_state_name γ) (E s)
(** the totality of resources: fp ∪ fa *)
own (flock_props_name γ) ( to_props_map (fp from_active fa))
(** but we also need to know the exact contents of fa *)
own (flock_props_active_name γ) ( Excl' fa)
own (flock_props_active_name γ) (E fa)
(** the invariant keeps track of the tokens (token₂) for the
pending resource; when we activate a resource, we transfer
this token to the client, which uses it to open the
......@@ -213,13 +212,13 @@ Section flock.
| Unlocked =>
(** If the lock is NOT acquired, then there are no active
proposition *)
own (flock_props_active_name γ) ( Excl' )
own (flock_props_active_name γ) (E )
end)%I.
Definition is_flock (γ : flock_name) (lk : val) : iProp Σ :=
(inv invN (flock_inv γ)
is_lock lockN (flock_lock_name γ) lk
(own (flock_state_name γ) ( (Excl' Unlocked))))%I.
(own (flock_state_name γ) (E Unlocked)))%I.
(** * Lemmata **)
......@@ -377,10 +376,7 @@ Section flock.
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_both_valid.
iPureIntro. by unfold_leibniz. }
iDestruct (own_valid_2 with "Haactive Hfactive") as %->%excl_auth_agreeL.
rewrite /from_active fmap_empty /= right_id.
iDestruct (own_valid_2 with "Haprops Hρ")
as %[Hfoo%to_props_map_singleton_included _]%auth_both_valid.
......@@ -472,13 +468,13 @@ Section flock.
{{{ True }}} newlock #() {{{ lk γ, RET lk; is_flock γ lk }}}.
Proof.
iIntros (Φ) "_ HΦ". rewrite -wp_fupd.
iMod (own_alloc ( (Excl' Unlocked) (Excl' Unlocked)))
as (γ_state) "[Hauth Hfrag]"; first by apply auth_both_valid.
iMod (own_alloc (E Unlocked E Unlocked))
as (γ_state) "[Hauth Hfrag]"; first by apply excl_auth_valid.
iMod (own_alloc ( to_props_map )) as (γ_props) "Hprops".
{ by apply auth_auth_valid. }
iMod (own_alloc (( Excl' ) ( Excl' ))) as (γ_ac_props) "[Hacprops1 Hacprops2]".
{ by apply auth_both_valid. }
iApply (newlock_spec lockN (own γ_state ( (Excl' Unlocked))) with "Hfrag").
iMod (own_alloc (E E )) as (γ_ac_props) "[Hacprops1 Hacprops2]".
{ by apply excl_auth_valid. }
iApply (newlock_spec lockN (own γ_state (E Unlocked)) with "Hfrag").
iNext. iIntros (lk γ_lock) "#Hlock".
pose (γ := (Build_flock_name γ_lock γ_state γ_props γ_ac_props)).
iMod (inv_alloc invN _ (flock_inv γ) with "[-HΦ]") as "#Hinv".
......@@ -556,17 +552,12 @@ Section flock.
(* Locked ~~> Unlocked *)
iMod (own_update_2 with "Hstate Hflkd") as "Hstate".
{ apply (auth_update _ _ (Excl' Unlocked) (Excl' Unlocked)).
apply option_local_update.
by apply exclusive_local_update. }
{ apply (excl_auth_update _ _ Unlocked). }
iDestruct "Hstate" as "[Hstate Hunflkd]".
(* Empty up the set of active propositions *)
iMod (own_update_2 with "Haactive Hfactive") as "[Haactive Hfactive]".
{ apply (auth_update _ _ (Excl' )
(Excl' )).
by apply option_local_update, exclusive_local_update. }
{ apply (excl_auth_update _ _ ). }
pose (fa := fst <$> I).
iMod (own_frag_empty with "Haprops") as "[Haprops Hemp]".
......@@ -605,17 +596,12 @@ Section flock.
- iDestruct "Hst" as "(>Hlocked2 & ?)".
iExFalso. iApply (locked_exclusive with "Hlocked Hlocked2").
- iDestruct "Hst" as ">Hfactive".
iAssert (fa = ∅⌝)%I with "[-]" as %->.
{ iDestruct (own_valid_2 with "Haactive Hfactive")
as %[Hfoo%Excl_included _]%auth_both_valid.
iPureIntro. by unfold_leibniz. }
iDestruct (own_valid_2 with "Haactive Hfactive") as %->%excl_auth_agreeL.
rewrite /from_active fmap_empty /= right_id.
(* Unlocked ~~> Locked *)
iMod (own_update_2 with "Hstate Hunlk") as "Hstate".
{ apply (auth_update _ _ (Excl' Locked) (Excl' Locked)).
apply option_local_update.
by apply exclusive_local_update. }
{ apply (excl_auth_update _ _ Locked). }
iDestruct "Hstate" as "[Hstate Hflkd]".
iApply "HΦ". rewrite /flocked.
......@@ -624,9 +610,7 @@ Section flock.
(* Designate the propositions from I as active *)
pose (fa := fst <$> I).
iMod (own_update_2 with "Haactive Hfactive") as "[Haactive Hfactive]".
{ apply (auth_update _ _ (Excl' fa)
(Excl' fa)).
by apply option_local_update, exclusive_local_update. }
{ apply (excl_auth_update _ _ fa). }
iFrame "Hfactive".
rewrite /flock_res. rewrite !big_sepM_sep.
......
From stdpp Require Import namespaces.
From iris_c.vcgen Require Import proofmode.
From iris_c.lib Require Import mset list.
From iris.algebra Require Import frac_auth csum excl agree.
From iris.algebra Require Import lib.excl_auth.
(** This example is meant to demonstrate the usage of atomic rules for
the primitive operations, as well as for function calls. In this file
......@@ -52,35 +52,9 @@ Section test.
iIntros "? H". iApply cwp_fun; simpl. vcg; iIntros "? !>". by iApply "H".
Qed.
(** Ghost state definitions and lemmas *)
Definition gpointsto γ (b : bool) := own γ ( (Excl' b)).
Notation "γ '≔' b" := (gpointsto γ b) (at level 80).
Definition gauth γ b := own γ ( (Excl' b)).
Lemma gagree γ b1 b2 :
γ b1 - gauth γ b2 - b1 = b2.
Proof.
iIntros "H1 H2".
by iDestruct (own_valid_2 with "H2 H1")
as %[<-%Excl_included%leibniz_equiv _]%auth_both_valid.
Qed.
Lemma gnew : (|==> γ, gauth γ false γ false)%I.
Proof.
iMod (own_alloc ( (Excl' false) (Excl' false)))%I as (γ) "[H1 H2]";
first by apply auth_both_valid.
eauto with iFrame.
Qed.
Lemma gupdate b3 γ b1 b2 :
γ b1 - gauth γ b2 == γ b3 gauth γ b3.
Proof.
iIntros "H1 H2".
iMod (own_update_2 with "H2 H1") as "[? ?]".
{ apply auth_update, option_local_update.
by apply (exclusive_local_update (Excl b2) (Excl b3)). }
by iFrame.
Qed.
(** The correctness of the test function. *)
Definition test_inv cl γl γr : iProp Σ := ( b1 b2, gauth γl b1 gauth γr b2
(** The correctness of the test function. *)
Definition test_inv cl γl γr : iProp Σ := ( b1 b2,
own γl (E b1) own γr (E b2)
match b1, b2 with
| false, false => cl C #0
| true, false => cl C #10
......@@ -94,52 +68,55 @@ Section test.
(cl C #10 cl C #11) }}.
Proof.
iIntros "Hl". iApply cwp_seq_bind. iApply cwp_fun. simpl.
iMod gnew as (γl) "[H1 lb]".
iMod gnew as (γr) "[H2 rb]".
iMod (own_alloc (E false E false)) as (γl) "[H1 lb]"; first by apply excl_auth_valid.
iMod (own_alloc (E false E false)) as (γr) "[H2 rb]"; first by apply excl_auth_valid.
iApply (cwp_insert_res _ _ (test_inv cl γl γr) with "[H1 H2 Hl]").
{ iNext. iExists false,false. iFrame. }
iApply (cwp_bin_op _ _ (λ v, v = #10 γl true)%I
(λ v, v = #11 γr true)%I
iApply (cwp_bin_op _ _ (λ v, v = #10 own γl (E true))%I
(λ v, v = #11 own γr (E true))%I
with "[lb] [rb]").
- vcg. unfold test_inv. iIntros "[H R]".
iDestruct "H" as (b1 b2) "(H1 & H2 & H)".
iDestruct (gagree with "lb H1") as %<-.
iDestruct (own_valid_2 with "H1 lb") as %->%excl_auth_agreeL.
destruct b2; iNext; iModIntro.
+ iMod (gupdate true with "lb H1") as "[lb H1]".
+ iMod (own_update_2 with "H1 lb") as "[H1 lb]";
first by apply (excl_auth_update _ _ true).
iApply (storeme_spec with "H").
iIntros "Hl". iFrame "R".
iSplitR "lb"; last by (vcg_continue; eauto with iFrame).
iExists _,_; eauto with iFrame.
+ iMod (gupdate true with "lb H1") as "[lb H1]".
iSplitR "lb"; first by (iExists _,_; eauto with iFrame).
vcg_continue; auto.
+ iMod (own_update_2 with "H1 lb") as "[H1 lb]";
first by apply (excl_auth_update _ _ true).
iApply (storeme_spec with "H").
iIntros "Hl". iFrame "R".
iSplitR "lb"; last by (vcg_continue; eauto with iFrame).
iExists _,_; eauto with iFrame.
iSplitR "lb"; first by (iExists _,_; eauto with iFrame).
vcg_continue; auto.
- iApply (cwp_store _ _ (λ v, v = cloc_to_val cl)%I
(λ v, v = #11)%I).
1,2: vcg; eauto.
iIntros (? ? -> ->) "[H R]". unfold test_inv.
iDestruct "H" as (b1 b2) "(H1 & H2 & H)".
iDestruct (gagree with "rb H2") as %<-.
iDestruct (own_valid_2 with "H2 rb") as %->%excl_auth_agreeL.
iModIntro.
destruct b1; iEval (simpl) in "H".
+ iExists cl, _. iFrame. iSplit; first done.
iIntros "Hl".
iMod (gupdate true with "rb H2") as "[rb H2]".
iMod (own_update_2 with "H2 rb") as "[H2 rb]";
first by apply (excl_auth_update _ _ true).
iModIntro. iSplitR "rb"; last by eauto with iFrame.
iExists _,_; eauto with iFrame.
+ iExists cl, _. iFrame. iSplit; first done.
iIntros "Hl".
iMod (gupdate true with "rb H2") as "[rb H2]".
iMod (own_update_2 with "H2 rb") as "[H2 rb]";
first by apply (excl_auth_update _ _ true).
iModIntro. iSplitR "rb"; last by eauto with iFrame.
iExists _,_; eauto with iFrame.
- iIntros (v1 v2) "[% lb] [% rb]"; simplify_eq/=.
iExists #21; simpl. iSplit; first done.
iIntros "H". iDestruct "H" as (b1 b2) "(H1 & H2 & H)".
do 3 iModIntro.
iDestruct (gagree with "lb H1") as %<-.
iDestruct (gagree with "rb H2") as %<-.
iDestruct (own_valid_2 with "lb H1") as %->%excl_auth_agreeL.
iDestruct (own_valid_2 with "rb H2") as %->%excl_auth_agreeL.
iDestruct "H" as "[H|H]"; iModIntro; vcg; eauto with iFrame.
Qed.
End test.
Markdown is supported
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