Commit 69857ac7 authored by Glen Mével's avatar Glen Mével
Browse files

ICFP21 paper: fix typo in code of pipeline; minor text improvements

parent e47e261e
...@@ -26,7 +26,7 @@ ...@@ -26,7 +26,7 @@
\LetIn \refYQueue {\make\;\Unit} \\ \LetIn \refYQueue {\make\;\Unit} \\
\Fork {(\pname{pipef}\;\nbelems\;\refXArray\;\refYQueue\;f)} ; \\ \Fork {(\pname{pipef}\;\nbelems\;\refXArray\;\refYQueue\;f)} ; \\
\LetIn \refZArray {\ArrayAllocNA \nbelems \Unit} \\ \LetIn \refZArray {\ArrayAllocNA \nbelems \Unit} \\
\pname{pipef}\;\nbelems\;\refYQueue\;\refZArray\;g ; \\ \pname{pipeg}\;\nbelems\;\refYQueue\;\refZArray\;g ; \\
\refZArray \refZArray
} }
\end{codeblock}\) \end{codeblock}\)
......
\section{A Simple Pipeline} \section{A Simple Pipeline}
\label{sec:pipeline} \label{sec:pipeline}
We now demonstrate the use of our specification in Cosmo of a concurrent queue We now demonstrate the use of our specification of a concurrent queue
library with a simple client application, that chains two treatments on a sequence by a simple client application, that chains two treatments on a sequence
of data, where each treatment is applied by a separate thread. Thus the of data, where each treatment is applied in a separate thread. Thus the
sequence of intermediate values is transferred from a producer to a consumer sequence of intermediate values is transferred from a producer to a consumer
using a concurrent queue. using a concurrent queue.
......
...@@ -139,7 +139,7 @@ In other words, we have the monotonicity of the value-view pair stored in a stat ...@@ -139,7 +139,7 @@ In other words, we have the monotonicity of the value-view pair stored in a stat
\status_1 < \status_2 \lor \left( \status_1 = \status_2 \land \sview_1 \viewgeq \sview_2 \right) \status_1 < \status_2 \lor \left( \status_1 = \status_2 \land \sview_1 \viewgeq \sview_2 \right)
\] \]
% %
This stronger monotonicity property will be used in the proof---specifically, when verifying \trydequeue---and specifying it is thus an additional requirement of working with a weak memory model. This stronger monotonicity property will be used in proofs, and specifying it is thus an additional requirement of working with a weak memory model.
To reflect monotonicity of the status of offset~$\offset$, To reflect monotonicity of the status of offset~$\offset$,
we use two assertions, we use two assertions,
...@@ -161,7 +161,7 @@ Rule~\ruleWitnessPers is the persistency just mentioned. ...@@ -161,7 +161,7 @@ Rule~\ruleWitnessPers is the persistency just mentioned.
% %
Rule~\ruleWitnessOrder asserts that a witness gives a lower bound on what the status cell currently stores. Rule~\ruleWitnessOrder asserts that a witness gives a lower bound on what the status cell currently stores.
% %
Rule~\ruleWitnessUpd asserts that we can update a status cell to any larger or equal content, and obtain a witness for that content. Rule~\ruleWitnessUpd asserts that we can update a status cell to any larger (or equal) content, and obtain a witness for that content.
We achieve these properties by constructing an adequate CMRA for the values taken by the ghost variable~$\gmonos$. Again, we will not explain standard Iris constructs here, except for one point. We achieve these properties by constructing an adequate CMRA for the values taken by the ghost variable~$\gmonos$. Again, we will not explain standard Iris constructs here, except for one point.
% %
...@@ -296,7 +296,7 @@ when updating the status. ...@@ -296,7 +296,7 @@ when updating the status.
%\input{figure-queue-ghost-token} %\input{figure-queue-ghost-token}
This time frame is also when the last piece of ghost state, stored in the ghost This time frame---when a slot is in a temporary state---is also when the last piece of ghost state, stored in the ghost
variable~$\gtokens$, intervenes. variable~$\gtokens$, intervenes.
Other threads can make the queue progress between the moment when an enqueuer is Other threads can make the queue progress between the moment when an enqueuer is
attributed rank~$\idx$, and the moment when it returns the updated slot to the attributed rank~$\idx$, and the moment when it returns the updated slot to the
......
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