relatomic.v 1.71 KB
Newer Older
Dan Frumin's avatar
Dan Frumin committed
1 2 3 4 5 6 7 8 9 10 11
From iris.proofmode Require Import tactics.
From iris_logrel Require Import logrel.
From iris.program_logic Require Import hoare.

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

Section contents.
12
  Context `{logrelG Σ}.
Dan Frumin's avatar
Dan Frumin committed
13 14 15 16

  Lemma FAI_atomic R1 R2 Γ E1 E2 K x t τ Δ :
    R2 -
     (|={E1,E2}=>  n : nat, x ↦ᵢ #n  R1 n 
17 18 19
       (( (m: nat), x ↦ᵢ #m  R1 m) ={E2,E1}= True) 
        ( m, x ↦ᵢ #(S m)  R1 m - R2 -
            {E2,E1;Δ;Γ}  fill K #m log t : τ))
Dan Frumin's avatar
Dan Frumin committed
20 21 22 23 24 25 26 27 28 29 30 31 32
    - ({E1;Δ;Γ}  fill K (FAI #x) log t : τ).
  Proof.
    iIntros "HR2 #H".
    iLöb as "IH".
    rewrite {2}/FAI. unlock; simpl.
    rel_rec_l.
    iPoseProof "H" as "H2". (* iMod later on destroys H *)
    rel_load_l_atomic.
    iMod "H" as (n) "[Hx [HR Hrev]]".
    iModIntro. iRename "H2" into "H".
    iExists #n. iFrame. iNext. iIntros "Hx".
    iDestruct "Hrev" as "[Hrev _]".
    iMod ("Hrev" with "[HR Hx]") as "_".
33
    { iExists _. by iFrame. }
Dan Frumin's avatar
Dan Frumin committed
34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49
    rel_rec_l. rel_op_l.
    rel_cas_l_atomic.
    iMod "H" as (n') "[Hx [HR HQ]]". iModIntro.
    iExists #n'. iFrame.
    destruct (decide (n = n')); subst.
    - iSplitR; eauto. { iDestruct 1 as %Hfoo. exfalso. done. }
      iIntros "_ !> Hx". simpl.
      iDestruct "HQ" as "[_ HQ]".
      iSpecialize ("HQ" with "[Hx HR]"). { iFrame. }
      rel_if_l. by iApply "HQ".
    - iSplitL; eauto; last first.
      { iDestruct 1 as %Hfoo. exfalso. simplify_eq. }
      iIntros "_ !> Hx". simpl.
      rel_if_l.
      iDestruct "HQ" as "[HQ _]".
      iMod ("HQ" with "[Hx HR]") as "_".
50
      { iExists _. by iFrame. }
Dan Frumin's avatar
Dan Frumin committed
51 52 53 54 55
      unlock FAI.
      by iApply "IH".
  Qed.

End contents.