Skip to content

GitLab

Verified Commit abd82a39 authored by Rodolphe Lepigre's avatar Rodolphe Lepigre
Browse files
Options

Add a copy of my Treiber stack example.

parent 36f0e548
Hide whitespace changes
Inline Side-by-side
Showing with 368 additions and 0 deletions
_CoqProject
View file @ abd82a39
......@@ -87,6 +87,7 @@ theories/hocap/concurrent_runners.v
theories/hocap/parfib.v
theories/logatom/treiber.v
theories/logatom/treiber2.v
theories/logatom/elimination_stack/hocap_spec.v
theories/logatom/elimination_stack/stack.v
theories/logatom/elimination_stack/spec.v
......
theories/logatom/treiber2.v 0 → 100644
View file @ abd82a39
(****************************************************************************)
(* 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.
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment