From abd82a3941970ceb2ab465a20f02d1fb15c5b852 Mon Sep 17 00:00:00 2001 From: Rodolphe Lepigre Date: Wed, 6 Mar 2019 14:07:11 +0100 Subject: [PATCH] Add a copy of my Treiber stack example. --- _CoqProject | 1 + theories/logatom/treiber2.v | 367 ++++++++++++++++++++++++++++++++++++ 2 files changed, 368 insertions(+) create mode 100644 theories/logatom/treiber2.v diff --git a/_CoqProject b/_CoqProject index 9b356ba..1d58c5e 100644 --- a/_CoqProject +++ b/_CoqProject @@ -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 diff --git a/theories/logatom/treiber2.v b/theories/logatom/treiber2.v new file mode 100644 index 0000000..156d5ca --- /dev/null +++ b/theories/logatom/treiber2.v @@ -0,0 +1,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. -- GitLab