The code above is a helper function \texttt{sync}, which constructs the syncer, partially applies internal state value \texttt{l} to the sequential operation \texttt{f\_seq}, and synchronizes the partially applied operation. There is an assumption that \texttt{l} should represent a valid state (either freshly constructed or whatever).
Now, if conditions $seqSpec(\texttt{f\_seq}, \phi, \alpha, \beta, \top)$ (see ?) and $mkSyncer(\texttt{mk\_syncer})$ are satisfied, then we have:
Now, if conditions $seqSpec(\texttt{f\_seq}, \phi, \alpha, \beta, \top)$ (see \ref{seq}) and $mkSyncer(\texttt{mk\_syncer})$ are satisfied, then we have:
\[
\All g_0.
...
...
@@ -170,7 +170,7 @@ Now, if conditions $seqSpec(\texttt{f\_seq}, \phi, \alpha, \beta, \top)$ (see ?)
In pre-condition, we have persistent $\alpha(g)$ and exclusive ownership of shared state, and when it returns, we got the updated physical state g’, as well as beta.
In pre-condition, we have persistent $\alpha(g)$ and exclusive ownership of shared state; and when it returns, we get back 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.
Funny thing is again that I have to apply $f$ to $l$ first ... because of currying problem.
To be more concrete, here is the invariant that will be used globally: \((\Exists g. \phi(l, g')*\ownGhost{\gname}{g^{1/2}}* P x \).
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 \]
\[\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\\
(&\Exists x, xs', hd'.
\begin{aligned}
&v = SOME(x)* hd \mapsto SOME(x, hd')*\\
&s \mapsto hd' * list(hd', xs')
\end{aligned})\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.
Apparently, the version 1 is more preferrable as a general spec, since the implementation might not necessarily be a linked-list.
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.
But if we want to iterate over it using \texttt{iter} using a per-item style spec, than we might expose enough implementation details to tie per-item resource to physical location. And as a result, to maintian such property, we must also make \texttt{push}'s LAT spec exposing enough details as well (And it doesn't even make sense to use \texttt{pop} in this case). Below is the discussion about per-item spec.
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.
...
...
@@ -283,6 +280,8 @@ So, having already talked a lot about per-item spec… here is how it looks like
note that global inv of stack is parametrised by per-item predicate R
\textbf{Problem}: This part is quite bad actually ... first, CaReSL have a smaller, nicer per-item spec; second, it doesn't sound perfectly legitimate that we can't pop things out ... I just need to make sure that the things \emph{currrently in} the stack conforms to certain resource predicate. So, if the structure of linking allows someone to control validities of all possible references into certain item, then it can pop like a breeze.
