Commit 74960dec authored by Ralf Jung's avatar Ralf Jung

move other exampkes back here

parent b5d6b7bb
......@@ -95,3 +95,5 @@ heap_lang/lib/barrier/proof.v
heap_lang/lib/barrier/client.v
tests/heap_lang.v
tests/program_logic.v
tests/one_shot.v
tests/joining_existentials.v
From iris.program_logic Require Import saved_one_shot hoare tactics.
From iris.heap_lang.lib.barrier Require Import proof specification.
From iris.heap_lang Require Import notation par.
Import uPred.
Definition client eM eW1 eW2 : expr [] :=
(let: "b" := newbarrier #() in (eM ;; ^signal '"b") ||
((^wait '"b" ;; eW1) || (^wait '"b" ;; eW2))).
Section proof.
Context (G : cFunctor).
Context {Σ : gFunctors} `{!heapG Σ, !barrierG Σ, !spawnG Σ, !oneShotG heap_lang Σ G}.
Context (heapN N : namespace).
Local Notation iProp := (iPropG heap_lang Σ).
Local Notation X := (G iProp).
Definition barrier_res γ (P : X iProp) : iProp :=
( x:X, one_shot_own γ x P x)%I.
Lemma worker_spec e γ l (P Q : X iProp) (R : iProp) :
R ( x, {{ P x }} e {{ λ _, Q x }})
R (recv heapN N l (barrier_res γ P))
R WP wait (%l) ;; e {{ λ _, barrier_res γ Q }}.
Proof.
intros He HΦ. rewrite -[R](idemp ()%I) {1}He HΦ always_and_sep_l {He HΦ}.
ewp (eapply wait_spec). ecancel [recv _ _ l _]. apply wand_intro_r. wp_seq.
rewrite /barrier_res sep_exist_l. apply exist_elim=>x.
rewrite (forall_elim x) /ht always_elim impl_wand !assoc.
to_front [P x; _ - _]%I. rewrite wand_elim_r !wp_frame_r.
apply wp_mono=>v. by rewrite -(exist_intro x) comm.
Qed.
Context (P' : iProp) (P P1 P2 Q Q1 Q2 : X -n> iProp).
Context {P_split : x:X, P x (P1 x P2 x)}.
Context {Q_join : x:X, (Q1 x Q2 x) Q x}.
Lemma P_res_split γ :
barrier_res γ P (barrier_res γ P1 barrier_res γ P2).
Proof.
rewrite /barrier_res. apply exist_elim=>x. do 2 rewrite -(exist_intro x).
rewrite P_split {1}[one_shot_own _ _]always_sep_dup.
solve_sep_entails.
Qed.
Lemma Q_res_join γ :
(barrier_res γ Q1 barrier_res γ Q2) barrier_res γ Q.
Proof.
rewrite /barrier_res sep_exist_r. apply exist_elim=>x1.
rewrite sep_exist_l. apply exist_elim=>x2.
rewrite [one_shot_own γ x1]always_sep_dup.
to_front [one_shot_own γ x1; one_shot_own γ x2]. rewrite one_shot_agree.
strip_later. rewrite -(exist_intro x1) -Q_join.
ecancel [one_shot_own γ _; Q1 _].
eapply (eq_rewrite x2 x1 (λ x, Q2 x)); last by eauto with I.
{ (* FIXME typeclass search should find this. *)
apply cofe_mor_ne. }
rewrite eq_sym. eauto with I.
Qed.
Lemma client_spec (eM eW1 eW2 : expr []) (eM' eW1' eW2' : expr ("b" :b: [])) (R : iProp) :
heapN N eM' = wexpr' eM eW1' = wexpr' eW1 eW2' = wexpr' eW2
R ({{ P' }} eM {{ λ _, x, P x }})
R ( x, {{ P1 x }} eW1 {{ λ _, Q1 x }})
R ( x, {{ P2 x }} eW2 {{ λ _, Q2 x }})
R heap_ctx heapN
R P'
R WP client eM' eW1' eW2' {{ λ _, γ, barrier_res γ Q }}.
Proof.
intros HN -> -> -> HeM HeW1 HeW2 Hheap HP'.
rewrite -4!{1}[R](idemp ()%I) {1}HeM {1}HeW1 {1}HeW2 {1}Hheap {1}HP' !always_and_sep_l {Hheap} /client.
to_front []. rewrite one_shot_alloc !pvs_frame_r !sep_exist_r.
apply wp_strip_pvs, exist_elim=>γ. rewrite {1}[heap_ctx _]always_sep_dup.
(ewp (eapply (newbarrier_spec heapN N (barrier_res γ P)))); last done.
cancel [heap_ctx heapN]. apply forall_intro=>l. apply wand_intro_r.
set (workers_post (v : val) := (barrier_res γ Q1 barrier_res γ Q2)%I).
wp_let. (ewp (eapply wp_par with (Ψ1 := λ _, True%I) (Ψ2 := workers_post))); last first.
{ done. } (* FIXME why does this simple goal even appear? *)
rewrite {1}[heap_ctx _]always_sep_dup. cancel [heap_ctx heapN].
sep_split left: [one_shot_pending γ; send _ _ _ _ ; P'; {{ _ }} eM {{ _ }}]%I.
{ (* Main thread. *)
wp_focus eM. rewrite /ht always_elim impl_wand wand_elim_r !wp_frame_l.
apply wp_mono=>v. wp_seq. rewrite !sep_exist_l. apply exist_elim=>x.
rewrite (one_shot_init _ γ x) !pvs_frame_r. apply wp_strip_pvs.
ewp (eapply signal_spec). ecancel [send _ _ _ _].
by rewrite /barrier_res -(exist_intro x). }
sep_split right: [].
- (* Worker threads. *)
rewrite recv_mono; last exact: P_res_split. rewrite (recv_split _ _ ) //.
rewrite ?pvs_frame_r !pvs_frame_l. apply wp_strip_pvs.
(ewp (eapply wp_par with (Ψ1 := λ _, barrier_res γ Q1) (Ψ2 := λ _, barrier_res γ Q2))); last first.
{ done. } ecancel [heap_ctx _].
sep_split left: [recv _ _ _ (barrier_res γ P1); _, {{ _ }} eW1 {{ _ }}]%I.
{ eapply worker_spec; eauto with I. }
sep_split left: [recv _ _ _ (barrier_res γ P2); _, {{ _ }} eW2 {{ _ }}]%I.
{ eapply worker_spec; eauto with I. }
rewrite /workers_post. do 2 apply forall_intro=>_.
(* FIXME: this should work: rewrite -later_intro. *)
apply wand_intro_r. rewrite -later_intro. solve_sep_entails.
- (* Merging. *)
rewrite /workers_post. do 2 apply forall_intro=>_. apply wand_intro_r.
rewrite !left_id Q_res_join. strip_later. by rewrite -(exist_intro γ).
Qed.
End proof.
From iris.algebra Require Import one_shot dec_agree.
From iris.program_logic Require Import hoare.
From iris.heap_lang Require Import heap assert wp_tactics notation.
Import uPred.
Definition one_shot_example : val := λ: <>,
let: "x" := ref (InjL #0) in (
(* tryset *) (λ: "n",
CAS '"x" (InjL #0) (InjR '"n")),
(* check *) (λ: <>,
let: "y" := !'"x" in λ: <>,
match: '"y" with
InjL <> => #()
| InjR "n" =>
match: !'"x" with
InjL <> => Assert #false
| InjR "m" => Assert ('"n" = '"m")
end
end)).
Class one_shotG Σ :=
OneShotG { one_shot_inG :> inG heap_lang Σ (one_shotR (dec_agreeR Z)) }.
Definition one_shotGF : gFunctorList :=
[GFunctor (constRF (one_shotR (dec_agreeR Z)))].
Instance inGF_one_shotG Σ : inGFs heap_lang Σ one_shotGF one_shotG Σ.
Proof. intros [? _]; split; apply: inGF_inG. Qed.
Section proof.
Context {Σ : gFunctors} `{!heapG Σ, !one_shotG Σ}.
Context (heapN N : namespace) (HN : heapN N).
Local Notation iProp := (iPropG heap_lang Σ).
Definition one_shot_inv (γ : gname) (l : loc) : iProp :=
(l InjLV #0 own γ OneShotPending
n : Z, l InjRV #n own γ (Shot (DecAgree n)))%I.
Lemma wp_one_shot (Φ : val iProp) :
(heap_ctx heapN f1 f2 : val,
( n : Z, WP f1 #n {{ λ w, w = #true w = #false }})
WP f2 #() {{ λ g, WP g #() {{ λ _, True }} }} - Φ (f1,f2)%V)
WP one_shot_example #() {{ Φ }}.
Proof.
wp_let.
wp eapply wp_alloc; eauto with I.
apply forall_intro=> l; apply wand_intro_l.
eapply sep_elim_True_l; first by apply (own_alloc OneShotPending).
rewrite !pvs_frame_r; apply wp_strip_pvs.
rewrite !sep_exist_r; apply exist_elim=>γ.
(* TODO: this is horrible *)
trans (heap_ctx heapN (|==> inv N (one_shot_inv γ l))
( f1 f2 : val,
( n : Z, WP f1 #n {{ λ w, w = #true w = #false }})
WP f2 #() {{ λ g, WP g #() {{ λ _, True }} }} - Φ (f1, f2)%V))%I.
{ ecancel [heap_ctx _; _, _]%I. rewrite -inv_alloc // -later_intro.
apply or_intro_l'. solve_sep_entails. }
rewrite pvs_frame_r pvs_frame_l; apply wp_strip_pvs; wp_let.
rewrite !assoc 2!forall_elim; eapply wand_apply_r'; first done.
rewrite (always_sep_dup (_ _)); apply sep_mono.
- apply forall_intro=>n. apply: always_intro. wp_let.
eapply (wp_inv_timeless _ _ _ (one_shot_inv γ l));
rewrite /= ?to_of_val; eauto 10 with I.
rewrite (True_intro (inv _ _)) right_id.
apply wand_intro_r; rewrite sep_or_l; apply or_elim.
+ rewrite -wp_pvs.
wp eapply wp_cas_suc; rewrite /= ?to_of_val; eauto with I ndisj.
rewrite (True_intro (heap_ctx _)) left_id.
ecancel [l _]%I; apply wand_intro_l.
rewrite (own_update); (* FIXME: canonical structures are not working *)
last by apply (one_shot_update_shoot (DecAgree n : dec_agreeR _)).
rewrite pvs_frame_l; apply pvs_mono, sep_intro_True_r; eauto with I.
rewrite /one_shot_inv -or_intro_r -(exist_intro n).
solve_sep_entails.
+ rewrite sep_exist_l; apply exist_elim=>m.
eapply wp_cas_fail with (v':=InjRV #m) (q:=1%Qp);
rewrite /= ?to_of_val; eauto with I ndisj; strip_later.
ecancel [l _]%I; apply wand_intro_l, sep_intro_True_r; eauto with I.
rewrite /one_shot_inv -or_intro_r -(exist_intro m).
solve_sep_entails.
- apply: always_intro. wp_seq.
wp_focus (Load (%l))%I.
eapply (wp_inv_timeless _ _ _ (one_shot_inv γ l));
rewrite /= ?to_of_val; eauto 10 with I.
apply wand_intro_r.
trans (heap_ctx heapN inv N (one_shot_inv γ l) v, l v
((v = InjLV #0 own γ OneShotPending)
n : Z, v = InjRV #n own γ (Shot (DecAgree n))))%I.
{ rewrite assoc. apply sep_mono_r, or_elim.
+ rewrite -(exist_intro (InjLV #0)). rewrite -or_intro_l const_equiv //.
solve_sep_entails.
+ apply exist_elim=> n. rewrite -(exist_intro (InjRV #n)) -(exist_intro n).
apply sep_mono_r, or_intro_r', sep_intro_True_l; eauto with I. }
rewrite !sep_exist_l; apply exist_elim=> w.
eapply wp_load with (q:=1%Qp) (v:=w); eauto with I ndisj.
rewrite -later_intro; cancel [l w]%I.
rewrite -later_intro; apply wand_intro_l.
trans (heap_ctx heapN inv N (one_shot_inv γ l) one_shot_inv γ l
(w = InjLV #0 ( n : Z, w = InjRV #n own γ (Shot (DecAgree n)))))%I.
{ cancel [heap_ctx heapN]. rewrite !sep_or_l; apply or_elim.
+ rewrite -or_intro_l. ecancel [inv _ _]%I.
rewrite [(_ _)%I]comm -assoc. apply const_elim_sep_l=>->.
rewrite const_equiv // right_id /one_shot_inv -or_intro_l .
solve_sep_entails.
+ rewrite -or_intro_r !sep_exist_l; apply exist_elim=> n.
rewrite -(exist_intro n). ecancel [inv _ _]%I.
rewrite [(_ _)%I]comm -assoc. apply const_elim_sep_l=>->.
rewrite const_equiv // left_id /one_shot_inv -or_intro_r.
rewrite -(exist_intro n) {1}(always_sep_dup (own _ _)).
solve_sep_entails. }
cancel [one_shot_inv γ l].
(* FIXME: why aren't laters stripped? *)
wp_let. rewrite -later_intro.
apply: always_intro. wp_seq. rewrite -later_intro.
rewrite !sep_or_l; apply or_elim.
{ rewrite assoc.
apply const_elim_sep_r=>->. wp_case; wp_seq; eauto with I. }
rewrite !sep_exist_l; apply exist_elim=> n.
rewrite [(w=_ _)%I]comm !assoc; apply const_elim_sep_r=>->.
(* FIXME: why do we need to fold? *)
wp_case; fold of_val. wp_let. wp_focus (Load (%l))%I.
eapply (wp_inv_timeless _ _ _ (one_shot_inv γ l));
rewrite /= ?to_of_val; eauto 10 with I.
rewrite (True_intro (inv _ _)) right_id.
apply wand_intro_r; rewrite sep_or_l; apply or_elim.
+ rewrite (True_intro (heap_ctx _)) (True_intro (l _)) !left_id.
rewrite -own_op own_valid_l one_shot_validI /= left_absorb.
apply False_elim.
+ rewrite !sep_exist_l; apply exist_elim=> m.
eapply wp_load with (q:=1%Qp) (v:=InjRV #m); eauto with I ndisj; strip_later.
cancel [l InjRV #m]%I. apply wand_intro_r.
rewrite (True_intro (heap_ctx heapN)) left_id.
rewrite -own_op own_valid_l one_shot_validI Shot_op /= discrete_valid.
rewrite -assoc. apply const_elim_sep_l=> /dec_agree_op_inv [->].
rewrite dec_agree_idemp. apply sep_intro_True_r.
{ rewrite /one_shot_inv -or_intro_r -(exist_intro m). solve_sep_entails. }
wp_case; fold of_val. wp_let. rewrite -wp_assert'.
wp_op; by eauto using later_intro with I.
Qed.
Lemma hoare_one_shot (Φ : val iProp) :
heap_ctx heapN {{ True }} one_shot_example #()
{{ λ ff,
( n : Z, {{ True }} Fst ff #n {{ λ w, w = #true w = #false }})
{{ True }} Snd ff #() {{ λ g, {{ True }} g #() {{ λ _, True }} }}
}}.
Proof.
apply: always_intro; rewrite left_id -wp_one_shot /=.
cancel [heap_ctx heapN].
apply forall_intro=> f1; apply forall_intro=> f2.
apply wand_intro_l; rewrite right_id; apply sep_mono.
- apply forall_mono=>n. apply always_mono; rewrite left_id. by wp_proj.
- apply always_mono; rewrite left_id. wp_proj.
apply wp_mono=> v. by apply always_mono; rewrite left_id.
Qed.
End proof.
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