Attention une mise à jour du service Gitlab va être effectuée le mardi 18 janvier (et non lundi 17 comme annoncé précédemment) entre 18h00 et 18h30. Cette mise à jour va générer une interruption du service dont nous ne maîtrisons pas complètement la durée mais qui ne devrait pas excéder quelques minutes.

Commit 0a27e850 authored by Glen Mével's avatar Glen Mével
Browse files

ICFP21 paper: changes regarding pointsto assertions

- add footnote about races on NA
- remove redundant paragraphs for introducing pointsto assertions
- "predicate" -> "assertion" everywhere
- minor improvements
parent d731f357
......@@ -51,8 +51,15 @@ without waiting for the completion of the new thread.
The memory model of \mocaml describes how the memory operations interact with the shared memory. \citet{dolan-18} give an operational account, which is out of the scope of the current paper. However, to give some intuition, we show in~\fref{fig:lang:triples} what this semantics translates to in the \hlog program logic. In the following paragraphs, we give an overview of these triples which are explained more thoroughly by~\citet{mevel-jourdan-pottier-20}.
Operations on nonatomic cells obey the usual-looking Hoare triples, but an important departure from sequential consistency is that their associated pointsto predicate $\nthpointstoNA \loc \idx \val$ is subjective: the knowledge of the latest value~$\val$ of a nonatomic cell~$\loc[\idx]$ is relative to the ambient view.
There are different pointsto assertions for atomic cells and for nonatomic cells. As is standard, these predicates assert unique ownership of the cells.
On the other hand, the pointsto predicate $\nthpointstoAT \loc \idx {\mkval\val\view}$ that represents an atomic cell is objective: this implies that an atomic cell~$\loc[\idx]$ stores a single value~$\val$ on which all threads agree.
Operations on nonatomic cells obey the usual-looking Hoare triples, but an important departure from sequential consistency is that their associated pointsto assertion $\nthpointstoNA \loc \idx \val$ is subjective: the knowledge of the latest value~$\val$ of a nonatomic cell~$\loc[\idx]$ is relative to the ambient view.%
\footnote{%
This single-value pointsto assertion effectively forbids reasoning about races on nonatomic cells. The operational semantics of~\citet{dolan-18} is more general, as it gives a well-defined (albeit nondeterministic) semantics to racy uses of nonatomic cells.
}
On the other hand, the pointsto assertion $\nthpointstoAT \loc \idx {\mkval\val\view}$ that represents an atomic cell is objective: this implies that an atomic cell~$\loc[\idx]$ stores a single value~$\val$ on which all threads agree.
%This value is thus read and updated in a sequentially consistent fashion.
In addition, an atomic cell also stores a view~$\view$. As can be seen in the triples of atomic operations, this view accumulates the knowledge of all writers and is transmitted to readers. This means that there is a happens-before relationship from a write operation to a read operation which reads from it (in a release-acquire fashion). Atomic accesses are thus the prime means of inter-thread synchronization in \mocaml. The last two triples say that a failed CAS operation behaves as an atomic read (returning $\False$), while a successful CAS operation behaves as the combination of an atomic read and an atomic write (returning $\True$).
In addition, an atomic cell also stores a view~$\view$. As can be seen in the triples of atomic operations, this view accumulates the knowledge of all writers and transmits this knowledge to readers. This means that there is a happens-before relationship from a write operation to a read operation which reads from it (in a release-acquire fashion). In fact, atomic accesses are the prime means of inter-thread synchronization in \mocaml.
The last two triples say that a failed CAS operation behaves as an atomic read (returning $\False$), while a successful CAS operation behaves as the combination of an atomic read and an atomic write (returning $\True$).
......@@ -54,7 +54,7 @@ ghost state, stored in a ghost variable~$\gqueue$.
%
More precisely, the public state is kept in sync with the values which appear in an authoritative assertion $\ownGhost\gqueue{\authfull \tuple{\tview, \hview, \elemViewList}}$, the latter being owned by the internal invariant.
%
In other words, the two assertions satisfy the following properties:
Formally, the two assertions satisfy the following properties:
%
\begin{mathpar}
%
......@@ -96,13 +96,14 @@ we provide the user with the persistent assertion $\queueInv$. It contains the
internal invariant governing the queue~$\queue$, whose public state is exposed
via the ghost variable~$\gqueue$. In addition to the public state, there are
two more ghost variables, named $\gmonos$ and $\gtokens$, which are hidden
to the user but needed by the queue operations. Thus they are
to the user of the queue but needed internally. Thus they are
existentially quantified in this persistent assertion. We will explain the
purpose and meaning of these ghost variables in a moment. For now, we look at
the internal invariant, $\queueInvInner$.
This invariant owns most of the physical locations of the queue: \reftail,
\refhead, \refstatuses, and some parts of the array \refelements.
Recall that pointsto assertions for atomic cells are objective and can be placed inside an invariant.
%
The array-pointsto assertion $\arraypointstoAT\refstatuses\statusViewList$ is
a shorthand for the following iterated conjunction:
......@@ -110,18 +111,15 @@ a shorthand for the following iterated conjunction:
\Sep_{0 \leq \offset < \capacity} \nthpointstoAT\refstatuses\offset{\mkval{\status_\offset}{\sview_\offset}}
\]
%
Recall that in \hlog, $\nthpointstoAT\refstatuses\offset{\mkval{\status_\offset}{\sview_\offset}}$
is the pointsto assertion for the atomic cell at index~\offset\ of
location~\refstatuses: it asserts the unique ownership of that cell, and states
that it currently contains the value $\status_\offset$ and the view
$\sview_\offset$ (or a larger view).
%Recall that in \hlog, $\nthpointstoAT\refstatuses\offset{\mkval{\status_\offset}{\sview_\offset}}$
%is the pointsto assertion for the atomic cell at index~\offset\ of
%location~\refstatuses: it asserts the unique ownership of that cell, and states
%that it currently contains the value $\status_\offset$ and the view
%$\sview_\offset$ (or a larger view).
%
Since we encode references as arrays of length~one,
$\pointstoAT\reftail{\mkval\tail\tview}$ is a shorthand for
Also, since we encode references as arrays of length~one,
we write $\pointstoAT\reftail{\mkval\tail\tview}$ as a shorthand for
$\nthpointstoAT\reftail0{\mkval\tail\tview}$.
%
Pointsto assertions for atomic cells are objective and can be placed
inside an invariant.
Apart from this physical state, the invariant also stores ghost state. It owns
the authority on all three ghost variables, $\gqueue$, $\gmonos$ and $\gtokens$.
......@@ -220,7 +218,7 @@ the following join-semilattice structure:
\pair{\status_1}{\sview_1}
\sqsubseteq
\pair{\status_2}{\sview_2}
&\Longleftrightarrow&
&\eqdef&
\status_1 < \status_2 \lor \left( \status_1 = \status_2 \land \sview_1 \viewgeq \sview_2 \right)
\\
\pair{\status_1}{\sview_1}
......@@ -250,13 +248,16 @@ whose value is $\elem$ with the associated view $\eview$.
%
In these two abbreviations, the status field of the slot has value~$\status$ and
stores view~$\sview$.
%
These abbreviations are also where we keep the ownership of the \emph{nonatomic} cell $\refelements[\modcap\idx]$, via a pointsto assertion.
%In both cases, we must own the memory cell.
Recall that in \hlog, $\nthpointstoNA\refelements{\modcap\idx}\elem$
is the pointsto assertion for the \emph{nonatomic} cell at index~$\modcap\idx$
of location~\refelements: it asserts the unique ownership of that cell, and
states that we have observed its latest write event, which wrote the value~$\elem$.
Unlike an atomic pointsto assertion, this one is \emph{subjective}: its truth
%Recall that in \hlog, $\nthpointstoNA\refelements{\modcap\idx}\elem$
%is the pointsto assertion for the \emph{nonatomic} cell at index~$\modcap\idx$
%of location~\refelements: it asserts the unique ownership of that cell, and
%states that we have observed its latest write event, which wrote the value~$\elem$.
%
Recall that, in \hlog, unlike an atomic pointsto assertion, a nonatomic pointsto assertion is \emph{subjective}: its truth
depends on the view of the subject thread. As a consequence, it cannot be placed in
an invariant as is.
%
......@@ -265,12 +266,12 @@ we must explicitly indicate at which view it holds.
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,
the view of the last writer thread when that write occurred.
At a view which contains the latest write event to that cell.
%; for instance, the view of the last writer thread when that write occurred.
%
Fortunately, in our case, any thread---enqueuer or dequeuer---which writes to the
nonatomic cell $\refelements[\modcap\idx]$ then writes to the atomic cell
$\refstatuses[\modcap\idx]$. Thus it adds its current view, including its own
$\refstatuses[\modcap\idx]$. Thus it adds its knowledge, including its own
write to the item field, to the view~$\sview$ stored by the status field.
With all this said, a first attempt at representing the buffer might look as follows:
......
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