structured_conc.v

From iris.algebra Require Import excl.
From iris.base_logic.lib Require Export invariants token.
From iris.heap_lang Require Import lang proofmode notation par.

(* ################################################################# *)
(** * Structured Concurrency *)

(* ================================================================= *)
(** ** Introduction *)

(**
  As the reader might recall from the HeapLang chapter, the only
  construct for concurrency supported natively by HeapLang is [Fork].
  The [Fork] construction is an example of _unstructured_ concurrency.
  When we use [Fork] to create a new thread, there are no control flow
  constructs to reason about the termination of the forked thread – it
  just runs until it is done and, upon completion, disappears.

  When such control flow constructs are available, we call it
  _structured_ concurrency. It turns out that we can implement
  structured concurrency from unstructured concurrency, and we have
  already seen two such examples: [spawn] and [par]. Both of these
  constructs are part of HeapLang's library, but under the hood, they
  are simply HeapLang programs defined in terms of the [Fork] primitive.

  The library definitions additionally give and prove specifications for
  the constructs, which we have used in previous chapters. In this
  chapter, we will define the constructs from scratch and write our own
  specifications for them.
*)

(** One simple form of structured concurrency is parallel composition [par].
  A program [e1 ||| e2] executes [e1] and [e2] in parallel; when both finish,
  it moves on to the rest of the program. Parallel composition has a very
  natural spec in separation logic:

                {{{ P1 }}} e1 {{{ Q1 }}}   {{{ P2 }}} e2 {{{ Q2 }}}
                ---------------------------------------------------
                    {{{ P1 ∗ P2 }}} e1 ||| e2 {{{ Q1 ∗ Q2 }}}

  We divide our resources into an [e1] part and an [e2] part, then recombine
  the results when both are finished. HeapLang's [par_spec] is phrased in
  terms of WP instead of triples, but otherwise says the same thing. *)
Check par_spec.

(**
  Let us try to use the [par] specification to prove a specification for a
  simple client. The client performs two `fetch and add' operations on
  the same location in parallel. The expression [FAA "l" #i] atomically
  fetches the value at location [l], adds [i] to it, and stores the
  result back in [l].

  Our specification will state that the resulting value is even.
*)

Definition parallel_add : expr :=
  let: "r" := ref #0 in
  (FAA "r" #2)
  |||
  (FAA "r" #6)
  ;;
  !"r".

Section parallel_add.

Context `{!heapGS Σ, !spawnG Σ}.

Let N := nroot .@ "par_add".

(**
  We will have an invariant stating that [r] points to an even integer.
*)
Definition parallel_add_inv (r : loc) : iProp Σ :=
  ∃ n : Z, r ↦ #n ∗ ⌜Zeven n⌝.

(** Exercise: Could we prove a stronger invariant? *)

Lemma parallel_add_spec :
  {{{ True }}} parallel_add {{{ n, RET #n; ⌜Zeven n⌝ }}}.
Proof.
  iIntros "%Φ H HΦ".
  rewrite /parallel_add.
  wp_alloc r as "Hr".
  wp_pures.
  iMod (inv_alloc N _ (parallel_add_inv r) with "[Hr]") as "#I".
  {
    iNext.
    unfold parallel_add_inv.
    iExists 0.
    iFrame.
  }
  (**
    We don't need information back from the threads, so we will simply
    use [λ _, True] as the postconditions. Similarly, we only need the
    invariant to prove the threads, and since this is in the persistent
    context, we let the preconditions be [True].
  *)
  wp_apply (par_spec (λ _, True%I) (λ _, True%I)).
  - wp_pure.
    iInv "I" as "H".
    unfold parallel_add_inv at 2.
    iDestruct "H" as "(%n & Hr & Heven)".
    wp_faa.
    iModIntro.
    iSplitL "Hr Heven".
    {
      iModIntro.
      unfold parallel_add_inv.
      iExists (n + 2)%Z.
      iFrame.
      iDestruct "Heven" as "%Heven".
      iPureIntro.
      apply Zeven_plus_Zeven.
      * done.
      * done.
    }
    done.
  (* exercise *)
Admitted.

End parallel_add.

(* ================================================================= *)
(** ** The Spawn Construct *)

(**
  Another common pattern is usually called "fork-join": we create a thread,
  let it run for a while, then wait for it to finish and read its result.
  We will use the name "spawn" instead of "fork", since HeapLang already
  uses "fork" for the non-returning version. *)

Definition factorial : val :=
  rec: "f" "n" := if: "n" = #0 then #1 else "n" * "f" ("n" - #1).

Definition spawn_join_ex (x : loc): expr :=
  let: "h" := spawn (λ: <>, factorial #10) in
  (* do some other work;; *)
  let: "r" := join "h" in
  #x <- "r".

(** Unlike fork or par, the two threads communicate directly: spawning
  a function returns a "handle" that we can use to join with it later,
  and when we join with it we receive the value returned by that function.
  Exercise: What should the specs for [spawn] and [join] be? *)












  (**  We give [spawn] the specification:

  [[
    {{{ P }}} f #() {{{ v, RET v; Ψ v }}} -∗
    {{{ P }}} spawn f {{{ h, RET h; join_handle h Ψ }}}
  ]]

  This states that to get a specification for [spawn f], we first must
  prove a specification for [f] which captures which resources [f]
  needs, [P], and what the value [f] terminates at satisfies, [Ψ]. If we
  can prove such a specification for [f], then, given [P], we can also
  run [spawn f], which will return a value [h] which satisfies a
  `join-handle' predicate. This predicate is a promise that if we
  invoke [join] with [h], then the value we get back satisfies [Ψ]. This
  is reflected in the specification for [join]:

  [[
    {{{ join_handle h Ψ }}} join h {{{ v, RET v; Ψ v }}}.
  ]]
*)

(** We can define [spawn] and [join] using [Fork] as follows.
*)

Definition spawn : val :=
  λ: "f",
    let: "c" := ref NONE in
    Fork ("c" <- SOME ("f" #()));;
    "c".

Definition join: val :=
  rec: "join" "c" :=
    match: !"c" with
      NONE => "join" "c"
    | SOME "x" => "x"
    end.

(**
  The idea with [spawn] is to create a `shared channel' which can be
  used to signal when the forked-off thread has terminated. In this
  case, the shared channel is simply a location containing an optional
  value. When forking off the function ["f"], we wrap it around a store
  operation, which writes the result of ["f"] into the location. The
  location is then returned to the spawning thread, which can use this
  so-called `handle' in the [join] function. The [join] function
  continuously checks if the location has been updated to contain a
  value. If this happens, the spawning thread knows that the forked-off
  thread has finished, so it can extract the return value from the
  location.

  Let us now prove that these implementations meet our specifications
  for [spawn] and [join].
*)

Section spawn.

Context `{!heapGS Σ}.
Let N := nroot .@ "handle".

Notation NONE := (InjL #()).
Notation NONEV := (InjLV #()).
Notation SOME x := (InjR x).
Notation SOMEV x := (InjRV x).

(**
  Since we are using a shared channel, we will use an invariant to allow
  the two (concurrently running) threads to access it. An initial
  attempt at stating this invariant looks as follows.
*)
Definition handle_inv1 (l : loc) (Ψ : val → iProp Σ) : iProp Σ :=
  ∃ v : val, l ↦ v ∗ (⌜v = NONEV⌝ ∨ ∃ w : val, ⌜v = SOMEV w⌝ ∗ Ψ w).

(**
  The stated invariant governs the shared channel (some location [l])
  and states that either no value has been sent yet or some value has
  been sent that satisfies the predicate [Ψ].

  We can then use the invariant to define the [join_handle] predicate.
*)
Definition join_handle1 (h : val) (Ψ : val → iProp Σ) : iProp Σ :=
  ∃ l : loc, ⌜h = #l⌝ ∗ inv N (handle_inv1 l Ψ).

(** Let us now attempt to prove the specification for [join]. *)
Lemma join_spec (h : val) (Ψ : val → iProp Σ) :
  {{{ join_handle1 h Ψ }}} join h {{{ v, RET v; Ψ v }}}.
Proof.
  iIntros "%Φ H HΦ".
  unfold join_handle1.
  iDestruct "H" as "(%l & -> & #I)". (* -> rewrites with the equation immediately *)
  iLöb as "IH".
  unfold join at 2.
  wp_rec.
  fold join.
  wp_bind (! _)%E.
  iInv "I" as "(%v & Hl & HI)".
  wp_load.
  iDestruct "HI" as "[% | (%w & % & HΨ)]".
  - iModIntro.
    rewrite H.
    iSplitL "Hl".
    {
      iNext.
      unfold handle_inv1 at 2.
      iExists NONEV.
      iFrame.
      by iLeft.
    }
    wp_pures.
    iApply "IH".
    done.
  - rewrite H.
    iModIntro.
    unfold handle_inv1 at 2.
    iSplitL "Hl HΨ".
    { iModIntro.
      iExists (SOMEV w).
      iFrame.
      iRight.
      iExists w.
      iFrame.
      done.
    }
    wp_pures.
    iApply "HΦ".
    (** 
      Now we need [HΨ] to reestablish the invariant, but we also need it
      for the postcondition. We are stuck... 
    *)
Abort.

(**
  We need a way to keep track of whether [Ψ w] has been `taken out' of
  the invariant or not. However, we do not have any program state to
  link it to. Instead, we will use _ghost state_ to track this
  information. In particular, we will use _tokens_, which we introduced
  in the Resource Algebra chapter. We here use the token implementation
  from the Iris library, but it is similar to the version we
  implemented.
*)
Context `{!tokenG Σ}.

(* token γ is an assertion *)
Check token _.

(* We can always make a new token with a fresh name: *)
Check token_alloc.
(* And we can never have the same token twice: *)
Check token_exclusive.

(**
  Now, the trick is to have an additional state in the invariant which
  represents the case where [Ψ w] has been taken out of the invariant.
  This state simply holds the token.
*)

Definition handle_inv (γ : gname) (l : loc) (Ψ : val → iProp Σ) : iProp Σ :=
  ∃ v, l ↦ v ∗ (⌜v = NONEV⌝ ∨ (∃ w, ⌜v = SOMEV w⌝ ∗ Ψ w) ∨ token γ).

(**
  This enables the owner of the token to open the invariant, extract
  [Ψ w], and close the invariant in the case that mentions the token. As
  such, we include the token in the join handle so that [join] gets
  access to the token.
*)

Definition join_handle (h : val) (Ψ : val → iProp Σ) : iProp Σ :=
  ∃ γ (l : loc), ⌜h = #l⌝ ∗ token γ ∗ inv N (handle_inv γ l Ψ).

(**
  Let us now try to prove the specifications again. We start with
  [spawn].
*)

Lemma spawn_spec (P : iProp Σ) (Ψ : val → iProp Σ) (f : val) :
  {{{ P }}} f #() {{{ v, RET v; Ψ v }}} -∗
  {{{ P }}} spawn f {{{ h, RET h; join_handle h Ψ }}}.
Proof.
  iIntros "#Hf %Φ !> HP HΦ".
  (* "Hf" is {{{ P }}} f #() {{{ v, RET v; Ψ v }}} *)
  unfold spawn.
  wp_lam.
  wp_alloc l as "Hl".
  wp_pures.
  iDestruct token_alloc as "H".
  iMod "H" as "H".
  iDestruct "H" as "[%γ Hγ]".
  iMod (inv_alloc N _ (handle_inv γ l Ψ) with "[Hl]") as "#I".
  {
    iNext.
    unfold handle_inv.
    iExists NONEV.
    iFrame.
    by iLeft.
  }
  wp_apply (wp_fork with "[Hf HP]").
  - iNext.
    wp_apply ("Hf" with "HP").
    iIntros "%v HΨ".
    wp_pures.
    iInv "I" as "(%w & Hl & ?)".
    wp_store.
    iModIntro.
    iSplitL; last done.
    iNext.
    unfold handle_inv at 2.
    iExists (SOMEV v).
    iFrame.
    iRight.
    iLeft.
    iExists v.
    iFrame.
    done.
  - wp_pures.
    iModIntro.
    iApply "HΦ".
    unfold join_handle.
    iExists γ, l.
    iFrame.
    iSplit.
    + done.
    + done.
Qed.

Lemma join_spec (Ψ : val → iProp Σ) (h : val) :
  {{{ join_handle h Ψ }}} join h {{{ v, RET v; Ψ v }}}.
Proof.
  iIntros "%Φ H HΦ".
  unfold join_handle.
  iDestruct "H" as "(%γ & %l & -> & Hγ & #I)".
  iLöb as "IH".
  wp_rec.
  wp_bind (! #l)%E.
  (** We open the invariant and consider the three possible states. *)
  iInv "I" as "(%v & Hl & HI)".
  wp_load.
  iDestruct "HI" as "[% | [(% & % & HΨ) | Hγ']]".
  - (** Case: The forked-off thread is not yet finished. *)
    iModIntro.
    rewrite H.
    iSplitL "Hl".
    {
      iNext.
      iExists NONEV.
      iFrame.
      by iLeft.
    }
    wp_pures.
    iApply ("IH" with "Hγ HΦ").
  - (** Case: The forked-off thread has finished. *)
    iModIntro.
    rewrite H.
    (**
      Note that now, since we own the token, we do not need to use [Ψ w]
      to close the invariant – we close it with the token.
    *)
    iSplitL "Hγ Hl".
    {
      iNext.
      unfold handle_inv at 2.
      iExists (SOMEV w).
      iFrame.
    }
    wp_pures.
    iApply "HΦ".
    done.
  - (**
      Case: [Ψ w] has already been taken out of the invariant.
      This case is impossible as we own the token.
    *)
    iDestruct (token_exclusive with "Hγ Hγ'") as "H".
    iDestruct "H" as "[]".
Qed.

End spawn.

(* ================================================================= *)
(** ** Building Par from Spawn *)

(**
  We can now rebuild the [par] operator from [spawn] and [join].
*)
Definition par : val :=
  λ: "f1" "f2",
  let: "h" := spawn "f1" in
  let: "v2" := "f2" #() in
  let: "v1" := join "h" in
  ("v1", "v2").

(** We introduce familiar notation for [par] that hides the thunks. *)
Notation "e1 ||| e2" := (par (λ: <>, e1)%E (λ: <>, e2)%E) : expr_scope.
Notation "e1 ||| e2" := (par (λ: <>, e1)%V (λ: <>, e2)%V) : val_scope.

(**
  As above, our desired specification for [par] is going to look as follows:

  [[
    {{{ P1 }}} e1 {{{ v, RET v; Ψ1 v }}} -∗
    {{{ P2 }}} e2 {{{ v, RET v; Ψ2 v }}} -∗
    {{{ P1 ∗ P2 }}} e1 ||| e2 {{{ v1 v2, RET (v1, v2); Ψ1 v1 ∗ Ψ2 v2 }}}
  ]]

  The rule states that we can run [e1] and [e2] in parallel if they have
  _disjoint_ footprints and that we can verify the two components
  separately.
*)

Section par.

(**
  Since [par] is implemented with [spawn], we will use [spawn_spec] and
  [par_spec] to prove the specification for [par]. As such, we will need
  to include the resource algebra that those specifications rely on:
  [token].
*)
Context `{!heapGS Σ, !tokenG Σ}.

(**
  It is actually quite straightforward to prove the [par] specification
  as most of the heavy lifting is done by [spawn_spec] and [join_spec].
*)
Lemma par_spec (P1 P2 : iProp Σ) (e1 e2 : expr) (Q1 Q2 : val → iProp Σ) :
  {{{ P1 }}} e1 {{{ v, RET v; Q1 v }}} -∗
  {{{ P2 }}} e2 {{{ v, RET v; Q2 v }}} -∗
  {{{ P1 ∗ P2 }}} (e1 ||| e2)%V {{{ v1 v2, RET (v1, v2); Q1 v1 ∗ Q2 v2 }}}.
Proof.
  iIntros "#H1 #H2 %Φ !> [HP1 HP2] HΦ".
  rewrite /par.
  wp_pures.
  (**
    We use [spawn_spec] to spawn a thread running [e1]. This requires us
    to prove that if [e1] terminates at value [v1], then [Q1 v1].
    However, this follows by our assumption ["H1"], so we easily prove
    this.
  *)
  wp_apply (spawn_spec P1 Q1 with "[] HP1").
  {
    iIntros "%Φ1 !> HP1  HΦ1".
    wp_pures.
    iApply ("H1" with "HP1 HΦ1").
  }
  (**
    We now get a join handle for the spawned thread, which guarantees us
    that the value we get upon joining with it satisfies [Q1].
  *)
  iIntros "%h Hh".
  wp_pures.
  (**
    Next, we execute [e2] in the current thread using its specification,
    ["H2"], which gives us that if [e2] terminates at some value [v2],
    then [Q2 v2].
  *)
  wp_apply ("H2" with "HP2").
  iIntros "%v2 HQ2".
  wp_pures.
  (**
    Finally, we join with the spawned thread using our join handle and
    [join_spec].
  *)
  wp_apply (join_spec with "Hh").
  iIntros "%v1 HQ1".
  wp_pures.
  iModIntro.
  iApply "HΦ".
  iFrame.
Qed.

End par.