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

WIP paper on queue: remove distinction between \atloc and \naloc, as access...

WIP paper on queue: remove distinction between \atloc and \naloc, as access modes are now ascribed to individual cells
parent 8b57dafd
......@@ -5,12 +5,10 @@
& \text{--- Boolean values} \\
n & \in & \mathbf{Z}
& \text{--- integer values} \\
\naloc & \in & \typeNALoc
& \text{--- nonatomic memory locations} \\
\atloc & \in & \typeATLoc
& \text{--- atomic memory locations} \\
\loc & \in & \typeLoc
& \text{--- memory locations} \\
\val & ::= &
\Rec\far\var\expr \mid \Unit \mid b \mid \None \mid \Some\val \mid n \mid \naloc \mid \atloc
\Rec\far\var\expr \mid \Unit \mid b \mid \None \mid \Some\val \mid n \mid \loc
& \text{--- values} \\
\AnyOp\! & \in & \{ \mathord{\PAnd}, \mathord{\POr},
\mathord+, \mathord\times, \mathord{\PMod}, \ldots \,\}
......@@ -28,6 +26,7 @@
\mid \None
\mid \Some\expr
\mid n
\mid \loc
\mid \expr \AnyOp \expr
& \text{--- primitive values and operations} \\
&\mid &
......@@ -45,18 +44,16 @@
&\mid & \Fork\expr
& \text{--- spawning a new thread} \\
% nonatomic store:
&\mid & \naloc
\mid \ArrayAllocNA\expr\expr
&\mid & \ArrayAllocNA\expr\expr
\mid \ArrayReadNA\expr\expr
\mid \ArrayWriteNA\expr\expr\expr
& \text{--- nonatomic locations} \\
& \text{--- operations on nonatomic cells} \\
% atomic store:
&\mid & \atloc
\mid \ArrayAllocAT\expr\expr
&\mid & \ArrayAllocAT\expr\expr
\mid \ArrayReadAT\expr\expr
\mid \ArrayWriteAT\expr\expr\expr
\mid \ArrayCAS\expr\expr\expr\expr
& \text{--- atomic locations}
& \text{--- operations on atomic cells}
\end{array}\]
\[\begin{array}{r@{\;}r@{\;}ll}%
\expr & ::= & \ldots
......@@ -76,13 +73,13 @@
&\mid & \AllocNA\expr
\mid \ReadNA\expr
\mid \WriteNA\expr\expr
& \text{--- nonatomic references} \\
& \text{--- operations on nonatomic references} \\
% atomic store (single cell):
&\mid & \AllocAT\expr
\mid \ReadAT\expr
\mid \WriteAT\expr\expr
\mid \CAS\expr\expr\expr
& \text{--- atomic references}
& \text{--- operations on atomic references}
\end{array}\]
\Description{A BNF definition of the abstract syntax of \mocaml expressions.}
\caption{\mocaml: Syntax}
......
......@@ -22,20 +22,20 @@ a location with $\nbelems$ cells whose access mode is $\accmode$ and whose
initial value is $\val$.
%
Reading from a cell with access mode~$\accmode$ at offset~$\idx$ of
location~$\naloc$ is written $\ArrayReadANY\naloc\idx$.
location~$\loc$ is written $\ArrayReadANY\loc\idx$.
%
Writing a value~$\val$ to a cell with access mode~$\accmode$ at offset~$\idx$ of
location~$\naloc$ is written $\ArrayWriteANY\naloc\idx\val$.
location~$\loc$ is written $\ArrayWriteANY\loc\idx\val$.
%
In addition, atomic cells support the usual compare-and-set operation:
%
$\ArrayCAS\atloc\idx{\val_1}{\val_2}$
reads the atomic cell at offset~$\idx$ of location~$\atloc$,
$\ArrayCAS\loc\idx{\val_1}{\val_2}$
reads the atomic cell at offset~$\idx$ of location~$\loc$,
tests whether its value is equal to $\val_1$, overwrites it with $\val_2$ if that
is the case, and returns the Boolean result of the test; importantly, the
read and the write operations happen \emph{atomically}.
%
There is syntactic sugar for single-cell locations, or ``references'':
$\AllocANY\val$ allocates a location of length~one, $\ReadANY\naloc$ reads at
offset~zero, $\WriteANY\naloc\val$ writes at offset~zero and
$\CAS\atloc{\val_1}{\val_2}$ performs compare-and-set at offset~zero.
$\AllocANY\val$ allocates a location of length~one, $\ReadANY\loc$ reads at
offset~zero, $\WriteANY\loc\val$ writes at offset~zero and
$\CAS\loc{\val_1}{\val_2}$ performs compare-and-set at offset~zero.
......@@ -348,8 +348,9 @@
% canonical variable names:
%\newcommand{\expr}{\ensuremath{e}} % already defined in iris.sty
%\newcommand{\val}{\ensuremath{v}} % already defined in iris.sty
\newcommand{\naloc}{\ensuremath{a}}
\newcommand{\atloc}{\ensuremath{A}}
\newcommand{\loc}{\ensuremath{\ell}}
%\newcommand{\naloc}{\ensuremath{a}}
%\newcommand{\atloc}{\ensuremath{A}}
\newcommand{\accmode}{\ensuremath{\alpha}}
\newcommand{\view}{\ensuremath{\mathcal{V}}}
\newcommand{\altview}{\ensuremath{\mathcal{W}}} % an auxiliary view variable, used in some definitions
......@@ -367,8 +368,9 @@
% types:
\newcommand{\typename}[1]{\text{\textsc{{#1}}}}
\newcommand{\typeNALoc}{\typename{Loc\NA}}
\newcommand{\typeATLoc}{\typename{Loc\AT}}
\newcommand{\typeLoc}{\typename{Loc}}
%\newcommand{\typeNALoc}{\typename{Loc\NA}}
%\newcommand{\typeATLoc}{\typename{Loc\AT}}
\newcommand{\typeTime}{\typename{Time}}
\newcommand{\typeExpr}{\typename{Expr}}
\newcommand{\typeVal}{\typename{Val}}
......
Supports Markdown
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