treiber2.v 17.3 KB
Newer Older
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 105 106 107 108 109 110 111 112 113 114 115 116 117 118 119 120 121 122 123 124 125 126 127 128 129 130 131 132 133 134 135 136 137 138 139 140 141 142 143 144 145 146 147 148 149 150 151 152 153 154 155 156 157 158 159 160 161 162 163 164 165 166 167 168 169 170 171 172 173 174 175 176 177 178 179 180 181 182 183 184 185 186 187 188 189 190 191 192 193 194 195 196 197 198 199 200 201 202 203 204 205 206 207 208 209 210 211 212 213 214 215 216 217 218 219 220 221 222 223 224 225 226 227 228 229 230 231 232 233 234 235 236 237 238 239 240 241 242 243 244 245 246 247 248 249 250 251 252 253 254 255 256 257 258 259 260 261 262 263 264 265 266 267 268 269 270 271 272 273 274 275 276 277 278 279 280 281 282 283 284 285 286 287 288 289 290 291 292 293 294 295 296 297 298 299 300 301 302 303 304 305 306 307 308 309 310 311 312 313 314 315 316 317 318 319 320 321 322 323 324 325 326 327 328 329 330 331 332 333 334 335 336 337 338 339 340 341 342 343 344 345 346 347 348 349 350 351 352 353 354 355 356 357 358 359 360 361 362 363 364 365 366 367
(****************************************************************************)
(*      Logically atomic specification of the Treiber stack algorithm       *)
(*                                                                          *)
(*         by Rodolphe Lepigre (with a lot of help from Ralf Jung)          *)
(*          see https://gitlab.mpi-sws.org/lepigre/treiber_stack            *)
(****************************************************************************)

From iris.program_logic Require Import atomic.
From iris.base_logic.lib Require Import invariants.
From iris.heap_lang Require Import proofmode notation.
From iris.algebra Require Import excl auth list.


(** * Definition of the functions *******************************************)

(** A stack is (physically) represented as a pointer to a linked list. When we
    create a new stack, it initially points to an empty list. And there is, of
    course, no potential race condition here since only the current thread can
    now the value of the freshly allocated pointer. *)
Definition new_stack : val :=
  λ: <>, ref NONEV.

(** To push an element on a stack we remember the old head of the pointed list
    list, create a new cell containing both the element and the old head,  and
    then we perform a CAS (Compare And Set). We thus (atomically) test whether
    the stack still points to the old head, and if that is indeed the case, we
    simultaneously set the stack to point to the newly created cell. Note that
    if the CAS was successful, then the element has been added to the list. If
    it failed, we start over from scratch with a recursive call. *)
Definition push_stack : val :=
  rec: "push" "elt" "stack" :=
    let: "old_head" := !"stack" in
    let: "cell" := ("elt", "old_head") in
    if: CAS "stack" "old_head" (SOME (ref "cell")) then #()
    else "push" "elt" "stack".

(** To pop an element from the stack, we first remember the head of the linked
    list, and then we match on its value. If it is the end of the list (NONE),
    then the function returns NONE. If the list is non-empty, we load the cell
    containing both: the head element and the pointer to the tail of the list.
    We then perform a CAS: if the stack still points to the (previous) head of
    the list, then we set it to point to the tail. If the CAS is successful we
    return the element (wrapped in a SOME). Otherwise we start over. Note that
    in the case where the pointed list is empty the linearization point occurs
    on the first access to the stack. Otherwise it occurs at the CAS. *)
Definition pop_stack : val :=
  rec: "pop" "stack" :=
    let: "old_top" := !"stack" in
    match: "old_top" with
      NONE     => NONE
    | SOME "p" =>
       let: "cell" := !"p" in
       if: CAS "stack" "old_top" (Snd "cell") then SOME (Fst "cell")
       else "pop" "stack"
    end.


(** * Definition of the required camera *************************************)

Class stackG Σ := StackG {
  stack_tokG :> inG Σ (authR (optionUR (exclR (listC valC)))) }.

Definition stackΣ : gFunctors :=
  #[GFunctor (authR (optionUR (exclR (listC valC))))].

Instance subG_stackΣ {Σ} : subG stackΣ Σ  stackG Σ.
Proof. solve_inG. Qed.

(* Put some things in the context. *)
Section treiber_stack.
Context `{!heapG Σ, !stackG Σ}.
Context (N : namespace).
Notation iProp := (iProp Σ).


(** * Representation relations and invariant used in the specification ******)

(** Utility function injecting (optional) locations into values. *)
Definition to_val (lopt : option loc) : val :=
  match lopt with
  | None   => NONEV
  | Some  => SOMEV #
  end%I.

(** Representation relation for lists: the (optional) location [lopt] (in fact
    [to_val lopt]) physically represents the (Coq) list [xs]. *)
Fixpoint phys_list (lopt : option loc) (xs : list val) : iProp :=
  match (lopt, xs) with
  | (None  , []     ) => True
  | (None  , _ :: _ ) => False
  | (Some _, []     ) => False
  | (Some , x :: xs) => r q,  {q} (x, to_val r)  phys_list r xs
  end%I.

(** Representation relation for stacks: the location [ℓ] physically represents
    a stack whose elements are those of [xs]. More precisely, [ℓ] is a pointer
    to a linked list, representing [xs]. *)
Definition phys_stack ( : loc) (xs : list val) : iProp :=
  ( r,   to_val r  phys_list r xs)%I.

(** Statement of the invariant maintained for a stack pointed to by (location)
    [ℓ], and uniquely identified by the global name [γ]. Intuitively, there is
    a coq list [xs] such that [ℓ] physically represents [xs], and the value of
    [xs] is stored in ghost state whose authoritative  part  is  (exclusively)
    owned by the invariants.  This always keeps the ghost state in  sync  with
    the physical state, meaning that the ownership of a fragment [own γ (◯ _)]
    actually becomes meaningful to make statements about the list because both
    are tied together by this invariant. *)
Definition stack_inv ( : loc) (γ : gname) : iProp :=
  ( xs, phys_stack  xs  own γ ( (Some ((Excl xs)))))%I.

(** Invariant assertion for a stack pointed to by [ℓ], and uniquely identified
    by the global name [γ].  Note that the namespace [N] is quantified over in
    the whole section. It can thus be instantiated to fit any particular need,
    when using this module as a library. *)
Definition is_stack ( : loc) (γ : gname) : iProp :=
  inv N (stack_inv  γ).

(** Local view of the contents [xs] of the stack that is (uniquely) identified
    by the global name [γ]. Note that this proposition is independent from the
    particular location at which the stack is stored,  which can only be owned
    by one particular thread at a time. *)
Definition stack_cont (γ : gname) (xs : list val) : iProp :=
  (own γ ( (Some ((Excl xs)))))%I.


(** * Useful lemmas and typeclass instances *********************************)

(** Injectivity of [to_val]. *)
Instance to_val_inj : Inj (=) (=) to_val.
Proof.
  intros l1 l2 H. case l1, l2; try done. inversion H. reflexivity.
Qed.

(** Duplicability of the [phys_list] relation. *)
Lemma phys_list_dup l xs : phys_list l xs - phys_list l xs  phys_list l xs.
Proof.
  iInduction xs as [|x xs] "IH" forall (l); destruct l as [l|]; try done.
  simpl. iIntros "H".
  iDestruct "H" as (r q) "[[Hl1 Hl2] HPhys]".
  iDestruct ("IH" with "HPhys") as "[HPhys1 HPhys2]".
  iSplitL "Hl1 HPhys1"; eauto with iFrame.
Qed.

(** Timelessness of the [phys_list] relation. *)
Global Instance phys_list_timeless l xs : Timeless (phys_list l xs).
Proof.
  revert l. induction xs; apply _.
Qed.

(** The following two lemmas have been borrowed from the POPL 18 Iris tutorial
    (see https://gitlab.mpi-sws.org/iris/tutorial-popl18). *)

(** The view of the authority agrees with the local view. *)
Lemma auth_agree γ xs ys :
  own γ ( (Excl' xs)) - own γ ( (Excl' ys)) - xs = ys.
Proof.
  iIntros "Hγ● Hγ◯". by iDestruct (own_valid_2 with "Hγ● Hγ◯")
    as %[<-%Excl_included%leibniz_equiv _]%auth_valid_discrete_2.
Qed.

(** The view of the authority can be updated together with the local view. *)
Lemma auth_update γ ys xs1 xs2 :
  own γ ( (Excl' xs1)) - own γ ( (Excl' xs2)) ==
    own γ ( (Excl' ys))  own γ ( (Excl' ys)).
Proof.
  iIntros "Hγ● Hγ◯".
  iMod (own_update_2 _ _ _ ( Excl' ys   Excl' ys)
    with "Hγ● Hγ◯") as "[$$]".
  { by apply auth_update, option_local_update, exclusive_local_update. }
  done.
Qed.


(** * Automation hints for [eauto] ******************************************)

(** The following hints allow [eauto] to work with the above definitions. When
    a simple goal involving only framing and the instantiation of existentials
    is encoutered, we can usually conclude with [eauto with iFrame]. The hints
    are mainly useful for unfolding definitions and instantiating existentials
    with a reasonable choice of head constructor. *)

Local Hint Extern 0 (environments.envs_entails _
  (phys_stack _ [])) => iExists None.

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

Local Hint Extern 10 (environments.envs_entails _
  (phys_stack _ _)) => unfold phys_stack.

Local Hint Extern 0 (environments.envs_entails _
  (stack_inv _ _)) => unfold stack_inv.

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

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


(** * Specification *********************************************************)

(** The specification of [new_stack] is straightforward: with no precondition,
    the creation of a new stack yields a location that is pointing to a stack,
    and it is initially empty. The only interesting thing to note here is that
    an existential quantifier is used in the postcondition to obtain a (fresh)
    name [γ] for the created stack. This ensures that different stacks will be
    given different names. *)
Lemma new_stack_spec :
  {{{ True }}}
    new_stack #()
  {{{  γ, RET #; is_stack  γ  stack_cont γ [] }}}.
Proof.
  (* Introduce things into the Coq and Iris contexts. Throw away the [True]
     precondition. *)
  iIntros (Φ) "_ HΦ".
  (* We introduce the fancy update modality in our WP (necessary later). *)
  iApply wp_fupd.
  (* We step through the program: β-reduce and allocate a location [ℓ]. *)
  wp_lam. wp_alloc  as "Hl". (* We have full ownership of [ℓ] in [Hl]. *)
  (* We now need to establish the invariant. First, we allocate an instance of
     our camera named [γ], containing the empty list. This step (and the next)
     requires the fancy update modality that was introduced earlier. *)
  iMod (own_alloc ( (Some (Excl []))   (Some (Excl []))))
    as (γ) "[Hγ● Hγ◯]"; (* Validity is trivial. *) first done.
  (* We can then allocate the invariant (with mask [N]).  Note that we can use
     [eauto 10 with iFrame] to prove [▷ stack_inv ℓ γ]. *) 
  iMod (inv_alloc N _ (stack_inv  γ) with "[Hl Hγ●]")
    as "#Inv"; first eauto 10 with iFrame.
  (* We can now eliminate the modality and establish the postcondition. *)
  iModIntro. iApply "HΦ". eauto with iFrame.
Qed.

(** The specification of [push_stack] depends on a location [ℓ] and a name [γ]
    assumed to correspond to a stack (created using [new_stack]),  and a value
    [v] that is being pushed. A logically atomic Hoare triple is used in order
    to ensure linearizability (i.e., the existence of a linearization point in
    the execution of the push operation). As a consequence the precondition of
    the triple can only be accessed during a physically atomic operation,  and
    the knowledge gained must then either be forgotten (abort operation) or it
    should lead to a one shot update (commit operation) during the same atomic
    operation where the precondition was accessed. In this second case we lose
    the possibility of accessing the precondition again, unlike with abort. *)
Lemma push_stack_spec ( : loc) (γ : gname) (v : val) :
  is_stack  γ -
  <<<  (xs : list val), stack_cont γ xs >>>
    push_stack v # @   N
  <<< stack_cont γ (v :: xs) , RET #() >>>.
Proof.
  (* Introduce things into the Coq and Iris contexts, and use induction. *)
  iIntros "#HInv" (Φ) "AU". iLöb as "IH".
  (* Evaluate the first steps of the program, and focus on the load. *)
  wp_lam. wp_let. wp_bind (! _)%E.
  (* Since an atomic operation is in focus we can access the invariant. Hence,
     we will be able to learn that [ℓ] actually points to something. *)
  iInv "HInv" as (xs) ">[HPhys Hγ●]".
  unfold phys_stack. iDestruct "HPhys" as (w) "[Hl HPhys]".
  (* We can now perform the load, and get rid of the modality. *)
  wp_load. iModIntro. iSplitL "Hl Hγ● HPhys"; first by eauto 10 with iFrame.
  (* We then resume stepping through the program, and focus on the CAS. *)
  wp_alloc r as "Hr". wp_inj. wp_bind (CAS _ _ _)%E.
  (* Now, we need to use the invariant again to gain information on [ℓ]. *)
  iInv "HInv" as (ys) ">[HPhys Hγ●]". iDestruct "HPhys" as (u) "[Hl HPhys]".
  (* We now reason by case on the success/failure of the CAS. *)
  destruct (decide (u = w)) as [[= ->]|NE].
  - (* The CAS succeeded. *)
    wp_cas_suc. { case w; done. (* Administrative stuff. *) }
    (* This was the linearization point. We access the preconditon. *)
    iMod "AU" as (zs) "[Hγ◯ [_ HClose]]".
    (* Use agreement on ressource [γ] to learn [zs = ys]. *)
    iDestruct (auth_agree with "Hγ● Hγ◯") as %->.
    (* Update the value of [γ] to [v::zs]. *)
    iMod (auth_update γ (v::zs) with "Hγ● Hγ◯") as "[Hγ● Hγ◯]".
    (* Commit operation. *)
    iMod ("HClose" with "Hγ◯") as "H".
    (* We can eliminate the modality. *)
    iModIntro. iSplitR "H"; first by eauto 10 with iFrame.
    (* And conclude the proof easily, after some computation steps. *)
    wp_if. iExact "H".
  - (* The CAS failed. *)
    wp_cas_fail. { eapply not_inj. done. }
    { case u, w; simpl; eauto. (* Administrative stuff. *) }
    (* We can eliminate the modality. *)
    iModIntro. iSplitL "Hγ● Hl HPhys"; first by eauto 10 with iFrame.
    (* And conclude the proof by induction hypothesis. *)
    wp_if. iApply "IH". iExact "AU".
Qed.

(** As for [push_stack] the specification of [pop_stack] depends on a location
    [ℓ] and a name [γ] (corresponding to some stack). A logically atomic Hoare
    triple is again used to ensure linearizability, but it must be accessed in
    a slightly more complicated way. In particular, the linearization point is
    not in the same place depending on the emptiness of the stack.  Of course,
    the postcondition also depends on the emptiness of the stack. *)
Lemma pop_stack_spec ( : loc) (γ : gname) :
  is_stack  γ -
  <<<  (xs : list val), stack_cont γ xs >>>
    pop_stack # @   N
  <<< stack_cont γ (match xs with [] => [] | _::xs => xs end)
    , RET (match xs with [] => NONEV | v::_ => SOMEV v end) >>>.
Proof.
  (* As for [push_stack], we need to use induction and the focus on a load. *)
  iIntros "#HInv" (Φ) "AU". iLöb as "IH". wp_lam. wp_bind (! _)%E.
  (* We can then use the invariant to be able to perform the load. *)
  iInv "HInv" as (xs) ">[HPhys Hγ●]".
  iDestruct "HPhys" as (w) "[Hl HPhys]". wp_load.
  (* We now duplicate [phys_list w xs] as we will need two copies. *)
  iDestruct (phys_list_dup with "HPhys") as "[HPhys1 HPhys2]".
  (* We then inspect the contents of the stack and the optional location. They
     must agree, otherwise the proof is trivial. *)
  destruct w as [w|], xs as [|x xs]; try done; simpl.
  - (* The stack is non-empty, we eliminate the modality. *)
    iModIntro. iSplitL "Hl Hγ● HPhys1"; first by eauto 10 with iFrame.
    (* We continue stepping through the program, and focus on the CAS. *)
    wp_let. wp_match. iDestruct "HPhys2" as (r q) "[Hw HP]".
    wp_load. wp_let. wp_proj. wp_bind (CAS _ _ _)%E.
    (* We need to use the invariant again to gain information on [ℓ]. *)
    iInv "HInv" as (ys) ">[H Hγ●]".
    unfold phys_stack. iDestruct "H" as (u) "[Hl HPhys]".
    (* We get rid of useless hypotheses to cleanup the context. *)
    iClear "HP". clear xs.
    (* We reason by case on the success/failure of the CAS. *)
    destruct (decide (u = Some w)) as [[= ->]|Hx].
    * (* The CAS succeeded, so this is the linearization point. *)
      wp_cas_suc; first done.
      (* The list [ys] must be non-empty, otherwise the proof is trivial. *)
      destruct ys; first done.
      (* We access the precondition, prior to performing an update. *)
      iMod "AU" as (zs) "[Hγ◯ [_ HClose]]". unfold stack_cont.
      (* Use agreement on ressource [γ] to learn [v :: ys = zs]. *)
      iDestruct (auth_agree with "Hγ● Hγ◯") as %<-.
      (* Update the value of [γ] to [ys] (the tail of previous value). *)
      iMod (auth_update γ ys with "Hγ● Hγ◯") as "[Hγ● Hγ◯]".
      (* We need to learn that [r = u] (true since mapsto must agree). *)
      iDestruct "HPhys" as (u q') "[Hw' HPhys]".
      iDestruct (mapsto_agree with "Hw Hw'") as %[=-> ->%to_val_inj].
      (* Perform the commit. *)
      iMod ("HClose" with "Hγ◯") as "HΦ".
      (* Eliminate the modality. *)
      iModIntro. iSplitR "HΦ"; first by eauto 10 with iFrame.
      (* And conclude the proof. *)
      wp_if. wp_proj. wp_inj. iExact "HΦ".
    * (* The CAS failed. *)
      wp_cas_fail. { intro H. apply Hx. destruct u; inversion H; done. }
      (* We can eliminate the modality. *)
      iModIntro. iSplitR "AU"; first by eauto 10 with iFrame.
      (* And conclude the proof using the induction hypothesis. *)
      wp_if. iApply "IH". iExact "AU".
  - (* The stack is empty, the load was the linearization point,  we can hence
       commit (without updating the stack). So we access the precondition. *)
    iClear "HPhys1 HPhys2". iMod "AU" as (xs) "[Hγ◯ [_ HClose]]".
    (* Thanks to agreement, we learn that [xs] must be the empty list. *)
    iDestruct (auth_agree with "Hγ● Hγ◯") as %<-.
    (* And we can commit (we are still at the linearization point). *)
    iMod ("HClose" with "Hγ◯") as "HΦ".
    (* We finally eliminate the modality and conclude the proof by taking some
       computation steps, and using our hypothesis. *)
    iModIntro. iSplitR "HΦ"; first by eauto 10 with iFrame.
    wp_let. wp_match. wp_inj. iExact "HΦ".
Qed.

End treiber_stack.

(** Make the exported Iris terms "Typeclass Opaque", so that clients using the
    library won't look into these definitions. *)
Typeclasses Opaque is_stack stack_cont.