Parallel increment.

_CoqProject

@@ -22,4 +22,5 @@ theories/tests/swap.v
 theories/tests/fact.v
 theories/tests/memcpy.v
 theories/tests/gcd.v
+theories/tests/par_inc.v
 # theories/tests/lists.v

theories/tests/par_inc.v

+From iris_c.vcgen Require Import proofmode.
+From iris.algebra Require Import frac_auth.
+
+Definition inc : val := λ: "l",
+  a_ret "l" +=ᶜ ♯ 1 ;ᶜ ♯ 1.
+
+Definition par_inc : val := λ: "l",
+  callᶜ (inc, a_ret "l") +ᶜ callᶜ (inc, a_ret "l").
+
+Section par_inc.
+  Context `{amonadG Σ, !inG Σ (frac_authR natR)}.
+
+  Lemma inc_spec R cl (n : Z) Φ :
+    cl ↦C #n -∗ (cl ↦C #(1 + n) -∗ Φ #1) -∗
+    AWP inc (cloc_to_val cl) @ R {{ Φ }}.
+  Proof. iIntros. awp_lam. by vcg. Qed.
+
+  Lemma par_inc_spec R cl (n : Z) :
+    cl ↦C #n -∗
+    AWP par_inc (cloc_to_val cl) @ R {{ v, ⌜ v = #2 ⌝ ∧ cl ↦C #(2 + n) }}.
+  Proof.
+    iIntros "Hl". awp_lam.
+    iMod (own_alloc (●! 0%nat ⋅ ◯! 0%nat)) as (γ) "[Hγ [Hγ1 Hγ2]]"; [done|].
+    set (par_inc_inv := (∃ n' : nat, cl ↦C #(n' + n) ∗ own γ (●! n'))%I).
+    iApply (awp_insert_res _ _ par_inc_inv with "[Hγ Hl]").
+    { iExists 0%nat. iFrame. }
+    iAssert (□ (own γ (◯!{1 / 2} 0%nat) -∗
+      AWP callᶜ (inc, a_ret (cloc_to_val cl)) @ par_inc_inv ∗ R
+      {{ v, ⌜v = #1⌝ ∧ own γ (◯!{1 / 2} 1%nat) }}))%I as "#H".
+    { iIntros "!> Hγ'". vcg; iIntros "!> [HR $]". iDestruct "HR" as (n') "[Hl Hγ]".
+      iApply awp_fupd. iApply (inc_spec with "[$]"); iIntros "Hl".
+      iMod (own_update_2 with "Hγ Hγ'") as "[Hγ Hγ']".
+      { apply frac_auth_update, (nat_local_update _ _ (S n') 1); lia. }
+      iModIntro. iSplitL "Hl Hγ"; last vcg_continue; eauto.
+      iExists (S n'). rewrite Nat2Z.inj_succ -Z.add_1_l -Z.add_assoc. iFrame. }
+    iApply (a_bin_op_spec _ _ (λ v, ⌜ v = #1 ⌝ ∧ own γ (◯!{1 / 2} 1%nat))%I
+      (λ v, ⌜ v = #1 ⌝ ∧ own γ (◯!{1 / 2} 1%nat))%I with "[Hγ1] [Hγ2]").
+    - by iApply "H".
+    - by iApply "H".
+    - iIntros (v1 v2) "[-> Hγ1] [-> Hγ2]". iExists #2; iSplit; first done.
+      iDestruct 1 as (n') ">[Hl Hγ]". iCombine "Hγ1 Hγ2" as "Hγ'".
+      iDestruct (own_valid_2 with "Hγ Hγ'") as %->%frac_auth_agreeL. by iFrame.
+  Qed.
+End par_inc.
\ No newline at end of file