client.v 3.91 KB
Newer Older
1
From barrier Require Import proof.
2
From heap_lang Require Import par.
3
From program_logic Require Import auth sts saved_prop hoare ownership.
Ralf Jung's avatar
Ralf Jung committed
4 5
Import uPred.

6
Definition worker (n : Z) : val :=
7 8
  λ: "b" "y", ^wait '"b" ;; !'"y" #n.
Definition client : expr [] :=
9
  let: "y" := ref #0 in
10
  let: "b" := ^newbarrier #() in
11 12
  ('"y" <- (λ: "z", '"z" + #42) ;; ^signal '"b") ||
    (^(worker 12) '"b" '"y" || ^(worker 17) '"b" '"y").
Ralf Jung's avatar
Ralf Jung committed
13 14

Section client.
15
  Context {Σ : gFunctors} `{!heapG Σ, !barrierG Σ, !spawnG Σ} (heapN N : namespace).
Ralf Jung's avatar
Ralf Jung committed
16 17
  Local Notation iProp := (iPropG heap_lang Σ).

18
  Definition y_inv q y : iProp :=
Ralf Jung's avatar
Ralf Jung committed
19
    ( f : val, y {q} f    n : Z, #> f #n {{ λ v, v = #(n + 42) }})%I.
20

Ralf Jung's avatar
Ralf Jung committed
21 22 23 24 25 26 27 28 29 30
  Lemma y_inv_split q y :
    y_inv q y  (y_inv (q/2) y  y_inv (q/2) y).
  Proof.
    rewrite /y_inv. apply exist_elim=>f.
    rewrite -!(exist_intro f). rewrite heap_mapsto_op_split.
    ecancel [y {_} _; y {_} _]%I. by rewrite [X in X  _]always_sep_dup.
  Qed.

  Lemma worker_safe q (n : Z) (b y : loc) :
    (heap_ctx heapN  recv heapN N b (y_inv q y))
Ralf Jung's avatar
Ralf Jung committed
31
       #> worker n (%b) (%y) {{ λ _, True }}.
Ralf Jung's avatar
Ralf Jung committed
32 33 34 35
  Proof.
    rewrite /worker. wp_lam. wp_let. ewp apply wait_spec.
    rewrite comm. apply sep_mono_r. apply wand_intro_l.
    rewrite sep_exist_r. apply exist_elim=>f. wp_seq.
36
    (* TODO these parenthesis are rather surprising. *)
Ralf Jung's avatar
Ralf Jung committed
37 38 39 40 41 42 43
    (ewp apply: (wp_load heapN _ _ q f)); eauto with I.
    strip_later. (* hu, shouldn't it do that? *)
    rewrite -assoc. apply sep_mono_r. apply wand_intro_l.
    rewrite always_elim (forall_elim n) sep_elim_r sep_elim_l.
    apply wp_mono=>?. eauto with I.
  Qed.

Ralf Jung's avatar
Ralf Jung committed
44
  Lemma client_safe :
Ralf Jung's avatar
Ralf Jung committed
45
    heapN  N  heap_ctx heapN  #> client {{ λ _, True }}.
Ralf Jung's avatar
Ralf Jung committed
46 47
  Proof.
    intros ?. rewrite /client.
Ralf Jung's avatar
Ralf Jung committed
48 49 50 51 52
    (ewp eapply wp_alloc); eauto with I. strip_later. apply forall_intro=>y.
    apply wand_intro_l. wp_let.
    ewp eapply (newbarrier_spec heapN N (y_inv 1 y)); last done.
    rewrite comm. rewrite {1}[heap_ctx _]always_sep_dup -!assoc.
    apply sep_mono_r. apply forall_intro=>b. apply wand_intro_l. 
53 54 55
    wp_let. (ewp eapply (wp_par heapN N (λ _, True%I) (λ _, True%I))); eauto.
    rewrite 2!{1}[heap_ctx _]always_sep_dup !assoc [(_  heap_ctx _)%I]comm.
    ecancel [heap_ctx _]. sep_split right: []; last first.
56 57
    { do 2 apply forall_intro=>_. apply wand_intro_l.
      eauto using later_intro with I. }
58 59 60 61
    sep_split left: [send heapN _ _ _; heap_ctx _; y  _]%I.
    - (* The original thread, the sender. *)
      (ewp eapply wp_store); eauto with I. strip_later.
      ecancel [y  _]%I. apply wand_intro_l.
Ralf Jung's avatar
Ralf Jung committed
62
      wp_seq. rewrite -signal_spec right_id assoc sep_elim_l comm.
63
      apply sep_mono_r. rewrite /y_inv -(exist_intro (λ: "z", '"z" + #42)%V).
Ralf Jung's avatar
Ralf Jung committed
64
      apply sep_intro_True_r; first done. apply: always_intro.
65 66 67 68 69 70 71
      apply forall_intro=>n. wp_let. wp_op. by apply const_intro.
    - (* The two spawned threads, the waiters. *)
      rewrite recv_mono; last exact: y_inv_split.
      rewrite (recv_split _ _ ) // pvs_frame_r. apply wp_strip_pvs.
      (ewp eapply (wp_par heapN N (λ _, True%I) (λ _, True%I))); eauto.
      do 2 rewrite {1}[heap_ctx _]always_sep_dup.
      ecancel [heap_ctx _]. rewrite !assoc. sep_split right: []; last first.
72 73
      { do 2 apply forall_intro=>_. apply wand_intro_l.
        eauto using later_intro with I. }
74 75
      sep_split left: [recv heapN _ _ _; heap_ctx _]%I; by rewrite -worker_safe comm.
Qed.
Ralf Jung's avatar
Ralf Jung committed
76
End client.
77 78

Section ClosedProofs.
79
  Definition Σ : gFunctors := #[ heapGF ; barrierGF ; spawnGF ].
80 81 82 83
  Notation iProp := (iPropG heap_lang Σ).

  Lemma client_safe_closed σ : {{ ownP σ : iProp }} client {{ λ v, True }}.
  Proof.
84
    apply ht_alt. rewrite (heap_alloc (nroot .@ "Barrier")); last done.
85
    apply wp_strip_pvs, exist_elim=> ?. rewrite and_elim_l.
Robbert Krebbers's avatar
Robbert Krebbers committed
86
    rewrite -(client_safe (nroot .@ "Barrier") (nroot .@ "Heap")) //.
87
    (* This, too, should be automated. *)
Robbert Krebbers's avatar
Robbert Krebbers committed
88
    by apply ndot_ne_disjoint.
89 90 91 92
  Qed.

  Print Assumptions client_safe_closed.
End ClosedProofs.