Commit 6f093ff9 authored by Ralf Jung's avatar Ralf Jung

Merge branch 'master' of https://gitlab.mpi-sws.org/FP/iris-coq

parents a5c777d9 ee6df099
Pipeline #3252 failed with stage
in 1 minute and 28 seconds
......@@ -5,7 +5,7 @@ Import uPred.
(* Non-atomic ("thread-local") invariants. *)
Definition thread_id := gname.
Definition na_inv_pool_name := gname.
Class na_invG Σ :=
tl_inG :> inG Σ (prodR coPset_disjR (gset_disjR positive)).
......@@ -13,12 +13,12 @@ Class na_invG Σ :=
Section defs.
Context `{invG Σ, na_invG Σ}.
Definition na_own (tid : thread_id) (E : coPset) : iProp Σ :=
own tid (CoPset E, ).
Definition na_own (p : na_inv_pool_name) (E : coPset) : iProp Σ :=
own p (CoPset E, ).
Definition na_inv (tid : thread_id) (N : namespace) (P : iProp Σ) : iProp Σ :=
Definition na_inv (p : na_inv_pool_name) (N : namespace) (P : iProp Σ) : iProp Σ :=
( i, i N
inv N (P own tid (, GSet {[i]}) na_own tid {[i]}))%I.
inv N (P own p (, GSet {[i]}) na_own p {[i]}))%I.
End defs.
Instance: Params (@na_inv) 3.
......@@ -27,36 +27,36 @@ Typeclasses Opaque na_own na_inv.
Section proofs.
Context `{invG Σ, na_invG Σ}.
Global Instance na_own_timeless tid E : TimelessP (na_own tid E).
Global Instance na_own_timeless p E : TimelessP (na_own p E).
Proof. rewrite /na_own; apply _. Qed.
Global Instance na_inv_ne tid N n : Proper (dist n ==> dist n) (na_inv tid N).
Global Instance na_inv_ne p N n : Proper (dist n ==> dist n) (na_inv p N).
Proof. rewrite /na_inv. solve_proper. Qed.
Global Instance na_inv_proper tid N : Proper (() ==> ()) (na_inv tid N).
Global Instance na_inv_proper p N : Proper (() ==> ()) (na_inv p N).
Proof. apply (ne_proper _). Qed.
Global Instance na_inv_persistent tid N P : PersistentP (na_inv tid N P).
Global Instance na_inv_persistent p N P : PersistentP (na_inv p N P).
Proof. rewrite /na_inv; apply _. Qed.
Lemma na_alloc : (|==> tid, na_own tid )%I.
Lemma na_alloc : (|==> p, na_own p )%I.
Proof. by apply own_alloc. Qed.
Lemma na_own_disjoint tid E1 E2 : na_own tid E1 - na_own tid E2 - E1 E2.
Lemma na_own_disjoint p E1 E2 : na_own p E1 - na_own p E2 - E1 E2.
Proof.
apply wand_intro_r.
rewrite /na_own -own_op own_valid -coPset_disj_valid_op. by iIntros ([? _]).
Qed.
Lemma na_own_union tid E1 E2 :
E1 E2 na_own tid (E1 E2) na_own tid E1 na_own tid E2.
Lemma na_own_union p E1 E2 :
E1 E2 na_own p (E1 E2) na_own p E1 na_own p E2.
Proof.
intros ?. by rewrite /na_own -own_op pair_op left_id coPset_disj_union.
Qed.
Lemma na_inv_alloc tid E N P : P ={E}= na_inv tid N P.
Lemma na_inv_alloc p E N P : P ={E}= na_inv p N P.
Proof.
iIntros "HP".
iMod (own_empty (prodUR coPset_disjUR (gset_disjUR positive)) tid) as "Hempty".
iMod (own_empty (prodUR coPset_disjUR (gset_disjUR positive)) p) as "Hempty".
iMod (own_updateP with "Hempty") as ([m1 m2]) "[Hm Hown]".
{ apply prod_updateP'. apply cmra_updateP_id, (reflexivity (R:=eq)).
apply (gset_disj_alloc_empty_updateP_strong' (λ i, i N)).
......@@ -71,14 +71,14 @@ Section proofs.
iNext. iLeft. by iFrame.
Qed.
Lemma na_inv_open tid E F N P :
Lemma na_inv_open p E F N P :
N E N F
na_inv tid N P - na_own tid F ={E}= P na_own tid (F∖↑N)
( P na_own tid (F∖↑N) ={E}= na_own tid F).
na_inv p N P - na_own p F ={E}= P na_own p (F∖↑N)
( P na_own p (F∖↑N) ={E}= na_own p F).
Proof.
rewrite /na_inv. iIntros (??) "#Htlinv Htoks".
iDestruct "Htlinv" as (i) "[% Hinv]".
rewrite [F as X in na_own tid X](union_difference_L (N) F) //.
rewrite [F as X in na_own p X](union_difference_L (N) F) //.
rewrite [X in (X _)](union_difference_L {[i]} (N)) ?na_own_union; [|set_solver..].
iDestruct "Htoks" as "[[Htoki $] $]".
iInv N as "[[$ >Hdis]|>Htoki2]" "Hclose".
......
\section{Derived constructions}
\subsection{Non-atomic invariants}
\subsection{Non-atomic (``thread-local'') invariants}
Sometimes it is necessary to maintain invariants that we need to open non-atomically.
Clearly, for this mechanism to be sound we need something that prevents us from opening the same invariant twice.
Access to these \emph{non-atomic invariants} is thus guarded by tokens that take the role that masks play for ``normal'', atomic invariants.
One way to think about them is as ``thread-local invariants''.
For every thread, we have a set of \emph{tokens}.
By giving up a token, you can obtain the invariant, and vice versa.
Such invariants can only be opened by their respective thread, and as a consequence they can be kept open around any sequence of expressions (\ie there is no restriction to atomic expressions).
To tie the threads and the tokens together, every thread is assigned a \emph{thread ID}.
Note that these thread IDs are completely fictional, there is no operational aspect to them.
In principle, the tokens could move between threads; that's not an issue at all.
Clearly, for this mechanism to be sound we need something that prevents us from opening the same invariant twice, something like the masks that avoid reentrancy on the ``normal'', atomic invariants.
The idea is to use tokens\footnote{Very much like the tokens that are used to encode ``normal'', atomic invariants} that guard access to non-atomic invariants.
Having the token $\NaTokE\pid\mask$ indicates that we can open all invariants in $\mask$.
The $\pid$ here is the name of the \emph{invariant pool}.
This mechanism allows us to have multiple, independent pools of invariants that all have their own namespaces.
One way to think about non-atomic invariants is as ``thread-local invariants'',
where every pool is a thread.
Every thread thus has its own, independent set of invariants.
Every thread threads through all the tokens for its own pool, so that each invariant can only be opened in the thread it belongs to.
As a consequence, they can be kept open around any sequence of expressions (\ie there is no restriction to atomic expressions) -- after all, there cannot be any races with other threads.
Concretely, this is the monoid structure we need:
\begin{align*}
\textdom{TId} \eqdef{}& \nat \\
\textmon{TTok} \eqdef{}& \textdom{TId} \fpfn \pset{\textdom{InvName}}\\
\textmon{TDis} \eqdef{}& \textdom{TId} \fpfn \finpset{\textdom{InvName}}
\textdom{PId} \eqdef{}& \GName \\
\textmon{NaTok} \eqdef{}& \finpset{\InvName} \times \pset{\InvName}
\end{align*}
For every thread, there is a set of tokens designating which invariants are \emph{enabled} (closed).
For every pool, there is a set of tokens designating which invariants are \emph{enabled} (closed).
This corresponds to the mask of ``normal'' invariants.
We re-use the structure given by namespaces for non-atomic invariants.
Furthermore, there is a \emph{finite} set of invariants that is \emph{disabled} (open).
We assume a global instance $\Gttok$ of \textmon{TTok}, and an instance $\Gtdis$ of $\textmon{TDis}$.
Then we can define some sugar for owning tokens:
Owning tokens is defined as follows:
\begin{align*}
\TTokE\tid\mask \eqdef{}& \ownGhost{\Gttok}{ \mapsingleton\tid\mask : \textmon{TTok} } \\
\TTok\tid \eqdef{}& \TTokE\tid\top
\NaTokE\pid\mask \eqdef{}& \ownGhost{\pid}{ (\emptyset, \mask) } \\
\NaTok\pid \eqdef{}& \NaTokE\pid\top
\end{align*}
Next, we define non-atomic invariants.
To simplify this construction,we piggy-back into ``normal'' invariants.
\begin{align*}
\NaInv\tid\namesp\prop \eqdef{}& \Exists \iname\in\namesp. \knowInv\namesp{\prop * \ownGhost\Gtdis{\set{\iname}} \lor \TTokE\tid{\set{\iname}}}
\NaInv\pid\namesp\prop \eqdef{}& \Exists \iname\in\namesp. \knowInv\namesp{\prop * \ownGhost\pid{(\set{\iname},\emptyset)} \lor \NaTokE\pid{\set{\iname}}}
\end{align*}
We easily obtain:
\begin{mathpar}
\axiom
{\TRUE \vs[\bot] \Exists\tid. \TTok\tid}
{\TRUE \vs[\bot] \Exists\pid. \NaTok\pid}
\axiom
{\TTokE\tid{\mask_1 \uplus \mask_2} \Lra \TTokE\tid{\mask_1} * \TTokE\tid{\mask_2}}
{\NaTokE\pid{\mask_1 \uplus \mask_2} \Lra \NaTokE\pid{\mask_1} * \NaTokE\pid{\mask_2}}
\axiom
{\later\prop \vs[\namesp] \always\NaInv\tid\namesp\prop}
{\later\prop \vs[\namesp] \always\NaInv\pid\namesp\prop}
\axiom
{\NaInv\tid\namesp\prop \proves \Acc[\namesp]{\TTokE\tid\namesp}{\later\prop}}
{\NaInv\pid\namesp\prop \proves \Acc[\namesp]{\NaTokE\pid\namesp}{\later\prop}}
\end{mathpar}
from which we can derive
\begin{mathpar}
\infer
{\namesp \subseteq \mask}
{\NaInv\tid\namesp\prop \proves \Acc[\namesp]{\TTokE\tid\mask}{\later\prop * \TTokE\tid{\mask \setminus \namesp}}}
{\NaInv\pid\namesp\prop \proves \Acc[\namesp]{\NaTokE\pid\mask}{\later\prop * \NaTokE\pid{\mask \setminus \namesp}}}
\end{mathpar}
......
......@@ -339,6 +339,9 @@
\newcommand{\physatomic}[1]{\textlog{atomic}($#1$)}
\newcommand{\infinite}{\textlog{infinite}}
\newcommand\InvName{\textdom{InvName}}
\newcommand\GName{\textdom{GName}}
\newcommand{\Prop}{\textlog{Prop}}
\newcommand{\Pred}{\textlog{Pred}}
......@@ -427,13 +430,11 @@
\newcommand{\mapstoprop}{\mathrel{\kern-0.5ex\tikz[baseline=(m)]{\node at (0,0) (m){}; \draw[line cap=round] (0,0.16) -- (0,-0.004);}\kern-1.5ex\Ra}}
% Non-atomic invariants
\newcommand*\Gttok{\gname_\textrm{TTok}}
\newcommand*\Gtdis{\gname_\textrm{TDis}}
\newcommand*\tid{t}
\newcommand\NaInv[3]{\textlog{NAInv}^{#1.#2}(#3)}
\newcommand*\pid{p}
\newcommand\NaInv[3]{\textlog{NaInv}^{#1.#2}(#3)}
\newcommand*\TTok[1]{{[}\textrm{T}:#1{]}}
\newcommand*\TTokE[2]{{[}\textrm{T}:#1.#2{]}}
\newcommand*\NaTok[1]{{[}\textrm{NaInv}:#1{]}}
\newcommand*\NaTokE[2]{{[}\textrm{NaInv}:#1.#2{]}}
\endinput
......@@ -27,8 +27,8 @@ To instantiate the program logic, the user picks a family of locally contractive
From this, we construct the bifunctor defining the overall resources as follows:
\begin{align*}
\mathcal G \eqdef{}& \nat \\
\textdom{ResF}(\ofe^\op, \ofe) \eqdef{}& \prod_{i \in \mathcal I} \mathcal G \fpfn \iFunc_i(\ofe^\op, \ofe)
\GName \eqdef{}& \nat \\
\textdom{ResF}(\ofe^\op, \ofe) \eqdef{}& \prod_{i \in \mathcal I} \GName \fpfn \iFunc_i(\ofe^\op, \ofe)
\end{align*}
We will motivate both the use of a product and the finite partial function below.
$\textdom{ResF}(\ofe^\op, \ofe)$ is a CMRA by lifting the individual CMRAs pointwise, and it has a unit (using the empty finite partial functions).
......@@ -112,10 +112,10 @@ To this end, we use tokens that manage which invariants are currently enabled.
We assume to have the following four CMRAs available:
\begin{align*}
\mathcal I \eqdef{}& \nat \\
\textmon{Inv} \eqdef{}& \authm(\mathcal I \fpfn \agm(\latert \iPreProp)) \\
\textmon{En} \eqdef{}& \pset{\mathcal I} \\
\textmon{Dis} \eqdef{}& \finpset{\mathcal I} \\
\InvName \eqdef{}& \nat \\
\textmon{Inv} \eqdef{}& \authm(\InvName \fpfn \agm(\latert \iPreProp)) \\
\textmon{En} \eqdef{}& \pset{\InvName} \\
\textmon{Dis} \eqdef{}& \finpset{\InvName} \\
\textmon{State} \eqdef{}& \authm(\maybe{\exm(\State)})
\end{align*}
The last two are the tokens used for managing invariants, $\textmon{Inv}$ is the monoid used to manage the invariants themselves.
......@@ -126,7 +126,7 @@ We assume that at the beginning of the verification, instances named $\gname_{\t
\paragraph{World Satisfaction.}
We can now define the assertion $W$ (\emph{world satisfaction}) which ensures that the enabled invariants are actually maintained:
\begin{align*}
W \eqdef{}& \Exists I : \mathcal I \fpfn \Prop.
W \eqdef{}& \Exists I : \InvName \fpfn \Prop.
\begin{array}[t]{@{} l}
\ownGhost{\gname_{\textmon{Inv}}}{\authfull
\mapComp {\iname}
......@@ -471,8 +471,8 @@ We use the notation $\namesp.\iname$ for the namespace $[\iname] \dplus \namesp$
The elements of a namespaces are \emph{structured invariant names} (think: Java fully qualified class name).
They, too, are lists of $\nat$, the same type as namespaces.
In order to connect this up to the definitions of \Sref{sec:invariants}, we need a way to map structued invariant names to $\mathcal I$, the type of ``plain'' invariant names.
Any injective mapping $\textlog{namesp\_inj}$ will do; and such a mapping has to exist because $\List(\nat)$ is countable and $\mathcal I$ is infinite.
In order to connect this up to the definitions of \Sref{sec:invariants}, we need a way to map structued invariant names to $\InvName$, the type of ``plain'' invariant names.
Any injective mapping $\textlog{namesp\_inj}$ will do; and such a mapping has to exist because $\List(\nat)$ is countable and $\InvName$ is infinite.
Whenever needed, we (usually implicitly) coerce $\namesp$ to its encoded suffix-closure, \ie to the set of encoded structured invariant names contained in the namespace: \[\namecl\namesp \eqdef \setComp{\iname}{\Exists \namesp'. \iname = \textlog{namesp\_inj}(\namesp' \dplus \namesp)}\]
We will overload the notation for invariant assertions for using namespaces instead of names:
......
......@@ -17,15 +17,17 @@ Implicit Types P Q : iProp Σ.
Implicit Types Φ : val iProp Σ.
(** Proof rules for the sugar *)
Lemma wp_lam E x ef e Φ :
is_Some (to_val e) Closed (x :b: []) ef
WP subst' x e ef @ E {{ Φ }} WP App (Lam x ef) e @ E {{ Φ }}.
Lemma wp_lam E x elam e1 e2 Φ :
e1 = Lam x elam
is_Some (to_val e2)
Closed (x :b: []) elam
WP subst' x e2 elam @ E {{ Φ }} WP App e1 e2 @ E {{ Φ }}.
Proof. intros. by rewrite -(wp_rec _ BAnon) //. Qed.
Lemma wp_let E x e1 e2 Φ :
is_Some (to_val e1) Closed (x :b: []) e2
WP subst' x e1 e2 @ E {{ Φ }} WP Let x e1 e2 @ E {{ Φ }}.
Proof. apply wp_lam. Qed.
Proof. by apply wp_lam. Qed.
Lemma wp_seq E e1 e2 Φ :
is_Some (to_val e1) Closed [] e2
......
......@@ -4,13 +4,13 @@ From iris.proofmode Require Import tactics.
From iris.heap_lang Require Import proofmode notation.
Definition assert : val :=
locked (λ: "v", if: "v" #() then #() else #0 #0)%V. (* #0 #0 is unsafe *)
λ: "v", if: "v" #() then #() else #0 #0. (* #0 #0 is unsafe *)
(* just below ;; *)
Notation "'assert:' e" := (assert (λ: <>, e))%E (at level 99) : expr_scope.
Lemma wp_assert `{heapG Σ} E (Φ : val iProp Σ) e `{!Closed [] e} :
WP e @ E {{ v, v = #true Φ #() }} WP assert: e @ E {{ Φ }}.
Proof.
iIntros "HΦ". rewrite /assert -lock. wp_let. wp_seq.
iIntros "HΦ". rewrite /assert. wp_let. wp_seq.
iApply (wp_wand with "HΦ"). iIntros (v) "[% ?]"; subst. by wp_if.
Qed.
From iris.heap_lang Require Export notation.
Definition newbarrier : val := locked (λ: <>, ref #false)%V.
Definition signal : val := locked (λ: "x", "x" <- #true)%V.
Definition newbarrier : val := λ: <>, ref #false.
Definition signal : val := λ: "x", "x" <- #true.
Definition wait : val :=
locked (rec: "wait" "x" := if: !"x" then #() else "wait" "x")%V.
rec: "wait" "x" := if: !"x" then #() else "wait" "x".
......@@ -95,7 +95,7 @@ Lemma newbarrier_spec (P : iProp Σ) :
{{{ heap_ctx }}} newbarrier #() {{{ l, RET #l; recv l P send l P }}}.
Proof.
iIntros (HN Φ) "#? HΦ".
rewrite -wp_fupd /newbarrier -lock /=. wp_seq. wp_alloc l as "Hl".
rewrite -wp_fupd /newbarrier /=. wp_seq. wp_alloc l as "Hl".
iApply ("HΦ" with ">[-]").
iMod (saved_prop_alloc (F:=idCF) P) as (γ) "#?".
iMod (sts_alloc (barrier_inv l P) _ N (State Low {[ γ ]}) with "[-]")
......@@ -119,7 +119,7 @@ Qed.
Lemma signal_spec l P :
{{{ send l P P }}} signal #l {{{ RET #(); True }}}.
Proof.
rewrite /signal /send /barrier_ctx -lock /=.
rewrite /signal /send /barrier_ctx /=.
iIntros (Φ) "(Hs&HP) HΦ"; iDestruct "Hs" as (γ) "[#(%&Hh&Hsts) Hγ]". wp_let.
iMod (sts_openS (barrier_inv l P) _ _ γ with "[Hγ]")
as ([p I]) "(% & [Hl Hr] & Hclose)"; eauto.
......
......@@ -4,12 +4,11 @@ From iris.proofmode Require Import tactics.
From iris.algebra Require Import frac auth.
From iris.heap_lang Require Import proofmode notation.
Definition newcounter : val := locked (λ: <>, ref #0)%V.
Definition incr : val := locked (
rec: "incr" "l" :=
Definition newcounter : val := λ: <>, ref #0.
Definition incr : val := rec: "incr" "l" :=
let: "n" := !"l" in
if: CAS "l" "n" (#1 + "n") then #() else "incr" "l")%V.
Definition read : val := locked (λ: "l", !"l")%V.
if: CAS "l" "n" (#1 + "n") then #() else "incr" "l".
Definition read : val := λ: "l", !"l".
(** Monotone counter *)
Class mcounterG Σ := MCounterG { mcounter_inG :> inG Σ (authR mnatUR) }.
......@@ -36,7 +35,7 @@ Section mono_proof.
heapN N
{{{ heap_ctx }}} newcounter #() {{{ l, RET #l; mcounter l 0 }}}.
Proof.
iIntros (? Φ) "#Hh HΦ". rewrite -wp_fupd /newcounter -lock /=. wp_seq. wp_alloc l as "Hl".
iIntros (? Φ) "#Hh HΦ". rewrite -wp_fupd /newcounter. wp_seq. wp_alloc l as "Hl".
iMod (own_alloc ( (O:mnat) (O:mnat))) as (γ) "[Hγ Hγ']"; first done.
iMod (inv_alloc N _ (mcounter_inv γ l) with "[Hl Hγ]").
{ iNext. iExists 0%nat. by iFrame. }
......@@ -72,7 +71,7 @@ Section mono_proof.
{{{ mcounter l j }}} read #l {{{ i, RET #i; j i%nat mcounter l i }}}.
Proof.
iIntros (ϕ) "Hc HΦ". iDestruct "Hc" as (γ) "(% & #? & #Hinv & Hγf)".
rewrite /read -lock /=. wp_let. iInv N as (c) ">[Hγ Hl]" "Hclose". wp_load.
rewrite /read /=. wp_let. iInv N as (c) ">[Hγ Hl]" "Hclose". wp_load.
iDestruct (own_valid_2 with "Hγ Hγf")
as %[?%mnat_included _]%auth_valid_discrete_2.
iMod (own_update_2 with "Hγ Hγf") as "[Hγ Hγf]".
......@@ -113,7 +112,7 @@ Section contrib_spec.
{{{ heap_ctx }}} newcounter #()
{{{ γ l, RET #l; ccounter_ctx γ l ccounter γ 1 0 }}}.
Proof.
iIntros (? Φ) "#Hh HΦ". rewrite -wp_fupd /newcounter -lock /=. wp_seq. wp_alloc l as "Hl".
iIntros (? Φ) "#Hh HΦ". rewrite -wp_fupd /newcounter /=. wp_seq. wp_alloc l as "Hl".
iMod (own_alloc ( (Some (1%Qp, O%nat)) (Some (1%Qp, 0%nat))))
as (γ) "[Hγ Hγ']"; first done.
iMod (inv_alloc N _ (ccounter_inv γ l) with "[Hl Hγ]").
......@@ -147,7 +146,7 @@ Section contrib_spec.
{{{ c, RET #c; n c%nat ccounter γ q n }}}.
Proof.
iIntros (Φ) "(#(%&?&?) & Hγf) HΦ".
rewrite /read -lock /=. wp_let. iInv N as (c) ">[Hγ Hl]" "Hclose". wp_load.
rewrite /read /=. wp_let. iInv N as (c) ">[Hγ Hl]" "Hclose". wp_load.
iDestruct (own_valid_2 with "Hγ Hγf")
as %[[? ?%nat_included]%Some_pair_included_total_2 _]%auth_valid_discrete_2.
iMod ("Hclose" with "[Hl Hγ]") as "_"; [iNext; iExists c; by iFrame|].
......@@ -159,7 +158,7 @@ Section contrib_spec.
{{{ n, RET #n; ccounter γ 1 n }}}.
Proof.
iIntros (Φ) "(#(%&?&?) & Hγf) HΦ".
rewrite /read -lock /=. wp_let. iInv N as (c) ">[Hγ Hl]" "Hclose". wp_load.
rewrite /read /=. wp_let. iInv N as (c) ">[Hγ Hl]" "Hclose". wp_load.
iDestruct (own_valid_2 with "Hγ Hγf") as %[Hn _]%auth_valid_discrete_2.
apply (Some_included_exclusive _) in Hn as [= ->]%leibniz_equiv; last done.
iMod ("Hclose" with "[Hl Hγ]") as "_"; [iNext; iExists c; by iFrame|].
......
......@@ -5,11 +5,11 @@ Import uPred.
Definition parN : namespace := nroot .@ "par".
Definition par : val :=
locked (λ: "fs",
λ: "fs",
let: "handle" := spawn (Fst "fs") in
let: "v2" := Snd "fs" #() in
let: "v1" := join "handle" in
("v1", "v2"))%V.
("v1", "v2").
Notation "e1 ||| e2" := (par (Pair (λ: <>, e1) (λ: <>, e2)))%E : expr_scope.
Section proof.
......@@ -26,7 +26,7 @@ Lemma par_spec (Ψ1 Ψ2 : val → iProp Σ) e (f1 f2 : val) (Φ : val → iProp
WP par e {{ Φ }}.
Proof.
iIntros (?) "(#Hh&Hf1&Hf2&HΦ)".
rewrite /par -lock. wp_value. wp_let. wp_proj.
rewrite /par. wp_value. wp_let. wp_proj.
wp_apply (spawn_spec parN with "[$Hh $Hf1]"); try wp_done; try solve_ndisj.
iIntros (l) "Hl". wp_let. wp_proj. wp_bind (f2 _).
iApply (wp_wand with "Hf2"); iIntros (v) "H2". wp_let.
......@@ -44,5 +44,3 @@ Proof.
iSplitL "H1"; by wp_let.
Qed.
End proof.
Global Opaque par.
......@@ -5,15 +5,15 @@ From iris.heap_lang Require Import proofmode notation.
From iris.algebra Require Import excl.
Definition spawn : val :=
locked (λ: "f",
λ: "f",
let: "c" := ref NONE in
Fork ("c" <- SOME ("f" #())) ;; "c")%V.
Fork ("c" <- SOME ("f" #())) ;; "c".
Definition join : val :=
locked (rec: "join" "c" :=
rec: "join" "c" :=
match: !"c" with
SOME "x" => "x"
| NONE => "join" "c"
end)%V.
end.
(** The CMRA & functor we need. *)
(* Not bundling heapG, as it may be shared with other users. *)
......@@ -50,7 +50,7 @@ Lemma spawn_spec (Ψ : val → iProp Σ) e (f : val) :
heapN N
{{{ heap_ctx WP f #() {{ Ψ }} }}} spawn e {{{ l, RET #l; join_handle l Ψ }}}.
Proof.
iIntros (<-%of_to_val ? Φ) "(#Hh & Hf) HΦ". rewrite /spawn -lock /=.
iIntros (<-%of_to_val ? Φ) "(#Hh & Hf) HΦ". rewrite /spawn /=.
wp_let. wp_alloc l as "Hl". wp_let.
iMod (own_alloc (Excl ())) as (γ) "Hγ"; first done.
iMod (inv_alloc N _ (spawn_inv γ l Ψ) with "[Hl]") as "#?".
......
......@@ -5,11 +5,11 @@ From iris.heap_lang Require Import proofmode notation.
From iris.algebra Require Import excl.
From iris.heap_lang.lib Require Import lock.
Definition newlock : val := ssreflect.locked (λ: <>, ref #false)%V.
Definition try_acquire : val := ssreflect.locked (λ: "l", CAS "l" #false #true)%V.
Definition newlock : val := λ: <>, ref #false.
Definition try_acquire : val := λ: "l", CAS "l" #false #true.
Definition acquire : val :=
ssreflect.locked (rec: "acquire" "l" := if: try_acquire "l" then #() else "acquire" "l")%V.
Definition release : val := ssreflect.locked (λ: "l", "l" <- #false)%V.
rec: "acquire" "l" := if: try_acquire "l" then #() else "acquire" "l".
Definition release : val := λ: "l", "l" <- #false.
(** The CMRA we need. *)
(* Not bundling heapG, as it may be shared with other users. *)
......@@ -48,7 +48,7 @@ Section proof.
heapN N
{{{ heap_ctx R }}} newlock #() {{{ lk γ, RET lk; is_lock γ lk R }}}.
Proof.
iIntros (? Φ) "[#Hh HR] HΦ". rewrite -wp_fupd /newlock. unlock.
iIntros (? Φ) "[#Hh HR] HΦ". rewrite -wp_fupd /newlock /=.
wp_seq. wp_alloc l as "Hl".
iMod (own_alloc (Excl ())) as (γ) "Hγ"; first done.
iMod (inv_alloc N _ (lock_inv γ l R) with "[-HΦ]") as "#?".
......@@ -83,7 +83,7 @@ Section proof.
Proof.
iIntros (Φ) "(Hlock & Hlocked & HR) HΦ".
iDestruct "Hlock" as (l) "(% & #? & % & #?)". subst.
rewrite /release. unlock. wp_let. iInv N as (b) "[Hl _]" "Hclose".
rewrite /release /=. wp_let. iInv N as (b) "[Hl _]" "Hclose".
wp_store. iApply "HΦ". iApply "Hclose". iNext. iExists false. by iFrame.
Qed.
End proof.
......
......@@ -7,24 +7,24 @@ From iris.heap_lang.lib Require Export lock.
Import uPred.
Definition wait_loop: val :=
ssreflect.locked (rec: "wait_loop" "x" "lk" :=
rec: "wait_loop" "x" "lk" :=
let: "o" := !(Fst "lk") in
if: "x" = "o"
then #() (* my turn *)
else "wait_loop" "x" "lk")%V.
else "wait_loop" "x" "lk".
Definition newlock : val :=
ssreflect.locked (λ: <>, ((* owner *) ref #0, (* next *) ref #0))%V.
λ: <>, ((* owner *) ref #0, (* next *) ref #0).
Definition acquire : val :=
ssreflect.locked (rec: "acquire" "lk" :=
rec: "acquire" "lk" :=
let: "n" := !(Snd "lk") in
if: CAS (Snd "lk") "n" ("n" + #1)
then wait_loop "n" "lk"
else "acquire" "lk")%V.
else "acquire" "lk".
Definition release : val :=
ssreflect.locked (λ: "lk", (Fst "lk") <- !(Fst "lk") + #1)%V.
λ: "lk", (Fst "lk") <- !(Fst "lk") + #1.
(** The CMRAs we need. *)
Class tlockG Σ :=
......@@ -77,7 +77,7 @@ Section proof.
heapN N
{{{ heap_ctx R }}} newlock #() {{{ lk γ, RET lk; is_lock γ lk R }}}.
Proof.
iIntros (HN Φ) "(#Hh & HR) HΦ". rewrite -wp_fupd /newlock. unlock.
iIntros (HN Φ) "(#Hh & HR) HΦ". rewrite -wp_fupd /newlock.
wp_seq. wp_alloc lo as "Hlo". wp_alloc ln as "Hln".
iMod (own_alloc ( (Excl' 0%nat, ) (Excl' 0%nat, ))) as (γ) "[Hγ Hγ']".
{ by rewrite -auth_both_op. }
......@@ -145,7 +145,7 @@ Section proof.
iIntros (Φ) "(Hl & Hγ & HR) HΦ".
iDestruct "Hl" as (lo ln) "(% & #? & % & #?)"; subst.
iDestruct "Hγ" as (o) "Hγo".
rewrite /release. unlock. wp_let. wp_proj. wp_proj. wp_bind (! _)%E.
rewrite /release. wp_let. wp_proj. wp_proj. wp_bind (! _)%E.
iInv N as (o' n) "(>Hlo & >Hln & >Hauth & Haown)" "Hclose".
wp_load.
iDestruct (own_valid_2 with "Hauth Hγo") as
......
......@@ -111,12 +111,6 @@ Proof.
intros; inv_head_step; eauto.
Qed.
Lemma wp_rec_locked E f x erec e1 e2 Φ `{!Closed (f :b: x :b: []) erec} :
e1 = of_val $ locked (RecV f x erec)
is_Some (to_val e2)
WP subst' x e2 (subst' f e1 erec) @ E {{ Φ }} WP App e1 e2 @ E {{ Φ }}.
Proof. unlock. auto using wp_rec. Qed.
Lemma wp_un_op E op e v v' Φ :
to_val e = Some v
un_op_eval op v = Some v'
......
......@@ -47,7 +47,7 @@ Notation "~ e" := (UnOp NegOp e%E) (at level 75, right associativity) : expr_sco
Notation "e1 <- e2" := (Store e1%E e2%E) (at level 80) : expr_scope.
Notation "'rec:' f x := e" := (Rec f%bind x%bind e%E)
(at level 102, f at level 1, x at level 1, e at level 200) : expr_scope.
Notation "'rec:' f x := e" := (RecV f%bind x%bind e%E)
Notation "'rec:' f x := e" := (locked (RecV f%bind x%bind e%E))
(at level 102, f at level 1, x at level 1, e at level 200) : val_scope.
Notation "'if:' e1 'then' e2 'else' e3" := (If e1%E e2%E e3%E)
(at level 200, e1, e2, e3 at level 200) : expr_scope.
......@@ -58,20 +58,20 @@ defined above. This is needed because App is now a coercion, and these
notations are otherwise not pretty printed back accordingly. *)
Notation "'rec:' f x y := e" := (Rec f%bind x%bind (Lam y%bind e%E))
(at level 102, f, x, y at level 1, e at level 200) : expr_scope.
Notation "'rec:' f x y := e" := (RecV f%bind x%bind (Lam y%bind e%E))
Notation "'rec:' f x y := e" := (locked (RecV f%bind x%bind (Lam y%bind e%E)))
(at level 102, f, x, y at level 1, e at level 200) : val_scope.
Notation "'rec:' f x y .. z := e" := (Rec f%bind x%bind (Lam y%bind .. (Lam z%bind e%E) ..))
(at level 102, f, x, y, z at level 1, e at level 200) : expr_scope.
Notation "'rec:' f x y .. z := e" := (RecV f%bind x%bind (Lam y%bind ..