Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

[basic.atomics] Use math mode for memory model placeholders. #3553

Merged
merged 1 commit into from
Dec 19, 2019
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
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