Commit 24c6930b authored by Glen Mével's avatar Glen Mével
Browse files

ICFP21 paper: move def of P@V to a more relevant place, rephrase

parent 8a9ac82b
......@@ -262,21 +262,7 @@ an invariant as is.
%
In order to share this assertion,
we must explicitly indicate at which view it holds.
That is precisely the purpose of the $\opat$ connective.
% TODO : déplacer plus haut là où on introduit P@V
In \hlog, for any potentially subjective assertion~$\prop$, the objective
assertion~$\prop \opat \view$ means that $\prop$ holds \emph{provided}
that the view of the subject thread contains~$\view$.
%
It can be roughly understood as $\seen\view \wand \prop$, but,
unlike this implication, it is objective.
%At which view do we own the item cell? In our queue implementation, the status
%field of a given slot plays the role of a ``lock'' for the item field of that slot.
%Not only does its value~$\status$ indicate whether the slot is available or occupied,
%it also guarantees synchronization from an user of the slot to the next user,
%through the view~$\sview$ it stores.
This is the purpose of the $\opat$ connective.
At which view can we own a nonatomic memory cell?
At a view which contains the latest write event to that cell; for instance,
......@@ -287,7 +273,6 @@ nonatomic cell $\refelements[\modcap\idx]$ then writes to the atomic cell
$\refstatuses[\modcap\idx]$. Thus it adds its current view, including its own
write to the item field, to the view~$\sview$ stored by the status field.
%(Not so) Naively, one may try to represent the buffer as follows:
With all this said, a first attempt at representing the buffer might look as follows:
%
\[\begin{array}{rcl}
......
......@@ -99,8 +99,22 @@ To the user of this logic, views (denoted in this paper by calligraphic capital
equipped with lattice structure:
the least view~$\emptyview$ is the empty view,
and larger views correspond to more recent knowledge.
If $\view$ is a view, the persistent assertion~$\seen\view$ indicates that the current thread has the knowledge contained in~$\view$.
\hlog{} provides reasoning rules about these assertions, shown in~\fref{fig:hlog:axioms}. We explain rule~\splitso in the next paragraph.
Cosmo features two kinds of assertions to deal with views.
First, if $\view$ is a view, then
the persistent assertion~$\seen\view$
indicates that the current thread has the knowledge contained in~$\view$.
Second, if $\view$ is a view and $\prop$ is a (subjective) assertion, then
$\prop \opat \view$
denotes the assertion~$\prop$ where $\view$ has been substituted for the ambient view;
as it does not depend on the ambient view anymore,
$\prop \opat \view$ is objective.%
\footnote{%
An equivalent definition is the following:
asserting $\prop \opat \view$ is asserting that, even without other knowledge, if we have the knowledge contained in~$\view$, then $\prop$ holds.
In other words, $\prop \opat \view$ is objective and entails $\seen\view \wand \prop$.
%The assertion~ $\prop$ requires no other knowledge than that of $\view$.
}
\hlog{} provides reasoning rules about these assertions, shown in~\fref{fig:hlog:axioms}. We comment on rule~\splitso in the next paragraph.
In \hlog{}, the usual way of specifying a happens-before relationship between two program points is by giving the client the ability to transfer any assertion of the form $\seen\view$ between these two points: this corresponds to saying that the destination program point has all the knowledge the source program point had about the shared memory.
%
......@@ -108,8 +122,9 @@ As seen later with the example of the pipeline~(\sref{sec:pipeline:proof}),
this is sufficient for transferring any subjective resource from a sender to a receiver.
Indeed, rule~\splitso says that we can split any subjective assertion~$\prop$ into two assertions $\seen \view$ and $\prop \opat \view$ for some view~$\view$
% (which happens to be the ambient view)
and, conversely, we can reconstruct $\prop$ from two such assertions. Here, $\prop \opat \view$ denotes the assertion~$\prop$ where $\view$ has been substituted for the ambient view; as it does not depend on the ambient view anymore, $\prop \opat \view$ is objective, thus it can be shared in an invariant.
Hence, to transfer $\prop$, it is enough to transfer its subjective part, $\seen \view$.
and, conversely, we can reconstruct $\prop$ from two such assertions.
The second part being objective, it can be shared in an invariant.
Hence, to transfer $\prop$, it is enough to transfer its subjective part~$\seen \view$.
In the specification of the queue,
to express the happens-before relationships mentioned earlier,
......
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