4.5. Concurrency🔗

HeapLang has only one primitive for concurrency: fork(_). The instruction fork(e) creates a new thread which executes e. The invoking thread continues execution after creation. If the computation of e terminates, then the resulting value is simply thrown away. Hence, e is only run for its side effects.

From the fork primitive, we can implement several other constructions for concurrency. The Rocq version of HeapLang ships with two such constructions, spawn and par, which are derived from fork. At the time of writing, iris-lean has not yet ported these libraries; the equivalent examples in the Rocq tutorial (Example spawn and Example par) therefore have no direct Lean counterpart in this chapter.

TODO (upstream — iris-lean): once the spawn / par libraries are ported, add the two corresponding examples here. The Rocq versions are reproduced below as reference for the port.

(* Rocq tutorial — to be ported once iris-lean has spawn/par *)
Example spawn_ex : expr :=
  let: "l" := ref #5 in
  let: "handle" := spawn (λ: "_", "l" <- #6;; #2) in
  let: "res" := spawn.join "handle" in
  let: "v" := !"l" in
  ("res", "v").
(* Evaluates to (2, 6). *)

Example par_ex : expr :=
  let: "l" := ref #5 in
  let: "res" := (!"l" + #1) ||| (!"l" + #2) in
  Fst "res" + Snd "res".
(* Evaluates to 13. *)