Remove overly specific examples

They will use Iris is a library, in that paper's repo

README.md

@@ -33,5 +33,5 @@ running:
   language-independent derived constructions (e.g., STSs).
 * The folder `heap_lang` defines the ML-like concurrent heap language, and a
   few derived constructions (e.g., parallel composition).
-* The folder `barrier` contains the implementation and proof of the barrier.
-* The folder `examples` contains the examples given in the paper.
+* The folder `barrier` contains the implementation and proof of the barrier
+  <http://doi.acm.org/10.1145/2818638>.

_CoqProject

@@ -94,5 +94,3 @@ barrier/specification.v
 barrier/protocol.v
 barrier/proof.v
 barrier/client.v
-examples/joining_existentials.v
-examples/one_shot.v

examples/joining_existentials.v

-From iris.program_logic Require Import saved_one_shot hoare tactics.
-From iris.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.

examples/one_shot.v

-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.