Commit de0c6689 authored by Hai Dang's avatar Hai Dang

Merge branch 'master' into hai/auth_frac

parents b8172744 3e8fcd4c
*.v gitlab-language=coq
......@@ -30,7 +30,6 @@ build-coq.8.8.2:
<<: *template
variables:
OPAM_PINS: "coq version 8.8.2"
TIMING_PROJECT: "iris-examples"
TIMING_CONF: "coq-8.8.2"
tags:
- fp-timing
......
......@@ -8,7 +8,7 @@ all: Makefile.coq
clean: Makefile.coq
+@make -f Makefile.coq clean
find theories $$(test -d tests && echo tests) \( -name "*.d" -o -name "*.vo" -o -name "*.aux" -o -name "*.cache" -o -name "*.glob" -o -name "*.vio" \) -print -delete
find theories tests \( -name "*.d" -o -name "*.vo" -o -name "*.aux" -o -name "*.cache" -o -name "*.glob" -o -name "*.vio" \) -print -delete || true
rm -f Makefile.coq
.PHONY: clean
......
......@@ -23,11 +23,11 @@ theories/spanning_tree/mon.v
theories/spanning_tree/spanning.v
theories/spanning_tree/proof.v
theories/concurrent_stacks/specs.v
theories/concurrent_stacks/concurrent_stack1.v
#theories/concurrent_stacks/concurrent_stack2.v
theories/concurrent_stacks/concurrent_stack2.v
theories/concurrent_stacks/concurrent_stack3.v
#theories/concurrent_stacks/concurrent_stack4.v
theories/concurrent_stacks/spec.v
theories/concurrent_stacks/concurrent_stack4.v
theories/logrel/prelude/base.v
theories/logrel/stlc/lang.v
......@@ -87,6 +87,7 @@ theories/hocap/concurrent_runners.v
theories/hocap/parfib.v
theories/logatom/treiber.v
theories/logatom/treiber2.v
theories/logatom/elimination_stack/hocap_spec.v
theories/logatom/elimination_stack/stack.v
theories/logatom/elimination_stack/spec.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-01-27.0.9896799d") | (= "dev") }
"coq-iris" { (= "dev.2019-04-17.0.60d28bbb") | (= "dev") }
"coq-autosubst" { = "dev.coq86" }
]
......@@ -41,8 +41,8 @@ Section client.
Proof.
iIntros ""; rewrite /client. wp_alloc y as "Hy". wp_let.
wp_apply (newbarrier_spec N (y_inv 1 y) with "[//]").
iIntros (l) "[Hr Hs]". wp_let.
iApply (wp_par (λ _, True%I) (λ _, True%I) with "[Hy Hs] [Hr]"); last auto.
iIntros (l) "[Hr Hs]".
wp_apply (wp_par (λ _, True%I) (λ _, True%I) with "[Hy Hs] [Hr]"); last auto.
- (* The original thread, the sender. *)
wp_store. iApply (signal_spec with "[-]"); last by iNext; auto.
iSplitR "Hy"; first by eauto.
......@@ -51,7 +51,7 @@ Section client.
iDestruct (recv_weaken with "[] Hr") as "Hr".
{ iIntros "Hy". by iApply (y_inv_split with "Hy"). }
iMod (recv_split with "Hr") as "[H1 H2]"; first done.
iApply (wp_par (λ _, True%I) (λ _, True%I) with "[H1] [H2]"); last auto.
wp_apply (wp_par (λ _, True%I) (λ _, True%I) with "[H1] [H2]"); last auto.
+ by iApply worker_safe.
+ by iApply worker_safe.
Qed.
......
......@@ -122,7 +122,7 @@ Proof.
as ([p I]) "(% & [Hl Hr] & Hclose)"; eauto.
destruct p; [|done]. wp_store.
iSpecialize ("HΦ" with "[#]") => //. iFrame "HΦ".
iMod ("Hclose" $! (State High I) ( : set token) with "[-]"); last done.
iMod ("Hclose" $! (State High I) ( : propset token) with "[-]"); last done.
iSplit; [iPureIntro; by eauto using signal_step|].
rewrite /barrier_inv /ress /=. iNext. iFrame "Hl".
iDestruct "Hr" as (Ψ) "[Hr Hsp]"; iExists Ψ; iFrame "Hsp".
......@@ -165,8 +165,8 @@ Proof.
iIntros (?). iDestruct 1 as (γ P Q i) "(#Hsts & Hγ & #HQ & HQR)".
iMod (sts_openS (barrier_inv l P) _ _ γ with "[Hγ]")
as ([p I]) "(% & [Hl Hr] & Hclose)"; eauto.
iMod (saved_prop_alloc_strong I) as (i1) "[% #Hi1]".
iMod (saved_prop_alloc_strong (I {[i1]}))
iMod (saved_prop_alloc_cofinite I) as (i1) "[% #Hi1]".
iMod (saved_prop_alloc_cofinite (I {[i1]}))
as (i2) "[Hi2' #Hi2]"; iDestruct "Hi2'" as %Hi2.
rewrite ->not_elem_of_union, elem_of_singleton in Hi2; destruct Hi2.
iMod ("Hclose" $! (State p ({[i1; i2]} I {[i]}))
......
......@@ -19,7 +19,7 @@ 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) : set token :=
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 !_ /.
......@@ -27,10 +27,10 @@ Global Arguments tok !_ /.
Canonical Structure sts := sts.Sts prim_step tok.
(* The set of states containing some particular i *)
Definition i_states (i : gname) : set state := {[ s | i state_I s ]}.
Definition i_states (i : gname) : propset state := {[ s | i state_I s ]}.
(* The set of low states *)
Definition low_states : set state := {[ s | state_phase s = Low ]}.
Definition low_states : propset state := {[ s | state_phase s = Low ]}.
Lemma i_states_closed i : sts.closed (i_states i) {[ Change i ]}.
Proof.
......@@ -77,7 +77,7 @@ Proof.
- 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 => : set token | High => {[Send]} end False)
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.
......
From iris.base_logic Require Import base_logic.
From iris.proofmode Require Import tactics.
From iris.base_logic.lib Require Import invariants.
From iris.program_logic Require Export weakestpre hoare.
From iris.heap_lang Require Export lang.
From iris.algebra Require Import agree list.
From iris.heap_lang Require Import assert proofmode notation.
From iris_examples.concurrent_stacks Require Import spec.
From iris.program_logic Require Export weakestpre.
From iris.heap_lang Require Import notation proofmode.
From iris_examples.concurrent_stacks Require Import specs.
Set Default Proof Using "Type".
(** Stack 1: No helping, bag spec. *)
Definition mk_stack : val :=
λ: "_",
let: "r" := ref NONEV in
(rec: "pop" "n" :=
match: !"r" with
NONE => NONE
| SOME "hd" =>
if: CAS "r" (SOME "hd") (Snd !"hd")
then SOME (Fst !"hd")
else "pop" "n"
end,
rec: "push" "n" :=
let: "r'" := !"r" in
let: "r''" := SOME (Alloc ("n", "r'")) in
if: CAS "r" "r'" "r''"
then #()
else "push" "n").
Definition new_stack : val := λ: "_", ref NONEV.
Definition push : val :=
rec: "push" "s" "v" :=
let: "tail" := ! "s" in
let: "new" := SOME (ref ("v", "tail")) in
if: CAS "s" "tail" "new" then #() else "push" "s" "v".
Definition pop : val :=
rec: "pop" "s" :=
match: !"s" with
NONE => NONEV
| SOME "l" =>
let: "pair" := !"l" in
if: CAS "s" (SOME "l") (Snd "pair")
then SOME (Fst "pair")
else "pop" "s"
end.
Section stacks.
Context `{!heapG Σ}.
Context `{!heapG Σ} (N : namespace).
Implicit Types l : loc.
Definition oloc_to_val (h : option loc) : val :=
match h with
| None => NONEV
| Some l => SOMEV #l
end.
Local Instance oloc_to_val_inj : Inj (=) (=) oloc_to_val.
Proof. rewrite /Inj /oloc_to_val=>??. repeat case_match; congruence. Qed.
Local Notation "l ↦{-} v" := ( q, l {q} v)%I
(at level 20, format "l ↦{-} v") : bi_scope.
Definition is_stack_pre (P : val iProp Σ) (F : option loc -c> iProp Σ) :
option loc -c> iProp Σ := λ v,
(match v with
| None => True
| Some l => q h t, l {q} (h, oloc_to_val t) P h F t
end)%I.
Lemma partial_mapsto_duplicable l v :
l {-} v - l {-} v l {-} v.
Proof.
iIntros "H"; iDestruct "H" as (?) "[Hl Hl']"; iSplitL "Hl"; eauto.
Qed.
Local Instance is_stack_contr (P : val iProp Σ): Contractive (is_stack_pre P).
Definition is_list_pre (P : val iProp Σ) (F : val -c> iProp Σ) :
val -c> iProp Σ := λ v,
(v NONEV (l : loc) (h t : val), v SOMEV #l l {-} (h, t)%V P h F t)%I.
Local Instance is_list_contr (P : val iProp Σ) : Contractive (is_list_pre P).
Proof.
rewrite /is_stack_pre => n f f' Hf v.
rewrite /is_list_pre => n f f' Hf v.
repeat (f_contractive || f_equiv).
apply Hf.
Qed.
Definition is_stack_def (P : val -> iProp Σ) := fixpoint (is_stack_pre P).
Definition is_stack_aux P : seal (@is_stack_def P). by eexists. Qed.
Definition is_stack P := unseal (is_stack_aux P).
Definition is_stack_eq P : @is_stack P = @is_stack_def P := seal_eq (is_stack_aux P).
Definition stack_inv P l :=
( ol, l oloc_to_val ol is_stack P ol)%I.
Definition is_list_def (P : val -> iProp Σ) := fixpoint (is_list_pre P).
Definition is_list_aux P : seal (@is_list_def P). by eexists. Qed.
Definition is_list P := unseal (is_list_aux P).
Definition is_list_eq P : @is_list P = @is_list_def P := seal_eq (is_list_aux P).
Lemma is_list_unfold (P : val iProp Σ) v :
is_list P v is_list_pre P (is_list P) v.
Proof.
rewrite is_list_eq. apply (fixpoint_unfold (is_list_pre P)).
Qed.
Lemma is_stack_unfold (P : val iProp Σ) v :
is_stack P v is_stack_pre P (is_stack P) v.
(* TODO: shouldn't have to explicitly return is_list *)
Lemma is_list_unboxed (P : val iProp Σ) v :
is_list P v - val_is_unboxed v is_list P v.
Proof.
rewrite is_stack_eq. apply (fixpoint_unfold (is_stack_pre P)).
iIntros "Hstack"; iSplit; last done;
iDestruct (is_list_unfold with "Hstack") as "[->|Hstack]";
last iDestruct "Hstack" as (l h t) "(-> & _)"; done.
Qed.
Lemma is_stack_copy (P : val iProp Σ) ol :
is_stack P ol - is_stack P ol
(match ol with None => True | Some l => q h t, l {q} (h, oloc_to_val t) end).
Lemma is_list_disj (P : val iProp Σ) v :
is_list P v - is_list P v (v NONEV (l : loc) h t, v SOMEV #l%V l {-} (h, t)%V).
Proof.
iIntros "Hstack".
iDestruct (is_stack_unfold with "Hstack") as "Hstack". destruct ol; last first.
- iSplitL; try iApply is_stack_unfold; auto.
- iDestruct "Hstack" as (q h t) "[[Hl1 Hl2] [HP Hrest]]".
iSplitR "Hl2"; try iApply is_stack_unfold; simpl; eauto 10 with iFrame.
iDestruct (is_list_unfold with "Hstack") as "[%|Hstack]"; simplify_eq.
- rewrite is_list_unfold; iSplitR; [iLeft|]; eauto.
- iDestruct "Hstack" as (l h t) "(% & Hl & Hlist)".
iDestruct (partial_mapsto_duplicable with "Hl") as "[Hl1 Hl2]"; simplify_eq.
rewrite (is_list_unfold _ (InjRV _)); iSplitR "Hl2"; iRight; iExists _, _, _; by iFrame.
Qed.
(* Per-element invariant (i.e., bag spec). *)
Theorem stack_works P Φ :
( (f f : val),
( WP f #() {{ v, ( v', v SOMEV v' P v') v NONEV }})
- ( (v : val), (P v - WP f v {{ v, True }}))
- Φ (f, f)%V)%I
- WP mk_stack #() {{ Φ }}.
Definition stack_inv P v :=
( l v', v = #l l v' is_list P v')%I.
Definition is_stack (P : val iProp Σ) v :=
inv N (stack_inv P v).
Theorem new_stack_spec P :
{{{ True }}} new_stack #() {{{ s, RET s; is_stack P s }}}.
Proof.
iIntros "HΦ".
iIntros (ϕ) "_ Hpost".
iApply wp_fupd.
wp_lam.
wp_alloc l as "Hl".
pose proof (nroot .@ "N") as N.
rewrite -wp_fupd.
iMod (inv_alloc N _ (stack_inv P l) with "[Hl]") as "#Hisstack".
{ iExists None; iFrame; auto.
iApply is_stack_unfold. auto. }
wp_pures.
wp_alloc as "Hl".
iMod (inv_alloc N (stack_inv P #) with "[Hl]") as "Hinv".
{ iNext; iExists , NONEV; iFrame;
by iSplit; last (iApply is_list_unfold; iLeft). }
by iApply "Hpost".
Qed.
Theorem push_spec P s v :
{{{ is_stack P s P v }}} push s v {{{ RET #(); True }}}.
Proof.
iIntros (Φ) "[#Hstack HP] HΦ".
iLöb as "IH".
wp_lam. wp_let. wp_bind (Load _).
iInv N as ( v') "(>% & Hl & Hlist)" "Hclose"; subst.
wp_load.
iMod ("Hclose" with "[Hl Hlist]") as "_".
{ iNext; iExists _, _; by iFrame. }
iModIntro. wp_let. wp_alloc ' as "Hl'". wp_pures. wp_bind (CAS _ _ _).
iInv N as ('' v'') "(>% & >Hl & Hlist)" "Hclose"; simplify_eq.
destruct (decide (v' = v'')) as [ -> |].
- iDestruct (is_list_unboxed with "Hlist") as "[>% Hlist]".
wp_cas_suc.
iMod ("Hclose" with "[HP Hl Hl' Hlist]") as "_".
{ iNext; iExists _, (InjRV #'); iFrame; iSplit; first done;
rewrite (is_list_unfold _ (InjRV _)). iRight; iExists _, _, _; iFrame; eauto. }
iModIntro.
wp_if.
by iApply "HΦ".
- iDestruct (is_list_unboxed with "Hlist") as "[>% Hlist]".
wp_cas_fail.
iMod ("Hclose" with "[Hl Hlist]") as "_".
{ iNext; iExists _, _; by iFrame. }
iModIntro.
wp_if.
iApply ("IH" with "HP HΦ").
Qed.
Theorem pop_spec P s :
{{{ is_stack P s }}} pop s {{{ ov, RET ov; ov = NONEV v, ov = SOMEV v P v }}}.
Proof.
iIntros (Φ) "#Hstack HΦ".
iLöb as "IH".
wp_lam. wp_bind (Load _).
iInv N as ( v') "(>% & Hl & Hlist)" "Hclose"; subst.
wp_load.
iDestruct (is_list_disj with "Hlist") as "[Hlist Hdisj]".
iMod ("Hclose" with "[Hl Hlist]") as "_".
{ iNext; iExists _, _; by iFrame. }
iModIntro.
iApply "HΦ".
- iIntros "!#".
iLöb as "IH".
wp_rec.
wp_bind (! #l)%E.
iInv N as "Hstack" "Hclose".
iDestruct "Hstack" as (v') "[Hl' Hstack]".
iDestruct "Hdisj" as "[-> | Heq]".
- wp_match.
iApply "HΦ"; by iLeft.
- iDestruct "Heq" as (l h t) "[-> Hl]".
wp_match. wp_bind (Load _).
iInv N as (' v') "(>% & Hl' & Hlist)" "Hclose". simplify_eq.
iDestruct "Hl" as (q) "Hl".
wp_load.
destruct v' as [l'|]; simpl; last first.
+ iMod ("Hclose" with "[Hl' Hstack]") as "_".
{ rewrite /stack_inv. eauto with iFrame. }
iModIntro. wp_match. wp_pures. by iRight.
+ iDestruct (is_stack_copy with "Hstack") as "[Hstack Hmy]".
iDestruct "Hmy" as (q h t) "Hl".
iMod ("Hclose" with "[Hl' Hstack]") as "_".
{ rewrite /stack_inv. eauto with iFrame. }
iModIntro. wp_match.
wp_load. wp_pures.
wp_bind (CAS _ _ _).
iInv N as "Hstack" "Hclose".
iDestruct "Hstack" as (v'') "[Hl'' Hstack]".
destruct (decide (oloc_to_val v'' = oloc_to_val (Some l'))) as [->%oloc_to_val_inj|Hne].
* simpl. wp_cas_suc.
iDestruct (is_stack_unfold with "Hstack") as "Hstack".
iDestruct "Hstack" as (q' h' t') "[Hl' [HP Hstack]]".
iDestruct (mapsto_agree with "Hl Hl'") as %[= <- <-%oloc_to_val_inj].
iMod ("Hclose" with "[Hl'' Hstack]").
{ iExists _. auto with iFrame. }
iModIntro.
wp_if.
wp_load.
wp_pures.
eauto.
* simpl in Hne. wp_cas_fail.
iMod ("Hclose" with "[Hl'' Hstack]").
{ iExists v''; iFrame; auto. }
iModIntro.
wp_if.
iApply "IH".
- iIntros (v) "!# HP".
iLöb as "IH".
wp_rec.
wp_bind (! _)%E.
iInv N as "Hstack" "Hclose".
iDestruct "Hstack" as (v') "[Hl' Hstack]".
wp_load.
iMod ("Hclose" with "[Hl' Hstack]").
{ iExists v'. iFrame. }
iMod ("Hclose" with "[Hl' Hlist]") as "_".
{ iNext; iExists _, _; by iFrame. }
iModIntro.
wp_let.
wp_alloc r'' as "Hr''".
wp_pures. wp_bind (CAS _ _ _).
iInv N as "Hstack" "Hclose".
iDestruct "Hstack" as (v'') "[Hl'' Hstack]".
wp_cas as ->%oloc_to_val_inj|_.
+ destruct v'; by right.
+ iMod ("Hclose" with "[Hl'' Hr'' HP Hstack]").
iExists (Some r'').
iFrame; auto.
iNext.
iApply is_stack_unfold.
simpl.
iExists _, _, v'. iFrame.
iInv N as ('' v'') "(>% & Hl' & Hlist)" "Hclose". simplify_eq.
destruct (decide (v'' = InjRV #l)) as [-> |].
* rewrite is_list_unfold.
iDestruct "Hlist" as "[>% | H]"; first done.
iDestruct "H" as (''' h' t') "(>% & Hl'' & HP & Hlist)"; simplify_eq.
iDestruct "Hl''" as (q') "Hl''".
wp_cas_suc.
iDestruct (mapsto_agree with "Hl'' Hl") as "%"; simplify_eq.
iMod ("Hclose" with "[Hl' Hlist]") as "_".
{ iNext; iExists '', _; by iFrame. }
iModIntro.
wp_if.
done.
+ iMod ("Hclose" with "[Hl'' Hstack]").
iExists v''; iFrame; auto.
wp_pures.
iApply ("HΦ" with "[HP]"); iRight; iExists h; by iFrame.
* wp_cas_fail.
iMod ("Hclose" with "[Hl' Hlist]") as "_".
{ iNext; iExists '', _; by iFrame. }
iModIntro.
wp_if.
iApply "IH".
done.
iApply ("IH" with "HΦ").
Qed.
End stacks.
Program Definition is_concurrent_bag `{!heapG Σ} : concurrent_bag Σ :=
{| spec.mk_bag := mk_stack |}.
Next Obligation.
iIntros (??? P Φ) "_ HΦ". iApply stack_works.
iNext. iIntros (f f) "Hpop Hpush". iApply "HΦ". iFrame.
Qed.
Program Definition spec {Σ} N `{heapG Σ} : concurrent_bag Σ :=
{| is_bag := is_stack N; new_bag := new_stack; bag_push := push; bag_pop := pop |} .
Solve Obligations of spec with eauto using pop_spec, push_spec, new_stack_spec.
(** THIS FILE CURRENTLY DOES NOT COMPILE because it has not been ported to the
stricter CAS requirements yet. *)
From iris.program_logic Require Export weakestpre hoare.
From iris.heap_lang Require Export lang proofmode notation.
From iris.heap_lang Require Import notation proofmode.
From iris.algebra Require Import excl.
From iris_examples.concurrent_stacks Require Import spec.
From iris.base_logic.lib Require Import invariants.
From iris.program_logic Require Export weakestpre.
From iris_examples.concurrent_stacks Require Import specs.
Set Default Proof Using "Type".
(** Stack 2: With helping, bag spec. *)
(** Stack 2: Helping, bag spec. *)
Definition mk_offer : val :=
λ: "v", ("v", ref #0).
......@@ -17,49 +14,49 @@ Definition revoke_offer : val :=
Definition take_offer : val :=
λ: "v", if: CAS (Snd "v") #0 #1 then SOME (Fst "v") else NONE.
Definition mailbox : val :=
λ: "_",
let: "r" := ref NONEV in
(rec: "put" "v" :=
let: "off" := mk_offer "v" in
"r" <- SOME "off";;
revoke_offer "off",
rec: "get" "n" :=
let: "offopt" := !"r" in
match: "offopt" with
NONE => NONE
| SOME "x" => take_offer "x"
end
).
Definition mk_stack : val :=
λ: "_",
let: "mailbox" := mailbox #() in
let: "put" := Fst "mailbox" in
let: "get" := Snd "mailbox" in
let: "r" := ref NONEV in
(rec: "pop" "n" :=
match: "get" #() with
NONE =>
(match: !"r" with
NONE => NONE
| SOME "hd" =>
if: CAS "r" (SOME "hd") (Snd "hd")
then SOME (Fst "hd")
else "pop" "n"
end)
| SOME "x" => SOME "x"
end,
rec: "push" "n" :=
match: "put" "n" with
NONE => #()
| SOME "n" =>
let: "r'" := !"r" in
let: "r''" := SOME ("n", "r'") in
if: CAS "r" "r'" "r''"
then #()
else "push" "n"
end).
Definition mk_mailbox : val := λ: "_", ref NONEV.
Definition put : val :=
λ: "r" "v",
let: "off" := mk_offer "v" in
"r" <- SOME "off";;
revoke_offer "off".
Definition get : val :=
λ: "r",
let: "offopt" := !"r" in
match: "offopt" with
NONE => NONE
| SOME "x" => take_offer "x"
end.
Definition new_stack : val := λ: "_", (mk_mailbox #(), ref NONEV).
Definition push : val :=
rec: "push" "p" "v" :=
let: "mailbox" := Fst "p" in
let: "s" := Snd "p" in
match: put "mailbox" "v" with
NONE => #()
| SOME "v'" =>
let: "tail" := ! "s" in
let: "new" := SOME (ref ("v'", "tail")) in
if: CAS "s" "tail" "new" then #() else "push" "p" "v'"
end.
Definition pop : val :=
rec: "pop" "p" :=