client.v 3.86 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 {Σ : rFunctorG} `{!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
36
37
38
39
40
41
42
43
  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.
    (* TODO these aprenthesis are rather surprising. *)
    (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
56
57
58
59
60
    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.
    { do 2 apply forall_intro=>_. apply wand_intro_l. eauto with I. }
    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
61
      wp_seq. rewrite -signal_spec right_id assoc sep_elim_l comm.
62
      apply sep_mono_r. rewrite /y_inv -(exist_intro (λ: "z", '"z" + #42)%V).
Ralf Jung's avatar
Ralf Jung committed
63
      apply sep_intro_True_r; first done. apply: always_intro.
64
65
66
67
68
69
70
71
72
73
      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.
      { do 2 apply forall_intro=>_. apply wand_intro_l. eauto with I. }
      sep_split left: [recv heapN _ _ _; heap_ctx _]%I; by rewrite -worker_safe comm.
Qed.
Ralf Jung's avatar
Ralf Jung committed
74
End client.
75
76

Section ClosedProofs.
77
  Definition Σ : rFunctorG := #[ heapGF ; barrierGF ; spawnGF ].
78
79
80
81
  Notation iProp := (iPropG heap_lang Σ).

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

  Print Assumptions client_safe_closed.
End ClosedProofs.