Commit 36882c54 authored by Jacques-Henri Jourdan's avatar Jacques-Henri Jourdan
Browse files

Typos.

parent 01425b32
......@@ -52,7 +52,7 @@
& \mid& \ArrayAllocNA\expr\expr
\mid \ArrayReadNA\expr\expr
\mid \ArrayWriteNA\expr\expr\expr
& \quad\text{-- nonatomic cells} \\
& \quad\text{-- non-atomic cells} \\
% atomic store:
& \mid& \ArrayAllocAT\expr{\,\expr}
\mid \ArrayReadAT\expr\expr \,
......@@ -74,7 +74,7 @@
& \mid& \AllocNA\expr
\mid \ReadNA\expr
\mid \WriteNA\expr\expr
& \quad\text{-- nonatomic references} \\
& \quad\text{-- non-atomic references} \\
% atomic store (single cell):
& \mid& \AllocAT{\,\expr}
\mid \ReadAT{\,\expr}
......
......@@ -20,7 +20,7 @@ memory cells with respect to the memory model.
%
Cells are rigidly ascribed an access mode~$\accmode$, which is either
``atomic''~($\accmode = \accmodeAT$) or
``nonatomic''~($\accmode = \accmodeNA$).
``non-atomic''~($\accmode = \accmodeNA$).
%
When~$0 \leq \nbelems$, the expression $\ArrayAllocANY\nbelems\val$ allocates
a block of $\nbelems$~cells whose access mode is~$\accmode$ and whose
......@@ -51,14 +51,14 @@ 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}.
There are different pointsto assertions for atomic cells and for nonatomic cells. As is standard, these predicates assert unique ownership of the cells.
There are different points-to assertions for atomic cells and for non-atomic cells. As is standard, these predicates assert unique ownership of the cells.
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.%
Operations on non-atomic cells obey the usual-looking Hoare triples, but an important departure from sequential consistency is that their associated points-to assertion $\nthpointstoNA \loc \idx \val$ is subjective: the knowledge of the latest value~$\val$ of a non-atomic 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.
This single-value points-to assertion effectively forbids reasoning about races on non-atomic cells. The operational semantics of~\citet{dolan-18} is more general, as it gives a well-defined (albeit nondeterministic) semantics to racy uses of non-atomic 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.
On the other hand, the points-to 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 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.
......
......@@ -10,7 +10,7 @@ obtained by applying $g \circ f$ to each item of the input sequence.
The functions~$g$ and~$f$ need not be pure: they can have side effects and rely
on some state.
For simplicity, input and output sequences are encoded as (nonatomic) arrays,
For simplicity, input and output sequences are encoded as (non-atomic) arrays,
whose length can be obtained via a primitive operation $\Length -$.
However the implementation can be modified to consume and produce lists of
unknown length, or even infinite streams, provided an encoding of such
......@@ -23,7 +23,7 @@ The queue is shared between the main thread and the forked thread, while
\refXArray is transmitted to the forked thread.
The forked thread reads items from~\refXArray in turn, applies $f$ to them
and enqueues the results.
The main thread creates a new (nonatomic) array~\refZArray to store the output;
The main thread creates a new (non-atomic) array~\refZArray to store the output;
then, it dequeues $\nbelems$~items, where $\nbelems$ is the number of items in
the input sequence, applies $g$ to them, and adds the results to \refZArray.
Finally, it returns~\refZArray.
......@@ -8,7 +8,7 @@
We know prove the following result.
\begin{theorem}%
The code shown in~\fref{fig:pipeline:impl} satistfies the specification appearing in~\fref{fig:pipeline:spec}.
The code shown in~\fref{fig:pipeline:impl} satisfies the specification appearing in~\fref{fig:pipeline:spec}.
\end{theorem}%
The proof uses the invariants presented in \fref{fig:pipeline:inv}.
......@@ -16,5 +16,5 @@ More precisely, $\pipelineInv R$ join together the queue invariant $\queueInv$ w
In addition, $\pipelineF R \curf \refXArray \xElemList$ and $\pipelineG R \curg \refZArray \zElemList$ are loop invariants used in the two computing threads.
The pipeline invariant uses the ghost variables $\gcurf$ and $\gcurg$ to agree with the loop invariants on their position, and, in addition to owning the exclusive ownership of the queue, states that each element of the queue is associated with a weakest precondition assertion at the element's view allowing to execute the function $g$ on this element.
Once the invariants are stated and initialized, the proof is a straightforward induction over the length of the input sequence: at each step of each thread, we execute either $f$ or $g$, we open the global pipeline invariant around the logically atomic triple of the enqueing or dequeueing operation.
Once the invariants are stated and initialized, the proof is a straightforward induction over the length of the input sequence: at each step of each thread, we execute either $f$ or $g$, we open the global pipeline invariant around the logically atomic triple of the enqueuing or dequeuing operation.
When this invariant is opened, the state of the queue can be updated, and we perform an update on the ghost variables $\gcurf$ or $\gcurg$ to reflect the state change in the corresponding thread.
......@@ -19,7 +19,7 @@ and functions~$f$ and~$g$ satisfy Hoare triples of the form:
\\
\hoare {Q\;k\;y} {g\;y} {\Lam z. R\;k\;z}
\end{align*}%
so that, by the chaining rule, the composition satifies:
so that, by the chaining rule, the composition satisfies:
\[%
\hoare {P\;k\;x} {g\;(f\;x)} {\Lam z. R\;k\;z}
\]%
......@@ -30,7 +30,7 @@ by taking advantage of the higher-order nature of Iris, we can nest the triples
so as to conceal the intermediate predicate~$Q$.
We use the primitive Cosmo assertion $\haslength\refXArray\nbelems$ to stipulate
that the length of a given array is~$\nbelems$ (recall that the array-pointsto
assertion is shorthand for a separating conjunction of pointsto assertions
that the length of a given array is~$\nbelems$ (recall that the array-points-to
assertion is shorthand for a separating conjunction of points-to assertions
for cells of the array in some range of indices, but it does not state that
there are no cells beyond those mentioned).
......@@ -22,7 +22,7 @@ It uses a ring buffer of fixed capacity~$\capacity \geq 1$.
The buffer is represented by two arrays of
length~\capacity, \refstatuses and \refelements; in each slot (whose offset ranges from~$0$
included to~$\capacity$ excluded), the buffer thus stores a \emph{status} in an
atomic field and an \emph{item} in a nonatomic field. The data~structure also
atomic field and an \emph{item} in a non-atomic field. The data~structure also
has two integers stored in atomic references, \refhead and \reftail.
Items are identified by their \emph{rank} (starting at zero) of insertion in the queue
......@@ -114,7 +114,7 @@ and ready for dequeuers.
%(after reading its status) is certain to read a correct value from the array
%\refelements. This is a typical release/acquire idiom.
Similarly, \dequeue repeatedly calls \trydequeue untils it succeeds;
Similarly, \dequeue repeatedly calls \trydequeue until it succeeds;
the latter works analogously to \tryenqueue,%
%
\footnote{%
......@@ -134,12 +134,12 @@ Once the queue has been created, the reference~\refhead is only accessed from
function~\tryenqueue. The only place where it is modified is the compare-and-set
operation in this function, which attempts to increment it by one, using
a compare-and-set operation. Hence this counter is strictly monotonic, and we
can regard a successful incrementation from~\head\ to~$\head+1$ as uniquely
can regard a successful increment from~\head\ to~$\head+1$ as uniquely
attributing rank~\head\ to the candidate enqueuer. Only then it is allowed to
write into slot~$\modcap\head$.
Similarly, \reftail is only accessed from function~\trydequeue, is strictly
monotonic, and a successful incrementation from~\tail\ to~$\tail+1$ uniquely
monotonic, and a successful increment from~\tail\ to~$\tail+1$ uniquely
attributes rank~\tail\ to the candidate dequeuer. Only then it is allowed to
write into slot~$\modcap\tail$.
......
......@@ -26,7 +26,7 @@ Ghost state values are assigned to ghost variables.
The separation logic assertion~$\ownGhost\gname{a}$, where $a$ is an element of
some CMRA, intuitively means that we own a fragment of the ghost variable
$\gname$ and that this fragment has value~$a$.
Unlike what happens with a traditional pointsto assertion, the ownership \emph{and value} of
Unlike what happens with a traditional points-to assertion, the ownership \emph{and value} of
a ghost variable can be split into fragments according to the composition
operation of the CMRA:
\(
......@@ -94,16 +94,16 @@ 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.
Recall that points-to assertions for atomic cells are objective and can be placed inside an invariant.
%
The array-pointsto assertion $\arraypointstoAT\refstatuses\statusViewList$ is
The array-points-to assertion $\arraypointstoAT\refstatuses\statusViewList$ is
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
%is the points-to 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).
......@@ -157,7 +157,7 @@ Importantly, a witness assertion is persistent: once it has been established, it
We thus have the properties summarized in~\fref{fig:queue:axioms:witness}.
%
Rule~\ruleWitnessPers is the persistency just mentioned.
Rule~\ruleWitnessPers is the persistence just mentioned.
%
Rule~\ruleWitnessOrder asserts that a witness gives a lower bound on what the status cell currently stores.
%
......@@ -198,15 +198,15 @@ 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.
These abbreviations are also where we keep the ownership of the \emph{non-atomic} cell $\refelements[\modcap\idx]$, via a points-to 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$
%is the points-to 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
Recall that, in \hlog, unlike an atomic points-to assertion, a non-atomic points-to 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.
%
......@@ -214,12 +214,12 @@ In order to share this assertion,
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 which view can we own a non-atomic 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.
%
Fortunately, in our case, any thread---enqueuer or dequeuer---which writes to the
nonatomic cell $\refelements[\modcap\idx]$ then writes to the atomic cell
non-atomic cell $\refelements[\modcap\idx]$ then writes to the atomic cell
$\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.
......@@ -277,7 +277,7 @@ The tentative invariant stated above, however, is not correct: while an
invariant has to hold at any point of the execution, the assertion above is
temporarily invalidated when a thread enqueues or dequeues.
Specifically, the thread breaks the assertion when it increments \refhead or
\reftail, thus commiting to enqueuing or dequeuing, until it updates the status
\reftail, thus committing to enqueuing or dequeuing, until it updates the status
of the corresponding slot. It is thus necessary to represent slots which are in
a temporary state. In the actual invariant shown in~\fref{fig:queue:inv:inv},
slots from~$\head-\capacity$ to~$\tail$ are either available or in a temporary
......@@ -289,7 +289,7 @@ finishes filling them.
When an enqueuer or dequeuer moves a slot into a temporary state, it takes
ownership of its item field, so that it can write to it. Hence the invariant
does not have the corresponding pointsto assertion. The thread must give it back
does not have the corresponding points-to assertion. The thread must give it back
when updating the status.
\subsection{Slot Tokens}
......@@ -495,17 +495,17 @@ After unfolding the logically atomic triple, we must prove
$\wpre {(\tryenqueue\;\queue\;\elem)} \predB$ for any~$\predB$,
when in the proof context
we have the internal invariant of the queue (with ghost variables~$\gqueue, \gmonos, \gtokens$)
as well as the atomic update whose precondition and postconditions are that of the triple above.
as well as the atomic update whose precondition and postcondition are that of the triple above.
We then step through the program using usual weakest-precondition calculus.
The first interesting step is the atomic read of \refhead. The ownership of that
reference is shared in the invariant of the queue. Hence, to access it, we must
open the invariant; then we get the pointsto assertion, we can step through the
read operation, return the pointsto assertion and close the invariant again.
open the invariant; then we get the points-to assertion, we can step through the
read operation, return the points-to assertion and close the invariant again.
After we have done so, and thus forgotten all the quantities which are
existentially quantified inside that invariant, we learn little about the value
that has just been read,
excepted that it is a nonnegative integer, say~$\idx$.
excepted that it is a non-negative integer, say~$\idx$.
The second interesting step is the atomic read at index~$\modcap\idx$
of the array~\refstatuses. Again the invariant owns this cell, so we open it
......@@ -579,7 +579,7 @@ From this
%$\emptyCell {(\idx-\capacity)} {\nthStatusView{\modcap\idx}}$,
we get
$\status_{\modcap\idx} = 2\idx = \status^1$,
the pointsto assertion $(\nthpointstoNA\refelements{\modcap\idx}-) \opat \sview_{\modcap\idx}$
the points-to assertion $(\nthpointstoNA\refelements{\modcap\idx}-) \opat \sview_{\modcap\idx}$
and the read~token of rank~$\idx-\capacity$.
The sets of read~tokens and write~tokens depend on the value of \reftail and
\refhead, and we have just incremented the latter, to $\idx+1$, so we
......@@ -590,7 +590,7 @@ are trying to enqueue.
This is also when the \emph{strict} monotonicity of the status comes into play:
because $\status_\idx = \status^1$, it gives us
$\sview_\idx \viewleq \sview^1$. But we have $\seen\sview^1$ in our proof
context, so we obtain the pointsto assertion as a subjective assertion:
context, so we obtain the points-to assertion as a subjective assertion:
$\nthpointstoNA\refelements{\modcap\idx}-$.
We commit the atomic update now. Indeed the successful CAS is the commit
......@@ -604,12 +604,12 @@ since $\True$ is the return value of the operation.
Along the way, we also collect the persistent assertion $\seen\eview$ from the
precondition of the logically atomic triple.
Finally, we keep on our side the write~token, the nonatomic pointsto assertion
Finally, we keep on our side the write~token, the non-atomic points-to assertion
$\nthpointstoNA\refelements{\modcap\idx}-$,
we reconstruct the invariant, updated for the new value of \refhead, and we close it.
The next step of the program writes the value~$\elem$ to the nonatomic item field,
which is easy since we have the pointsto assertion at hand. This assertion then becomes
The next step of the program writes the value~$\elem$ to the non-atomic item field,
which is easy since we have the points-to assertion at hand. This assertion then becomes
$\nthpointstoNA\refelements{\modcap\idx}\elem$.
We turn it back to an objective assertion, which gives us a view~$\viewB$ and
two assertions $\seen\viewB$ and
......@@ -648,7 +648,7 @@ We then switch to the left disjunct, by constituting the assertion:
}
\]%
%
Hence we return the nonatomic pointsto assertion and the write~token to the
Hence we return the non-atomic points-to assertion and the write~token to the
invariant before closing it.
% FP: ça me paraît bien, tout ça.
......
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