Commit 36f0e548 authored by Ralf Jung's avatar Ralf Jung
Browse files

Merge branch 'master' into 'master'

Master

See merge request !13
parents 73e3afad 14821493
Pipeline #15272 passed with stage
in 6 minutes and 25 seconds
......@@ -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
......
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.
From iris.program_logic Require Export weakestpre hoare.
From iris.heap_lang Require Export lang proofmode notation.
From iris.algebra Require Import excl.
From iris_examples.concurrent_stacks Require Import spec.
From iris_examples.concurrent_stacks Require Import specs.
Set Default Proof Using "Type".
(** Stack 3: No helping, view-shift 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").
(** Stack 3: No helping, CAP spec. *)
Definition mk_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 stack_works.
Context `{!heapG Σ}.
Context `{!heapG Σ} (N : namespace).
Implicit Types l : loc.
Fixpoint is_stack xs v : iProp Σ :=
Local Notation "l ↦{-} v" := ( q, l {q} v)%I
(at level 20, format "l ↦{-} v") : bi_scope.
Lemma partial_mapsto_duplicable l v :
l {-} v - l {-} v l {-} v.
Proof.
iIntros "H"; iDestruct "H" as (?) "[Hl Hl']"; iSplitL "Hl"; eauto.
Qed.
Lemma partial_mapsto_agree l v1 v2 :
l {-} v1 - l {-} v2 - v1 = v2.
Proof.
iIntros "H1 H2".
iDestruct "H1" as (?) "H1".
iDestruct "H2" as (?) "H2".
iApply (mapsto_agree with "H1 H2").
Qed.
Fixpoint is_list xs v : iProp Σ :=
(match xs with
| [] => v = NONEV
| x :: xs => q (l : loc) (t : val), v = SOMEV #l l {q} (x, t) is_stack xs t
| x :: xs => l (t : val), v = SOMEV #l%V l {-} (x, t)%V is_list xs t
end)%I.
Definition stack_inv P v :=
( l v' xs, v = #l l v' is_stack xs v' P xs)%I.
Lemma is_stack_disj xs v :
is_stack xs v - is_stack xs v (v = NONEV q (l : loc) (h t : val), v = SOMEV #l l {q} (h, t)).
Lemma is_list_disj xs v :
is_list xs v - is_list xs v (v = NONEV l (h t : val), v = SOMEV #l l {-} (h, t)%V).
Proof.
iIntros "Hstack".
destruct xs.
- iSplit; try iLeft; auto.
- simpl. iDestruct "Hstack" as (q l t) "[-> [[Hl Hl'] Hstack]]".
iSplitR "Hl"; eauto 10 with iFrame.
destruct xs; auto.
iIntros "H"; iDestruct "H" as (l t) "(-> & Hl & Hstack)".
iDestruct (partial_mapsto_duplicable with "Hl") as "[Hl1 Hl2]".
iSplitR "Hl2"; first by (iExists _, _; iFrame). iRight; auto.
Qed.
Lemma is_stack_unboxed xs v :
is_stack xs v - val_is_unboxed v.
Lemma is_list_unboxed xs v :
is_list xs v - val_is_unboxed v is_list xs v.
Proof.
iIntros "Hstack". iDestruct (is_stack_disj with "Hstack") as "[_ [->|Hdisj]]".
- done.
- iDestruct "Hdisj" as (???? ->) "_". done.
iIntros "Hlist"; iDestruct (is_list_disj with "Hlist") as "[$ Heq]".
iDestruct "Heq" as "[-> | H]"; first done; by iDestruct "H" as (? ? ?) "[-> ?]".
Qed.
Lemma is_stack_uniq : xs ys v,
is_stack xs v is_stack ys v - xs = ys.
Lemma is_list_empty xs :
is_list xs (InjLV #()) - xs = [].
Proof.
induction xs, ys; iIntros (v') "[Hstack1 Hstack2]"; auto.
- iDestruct "Hstack1" as "%".
iDestruct "Hstack2" as (???) "[% _]".
subst.
discriminate.
- iDestruct "Hstack2" as "%".
iDestruct "Hstack1" as (???) "[% _]".
subst.
discriminate.
- simpl. iDestruct "Hstack1" as (q1 l1 t) "[% [Hl1 Hstack1]]".
iDestruct "Hstack2" as (q2 l2 t') "[% [Hl2 Hstack2]]".
subst; injection H0; intros; subst; clear H0.
iDestruct (mapsto_agree with "Hl1 Hl2") as %[= -> ->].
iDestruct (IHxs with "[Hstack1 Hstack2]") as "%". by iFrame.
subst; auto.
destruct xs; iIntros "Hstack"; auto.
iDestruct "Hstack" as (? ?) "(% & H)"; discriminate.
Qed.
Lemma is_stack_empty : xs,
is_stack xs NONEV - xs = [].
Lemma is_list_cons xs l h t :
l {-} (h, t)%V -
is_list xs (InjRV #l) -
ys, xs = h :: ys.
Proof.
iIntros (xs) "Hstack".
destruct xs; auto.
iDestruct "Hstack" as (?? t) "[% rest]".
discriminate.
destruct xs; first by iIntros "? %".
iIntros "Hl Hstack"; iDestruct "Hstack" as (l' t') "(% & Hl' & Hrest)"; simplify_eq.
iDestruct (partial_mapsto_agree with "Hl Hl'") as "%"; simplify_eq; iExists _; auto.
Qed.
Lemma is_stack_cons : xs l,
is_stack xs (SOMEV #l) -
is_stack xs (SOMEV #l) q h t ys, xs = h :: ys l {q} (h, t).
Definition stack_inv P l :=
( v xs, l v is_list xs v P xs)%I.
Definition is_stack_pred P v :=
( l, v = #l inv N (stack_inv P l))%I.
Theorem mk_stack_spec P :
{{{ P [] }}} mk_stack #() {{{ v, RET v; is_stack_pred P v }}}.
Proof.
iIntros ([|x xs] l) "Hstack".
- iDestruct "Hstack" as "%"; discriminate.
- simpl. iDestruct "Hstack" as (q l' t') "[% [[Hl Hl'] Hstack]]".
injection H; intros; subst; clear H.
iSplitR "Hl'"; eauto 10 with iFrame.
iIntros (Φ) "HP HΦ".
rewrite -wp_fupd.
wp_lam. wp_alloc l as "Hl".
iMod (inv_alloc N _ (stack_inv P l) with "[Hl HP]") as "#Hinv".
{ by iNext; iExists _, []; iFrame. }
iModIntro; iApply "HΦ"; iExists _; auto.
Qed.
(* Whole-stack invariant (P). However:
- The resources for the successful and failing pop must be disjoint.
Instead, there should be a normal conjunction between them.
Open question: How does this relate to a logically atomic spec? *)
Theorem stack_works ι P Q Q' Q'' (Φ : val iProp Σ) :
( (f f : val),
((( v vs, P (v :: vs) ={∖↑ι}= Q v P vs) (* pop *)
(P [] ={∖↑ι}= Q' P []) -
WP f #() {{ v, ( (v' : val), v SOMEV v' Q v') (v NONEV Q')}}))
- ( (v : val), (* push *)
(( vs, P vs ={∖↑ι}= P (v :: vs) Q'') -
WP f v {{ v, Q'' }}))
- Φ (f, f)%V)%I