barrier_client.v

From iris_automation.heap_lang Require Import stepping_tacs.
From iris_automation.biabd Require Import biabd_local_updates.
From iris.algebra Require Import frac_auth numbers csum agree.
From iris.heap_lang Require Import proofmode.
From iris_automation.lib Require Import frac_token int_as_nat_diff.
From iris_automation.examples.comparison Require Import barrier.

Definition increment : val := 
  rec: "inc" "c" := 
    let: "v" := ! "c" in
    if: CAS "c" "v" ("v" + #1) then 
      #()
    else 
      "inc" "c".

Definition decrement : val := 
  rec: "dec" "c" := 
    let: "v" := ! "c" in
    if: CAS "c" "v" ("v" - #1) then 
      #()
    else 
      "dec" "c".

Definition check_rising : val := 
  λ: "c",
    let: "a" := ! "c" in
    let: "b" := ! "c" in
    if: "b" < "a" then 
      #() #() (* unsafe *)
    else 
      #().

Definition check_falling : val := 
  λ: "c",
    let: "a" := ! "c" in
    let: "b" := ! "c" in
    if: "a" < "b" then 
      #() #() (* unsafe *)
    else 
      #().

Definition client_thread p : val := 
  λ: "c" "b",
    increment "c";;
    check_rising "c" ;;
    sync_up p "b" ;; 
    decrement "c" ;;
    check_falling "c".

Definition client_run p : val := 
  rec: "spawn_clients" "c" "b" "n" :=
    if: "n" = #0 
    then 
      #()
    else 
      Fork (client_thread p "c" "b") ;;
      "spawn_clients" "c" "b" ("n" - #1).

Definition client p : val := 
  λ: <>, 
    let: "c" := ref #0 in
    let: "b" := make_barrier #() in
    client_run p "c" "b" #(Zpos p).

Definition barrier_clientUR := frac_authUR $ prodR (csumR max_natR max_natR) $ agreeR natO.
Class barrier_clientG Σ :=
  BarrierClientG { 
    barrier_client_clientG :> inG Σ barrier_clientUR;
    barrier_client_barrierG :> barrierG Σ
  }.
Definition barrier_clientΣ : gFunctors :=
  #[GFunctor barrier_clientUR; barrierΣ].

Local Obligation Tactic := program_smash_verify.

Program Instance subG_barrier_clientΣ {Σ} : subG barrier_clientΣ Σ → barrier_clientG Σ.

Section proof.
  Context `{!heapGS Σ, barrier_clientG Σ}.
  Let N := nroot.@"client".

  Definition counter_inv γ (l : loc) : iProp Σ :=
    ∃ (z : Z), l ↦ #z ∗ ∃ (n1 n2 : nat), int_as_nat_diff z n1 n2 ∗
      (own γ (●F (Cinl $ MaxNat n1, to_agree n2)) ∨ own γ (●F (Cinr $ MaxNat n2, to_agree n1))).

  Definition P1 γ : Qp → iProp Σ := λ q,
    (∃ (n1 n2 : nat), own γ (◯F{q} (Cinl $ MaxNat n1, to_agree n2)))%I.

  Definition P2 γ : Qp → iProp Σ := λ q,
    (∃ (n1 n2 : nat), own γ (◯F{q} (Cinr $ MaxNat n1, to_agree n2)))%I.

  Hint Extern 4 (_ ≤ _)%nat => eapply Nat.le_refl : solve_pure_add.

  Lemma p1_fractional γ : Fractional (P1 γ).
  Proof. rewrite /Fractional => p q. apply (anti_symm _); iStepsS. Qed.
  Lemma p2_fractional γ : Fractional (P2 γ).
  Proof. rewrite /Fractional => p q. apply (anti_symm _); iStepsS. Qed.
  Existing Instance p1_fractional. Existing Instance p2_fractional.

  Definition is_counter_barrier threads γp1 γp2 γt γb (v : val) γc : iProp Σ :=
    is_barrier (P1 γc) (P2 γc) threads γp1 γp2 γt γb (v : val).

  Program Instance increment_spec γc (l : loc) :
    SPEC q, {{ P1 γc q ∗ inv N (counter_inv γc l) }}
      increment #l
    {{ RET #(); P1 γc q }}.

  Instance check_rising_spec γc (l : loc) :
    SPEC q, {{ P1 γc q ∗ inv N (counter_inv γc l) }}
      check_rising #l
    {{ RET #(); P1 γc q }}.
  Proof.
    iStepsS.
    assert (x8 = x8 `max` x1) by lia. rewrite {2}H1.
    iLeft. iStepS. rewrite -H1. iSmash.
  Qed.

  Program Instance decrement_spec γc (l : loc) :
    SPEC q, {{ P2 γc q ∗ inv N (counter_inv γc l) }}
      decrement #l
    {{ RET #(); P2 γc q }}.

  Instance check_falling_spec γc (l : loc) :
    SPEC q, {{ P2 γc q ∗ inv N (counter_inv γc l) }}
      check_falling #l
    {{ RET #(); P2 γc q }}.
  Proof.
    iStepsS.
    assert (x9 = x9 `max` x1) by lia. rewrite {3}H1.
    iRight. iStepS. rewrite -H1. iSmash.
  Qed.

  Opaque P1 P2.

  Program Instance client_thread_spec threads γp1 γp2 γt γb (v : val) γc (l : loc) :
    SPEC {{ is_counter_barrier threads γp1 γp2 γt γb v γc ∗ token (P1 γc) γp1 ∗ inv N (counter_inv γc l) }}
      client_thread threads #l v
    {{ RET #(); token (P2 γc) γp2 }}.

  Instance client_run_spec threads γp1 γp2 γt γb (v : val) γc (l : loc) (z : Z) :
    SPEC {{ is_counter_barrier threads γp1 γp2 γt γb v γc ∗ ⌜0 ≤ z⌝%Z ∗ 
          token_iter (P1 γc) (Z.to_nat z) γp1 ∗ inv N (counter_inv γc l) }}
      client_run threads #l v #z
    {{ RET #(); True }}.
  Proof.
    iStepsS. rewrite -{2}(Z2Nat.id z) //.
    generalize (Z.to_nat z) => n.
    iInduction n as [|n] "IH"; wp_lam; first iStepsS.
    change (token_iter (P1 γc) (S n) γp1) with (token (P1 γc) γp1 ∗ token_iter (P1 γc) n γp1)%I.
    iStepsS.
    replace (NtoZ (S n) - 1)%Z with (NtoZ n) by lia.
    iStepsS.
  Qed.

  Transparent P1 P2. 
  (* currently needed because of bug in repeated applications of into_texist; notypeclasses refine works, simple eapply does not.
     problem occurs for biabd_exist lemma, and for TeleSummarize typeclass *)

  Instance client_spec threads :
    SPEC {{ True }}
      client threads #()
    {{ RET #(); True }}.
  Proof.
    iStepsS.
    iAssert (|={⊤}=> ∃ γc, inv N (counter_inv γc x0) ∗ P1 γc 1)%I with "[H2]" as ">[%γc [#HI [%n1 [%n2 HPn]]]]".
    { iSmash. }
    assert (H' := newbarrier_spec (P1 γc) (P2 γc) threads).
    iStepS.
    iStepS.
    rewrite /SolveSep /=.
    iSplitR; [ | iSplitR; iIntros "!>"; [ | iStepsS]].
    - iIntros "!> !>". iStepS. 
      iInv N as "HN". iRevert "HN".
      iStepsS; case: H0 => /= H1 H2; simplify_eq.
      apply biabd_local_updates.agree_equiv in H2. fold_leibniz. subst.
      iRight. iStepsS.
    - iIntros "!> !>". iStepS. 
      iInv N as "HN". iRevert "HN".
      iStepsS; case: H0 => /= H1 H2; simplify_eq.
      apply biabd_local_updates.agree_equiv in H2. fold_leibniz. subst.
      iSmash.
    Unshelve. all: apply inhabitant.
  Qed.
End proof.