\documentclass[11pt]{article} \usepackage{lmodern} \usepackage[T1]{fontenc} \usepackage[utf8]{inputenc} \usepackage{fontspec} \setmonofont{Source Code Pro} \newif\ifslow\slowfalse %\slowtrue \ifslow \usepackage[english]{babel} \usepackage[babel=true]{microtype} \fi \usepackage[top=1in, bottom=1in, left=1.25in, right=1.25in]{geometry} \usepackage[backend=biber]{biblatex} \bibliography{bib} \newcommand{\bdia}{\blacklozenge} \newcommand{\dia}{\Diamond} \newcommand{\injR}{\texttt{injR}} \newcommand{\injL}{\texttt{injL}} \input{setup} \begin{document} \title{\bfseries iris-atomic} \author{Zhen Zhang} \maketitle \section{Overview} \begin{figure}[hb] \centering \includegraphics[width=0.5\textwidth]{ispace} \caption {Two dimensions of atomicity verification in Iris} \end{figure} \section{Generic syncer spec} \begin{align*} \text{synced}(R, f', f) \eqdef \All P, Q, x. &\hoare{ R * P(x)}{f(x)}{ v.\,R * Q(x,v) } \ra \\ &\hoare{ P(x)}{f'(x)}{ v.\,Q(x,v) } \end{align*} $\text{syncer}(R, s) \eqdef \All f. \wpre{s(f)}{ f'.\, \text{synced}(R, f', f)}$ $\text{mkSyncer}(f) \eqdef \All R. \hoare{R}{f()}{ s.\,\always \text{syncer}(R, s)}$ This \textbf{generic syncer spec} is inspired by CaReSL. In CaReSL, fine-grained syncer (e.g. flat combiner) is proven to be contextual refinement of coarse-grained \texttt{mkSync} (See section \ref{mksync}). However, there is no program refinement yet in Iris, so I made this generalization and prove that flat combiner satisfies this \emph{directly}. In fact, any sensible syncer is expected to satisfy this generic spec. Besides generalization, I also split original spec into two parts, corresponding to two calls that happen at different times. More generally speaking, this problem is caused by a special case of curried function (e.g. $\lambda x_1.\, \lambda x_2.\,...$): Is it possible to go from $\All x_1, x_2. \hoare{P(x_1, x_2)}{f(x_1, x_2)}{Q(x_1, x_2)}$ to $\All x_1. \hoare{\top}{f(x_1)}{f_1.\, \All x_2. \hoare{P(x_1, x_2)}{f_1(x_2)}{Q(x_1, x_2)}}$, assuming that $$f \eqdef \lambda x_1, x_2.\, e$$. Finally, I'd like to point out that pre- and post-conditions $P, Q$ are universally qualified per application, that is to say, $P, Q$ are arbitrary depending on the context. And similarly, $f$ is universally qualified per synchronization, which means that syncer is only parameterized by the shared resource $R$, it can work with any operation that needs to access this $R$. \section{Logically atomic triple (LAT)} \begin{align*} &\lahoare{g.\, \alpha(g)}{e}{v.\, \beta(g, v)}[E_i][E_o] \eqdef\\ &\All P, Q. \begin{aligned} &P \vs[Eo][Ei] \Exists g, \alpha(g) * (\alpha(g) \vsW[Ei][Eo] P \land \All v. \beta(g, v) \vsW[Ei][Eo] Q(g, v)) \wand \\ &\hoare{P}{e}{v.\, \Exists g. Q(g, v)} \end{aligned} \end{align*} Note again, the $P, Q$ are arbitrary depending on the context. And also, note the separation product of two linear view shifts: First one represents \textbf{abandon} direction, while the second one represents \textbf{commit} direction. Using linear view shifts enables us to frame alongside the transition some non-persistent resource. \begin{figure}[hb] \centering \includegraphics[width=0.5\textwidth]{lat} \caption {Sketch of how library function specified with LAT will be used} \end{figure} \section{Coarse-grained syncer}\label{mksync} First, we give the CaReSL's \texttt{mkSync} written in heap-lang (which is basically the same as in Coq, despite a few cosmetics). \begin{verbatim} mk_sync := λ: <>, let l := newlock() in λ: f x, acquire l; let ret := f x in release l; ret. \end{verbatim} Okay, now the question is: can we give a LAT spec for \texttt{mk\_sync}? Actually, we can! and we can do this in a general way (i.e. for any syncer satisfying the generic syncer spec). We will briefly discuss about it in the next section. \section{Encoding generic syncer spec as a LAT-style spec} The first question is: \textbf{Why do we want to do so?} First, they both talk about atomicity, so we will naturally want to know what is the possible relationship between them. And second, the generic syncer spec is not canonical -- it doesn't tell explicitly what effects that operation has. When use the generic syncer spec as a client, you have to prove something about $e$ every time. But LAT, on the contrary, gives you the exact specification of the operation itself, which means that you only need to prove the viewshifts (in some sense similar to weakening/strengthening rules). And most importantly, this exact specification, should look exactly like the sequential specification! Just consider the following illustrative comparison of a sequential/concurrent stack \texttt{push} spec: \begin{align*} \All xs.\hoare{stack(s, xs)}{\texttt{push}(x, s)}{\_.\, stack(s, x::xs)}\\ \lahoare{xs.\, stack'(s, xs)}{\texttt{push'}(x, s)}{\_.\, stack'(s, x::xs)} \end{align*} The second question is: \textbf{Is it possible to do so?} Intuitively, what syncer spec says is that the $e$'s sequential effects are \emph{compressed} to a single point. Consider the coarse-grained implementation of generic syncer spec, \texttt{mk\_sync}, it guards the resource $R$ by putting it inside a lock, thus every operation will exclusively own $R$ for a certain period, which makes the whole operation look atomic, when observed from outside in terms of resource accessing. The last question is: \textbf{How to do it?} First, consider what LAT's client can provide to the library: abandoning and committing viewshifts. And these two actions must happen instantly. So, naturally, we will try to commit at the time of finishing the operation and give back the $R$ to lock. But what about abandoning? What role will it have in the syncer spec? Remember that there is a canonical pre-condition $\alpha$ in LAT, which should coincide with the sequential spec. But the sequential code, when executed between the lock/unlock, is still non-atomic. So after we exchange $P$ for $\alpha$, we must retain $\alpha$ for a long time, while we also have to close the LAT viewshifts in an instant. We can't close by abandoning, since we need to give back the $\alpha$; and we can't close by committing, since we haven't started the action yet! But wait, why we \emph{must} give back $\alpha$ while losing it? What if we require that $\alpha$ is duplicable? Then problem solved! We just need to abandon in the beginning to get a duplicated $\alpha$ out, then committing with $P$ when finishing off. Now, with a sketch in mind, I will introduce you to the detailed construction: First, here is the specialized logically atomic triple for such purpose: $\lahoare{g.\, \ownGhost{\gname}{g^{1/2}} * \always \alpha(g)} {f(x)} {v.\, \Exists g'. \ownGhost{\gname}{g'^{1/2}} * \beta(x, g, g', v)}[E_i][E_o]$ Here, $g$ represents \textbf{ghost state}. $g$ can be of any proper type. $\ownGhost{\gname}{g'^{1/2}}$ is a snapshot of $g$, i.e. local knowledge about the physical configuration. (Why it is written in such way? Well, this is the implementation detail related to the monoid used to encode this). Here, the persistent (thus duplicable) $\alpha(g)$ is some extra condition. And in the post condition, we say there exists an updated ghost state $g'$, which satisfy $\beta$, a relation over input, previous state, current state, and output. Let's take concurrent \texttt{push} again as an example. If $s$ is a stack pointer, $R_s \eqdef \Exists xs. stack(s, xs) * \ownGhost{\gname}{xs^{1/2}}$ is the physical configuration plus global snapshot, then $\text{synced}(stack(s, xs), \texttt{push'}, \texttt{push}(s))$ should expand like this: \begin{align*} \All P, Q, x. &\hoare{ R_s * P(x)}{\texttt{push}(s)(x)}{ v.\,R_s * Q(x,v) } \ra \\ &\hoare{ P(x)}{\texttt{push'}(x)}{ v.\,Q(x,v) } \end{align*} And the LAT we can get from it looks like this: $\lahoare{xs.\, \ownGhost{\gname}{xs^{1/2}}}{\texttt{push'}(x)}{\_.\, \Exists xs'. \ownGhost{\gname}{xs'^{1/2}} * (xs' = x::xs)}$ Here, note that in this case $\always \alpha(g)$ is selected as $\top$ (thus we can imagine that in most cases persistent restriction is not much of a problem); also, $s$ is entirely hidden somewhere in some global place, i.e., using $\ownGhost{\gname}{xs^{1/2}}$, you can also atomically access $\Exists s. stack(s, xs)$, even though such accessing is not specified as a LAT. \begin{verbatim} sync(mk_syncer) := λ: f_seq l, let s := mk_syncer() in s (f_seq l). \end{verbatim} seq\_spec(f, \phi, \alpha, \beta, E) \eqdef \All l. \hoare{\top}{f(l)}{f'.\, \begin{aligned} \pure &\All x, \Phi, g.\\ &\phi (l, g) * \always \alpha(x) *\\ &(\All v, g'. \phi(l, g') \wand \beta(x, g, g', v) \wand \pvs[E][E] \Phi(v))\\ &\proves \wpre{f'(x)}[E]{ \Phi } \end{aligned} } Here is the sequential spec. pre-condition is the persistent alpha and exclusive ownership of shared state, and when it returns, we got the updated physical state g’, as well as beta. Funny thing is again that I have to apply f to l first ... because of currying and call site problem. \begin{aligned} &\text{atomic\_spec}(mk\_syncer, f\_seq, l, \phi, \alpha, \beta, E_i) \eqdef\\ &\All g_0. seq\_spec(f\_seq, \phi, \alpha, \beta, \top) \ra mk\_syncer\_spec(mk\_syncer) \ra\\ &\phi(l, g_0) \proves \wpre{sync(mk\_syncer, f\_seq, l)}{ f.\, \Exists \gname. \ownGhost{\gname}{g_0^{1/2}} * \All x. \always \lahoare{g.\, \ownGhost{\gname}{g^{1/2}} * \always \alpha(g)}{f(x)} {v.\, \Exists g'. \ownGhost{\gname}{g'^{1/2}} * \beta(x, g, g', v)}[E_i][\top]} \end{aligned} So, here is the theorem that states such derivation. Inside the blue box is the triple defined earlier, it is returned in the post-condition. The meta procedure “sync” is parameterised in Coq with any kind of syncer constructor you want to prove about. Its heap-lang parameters are sequential code closure and the location to internal state. As you can see from its definition, it partially applies \texttt{f\_seq} with l, i.e., binding operation with shared state pointer, and return a concurrent operation synchronized by newly-created syncer. Now let’s observe its two pure conditions: first, sequential code must have a spec; second, \texttt{mk\_syncer} satisfies the syncer constructor spec [review] $(\Exists g. \phi(l, g') * \ownGhost{\gname}{g^{1/2}} * P x$ \includegraphics[width=0.5\textwidth]{atomic_sync} \section{treiber.v} \begin{verbatim} push s x := let hd := !s in let s' := ref SOME (x, hd) in if CAS s hd s' then () else push s x. pop s := let hd := !s in match !hd with | SOME (x, hd') => if: CAS s hd hd' then SOME x else pop s | NONE => NONE end. iter hd f := match !hd with | NONE => () | SOME (x, hd') => f x ; iter hd' f end. \end{verbatim} Finally, it is time to talk about flat combiner …. oh no, not yet. We need to talk about treiber’s stack first. These push and pop are all standard lock-free implementation. We will give LAT spec for these two operations first Logiall atomic spec (version 1): $\lahoare{xs.\, stack(s, xs)}{push(s, x)}{stack(s, x::xs)}[heapN][\top]$ $\lahoare{xs.\, stack(s, xs)}{pop(s)}{v. \begin{split} (&\Exists x, xs'. v = SOME(x) * stack(s, xs')) \lor\\ (&v = NONE * xs = \emptyset * stack(s, \emptyset)) \end{split}}[heapN][\top]$ Logiall atomic spec (version 2): $\lahoare{hd, xs.\, s \mapsto hd * list(hd, xs)}{push(s, x)}{\Exists hd'. s \mapsto hd' * hd' \mapsto SOME(x, hd) * list(hd, xs)}[heapN][\top]$ $\lahoare{hd, xs.\, s \mapsto hd * list(hd, xs)}{pop(s)}{v. \begin{split} (&\Exists x, xs', hd'. v = SOME(x) * hd \mapsto SOME(x, hd') * s \mapsto hd' * list(hd', xs')) \lor\\ (&v = NONE * xs = \emptyset * hd \mapsto NONE) \end{split} }[heapN][\top]$ For these two operations, we usually will give a more abstract spec, like the one above, which talks about s and elements in it, but no more. However, we can also give one that exposes how stack is implemented (here, as a linked list). Actually, if we want to prove push spec in per-item-invariant style, we must expose enough details. Why? The intuition is that, when push some element in a per-item setting, we need to open, modify where s points to, and then close the invariant. But how can we make sure that the rest of the stack is always satisfying the per-item invariants? If we want such evidence, we need to expose something physical, such as the head pointer in this case. \section{peritem.v} A crappy but working spec: $f\_spec (\gname, xs, s, f, Rf, RI) \eqdef \All x. \hoare{x \in xs * \knowInv\iname{\Exists xs. stack'(\gname, xs, s) * RI} * Rf}{f(x)}{ v.\, v = () }.$ $\begin{split} iter\_spec(\gname, s, Rf, RI) \eqdef &\All xs, hd, f.\\ &f\_spec(xs, s, f', Rf, RI) \ra\\ &\hoare{\knowInv\iname{\Exists xs. stack'(xs, s) * RI} * list'(\gname, hd, xs) * Rf}{iter(hd, f)}{ v.\, v = () * Rf} \end{split}$ $push\_spec (\gname, s, x, RI) \eqdef \hoare{R(x) * \knowInv\iname{\Exists xs. stack'(xs, s) * RI}}{push(s, x)}{v.\, v = () * (\Exists hd. ev(\gname, hd, x))}$ Okay, but in per-item spec, why do you need to make sure that the stack is growth-only, and governed by a global invariant? Answer: because we need to iterate thought it non-atomically. I mean, the process of iteration is not atomic. The single operation f still needs to atomically access any resource related x. So, having already talked a lot about per-item spec… here is how it looks like in my implementation. Well, I agree with you that this is a bit messy. note that global inv of stack is parametrised by per-item predicate R \section{flat.v} \begin{verbatim} doOp := λ: p, match !p with | InjL (f, x) => p <- InjR (f x) | InjR _ => () end. try_srv := λ: lk s, if try_acquire lk then let hd := !s in iter hd doOp; release lk else (). loop p s lk := match !p with | InjL _ => try_srv lk s; loop p s lk | InjR r => r end. install := λ: f x s, let p := ref (InjL (f, x)) in push s p; p. mk_flat := λ: <>, let lk := newlock() in let s := new_stack() in λ: f x, let p := install f x s in let r := loop p s lk in r. \end{verbatim} Let’s go to my flat combiner code now. Compared to CaReSL, here are several notable differences: I break them down into five procedures, instead of nesting them inside the constructor. It is easier to specify. CaReSL’s flat constructor takes f; this doesn’t, which makes it more flexible. CaReSL’s install utilize TLS to avoid blowup of space use. I push in a new slot every time, which is terrible in practice, but follows the same spec. Also, another problem that exist both in my, CaReSL, and FCSL’s example code, is that we never recycle the slots. $p \mapsto \injR(-)$ $p \mapsto \texttt{injL}(f, x)$ $p \mapsto \injR(y)$ $\circ_i, \bullet_i, \dia_i, \bdia, \dia_i \circ_i, \dia_i \bullet_i, \bdia \bullet_i$ \includegraphics[width=0.5\textwidth]{helping} This is the protocol of helping … The black diamond is a token owned by server lock. The other three kinds of token are all tagged with i, which should be similar to thread id in CaReSL’s reasoning, but in my case, it is the slot address (Is it more flexible than using tid to index?). And the indexing is essentially done through a ghost map in invariant. Note that this graph is heavily simplified to reflect how I encode protocol with bare exclusive monoids. Next slide gives the detailed invariant construction \begin{align*} &\Exists y. &&p \fmapsto[1/2] \injR(-) * \dia_i * \circ_i\\ \lor &\Exists f, x, P, Q. &&p \fmapsto[1/2] \injL(f, x) * \ownGhost{\gname}{x^{1/2}} * P(x) * (\hoare{R * P(x)}{f(x)}{v.\,R * Q(x, v)}) * \gamma \mapstoprop Q(x) * \dia_i * \bullet_i\\ \lor &\Exists x. &&p \fmapsto[1/2] \injL(-, x) * \ownGhost{\gname}{x^{1/4}} * \bdia * \bullet_i\\ \lor &\Exists x, y. &&p \fmapsto[1/2] \injR(y) * \ownGhost{\gname}{x^{1/2}} * \gamma \mapstoprop Q(x) * Q(x, y) * \dia_i * \bullet_i \end{align*} Here is the per-item (i.e. request slot) invariant, which have four branches. Note how f x P Q are all hidden under existential qualification, while (Q x) is saved under some name. It means that only post-condition matter to waiting client. This is basically the core of flat combiner proofs. There are just a couple of critical points, the rest are all boilerplates like open/close invariant. A nicer per-item spec could improve it I guess. $\alpha = \alpha_a * \alpha_o, \alpha = \alpha_a' * \alpha_o$ $\alpha = \alpha_o * \alpha_a, \alpha_a' * \alpha_o = \beta$ $\alpha = \alpha_a * \alpha_o, \alpha = \alpha_a' * \alpha_o$ \end{document}