spawn.v 3.21 KB
Newer Older
1
From iris.program_logic Require Export global_functor.
Robbert Krebbers's avatar
Robbert Krebbers committed
2 3
From iris.proofmode Require Import invariants ghost_ownership.
From iris.heap_lang Require Import proofmode notation.
Ralf Jung's avatar
Ralf Jung committed
4 5 6
Import uPred.

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

18
(** The CMRA we need. *)
Ralf Jung's avatar
Ralf Jung committed
19 20 21 22
(* Not bundling heapG, as it may be shared with other users. *)
Class spawnG Σ := SpawnG {
  spawn_tokG :> inG heap_lang Σ (exclR unitC);
}.
23
(** The functor we need. *)
24
Definition spawnGF : gFunctorList := [GFunctor (constRF (exclR unitC))].
25
(* Show and register that they match. *)
26
Instance inGF_spawnG `{H : inGFs heap_lang Σ spawnGF} : spawnG Σ.
27
Proof. destruct H as (?&?). split. apply: inGF_inG. Qed.
Ralf Jung's avatar
Ralf Jung committed
28 29 30

(** Now we come to the Iris part of the proof. *)
Section proof.
31
Context `{!heapG Σ, !spawnG Σ} (N : namespace).
Ralf Jung's avatar
Ralf Jung committed
32 33 34
Local Notation iProp := (iPropG heap_lang Σ).

Definition spawn_inv (γ : gname) (l : loc) (Ψ : val  iProp) : iProp :=
Robbert Krebbers's avatar
Robbert Krebbers committed
35 36
  ( lv, l  lv  (lv = NONEV 
                    v, lv = SOMEV v  (Ψ v  own γ (Excl ()))))%I.
Ralf Jung's avatar
Ralf Jung committed
37 38

Definition join_handle (l : loc) (Ψ : val  iProp) : iProp :=
39 40
  (heapN  N   γ, heap_ctx  own γ (Excl ()) 
                    inv N (spawn_inv γ l Ψ))%I.
Ralf Jung's avatar
Ralf Jung committed
41

Robbert Krebbers's avatar
Robbert Krebbers committed
42 43
Typeclasses Opaque join_handle.

Ralf Jung's avatar
Ralf Jung committed
44 45 46 47 48 49 50 51
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
52 53
Lemma spawn_spec (Ψ : val  iProp) e (f : val) (Φ : val  iProp) :
  to_val e = Some f 
54
  heapN  N 
55
  heap_ctx  WP f #() {{ Ψ }}  ( l, join_handle l Ψ - Φ #l)
56
   WP spawn e {{ Φ }}.
Ralf Jung's avatar
Ralf Jung committed
57
Proof.
58
  iIntros (<-%of_to_val ?) "(#Hh & Hf & HΦ)". rewrite /spawn.
59
  wp_let. wp_alloc l as "Hl". wp_let.
60
  iPvs (own_alloc (Excl ())) as (γ) "Hγ"; first done.
61
  iPvs (inv_alloc N _ (spawn_inv γ l Ψ) with "[Hl]") as "#?"; first done.
Robbert Krebbers's avatar
Robbert Krebbers committed
62
  { iNext. iExists NONEV. iFrame; eauto. }
Robbert Krebbers's avatar
Robbert Krebbers committed
63
  wp_apply wp_fork. iSplitR "Hf".
64
  - iPvsIntro. wp_seq. iPvsIntro. iApply "HΦ". rewrite /join_handle. eauto.
65
  - wp_focus (f _). iApply wp_wand_l. iFrame "Hf"; iIntros (v) "Hv".
66
    iInv N as (v') "[Hl _]".
67
    wp_store. iPvsIntro. iSplit; [iNext|done].
Robbert Krebbers's avatar
Robbert Krebbers committed
68
    iExists (SOMEV v). iFrame. eauto.
Ralf Jung's avatar
Ralf Jung committed
69 70 71
Qed.

Lemma join_spec (Ψ : val  iProp) l (Φ : val  iProp) :
72
  join_handle l Ψ  ( v, Ψ v - Φ v)  WP join #l {{ Φ }}.
Ralf Jung's avatar
Ralf Jung committed
73
Proof.
74 75
  rewrite /join_handle; iIntros "[[% H] Hv]". iDestruct "H" as (γ) "(#?&Hγ&#?)".
  iLöb as "IH". wp_rec. wp_focus (! _)%E. iInv N as (v) "[Hl Hinv]".
Robbert Krebbers's avatar
Robbert Krebbers committed
76
  wp_load. iDestruct "Hinv" as "[%|Hinv]"; subst.
77
  - iPvsIntro; iSplitL "Hl"; [iNext; iExists _; iFrame; eauto|].
78
    wp_match. iApply ("IH" with "Hγ Hv").
79
  - iDestruct "Hinv" as (v') "[% [HΨ|Hγ']]"; simplify_eq/=.
80
    + iPvsIntro; iSplitL "Hl Hγ".
81
      { iNext. iExists _; iFrame; eauto. }
82
      wp_match. by iApply "Hv".
83
    + iCombine "Hγ" "Hγ'" as "Hγ". iDestruct (own_valid with "Hγ") as %[].
Ralf Jung's avatar
Ralf Jung committed
84
Qed.
Ralf Jung's avatar
Ralf Jung committed
85
End proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
86 87

Typeclasses Opaque join_handle.