spawn.v 5.57 KB
Newer Older
Ralf Jung's avatar
Ralf Jung committed
1
2
3
4
5
6
From program_logic Require Export global_functor.
From heap_lang Require Export heap.
From heap_lang Require Import wp_tactics notation.
Import uPred.

Definition spawn : val :=
Robbert Krebbers's avatar
Robbert Krebbers committed
7
8
9
  λ: "f",
    let: "c" := ref (InjL #0) in
    Fork ('"c" <- InjR ('"f" #())) ;; '"c".
Ralf Jung's avatar
Ralf Jung committed
10
Definition join : val :=
Robbert Krebbers's avatar
Robbert Krebbers committed
11
12
13
14
15
  rec: "join" "c" :=
    match: !'"c" with
      InjR "x" => '"x"
    | InjL <>  => '"join" '"c"
    end.
Ralf Jung's avatar
Ralf Jung committed
16

17
(** The CMRA we need. *)
Ralf Jung's avatar
Ralf Jung committed
18
19
20
21
(* Not bundling heapG, as it may be shared with other users. *)
Class spawnG Σ := SpawnG {
  spawn_tokG :> inG heap_lang Σ (exclR unitC);
}.
22
(** The functor we need. *)
Ralf Jung's avatar
Ralf Jung committed
23
Definition spawnGF : rFunctors := [constRF (exclR unitC)].
24
(* Show and register that they match. *)
Ralf Jung's avatar
Ralf Jung committed
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
Instance inGF_spawnG
  `{inGF heap_lang Σ (constRF (exclR unitC))} : spawnG Σ.
Proof. split. apply: inGF_inG. Qed.

(** Now we come to the Iris part of the proof. *)
Section proof.
Context {Σ : rFunctorG} `{!heapG Σ, !spawnG Σ}.
Context (heapN N : namespace).
Local Notation iProp := (iPropG heap_lang Σ).

Definition spawn_inv (γ : gname) (l : loc) (Ψ : val  iProp) : iProp :=
  ( lv, l  lv  (lv = InjLV #0   v, lv = InjRV v  (Ψ v  own γ (Excl ()))))%I.

Definition join_handle (l : loc) (Ψ : val  iProp) : iProp :=
  ( (heapN  N)   γ, heap_ctx heapN  own γ (Excl ()) 
                        inv N (spawn_inv γ l Ψ))%I.

Global Instance spawn_inv_ne n γ l :
  Proper (pointwise_relation val (dist n) ==> dist n) (spawn_inv γ l).
Proof. solve_proper. Qed.
Global Instance join_handle_ne n l :
  Proper (pointwise_relation val (dist n) ==> dist n) (join_handle l).
Proof. solve_proper. Qed.

(** The main proofs. *)
Ralf Jung's avatar
Ralf Jung committed
50
51
Lemma spawn_spec (Ψ : val  iProp) e (f : val) (Φ : val  iProp) :
  to_val e = Some f 
Ralf Jung's avatar
Ralf Jung committed
52
  heapN  N 
53
  (heap_ctx heapN  #> f #() {{ Ψ }}   l, join_handle l Ψ - Φ (%l))
Ralf Jung's avatar
Ralf Jung committed
54
   #> spawn e {{ Φ }}.
Ralf Jung's avatar
Ralf Jung committed
55
Proof.
Ralf Jung's avatar
Ralf Jung committed
56
57
58
59
60
61
  intros Hval Hdisj. rewrite /spawn.
  (* TODO: Make this more convenient. *)
  wp_focus e. etransitivity; last by eapply wp_value. wp_let.
  (* FIXME: can we change the ewp notation so that the parentheses become unnecessary? *)
  (ewp eapply wp_alloc); eauto with I. strip_later.
  apply forall_intro=>l. apply wand_intro_l. wp_let.
Ralf Jung's avatar
Ralf Jung committed
62
63
64
65
66
  rewrite (forall_elim l). eapply sep_elim_True_l.
  { eapply (own_alloc (Excl ())). done. }
  rewrite !pvs_frame_r. eapply wp_strip_pvs. rewrite !sep_exist_r.
  apply exist_elim=>γ.
  (* TODO: Figure out a better way to say "I want to establish ▷ spawn_inv". *)
67
  trans (heap_ctx heapN  #> f #() {{ Ψ }}  (join_handle l Ψ - Φ (%l)%V) 
Ralf Jung's avatar
Ralf Jung committed
68
         own γ (Excl ())   (spawn_inv γ l Ψ))%I.
Ralf Jung's avatar
Ralf Jung committed
69
  { ecancel [ #> _ {{ _ }}; _ - _; heap_ctx _; own _ _]%I.
Ralf Jung's avatar
Ralf Jung committed
70
71
72
73
    rewrite -later_intro /spawn_inv -(exist_intro (InjLV #0)).
    cancel [l  InjLV #0]%I. apply or_intro_l'. by rewrite const_equiv. }
  rewrite (inv_alloc N) // !pvs_frame_l. eapply wp_strip_pvs.
  ewp eapply wp_fork. rewrite [heap_ctx _]always_sep_dup [inv _ _]always_sep_dup.
74
75
  sep_split left: [_ - _; inv _ _; own _ _; heap_ctx _]%I.
  - wp_seq. eapply wand_apply_l; [done..|].
Ralf Jung's avatar
Ralf Jung committed
76
77
    rewrite /join_handle. rewrite const_equiv // left_id -(exist_intro γ).
    solve_sep_entails.
Ralf Jung's avatar
Ralf Jung committed
78
79
  - wp_focus (f _). rewrite wp_frame_r wp_frame_l.
    rewrite (of_to_val e) //. apply wp_mono=>v.
Ralf Jung's avatar
Ralf Jung committed
80
81
82
83
    eapply (inv_fsa (wp_fsa _)) with (N0:=N); simpl;
      (* TODO: Collect these in some Hint DB? Or add to an existing one? *)
      eauto using to_val_InjR,to_val_InjL,to_of_val with I ndisj.
    apply wand_intro_l. rewrite /spawn_inv {1}later_exist !sep_exist_r.
Ralf Jung's avatar
Ralf Jung committed
84
    apply exist_elim=>lv. rewrite later_sep.
Ralf Jung's avatar
Ralf Jung committed
85
    eapply wp_store; eauto using to_val_InjR,to_val_InjL,to_of_val with I ndisj.
Ralf Jung's avatar
Ralf Jung committed
86
    cancel [ (l  lv)]%I. strip_later. apply wand_intro_l.
Ralf Jung's avatar
Ralf Jung committed
87
88
89
90
91
92
    rewrite right_id -later_intro -{2}[( _, _  _  _)%I](exist_intro (InjRV v)).
    ecancel [l  _]%I. apply or_intro_r'. rewrite sep_elim_r sep_elim_r sep_elim_l.
    rewrite -(exist_intro v). rewrite const_equiv // left_id. apply or_intro_l.
Qed.

Lemma join_spec (Ψ : val  iProp) l (Φ : val  iProp) :
Ralf Jung's avatar
Ralf Jung committed
93
  (join_handle l Ψ   v, Ψ v - Φ v)
Ralf Jung's avatar
Ralf Jung committed
94
95
   #> join (%l) {{ Φ }}.
Proof.
Ralf Jung's avatar
Ralf Jung committed
96
97
98
99
100
101
102
103
104
105
106
  wp_rec. wp_focus (! _)%E.
  rewrite {1}/join_handle sep_exist_l !sep_exist_r. apply exist_elim=>γ.
  rewrite -!assoc. apply const_elim_sep_l=>Hdisj.
  eapply (inv_fsa (wp_fsa _)) with (N0:=N); simpl; eauto with I ndisj.
  apply wand_intro_l. rewrite /spawn_inv {1}later_exist !sep_exist_r.
  apply exist_elim=>lv. rewrite later_sep.
  eapply wp_load; eauto with I ndisj. cancel [ (l  lv)]%I. strip_later.
  apply wand_intro_l. rewrite -later_intro -[X in _  (X  _)](exist_intro lv).
  cancel [l  lv]%I. rewrite sep_or_r. apply or_elim.
  - (* Case 1 : nothing sent yet, we wait. *)
    rewrite -or_intro_l. apply const_elim_sep_l=>-> {lv}.
107
    do 2 rewrite const_equiv // left_id. wp_case; eauto.
Ralf Jung's avatar
Ralf Jung committed
108
109
110
111
112
113
114
115
116
117
    wp_seq. rewrite -always_wand_impl always_elim.
    rewrite !assoc. eapply wand_apply_r'; first done.
    rewrite -(exist_intro γ). solve_sep_entails.
  - rewrite [(_   _)%I]sep_elim_l -or_intro_r !sep_exist_r. apply exist_mono=>v.
    rewrite -!assoc. apply const_elim_sep_l=>->{lv}. rewrite const_equiv // left_id.
    rewrite sep_or_r. apply or_elim; last first.
    { (* contradiction: we have the token twice. *)
      rewrite [(heap_ctx _  _)%I]sep_elim_r !assoc. rewrite -own_op own_valid_l.
      rewrite -!assoc discrete_valid. apply const_elim_sep_l=>-[]. }
    rewrite -or_intro_r. ecancel [own _ _].
118
    wp_case; eauto using to_of_val.
Ralf Jung's avatar
Ralf Jung committed
119
120
121
    wp_let. etransitivity; last by eapply wp_value, to_of_val.
    rewrite (forall_elim v). rewrite !assoc. eapply wand_apply_r'; eauto with I.
Qed.
Ralf Jung's avatar
Ralf Jung committed
122
123

End proof.