...
 
Commits (75)
......@@ -26,18 +26,19 @@ variables:
## Build jobs
build-coq.8.8.2:
build-coq.8.9.0:
<<: *template
variables:
OPAM_PINS: "coq version 8.8.2"
TIMING_CONF: "coq-8.8.2"
OPAM_PINS: "coq version 8.9.0"
TIMING_CONF: "coq-8.9.0"
tags:
- fp-timing
build-iris.dev:
<<: *template
variables:
OPAM_PINS: "coq version 8.8.2 coq-stdpp.dev git git+https://gitlab.mpi-sws.org/iris/stdpp.git#$STDPP_REV coq-iris.dev git git+https://gitlab.mpi-sws.org/FP/iris-coq.git#$IRIS_REV"
OCAML: "ocaml-base-compiler.4.07.0"
OPAM_PINS: "coq version 8.10.dev coq-stdpp.dev git git+https://gitlab.mpi-sws.org/iris/stdpp.git#$STDPP_REV coq-iris.dev git git+https://gitlab.mpi-sws.org/FP/iris-coq.git#$IRIS_REV"
except:
only:
- triggers
......
......@@ -6,7 +6,7 @@ Some example verification demonstrating the use of Iris.
This version is known to compile with:
- Coq 8.8.2
- Coq 8.9.0
- A development version of [Iris](https://gitlab.mpi-sws.org/FP/iris-coq/)
- The coq86-devel branch of [Autosubst](https://github.com/uds-psl/autosubst)
......
-Q theories iris_examples
-arg -w -arg -notation-overridden,-redundant-canonical-projection,-several-object-files
# We sometimes want to locally override notation and there is no good way to do that with scopes.
-arg -w -arg -notation-overridden
# non-canonical projections (https://github.com/coq/coq/pull/10076) do not exist yet in 8.9.
-arg -w -arg -redundant-canonical-projection
# change_no_check does not exist yet in 8.9.
-arg -w -arg -convert_concl_no_check
theories/barrier/proof.v
theories/barrier/specification.v
theories/barrier/barrier.v
theories/barrier/protocol.v
theories/barrier/example_client.v
theories/barrier/example_joining_existentials.v
......@@ -99,3 +104,8 @@ theories/logatom/flat_combiner/atomic_sync.v
theories/logatom/flat_combiner/misc.v
theories/logatom/snapshot/spec.v
theories/logatom/snapshot/atomic_snapshot.v
theories/logatom/conditional_increment/spec.v
theories/logatom/conditional_increment/cinc.v
theories/logatom/rdcss/rdcss.v
theories/logatom/rdcss/spec.v
theories/logatom/rdcss/lib/gc.v
......@@ -9,6 +9,6 @@ build: [make "-j%{jobs}%"]
install: [make "install"]
remove: ["rm" "-rf" "%{lib}%/coq/user-contrib/iris_examples"]
depends: [
"coq-iris" { (= "dev.2019-04-17.0.60d28bbb") | (= "dev") }
"coq-iris" { (= "dev.2019-06-13.0.860bd8e4") | (= "dev") }
"coq-autosubst" { = "dev.coq86" }
]
......@@ -7,9 +7,9 @@ From iris_examples.barrier Require Import proof specification.
Set Default Proof Using "Type".
Definition one_shotR (Σ : gFunctors) (F : cFunctor) :=
csumR (exclR unitC) (agreeR $ laterC $ F (iPreProp Σ)).
csumR (exclR unitC) (agreeR $ laterC $ F (iPreProp Σ) _).
Definition Pending {Σ F} : one_shotR Σ F := Cinl (Excl ()).
Definition Shot {Σ} {F : cFunctor} (x : F (iProp Σ)) : one_shotR Σ F :=
Definition Shot {Σ} {F : cFunctor} (x : F (iProp Σ) _) : one_shotR Σ F :=
Cinr $ to_agree $ Next $ cFunctor_map F (iProp_fold, iProp_unfold) x.
Class oneShotG (Σ : gFunctors) (F : cFunctor) :=
......@@ -28,7 +28,7 @@ Section proof.
Local Set Default Proof Using "Type*".
Context `{!heapG Σ, !barrierG Σ, !spawnG Σ, !oneShotG Σ F}.
Context (N : namespace).
Local Notation X := (F (iProp Σ)).
Local Notation X := (F (iProp Σ) _).
Definition barrier_res γ (Φ : X iProp Σ) : iProp Σ :=
( x, own γ (Shot x) Φ x)%I.
......
This diff is collapsed.
From iris.algebra Require Export sts.
From iris.base_logic Require Import lib.own.
From stdpp Require Export gmap.
Set Default Proof Using "Type".
(** The STS describing the main barrier protocol. Every state has an index-set
associated with it. These indices are actually [gname], because we use them
with saved propositions. *)
Inductive phase := Low | High.
Record state := State { state_phase : phase; state_I : gset gname }.
Add Printing Constructor state.
Inductive token := Change (i : gname) | Send.
Global Instance stateT_inhabited: Inhabited state := populate (State Low ).
Global Instance Change_inj : Inj (=) (=) Change.
Proof. by injection 1. Qed.
Inductive prim_step : relation state :=
| ChangeI p I2 I1 : prim_step (State p I1) (State p I2)
| ChangePhase I : prim_step (State Low I) (State High I).
Definition tok (s : state) : propset token :=
{[ t | i, t = Change i i state_I s ]}
(if state_phase s is High then {[ Send ]} else ).
Global Arguments tok !_ /.
Canonical Structure sts := sts.Sts prim_step tok.
(* The set of states containing some particular i *)
Definition i_states (i : gname) : propset state := {[ s | i state_I s ]}.
(* The set of low states *)
Definition low_states : propset state := {[ s | state_phase s = Low ]}.
Lemma i_states_closed i : sts.closed (i_states i) {[ Change i ]}.
Proof.
split; first (intros [[] I]; set_solver).
(* If we do the destruct of the states early, and then inversion
on the proof of a transition, it doesn't work - we do not obtain
the equalities we need. So we destruct the states late, because this
means we can use "destruct" instead of "inversion". *)
intros s1 s2 Hs1 [T1 T2 Hdisj Hstep'].
inversion_clear Hstep' as [? ? ? ? Htrans _ _ Htok].
destruct Htrans as [[] ??|]; done || set_solver.
Qed.
Lemma low_states_closed : sts.closed low_states {[ Send ]}.
Proof.
split; first (intros [??]; set_solver).
intros s1 s2 Hs1 [T1 T2 Hdisj Hstep'].
inversion_clear Hstep' as [? ? ? ? Htrans _ _ Htok].
destruct Htrans as [[] ??|]; done || set_solver.
Qed.
(* Proof that we can take the steps we need. *)
Lemma signal_step I : sts.steps (State Low I, {[Send]}) (State High I, ).
Proof. apply rtc_once. constructor; first constructor; set_solver. Qed.
Lemma wait_step i I :
i I
sts.steps (State High I, {[ Change i ]}) (State High (I {[ i ]}), ).
Proof.
intros. apply rtc_once.
constructor; first constructor; [set_solver..|].
apply elem_of_equiv=>-[j|]; last set_solver.
destruct (decide (i = j)); set_solver.
Qed.
Lemma split_step p i i1 i2 I :
i I i1 I i2 I i1 i2
sts.steps
(State p I, {[ Change i ]})
(State p ({[i1; i2]} I {[i]}), {[ Change i1; Change i2 ]}).
Proof.
intros. apply rtc_once. constructor; first constructor.
- destruct p; set_solver.
- destruct p; set_solver.
- apply elem_of_equiv=> /= -[j|]; last set_solver.
set_unfold; rewrite !(inj_iff Change).
assert (Change j match p with Low => : propset token | High => {[Send]} end False)
as -> by (destruct p; set_solver).
destruct (decide (i1 = j)) as [->|]; first naive_solver.
destruct (decide (i2 = j)) as [->|]; first naive_solver.
destruct (decide (i = j)) as [->|]; naive_solver.
Qed.
......@@ -16,11 +16,11 @@ Section proof.
Context `{inG Σ (frac_authR (gmultisetUR val))}.
Definition bagM_inv (γb : name Σ b) (γ : gname) : iProp Σ :=
inv NI ( X, bag_contents b γb X own γ (! X))%I.
inv NI ( X, bag_contents b γb X own γ (F X))%I.
Definition bagM (γb : name Σ b) (γ : gname) (x : val) : iProp Σ :=
(is_bag b NB γb x bagM_inv γb γ)%I.
Definition bagPart (γ : gname) (q : Qp) (X : gmultiset val) : iProp Σ :=
(own γ (!{q} X))%I.
(own γ (F{q} X))%I.
Lemma bagPart_compose (γ: gname) (q1 q2: Qp) (X Y : gmultiset val) :
bagPart γ q1 X - bagPart γ q2 Y - bagPart γ (q1+q2) (X Y).
......@@ -50,8 +50,8 @@ Section proof.
iIntros (Φ) "_ HΦ". iApply wp_fupd.
iApply (newBag_spec b NB); eauto.
iNext. iIntros (v γb) "[#Hbag Hcntn]".
iMod (own_alloc (! ! )) as (γ) "[Hown Hpart]"; first done.
iMod (inv_alloc NI _ ( X, bag_contents b γb X own γ (! X))%I with "[Hcntn Hown]") as "#Hinv".
iMod (own_alloc (F F )) as (γ) "[Hown Hpart]"; first by apply auth_both_valid.
iMod (inv_alloc NI _ ( X, bag_contents b γb X own γ (F X))%I with "[Hcntn Hown]") as "#Hinv".
{ iNext. iExists _. iFrame. }
iApply "HΦ". iModIntro. iExists _,_. iFrame "Hinv Hbag Hpart".
Qed.
......
......@@ -16,28 +16,28 @@ Proof. solve_inG. Qed.
Section ccounter.
Context `{!heapG Σ, !cntG Σ, !ccounterG Σ} (N : namespace).
Lemma ccounterRA_valid (m n : natR) (q : frac): (! m !{q} n) (n m)%nat.
Lemma ccounterRA_valid (m n : natR) (q : frac): (F m F{q} n) (n m)%nat.
Proof.
intros ?.
(* This property follows directly from the generic properties of the relevant RAs. *)
by apply nat_included, (frac_auth_included_total q).
Qed.
Lemma ccounterRA_valid_full (m n : natR): (! m ! n) (n = m)%nat.
Lemma ccounterRA_valid_full (m n : natR): (F m F n) (n = m)%nat.
Proof.
by intros ?%frac_auth_agree.
Qed.
Lemma ccounterRA_update (m n : natR) (q : frac): (! m !{q} n) ~~> (! (S m) !{q} (S n)).
Lemma ccounterRA_update (m n : natR) (q : frac): (F m F{q} n) ~~> (F (S m) F{q} (S n)).
Proof.
apply frac_auth_update, (nat_local_update _ _ (S _) (S _)).
lia.
Qed.
Definition ccounter_inv (γ₁ γ₂ : gname): iProp Σ :=
( n, own γ₁ (! n) γ₂ ⤇½ (Z.of_nat n))%I.
( n, own γ₁ (F n) γ₂ ⤇½ (Z.of_nat n))%I.
Definition is_ccounter (γ₁ γ₂ : gname) (l : loc) (q : frac) (n : natR) : iProp Σ := (own γ₁ (!{q} n) inv (N .@ "counter") (ccounter_inv γ₁ γ₂) Cnt N l γ₂)%I.
Definition is_ccounter (γ₁ γ₂ : gname) (l : loc) (q : frac) (n : natR) : iProp Σ := (own γ₁ (F{q} n) inv (N .@ "counter") (ccounter_inv γ₁ γ₂) Cnt N l γ₂)%I.
(** The main proofs. *)
Lemma is_ccounter_op γ₁ γ₂ q1 q2 (n1 n2 : nat) :
......@@ -58,7 +58,7 @@ Section ccounter.
iIntros (Φ) "_ HΦ". rewrite -wp_fupd.
wp_apply newcounter_spec; auto.
iIntros () "H"; iDestruct "H" as (γ₂) "[#HCnt Hown]".
iMod (own_alloc (! m%nat ! m%nat)) as (γ₁) "[Hγ Hγ']"; first done.
iMod (own_alloc (F m%nat F m%nat)) as (γ₁) "[Hγ Hγ']"; first by apply auth_both_valid.
iMod (inv_alloc (N .@ "counter") _ (ccounter_inv γ₁ γ₂) with "[Hγ Hown]").
{ iNext. iExists _. by iFrame. }
iModIntro. iApply "HΦ". rewrite /is_ccounter; eauto.
......@@ -70,7 +70,7 @@ Section ccounter.
{{{ (y : Z), RET #y; is_ccounter γ₁ γ₂ q (S n) }}}.
Proof.
iIntros (Φ) "[Hown #[Hinv HCnt]] HΦ".
iApply (incr_spec N γ₂ _ (own γ₁ (!{q} n))%I (λ _, (own γ₁ (!{q} (S n))))%I with "[] [Hown]"); first set_solver.
iApply (incr_spec N γ₂ _ (own γ₁ (F{q} n))%I (λ _, (own γ₁ (F{q} (S n))))%I with "[] [Hown]"); first set_solver.
- iIntros (m) "!# [HOwnElem HP]".
iInv (N .@ "counter") as (k) "[>H1 >H2]" "HClose".
iDestruct (makeElem_eq with "HOwnElem H2") as %->.
......@@ -94,7 +94,7 @@ Section ccounter.
{{{ (c : Z), RET #c; Z.of_nat n c is_ccounter γ₁ γ₂ q n }}}.
Proof.
iIntros (Φ) "[Hown #[Hinv HCnt]] HΦ".
wp_apply (read_spec N γ₂ _ (own γ₁ (!{q} n))%I (λ m, n m (own γ₁ (!{q} n)))%I with "[] [Hown]"); first set_solver.
wp_apply (read_spec N γ₂ _ (own γ₁ (F{q} n))%I (λ m, n m (own γ₁ (F{q} n)))%I with "[] [Hown]"); first set_solver.
- iIntros (m) "!# [HownE HOwnfrag]".
iInv (N .@ "counter") as (k) "[>H1 >H2]" "HClose".
iDestruct (makeElem_eq with "HownE H2") as %->.
......@@ -115,7 +115,7 @@ Section ccounter.
{{{ RET #n; is_ccounter γ₁ γ₂ 1 n }}}.
Proof.
iIntros (Φ) "[Hown #[Hinv HCnt]] HΦ".
wp_apply (read_spec N γ₂ _ (own γ₁ (! n))%I (λ m, Z.of_nat n = m (own γ₁ (! n)))%I with "[] [Hown]"); first set_solver.
wp_apply (read_spec N γ₂ _ (own γ₁ (F n))%I (λ m, Z.of_nat n = m (own γ₁ (F n)))%I with "[] [Hown]"); first set_solver.
- iIntros (m) "!# [HownE HOwnfrag]".
iInv (N .@ "counter") as (k) "[>H1 >H2]" "HClose".
iDestruct (makeElem_eq with "HownE H2") as %->.
......
......@@ -29,7 +29,7 @@ Section monotone_counter.
algebra we shall be using. The Iris library contains all the ingredients
needed to compose this particular resource algebra from simpler components,
however to illustrate how to define our own we will define it from scratch.
In the subsequent section we show how to obtain an equivalent resource
algebra from the building blocks provided by the Iris Coq library.
*)
......@@ -423,7 +423,7 @@ Section monotone_counter'.
Proof.
(* Use a simplified definition of validity for when the underlying CMRA is discrete, i.e., an RA.
The general definition also involves the use of step-indices, which is not needed in our case. *)
rewrite auth_valid_discrete_2.
rewrite auth_both_valid.
split.
- intros [? _]; by apply mnat_included.
- intros ?%mnat_included; done.
......@@ -460,7 +460,7 @@ Section monotone_counter'.
iIntros (Φ) "_ HCont".
rewrite /newCounter -wp_fupd.
wp_lam.
iMod (own_alloc ( (0%nat : mnatUR) 0%nat)) as (γ) "[HAuth HFrac]".
iMod (own_alloc ( (0%nat : mnatUR) (0%nat : mnatUR))) as (γ) "[HAuth HFrac]".
- apply mcounterRA_valid_auth_frag'; auto.
- wp_alloc as "Hpt".
iMod (inv_alloc N _ (counter_inv' γ) with "[Hpt HAuth]") as "HInv".
......@@ -505,7 +505,7 @@ Section monotone_counter'.
iInv N as (k) ">[Hpt HOwnAuth]" "HClose".
destruct (decide (k = m)); subst.
+ wp_cas_suc.
iMod (own_update γ (( m n)) ( (S m : mnatUR) ( S n)) with "[HOwnFrag HOwnAuth]") as "[HOwnAuth HOwnFrag]".
iMod (own_update γ (( m n)) ( (S m : mnatUR) ( (S n : mnatUR))) with "[HOwnFrag HOwnAuth]") as "[HOwnAuth HOwnFrag]".
{ apply mcounterRA_update'. }
{ rewrite own_op; iFrame. }
iMod ("HClose" with "[Hpt HOwnAuth]") as "_".
......@@ -547,21 +547,21 @@ Section ccounter.
algebra, specialized to our use case. These are listed in the exercise in
the relevant section of the lecture notes. *)
(* We are using some new notation. The frac_auth library defines the notation
!{q} n to mean ◯ (q, n) as we used in the lecture notes. Further, ●! m
means ● (1, m) and ◯! n means ◯ (1, n). *)
Lemma ccounterRA_valid (m n : natR) (q : frac): (! m !{q} n) (n m)%nat.
F{q} n to mean ◯ (q, n) as we used in the lecture notes. Further, ●F m
means ● (1, m) and ◯F n means ◯ (1, n). *)
Lemma ccounterRA_valid (m n : natR) (q : frac): (F m F{q} n) (n m)%nat.
Proof.
intros ?.
(* This property follows directly from the generic properties of the relevant RAs. *)
by apply nat_included, (frac_auth_included_total q).
Qed.
Lemma ccounterRA_valid_full (m n : natR): (! m ! n) (n = m)%nat.
Lemma ccounterRA_valid_full (m n : natR): (F m F n) (n = m)%nat.
Proof.
by intros ?%frac_auth_agree.
Qed.
Lemma ccounterRA_update (m n : natR) (q : frac): (! m !{q} n) ~~> (! (S m) !{q} (S n)).
Lemma ccounterRA_update (m n : natR) (q : frac): (F m F{q} n) ~~> (F (S m) F{q} (S n)).
Proof.
apply frac_auth_update, (nat_local_update _ _ (S _) (S _)).
lia.
......@@ -580,10 +580,10 @@ Section ccounter.
Context `{!heapG Σ, !ccounterG Σ} (N : namespace).
Definition ccounter_inv (γ : gname) (l : loc) : iProp Σ :=
( n, own γ (! n) l #n)%I.
( n, own γ (F n) l #n)%I.
Definition is_ccounter (γ : gname) (l : loc) (q : frac) (n : natR) : iProp Σ :=
(own γ (!{q} n) inv N (ccounter_inv γ l))%I.
(own γ (F{q} n) inv N (ccounter_inv γ l))%I.
(** The main proofs. *)
......@@ -606,7 +606,7 @@ Section ccounter.
{{{ γ , RET #; is_ccounter γ 1 0%nat }}}.
Proof.
iIntros (Φ) "_ HΦ". rewrite -wp_fupd /newCounter /=. wp_lam. wp_alloc as "Hpt".
iMod (own_alloc (! O%nat ! 0%nat)) as (γ) "[Hγ Hγ']"; first done.
iMod (own_alloc (F O%nat F 0%nat)) as (γ) "[Hγ Hγ']"; first by apply auth_both_valid.
iMod (inv_alloc N _ (ccounter_inv γ ) with "[Hpt Hγ]").
{ iNext. iExists 0%nat. by iFrame. }
iModIntro. iApply "HΦ". rewrite /is_ccounter; eauto.
......
This diff is collapsed.
From stdpp Require Import namespaces.
From iris.heap_lang Require Export lifting notation.
From iris.program_logic Require Export atomic.
Set Default Proof Using "Type".
(** A general logically atomic interface for conditional increment. *)
Record atomic_cinc {Σ} `{!heapG Σ} := AtomicCinc {
(* -- operations -- *)
new_counter : val;
cinc : val;
set_flag : val;
get : val;
(* -- other data -- *)
name : Type;
name_eqdec : EqDecision name;
name_countable : Countable name;
(* -- predicates -- *)
is_counter (N : namespace) (γs : name) (v : val) : iProp Σ;
counter_content (γs : name) (flag : bool) (c : Z) : iProp Σ;
(* -- predicate properties -- *)
is_counter_persistent N γs v : Persistent (is_counter N γs v);
counter_content_timeless γs f c : Timeless (counter_content γs f c);
counter_content_exclusive γs f1 c1 f2 c2 :
counter_content γs f1 c1 - counter_content γs f2 c2 - False;
(* -- operation specs -- *)
new_counter_spec N :
{{{ True }}}
new_counter #()
{{{ ctr γs, RET ctr ; is_counter N γs ctr counter_content γs true 0 }}};
cinc_spec N γs v :
is_counter N γs v -
<<< (b : bool) (n : Z), counter_content γs b n >>>
cinc v @∖↑N
<<< counter_content γs b (if b then n + 1 else n), RET #() >>>;
set_flag_spec N γs v (new_b: bool) :
is_counter N γs v -
<<< (b : bool) (n : Z), counter_content γs b n >>>
set_flag v #new_b @∖↑N
<<< counter_content γs new_b n, RET #() >>>;
get_spec N γs v:
is_counter N γs v -
<<< (b : bool) (n : Z), counter_content γs b n >>>
get v @∖↑N
<<< counter_content γs b n, RET #n >>>;
}.
Arguments atomic_cinc _ {_}.
Existing Instances
is_counter_persistent counter_content_timeless
name_countable name_eqdec.
......@@ -27,6 +27,8 @@ Record hocap_stack {Σ} `{!heapG Σ} := AtomicStack {
pop : val;
(* -- other data -- *)
name : Type;
name_eqdec : EqDecision name;
name_countable : Countable name;
(* -- predicates -- *)
is_stack (N : namespace) (γs : name) (v : val) : iProp Σ;
stack_content_frag (γs : name) (l : list val) : iProp Σ;
......@@ -61,9 +63,9 @@ Record hocap_stack {Σ} `{!heapG Σ} := AtomicStack {
}.
Arguments hocap_stack _ {_}.
Existing Instance is_stack_persistent.
Existing Instance stack_content_frag_timeless.
Existing Instance stack_content_auth_timeless.
Existing Instances
is_stack_persistent stack_content_frag_timeless stack_content_auth_timeless
name_eqdec name_countable.
(** Show that our way of writing the [pop_spec] is equivalent to what is done in
[concurrent_stack.spec]. IOW, the conjunction-vs-match doesn't matter. Fixing
......@@ -165,7 +167,7 @@ Section logatom_hocap.
iIntros (Φ) "_ HΦ". iApply wp_fupd. iApply logatom.new_stack_spec; first done.
iIntros "!>" (γs s) "[Hstack Hcont]".
iMod (own_alloc ( Excl' [] Excl' [])) as (γw) "[Hs● Hs◯]".
{ apply auth_valid_discrete_2. split; done. }
{ apply auth_both_valid. split; done. }
iApply ("HΦ" $! (γs, γw)). rewrite /hocap_is_stack. iFrame.
iApply inv_alloc. eauto with iFrame.
Qed.
......@@ -212,11 +214,11 @@ Section logatom_hocap.
iIntros (???) "Hf1 Hf2". iDestruct (own_valid_2 with "Hf1 Hf2") as %[].
Qed.
Next Obligation.
iIntros (???) "Ha1 Ha2". iDestruct (own_valid_2 with "Ha1 Ha2") as %[].
iIntros (???) "Ha1 Ha2". by iDestruct (own_valid_2 with "Ha1 Ha2") as %[].
Qed.
Next Obligation.
iIntros (???) "Hf Ha". iDestruct (own_valid_2 with "Ha Hf") as
%[->%Excl_included%leibniz_equiv _]%auth_valid_discrete_2. done.
%[->%Excl_included%leibniz_equiv _]%auth_both_valid. done.
Qed.
Next Obligation.
iIntros (???) "Hf Ha". iMod (own_update_2 with "Ha Hf") as "[? ?]".
......
......@@ -11,6 +11,8 @@ Record atomic_stack {Σ} `{!heapG Σ} := AtomicStack {
pop : val;
(* -- other data -- *)
name : Type;
name_eqdec : EqDecision name;
name_countable : Countable name;
(* -- predicates -- *)
is_stack (N : namespace) (γs : name) (v : val) : iProp Σ;
stack_content (γs : name) (l : list val) : iProp Σ;
......@@ -36,5 +38,6 @@ Record atomic_stack {Σ} `{!heapG Σ} := AtomicStack {
}.
Arguments atomic_stack _ {_}.
Existing Instance is_stack_persistent.
Existing Instance stack_content_timeless.
Existing Instances
is_stack_persistent stack_content_timeless
name_countable name_eqdec.
......@@ -175,7 +175,7 @@ Section stack.
wp_apply alloc_spec; first done. iIntros (head) "Hhead". wp_let.
wp_apply alloc_spec; first done. iIntros (offer) "Hoffer". wp_let.
iMod (own_alloc ( Excl' [] Excl' [])) as (γs) "[Hs● Hs◯]".
{ apply auth_valid_discrete_2. split; done. }
{ apply auth_both_valid. split; done. }
iMod (inv_alloc stackN _ (stack_inv γs head offer) with "[-HΦ Hs◯]").
{ iNext. iExists None, None, _. iFrame. done. }
wp_pures. iApply "HΦ". iFrame "Hs◯". iModIntro. iExists _, _. auto.
......@@ -209,7 +209,7 @@ Section stack.
- (* The CAS succeeded. Update everything accordingly. *)
iMod "AU" as (l') "[Hl' [_ Hclose]]".
iDestruct (own_valid_2 with "Hs● Hl'") as
%[->%Excl_included%leibniz_equiv _]%auth_valid_discrete_2.
%[->%Excl_included%leibniz_equiv _]%auth_both_valid.
iMod (own_update_2 with "Hs● Hl'") as "[Hs● Hl']".
{ eapply auth_update, option_local_update, (exclusive_local_update _ (Excl _)). done. }
iMod ("Hclose" with "Hl'") as "HΦ". iModIntro.
......@@ -283,7 +283,7 @@ Section stack.
iDestruct "Hlist" as ">%". subst stack_rep.
iMod "AU" as (l') "[Hl' [_ Hclose]]".
iDestruct (own_valid_2 with "Hs● Hl'") as
%[->%Excl_included%leibniz_equiv _]%auth_valid_discrete_2.
%[->%Excl_included%leibniz_equiv _]%auth_both_valid.
iMod ("Hclose" with "Hl'") as "HΦ".
iSplitR "HΦ"; first by eauto 10 with iFrame.
iIntros "!>". wp_pures. by iApply "HΦ".
......@@ -305,7 +305,7 @@ Section stack.
and we are done. *)
iMod "AU" as (l') "[Hl' [_ Hclose]]".
iDestruct (own_valid_2 with "Hs● Hl'") as
%[->%Excl_included%leibniz_equiv _]%auth_valid_discrete_2.
%[->%Excl_included%leibniz_equiv _]%auth_both_valid.
destruct l as [|v' l]; simpl.
{ (* Contradiction. *) iDestruct "Hlist" as ">%". done. }
iDestruct "Hlist" as (tail' q' rep') "[>Heq [>Htail' Hlist]]".
......@@ -345,13 +345,13 @@ Section stack.
iInv stackN as (stack_rep offer_rep l) "(>Hs● & >H↦ & Hlist & Hoff)".
iMod "AUoff" as (l') "[Hl' [_ Hclose]]".
iDestruct (own_valid_2 with "Hs● Hl'") as
%[->%Excl_included%leibniz_equiv _]%auth_valid_discrete_2.
%[->%Excl_included%leibniz_equiv _]%auth_both_valid.
iMod (own_update_2 with "Hs● Hl'") as "[Hs● Hl']".
{ eapply auth_update, option_local_update, (exclusive_local_update _ (Excl _)). done. }
iMod ("Hclose" with "Hl'") as "HQoff".
iMod "AU" as (l') "[Hl' [_ Hclose]]".
iDestruct (own_valid_2 with "Hs● Hl'") as
%[->%Excl_included%leibniz_equiv _]%auth_valid_discrete_2.
%[->%Excl_included%leibniz_equiv _]%auth_both_valid.
iMod (own_update_2 with "Hs● Hl'") as "[Hs● Hl']".
{ eapply auth_update, option_local_update, (exclusive_local_update _ (Excl _)). done. }
iMod ("Hclose" with "Hl'") as "HΦ".
......
......@@ -11,7 +11,7 @@ Class syncG Σ := sync_tokG :> inG Σ syncR.
Definition syncΣ : gFunctors := #[GFunctor (constRF syncR)].
Instance subG_syncΣ {Σ} : subG syncΣ Σ syncG Σ.
Proof. by intros ?%subG_inG. Qed.
Proof. solve_inG. Qed.
Section atomic_sync.
Context `{EqDecision A, !heapG Σ, !lockG Σ}.
......
......@@ -58,7 +58,7 @@ Definition flatΣ : gFunctors :=
savedPredΣ val ].
Instance subG_flatΣ {Σ} : subG flatΣ Σ flatG Σ.
Proof. intros [?%subG_inG [? _]%subG_inv]%subG_inv. split; apply _. Qed.
Proof. solve_inG. Qed.
Section proof.
Context `{!heapG Σ, !lockG Σ, !flatG Σ} (N: namespace).
......
......@@ -2,7 +2,7 @@
From iris.program_logic Require Export weakestpre.
From iris.heap_lang Require Export lang proofmode notation.
From iris.algebra Require Import auth frac gmap agree.
From iris.algebra Require Import excl auth frac gmap agree.
From iris.bi Require Import fractional.
From iris.base_logic Require Import auth.
......
From iris.algebra Require Import auth excl gmap.
From iris.base_logic.lib Require Export own invariants.
From iris.proofmode Require Import tactics.
From iris.heap_lang Require Export lang locations lifting.
Set Default Proof Using "Type".
Import uPred.
Definition gcN: namespace := nroot .@ "gc".
Definition gc_mapUR : ucmraT := gmapUR loc $ optionR $ exclR $ valC.
Definition to_gc_map (gcm: gmap loc val) : gc_mapUR := (λ v : val, Excl' v) <$> gcm.
Class gcG (Σ : gFunctors) := GcG {
gc_inG :> inG Σ (authR (gc_mapUR));
gc_name : gname
}.
Arguments gc_name {_} _ : assert.
Class gcPreG (Σ : gFunctors) := {
gc_preG_inG :> inG Σ (authR (gc_mapUR))
}.
Definition gcΣ : gFunctors :=
#[ GFunctor (authR (gc_mapUR)) ].
Instance subG_gcPreG {Σ} : subG gcΣ Σ gcPreG Σ.
Proof. solve_inG. Qed.
Section defs.
Context `{!invG Σ, !heapG Σ, gG: gcG Σ}.
Definition gc_inv_P: iProp Σ :=
(((gcm: gmap loc val), own (gc_name gG) ( to_gc_map gcm) ([ map] l v gcm, (l v)) ) )%I.
Definition gc_inv : iProp Σ := inv gcN gc_inv_P.
Definition gc_mapsto (l: loc) (v: val) : iProp Σ := own (gc_name gG) ( {[l := Excl' v]}).
Definition is_gc_loc (l: loc) : iProp Σ := own (gc_name gG) ( {[l := None]}).
End defs.
Section to_gc_map.
Lemma to_gc_map_valid gcm: to_gc_map gcm.
Proof. intros l. rewrite lookup_fmap. by case (gcm !! l). Qed.
Lemma to_gc_map_empty: to_gc_map = .
Proof. by rewrite /to_gc_map fmap_empty. Qed.
Lemma to_gc_map_singleton l v: to_gc_map {[l := v]} = {[l := Excl' v]}.
Proof. by rewrite /to_gc_map fmap_insert fmap_empty. Qed.
Lemma to_gc_map_insert l v gcm:
to_gc_map (<[l := v]> gcm) = <[l := Excl' v]> (to_gc_map gcm).
Proof. by rewrite /to_gc_map fmap_insert. Qed.
Lemma to_gc_map_delete l gcm :
to_gc_map (delete l gcm) = delete l (to_gc_map gcm).
Proof. by rewrite /to_gc_map fmap_delete. Qed.
Lemma lookup_to_gc_map_None gcm l :
gcm !! l = None to_gc_map gcm !! l = None.
Proof. by rewrite /to_gc_map lookup_fmap=> ->. Qed.
Lemma lookup_to_gc_map_Some gcm l v :
gcm !! l = Some v to_gc_map gcm !! l = Some (Excl' v).
Proof. by rewrite /to_gc_map lookup_fmap=> ->. Qed.
Lemma lookup_to_gc_map_Some_2 gcm l w :
to_gc_map gcm !! l = Some w v, gcm !! l = Some v.
Proof.
rewrite /to_gc_map lookup_fmap. rewrite fmap_Some.
intros (x & Hsome & Heq). eauto.
Qed.
Lemma lookup_to_gc_map_Some_3 gcm l w :
to_gc_map gcm !! l = Some (Excl' w) gcm !! l = Some w.
Proof.
rewrite /to_gc_map lookup_fmap. rewrite fmap_Some.
intros (x & Hsome & Heq). by inversion Heq.
Qed.
Lemma excl_option_included (v: val) y:
y Excl' v y y = Excl' v.
Proof.
intros ? H. destruct y.
- apply Some_included_exclusive in H;[ | apply _ | done ].
setoid_rewrite leibniz_equiv_iff in H.
by rewrite H.
- apply is_Some_included in H.
+ by inversion H.
+ by eapply mk_is_Some.
Qed.
Lemma gc_map_singleton_included gcm l v :
{[l := Some (Excl v)]} to_gc_map gcm gcm !! l = Some v.
Proof.
rewrite singleton_included.
setoid_rewrite Some_included_total.
intros (y & Hsome & Hincluded).
pose proof (lookup_valid_Some _ _ _ (to_gc_map_valid gcm) Hsome) as Hvalid.
pose proof (excl_option_included _ _ Hvalid Hincluded) as Heq.
rewrite Heq in Hsome.
apply lookup_to_gc_map_Some_3.
by setoid_rewrite leibniz_equiv_iff in Hsome.
Qed.
End to_gc_map.
Lemma gc_init `{!invG Σ, !heapG Σ, !gcPreG Σ} E:
(|==> _ : gcG Σ, |={E}=> gc_inv)%I.
Proof.
iMod (own_alloc ( (to_gc_map ))) as (γ) "H●".
{ rewrite auth_auth_valid. exact: to_gc_map_valid. }
iModIntro.
iExists (GcG Σ _ γ).
iAssert (gc_inv_P (gG := GcG Σ _ γ)) with "[H●]" as "P".
{
iExists _. iFrame.
by iApply big_sepM_empty.
}
iMod ((inv_alloc gcN E gc_inv_P) with "P") as "#InvGC".
iModIntro. iFrame "#".
Qed.
Section gc.
Context `{!invG Σ, !heapG Σ, !gcG Σ}.
(* FIXME: still needs a constructor. *)
Global Instance is_gc_loc_persistent (l: loc): Persistent (is_gc_loc l).
Proof. rewrite /is_gc_loc. apply _. Qed.
Global Instance is_gc_loc_timeless (l: loc): Timeless (is_gc_loc l).
Proof. rewrite /is_gc_loc. apply _. Qed.
Global Instance gc_mapsto_timeless (l: loc) (v: val): Timeless (gc_mapsto l v).
Proof. rewrite /is_gc_loc. apply _. Qed.
Global Instance gc_inv_P_timeless: Timeless gc_inv_P.
Proof. rewrite /gc_inv_P. apply _. Qed.
Lemma make_gc l v E: gcN E gc_inv - l v ={E}= gc_mapsto l v.
Proof.
iIntros (HN) "#Hinv Hl".
iMod (inv_open_timeless _ gcN _ with "Hinv") as "[P Hclose]"=>//.
iDestruct "P" as (gcm) "[H● HsepM]".
destruct (gcm !! l) as [v' | ] eqn: Hlookup.
- (* auth map contains l --> contradiction *)
iDestruct (big_sepM_lookup with "HsepM") as "Hl'"=>//.
by iDestruct (mapsto_valid_2 with "Hl Hl'") as %?.
- iMod (own_update with "H●") as "[H● H◯]".
{
apply lookup_to_gc_map_None in Hlookup.
apply (auth_update_alloc _ (to_gc_map (<[l := v]> gcm)) (to_gc_map ({[l := v]}))).
rewrite to_gc_map_insert to_gc_map_singleton.
pose proof (to_gc_map_valid gcm).
setoid_rewrite alloc_singleton_local_update=>//.
}
iMod ("Hclose" with "[H● HsepM Hl]").
+ iExists _.
iDestruct (big_sepM_insert with "[HsepM Hl]") as "HsepM"=>//; iFrame. iFrame.
+ iModIntro. by rewrite /gc_mapsto to_gc_map_singleton.
Qed.
Lemma gc_is_gc l v: gc_mapsto l v - is_gc_loc l.
Proof.
iIntros "Hgc_l". rewrite /gc_mapsto.
assert (Excl' v = (Excl' v) None)%I as ->. { done. }
rewrite -op_singleton auth_frag_op own_op.
iDestruct "Hgc_l" as "[_ H◯_none]".
iFrame.
Qed.
Lemma is_gc_lookup_Some l gcm: is_gc_loc l - own (gc_name _) ( to_gc_map gcm) - v, gcm !! l = Some v.
iIntros "Hgc_l H◯".
iCombine "H◯ Hgc_l" as "Hcomb".
iDestruct (own_valid with "Hcomb") as %Hvalid.
iPureIntro.
apply auth_both_valid in Hvalid as [Hincluded Hvalid].
setoid_rewrite singleton_included in Hincluded.
destruct Hincluded as (y & Hsome & _).
eapply lookup_to_gc_map_Some_2.
by apply leibniz_equiv_iff in Hsome.
Qed.
Lemma gc_mapsto_lookup_Some l v gcm: gc_mapsto l v - own (gc_name _) ( to_gc_map gcm) - gcm !! l = Some v .
Proof.
iIntros "Hgc_l H●".
iCombine "H● Hgc_l" as "Hcomb".
iDestruct (own_valid with "Hcomb") as %Hvalid.
iPureIntro.
apply auth_both_valid in Hvalid as [Hincluded Hvalid].
by apply gc_map_singleton_included.
Qed.
(** An accessor to make use of [gc_mapsto].
This opens the invariant *before* consuming [gc_mapsto] so that you can use
this before opening an atomic update that provides [gc_mapsto]!. *)
Lemma gc_access E:
gcN E
gc_inv ={E, E gcN}= l v, gc_mapsto l v -
(l v ( w, l w == gc_mapsto l w |={E gcN, E}=> True)).
Proof.
iIntros (HN) "#Hinv".
iMod (inv_open_timeless _ gcN _ with "Hinv") as "[P Hclose]"=>//.
iIntros "!>" (l v) "Hgc_l".
iDestruct "P" as (gcm) "[H● HsepM]".
iDestruct (gc_mapsto_lookup_Some with "Hgc_l H●") as %Hsome.
iDestruct (big_sepM_delete with "HsepM") as "[Hl HsepM]"=>//.
iFrame. iIntros (w) "Hl".
iMod (own_update_2 with "H● Hgc_l") as "[H● H◯]".
{ apply (auth_update _ _ (<[l := Excl' w]> (to_gc_map gcm)) {[l := Excl' w]}).
eapply singleton_local_update.
{ by apply lookup_to_gc_map_Some in Hsome. }
by apply option_local_update, exclusive_local_update.
}
iDestruct (big_sepM_insert with "[Hl HsepM]") as "HsepM"; [ | iFrame | ].
{ apply lookup_delete. }
rewrite insert_delete. rewrite <- to_gc_map_insert.
iModIntro. iFrame.
iMod ("Hclose" with "[H● HsepM]"); [ iExists _; by iFrame | by iModIntro].
Qed.
Lemma is_gc_access l E: gcN E gc_inv - is_gc_loc l ={E, E gcN}= v, l v (l v ={E gcN, E}= True).
Proof.
iIntros (HN) "#Hinv Hgc_l".
iMod (inv_open_timeless _ gcN _ with "Hinv") as "[P Hclose]"=>//.
iModIntro.
iDestruct "P" as (gcm) "[H● HsepM]".
iDestruct (is_gc_lookup_Some with "Hgc_l H●") as %Hsome.
destruct Hsome as [v Hsome].
iDestruct (big_sepM_lookup_acc with "HsepM") as "[Hl HsepM]"=>//.
iExists _. iFrame.
iIntros "Hl".
iMod ("Hclose" with "[H● HsepM Hl]"); last done.
iExists _. iFrame.
by (iApply ("HsepM" with "Hl")).
Qed.
End gc.
This diff is collapsed.
From stdpp Require Import namespaces.
From iris.heap_lang Require Export lifting notation.
From iris.program_logic Require Export atomic.
From iris_examples.logatom.rdcss Require Export gc.
Set Default Proof Using "Type".
(** A general logically atomic interface for conditional increment. *)
Record atomic_rdcss {Σ} `{!heapG Σ, !gcG Σ} := AtomicRdcss {
(* -- operations -- *)
new_rdcss : val;
rdcss: val;
get : val;
(* -- other data -- *)
name : Type;
name_eqdec : EqDecision name;
name_countable : Countable name;
(* -- predicates -- *)
is_rdcss (N : namespace) (γ : name) (v : val) : iProp Σ;
rdcss_content (γ : name) (n : Z) : iProp Σ;
(* -- predicate properties -- *)
is_rdcss_persistent N γ v : Persistent (is_rdcss N γ v);
rdcss_content_timeless γ n : Timeless (rdcss_content γ n);
rdcss_content_exclusive γ n1 n2 : rdcss_content γ n1 - rdcss_content γ n2 - False;
(* -- operation specs -- *)
new_rdcss_spec N :
N ## gcN gc_inv -
{{{ True }}}
new_rdcss #()
{{{ lln γ, RET lln ; is_rdcss N γ lln rdcss_content γ 0 }}};
rdcss_spec N γ v lm (m1 n1 n2 : Z):
is_rdcss N γ v - is_gc_loc lm -
<<< (m n: Z), gc_mapsto lm #m rdcss_content γ n >>>
rdcss #lm v #m1 #n1 #n2 @((∖↑N)∖↑gcN)
<<< gc_mapsto lm #m rdcss_content γ (if decide (m = m1 n = n1) then n2 else n), RET #n >>>;
get_spec N γ v:
is_rdcss N γ v -
<<< (n : Z), rdcss_content γ n >>>
get v @(∖↑N)
<<< rdcss_content γ n, RET #n >>>;
}.
Arguments atomic_rdcss _ {_} {_}.
Existing Instances
is_rdcss_persistent rdcss_content_timeless
name_countable name_eqdec.
This diff is collapsed.
......@@ -11,40 +11,46 @@ Set Default Proof Using "Type".
Implementing atomic pair snapshot data structure from Sergey et al. (ESOP 2015) *)
Record atomic_snapshot {Σ} `{!heapG Σ} := AtomicSnapshot {
newPair : val;
writeX : val;
writeY : val;
readPair : val;
new_snapshot : val;
read : val;
write : val;
read_with : val;
(* other data *)
name: Type;
name_eqdec : EqDecision name;
name_countable : Countable name;
(* predicates *)
is_pair (N : namespace) (γ : name) (p : val) : iProp Σ;
pair_content (γ : name) (a: val * val) : iProp Σ;
is_snapshot (N : namespace) (γ : name) (p : val) : iProp Σ;
snapshot_content (γ : name) (a: val) : iProp Σ;
(* predicate properties *)
is_pair_persistent N γ p : Persistent (is_pair N γ p);
pair_content_timeless γ a : Timeless (pair_content γ a);
pair_content_exclusive γ a1 a2 :
pair_content γ a1 - pair_content γ a2 - False;
is_snapshot_persistent N γ p : Persistent (is_snapshot N γ p);
snapshot_content_timeless γ a : Timeless (snapshot_content γ a);
snapshot_content_exclusive γ a1 a2 :
snapshot_content γ a1 - snapshot_content γ a2 - False;
(* specs *)
newPair_spec N (v1 v2 : val) :
{{{ True }}} newPair (v1, v2)%V {{{ γ p, RET p; is_pair N γ p pair_content γ (v1, v2) }}};
writeX_spec N γ (v: val) p :
is_pair N γ p -
<<< v1 v2 : val, pair_content γ (v1, v2) >>>
writeX (p, v)%V
new_snapshot_spec N (v : val) :
{{{ True }}} new_snapshot v {{{ γ p, RET p; is_snapshot N γ p snapshot_content γ v }}};
read_spec N γ p :
is_snapshot N γ p -
<<< v : val, snapshot_content γ v >>>
read p
@ ∖↑N
<<< pair_content γ (v, v2), RET #() >>>;
writeY_spec N γ (v: val) p :
is_pair N γ p -
<<< v1 v2 : val, pair_content γ (v1, v2) >>>
writeY (p, v)%V
<<< snapshot_content γ v, RET v >>>;
write_spec N γ (v: val) p :
is_snapshot N γ p -
<<< w : val, snapshot_content γ w >>>
write p v
@ ∖↑N
<<< pair_content γ (v1, v), RET #() >>>;
readPair_spec N γ p :
is_pair N γ p -
<<< v1 v2 : val, pair_content γ (v1, v2) >>>
readPair p
<<< snapshot_content γ v, RET #() >>>;
read_with_spec N γ p (l : loc) :
is_snapshot N γ p -
<<< v w : val, snapshot_content γ v l w >>>
read_with p #l
@ ∖↑N
<<< pair_content γ (v1, v2), RET (v1, v2) >>>;
<<< snapshot_content γ v l w, RET (v, w) >>>;
}.
Arguments atomic_snapshot _ {_}.
Existing Instances
is_snapshot_persistent snapshot_content_timeless
name_countable name_eqdec.