proof_treiber.v

From iris.base_logic.lib Require Import invariants ghost_var.
From smr.program_logic Require Import atomic.
From smr.lang Require Import proofmode notation.
From iris.prelude Require Import options.

From smr Require Import helpers no_recl.spec_stack no_recl.code_treiber.

Class treiberG Σ := TreiberG {
  #[local] treiber_ghost_varG :: ghost_varG Σ (list val);
}.

Definition treiberΣ : gFunctors := #[ghost_varΣ (list val)].

Global Instance subG_treiberΣ {Σ} :
  subG treiberΣ Σ → treiberG Σ.
Proof. solve_inG. Qed.

Section treiber_stack.
Context `{!heapGS Σ, !treiberG Σ}.
Notation iProp := (iProp Σ).
Context (treiberN : namespace).

Ltac exfr := repeat (repeat iExists _; iFrame "∗#%").

Fixpoint phys_list (lopt : option loc) (xs : list val) : iProp :=
  match (lopt, xs) with
  | (None  , []     ) => True
  | (None  , _ :: _ ) => False
  | (Some _, []     ) => False
  | (Some l, x :: xs) => ∃ n,
      l ↦∗□ [ x; #(oloc_to_lit n) ] ∗
      phys_list n xs
  end.

(* Ownership of the stack *)
Definition TStack (γ : gname) (xs : list val) : iProp :=
  ghost_var γ (1/2)%Qp xs.

Global Instance TStack_Timeless γ xs: Timeless (TStack γ xs).
Proof. apply _. Qed.

Definition TStackInternalInv (st : loc) (γs : gname) : iProp :=
  ∃ (h : option loc) (xs : list val),
    phys_list h xs ∗ (st +ₗ head) ↦ #(oloc_to_lit h) ∗ ghost_var γs (1/2)%Qp xs.

(* Persistent assertions about the stack *)
Definition IsTStack (γ : gname) (st : loc) : iProp :=
    inv treiberN (TStackInternalInv st γ).

Global Instance IsTStack_Persistent γ l : Persistent (IsTStack γ l).
Proof. apply _. Qed.

(** * Automation hints for [eauto] ******************************************)
Local Hint Extern 0 (environments.envs_entails _
  (TStack _ _ [])) => iExists None : core.

Local Hint Extern 0 (environments.envs_entails _
  (TStack _ _ (_ :: _))) => iExists (Some _) : core.

Local Hint Extern 10 (environments.envs_entails _
  (TStack _ _ _)) => unfold TStack : core.

Local Hint Extern 0 (environments.envs_entails _
  (phys_list _ None [])) => simpl : core.

Local Hint Extern 0 (environments.envs_entails _
  (phys_list _ (Some _) (_ :: _))) => simpl : core.

Local Hint Extern 0 (environments.envs_entails _
  (IsTStack _ _)) => iExists _ : core.

Lemma tstack_new_spec :
  stack_new_spec' treiberN tstack_new TStack IsTStack.
Proof.
  iIntros (Φ) "!> _ HΦ".
  wp_lam. wp_alloc st as "st↦" "†st". wp_pures.
  rewrite array_singleton Loc.add_0. wp_store.
  iMod (ghost_var_alloc []) as (γs) "[γs γs_I]".
  iAssert (TStack γs []) with "γs_I" as "S".
  iMod (inv_alloc treiberN _ (TStackInternalInv st γs) with "[-HΦ S]") as "#Inv".
  { iNext. iExists None, []. rewrite Loc.add_0. iFrame "∗#". }
  iApply "HΦ". by iFrame "∗#%".
Qed.

Lemma tstack_push_spec :
  stack_push_spec' treiberN tstack_push TStack IsTStack.
Proof.
  iIntros (γ st x).
  iDestruct 1 as "#Inv".
  iIntros (Φ) "AU".

  wp_lam. wp_alloc new as "new↦" "†new". wp_pures.
  wp_apply (wp_store_offset with "new↦") as "new↦"; [by simplify_list_eq|]. wp_pures.
  move: #0 => next.

  iLöb as "IH" forall (next).
  wp_rec. wp_pures. wp_bind (! _)%E.

  (* Open inv to load head from st. *)
  iInv "Inv" as (h1 xs1) "[Nodes >(st.h↦ & γs)]".
  wp_load.
  (* close inv *)
  iModIntro. iSplitL "Nodes st.h↦ γs"; first by exfr.

  wp_pures.
  wp_apply (wp_store_offset with "new↦") as "new↦"; [by simplify_list_eq|]. wp_pures.

  wp_bind (CmpXchg _ _ _).
  iInv "Inv" as (h2 xs2) "[Nodes >(st.h↦ & γs)]".
  case (decide (h2 = h1)) as [->|NE].
  - (* successful CAS; commit push *) iClear "IH".
    iMod (array_persist with "new↦") as "new↦".
    wp_cmpxchg_suc.
    iAssert (phys_list (Some (Loc.blk_to_loc new)) (x::xs2)) with "[new↦ Nodes]" as "Nodes'"; first by exfr.

    iMod "AU" as (?) "[γs' [_ Commit]]".

    iDestruct (ghost_var_agree with "γs γs'") as %<-.
    iMod (ghost_var_update_halves (x :: xs2) with "γs γs'") as "[γs γs']".

    iMod ("Commit" with "γs'") as "HΦ".
    (* close inv *)
    iModIntro. iSplitL "Nodes' st.h↦ γs"; first by exfr.
    wp_pures. by iApply "HΦ".

  - (* failed CAS; restore AU *)
    wp_cmpxchg_fail.
    (* close inv *)
    iModIntro. iSplitL "Nodes st.h↦ γs"; first by exfr.
    wp_pure. wp_if. wp_apply ("IH" with "AU †new new↦").
Qed.

Lemma tstack_pop_spec :
  stack_pop_spec' treiberN tstack_pop TStack IsTStack.
Proof using All.
  iIntros (γ st) "#Inv".
  iIntros (Φ) "AU".

  iLöb as "IH".
  wp_rec. wp_pures. wp_bind (! _)%E.

  (* If the validation read is null, commit empty pop. Otherwise, restore AU. *)
  iInv "Inv" as (h1 xs1) "[Nodes >(st.h↦ & γs)]".
  wp_load.
  destruct h1 as [h1|], xs1 as [|x1 xs1']; simpl;
  try done; last first.
  { iClear "IH".
    iMod "AU" as (xs1') "[γs' [_ Commit]]".
    iDestruct (ghost_var_agree with "γs γs'") as %<-.
    iMod ("Commit" with "γs'") as "HΦ".
    (* close inv *)
    iModIntro. iSplitL "Nodes st.h↦ γs"; first by (iExists None,[]; exfr).
    wp_pures.
    iApply "HΦ".
  }

  (* prove for non-empty stack case and restore AU *)
  iDestruct "Nodes" as (n1) "(#h↦ & Nodes)".
  (* close inv *) iModIntro.
  iSplitL "Nodes st.h↦ γs".
  { iExists (Some h1), _. iFrame. repeat iExists _. iFrame "∗#%". }

  wp_pures.

  wp_apply (wp_load_offset with "h↦") as "_"; [by simplify_list_eq|].

  wp_pures. wp_bind (CmpXchg _ _ _).
  iInv "Inv" as (h2 xs2) "[Nodes >(st.h↦ & γs)]".
  case (decide (h2 = Some h1)) as [->|NE].
  - (* successful CAS; commit pop *) iClear "IH".
    destruct xs2 as [|x2 xs2']; [iMod "Nodes"; done|]. simpl.
    iDestruct "Nodes" as (n2) "(#h'↦ & Nodes')".
    wp_cmpxchg_suc.
    iDestruct (array_agree with "h↦ h'↦") as %[= <- <-]; [done|].
    iMod "AU" as (xs2) "[γs' [_ Commit]]".

    iDestruct (ghost_var_agree with "γs γs'") as %<-.
    iMod (ghost_var_update_halves (xs2') with "γs γs'") as "[γs γs']".
    iMod ("Commit" with "γs'") as "HΦ".

    iModIntro. iSplitL "Nodes' st.h↦ γs"; first by exfr. wp_pures.

    wp_apply (wp_load_offset with "h↦") as "_"; [by simplify_list_eq|].

    wp_pures. iApply "HΦ".

  - (* failed CAS; restore AU *)
    wp_cmpxchg_fail.
    iModIntro. iSplitL "Nodes st.h↦ γs"; first by exfr.
    wp_pure. wp_if. wp_apply ("IH" with "AU").
Qed.

#[export] Typeclasses Opaque TStack IsTStack.

End treiber_stack.