5.6. Concurrency🔗

We finish this chapter with a final example that illustrates how ownership of resources can be transferred between threads. The program forks two threads that each write to a separate location.

iris-lean's port of the par library (Iris.HeapLang.Lib.Par) provides:

• the parallel-composition operator e1 ‖ e2 (Rocq tutorial: e1 ||| e2);

• the wp_par lemma which lifts pairs of WP specifications for the two threads to a WP specification of their composition;

• the SpawnG GF class capturing the resources par needs.

Each thread's WP is a separate subgoal of iapply wp_par. The $$ [Hl1] [Hl2] [] annotation explicitly partitions the spatial context: Hl1 goes to the first thread, Hl2 to the second, and the postcondition-handler subgoal receives nothing (it is closed purely from the values returned by the two threads).

The Rocq tutorial's full par_client example wraps this pattern inside a larger let chain that also multiplies the two final values to assert 21 * 2 = 42. That multiplication still depends on a PureExec instance for * on integers, which iris-lean does not yet ship.

-- TODO (upstream — iris-lean): once `PureExec` for arithmetic
-- lands, restore the full `par_client` postcondition with
-- `⌜life = 42⌝`. The `wp_par`-level reasoning above is the
-- complete one — only the post-join arithmetic check is blocked.

-- Rocq tutorial reference:
--   Example par_client : expr :=
--     let: "l1" := ref #0 in
--     let: "l2" := ref #0 in
--     (("l1" <- #21) ||| ("l2" <- #2)) ;;
--     let: "life" := !"l1" * !"l2" in
--     ("l1", "l2", "life").
--   Lemma par_client_spec :
--     {{{ True }}}
--       par_client
--     {{{ l1 l2 life, RET (#l1, #l2, #life);
--         l1 ↦ #21 ∗ l2 ↦ #2 ∗ ⌜life = 42⌝ }}}.