Skip to content

Commit

Permalink
[basic.atomics] Use math mode for memory model placeholders.
Browse files Browse the repository at this point in the history
  • Loading branch information
jensmaurer authored and zygoloid committed Dec 19, 2019
1 parent 108bb54 commit 3f09e6b
Show file tree
Hide file tree
Showing 2 changed files with 181 additions and 184 deletions.
132 changes: 66 additions & 66 deletions source/atomics.tex
Original file line number Diff line number Diff line change
Expand Up @@ -419,78 +419,78 @@
\end{note}

\pnum
An atomic operation \placeholder{A} that performs a release operation on an atomic
object \placeholder{M} synchronizes with an atomic operation \placeholder{B} that performs
an acquire operation on \placeholder{M} and takes its value from any side effect in the
release sequence headed by \placeholder{A}.
An atomic operation $A$ that performs a release operation on an atomic
object $M$ synchronizes with an atomic operation $B$ that performs
an acquire operation on $M$ and takes its value from any side effect in the
release sequence headed by $A$.

\pnum
An atomic operation \placeholder{A} on some atomic object \placeholder{M} is
An atomic operation $A$ on some atomic object $M$ is
\defn{coherence-ordered before}
another atomic operation \placeholder{B} on \placeholder{M} if
another atomic operation $B$ on $M$ if
\begin{itemize}
\item \placeholder{A} is a modification, and
\placeholder{B} reads the value stored by \placeholder{A}, or
\item \placeholder{A} precedes \placeholder{B}
in the modification order of \placeholder{M}, or
\item \placeholder{A} and \placeholder{B} are not
\item $A$ is a modification, and
$B$ reads the value stored by $A$, or
\item $A$ precedes $B$
in the modification order of $M$, or
\item $A$ and $B$ are not
the same atomic read-modify-write operation, and
there exists an atomic modification \placeholder{X} of \placeholder{M}
such that \placeholder{A} reads the value stored by \placeholder{X} and
\placeholder{X} precedes \placeholder{B}
in the modification order of \placeholder{M}, or
\item there exists an atomic modification \placeholder{X} of \placeholder{M}
such that \placeholder{A} is coherence-ordered before \placeholder{X} and
\placeholder{X} is coherence-ordered before \placeholder{B}.
there exists an atomic modification $X$ of $M$
such that $A$ reads the value stored by $X$ and
$X$ precedes $B$
in the modification order of $M$, or
\item there exists an atomic modification $X$ of $M$
such that $A$ is coherence-ordered before $X$ and
$X$ is coherence-ordered before $B$.
\end{itemize}

\pnum
There is a single total order \placeholder{S}
There is a single total order $S$
on all \tcode{memory_order::seq_cst} operations, including fences,
that satisfies the following constraints.
First, if \placeholder{A} and \placeholder{B} are
First, if $A$ and $B$ are
\tcode{memory_order::seq_cst} operations and
\placeholder{A} strongly happens before \placeholder{B},
then \placeholder{A} precedes \placeholder{B} in \placeholder{S}.
Second, for every pair of atomic operations \placeholder{A} and
\placeholder{B} on an object \placeholder{M},
where \placeholder{A} is coherence-ordered before \placeholder{B},
the following four conditions are required to be satisfied by \placeholder{S}:
$A$ strongly happens before $B$,
then $A$ precedes $B$ in $S$.
Second, for every pair of atomic operations $A$ and
$B$ on an object $M$,
where $A$ is coherence-ordered before $B$,
the following four conditions are required to be satisfied by $S$:
\begin{itemize}
\item if \placeholder{A} and \placeholder{B} are both
\item if $A$ and $B$ are both
\tcode{memory_order::seq_cst} operations,
then \placeholder{A} precedes \placeholder{B} in \placeholder{S}; and
\item if \placeholder{A} is a \tcode{memory_order::seq_cst} operation and
\placeholder{B} happens before
a \tcode{memory_order::seq_cst} fence \placeholder{Y},
then \placeholder{A} precedes \placeholder{Y} in \placeholder{S}; and
\item if a \tcode{memory_order::seq_cst} fence \placeholder{X}
happens before \placeholder{A} and
\placeholder{B} is a \tcode{memory_order::seq_cst} operation,
then \placeholder{X} precedes \placeholder{B} in \placeholder{S}; and
\item if a \tcode{memory_order::seq_cst} fence \placeholder{X}
happens before \placeholder{A} and
\placeholder{B} happens before
a \tcode{memory_order::seq_cst} fence \placeholder{Y},
then \placeholder{X} precedes \placeholder{Y} in \placeholder{S}.
then $A$ precedes $B$ in $S$; and
\item if $A$ is a \tcode{memory_order::seq_cst} operation and
$B$ happens before
a \tcode{memory_order::seq_cst} fence $Y$,
then $A$ precedes $Y$ in $S$; and
\item if a \tcode{memory_order::seq_cst} fence $X$
happens before $A$ and
$B$ is a \tcode{memory_order::seq_cst} operation,
then $X$ precedes $B$ in $S$; and
\item if a \tcode{memory_order::seq_cst} fence $X$
happens before $A$ and
$B$ happens before
a \tcode{memory_order::seq_cst} fence $Y$,
then $X$ precedes $Y$ in $S$.
\end{itemize}

\pnum
\begin{note}
This definition ensures that \placeholder{S} is consistent with
the modification order of any atomic object \placeholder{M}.
This definition ensures that $S$ is consistent with
the modification order of any atomic object $M$.
It also ensures that
a \tcode{memory_order::seq_cst} load \placeholder{A} of \placeholder{M}
gets its value either from the last modification of \placeholder{M}
that precedes \placeholder{A} in \placeholder{S} or
from some non-\tcode{memory_order::seq_cst} modification of \placeholder{M}
that does not happen before any modification of \placeholder{M}
that precedes \placeholder{A} in \placeholder{S}.
a \tcode{memory_order::seq_cst} load $A$ of $M$
gets its value either from the last modification of $M$
that precedes $A$ in $S$ or
from some non-\tcode{memory_order::seq_cst} modification of $M$
that does not happen before any modification of $M$
that precedes $A$ in $S$.
\end{note}

\pnum
\begin{note}
We do not require that \placeholder{S} be consistent with
We do not require that $S$ be consistent with
``happens before''\iref{intro.races}.
This allows more efficient implementation
of \tcode{memory_order::acquire} and \tcode{memory_order::release}
Expand Down Expand Up @@ -3522,27 +3522,27 @@
fence}.

\pnum
A release fence \placeholder{A} synchronizes with an acquire fence \placeholder{B} if there exist
atomic operations \placeholder{X} and \placeholder{Y}, both operating on some atomic object
\placeholder{M}, such that \placeholder{A} is sequenced before \placeholder{X}, \placeholder{X} modifies
\placeholder{M}, \placeholder{Y} is sequenced before \placeholder{B}, and \placeholder{Y} reads the value
written by \placeholder{X} or a value written by any side effect in the hypothetical release
sequence \placeholder{X} would head if it were a release operation.
A release fence $A$ synchronizes with an acquire fence $B$ if there exist
atomic operations $X$ and $Y$, both operating on some atomic object
$M$, such that $A$ is sequenced before $X$, $X$ modifies
$M$, $Y$ is sequenced before $B$, and $Y$ reads the value
written by $X$ or a value written by any side effect in the hypothetical release
sequence $X$ would head if it were a release operation.

\pnum
A release fence \placeholder{A} synchronizes with an atomic operation \placeholder{B} that
performs an acquire operation on an atomic object \placeholder{M} if there exists an atomic
operation \placeholder{X} such that \placeholder{A} is sequenced before \placeholder{X}, \placeholder{X}
modifies \placeholder{M}, and \placeholder{B} reads the value written by \placeholder{X} or a value
written by any side effect in the hypothetical release sequence \placeholder{X} would head if
A release fence $A$ synchronizes with an atomic operation $B$ that
performs an acquire operation on an atomic object $M$ if there exists an atomic
operation $X$ such that $A$ is sequenced before $X$, $X$
modifies $M$, and $B$ reads the value written by $X$ or a value
written by any side effect in the hypothetical release sequence $X$ would head if
it were a release operation.

\pnum
An atomic operation \placeholder{A} that is a release operation on an atomic object
\placeholder{M} synchronizes with an acquire fence \placeholder{B} if there exists some atomic
operation \placeholder{X} on \placeholder{M} such that \placeholder{X} is sequenced before \placeholder{B}
and reads the value written by \placeholder{A} or a value written by any side effect in the
release sequence headed by \placeholder{A}.
An atomic operation $A$ that is a release operation on an atomic object
$M$ synchronizes with an acquire fence $B$ if there exists some atomic
operation $X$ on $M$ such that $X$ is sequenced before $B$
and reads the value written by $A$ or a value written by any side effect in the
release sequence headed by $A$.

\indexlibraryglobal{atomic_thread_fence}%
\begin{itemdecl}
Expand Down
Loading

0 comments on commit 3f09e6b

Please sign in to comment.