Add formal API-level memory consistency model

content/context_intro.tex

@@ -65,8 +65,8 @@
 
 \apitablerow{\LibConstRef{SHMEM\_CTX\_NOSTORE}}{
     Quiet and fence operations performed on the given context are not
-    required to enforce completion and ordering of memory store
-    operations performed by the application.
-    When ordering of store operations is needed, the application must
+    required to enforce completion and ordering of memory accesses
+    performed by the application.
+    When ordering of memory accesses is needed, the application must
     perform a synchronization operation on a context without the
     \CONST{SHMEM\_CTX\_NOSTORE} option enabled.}

content/library_constants.tex

@@ -80,7 +80,7 @@
 \LibConstDecl{SHMEM\_CTX\_NOSTORE} &
 The context creation option which specifies that quiet and fence operations
 performed on the given context are not required to enforce completion and
-ordering of memory store operations.
+ordering of memory accesses.
 See Section~\ref{subsec:shmem_ctx_create} for more detail about its use.
 \tabularnewline \hline
 %%

content/shmem_barrier_all.tex

@@ -1,7 +1,7 @@
 \apisummary{
     Registers the arrival of a \ac{PE} at a barrier and blocks the \ac{PE}
     until all other \acp{PE} arrive at the barrier and all local
-    updates and remote memory updates on the default context are completed.
+    memory accesses and remote memory updates on the default context are completed.
 }
 
 \begin{apidefinition}
@@ -25,7 +25,7 @@
     it may not be called concurrently by multiple threads in the same \ac{PE}.
 
     Prior to synchronizing with other \acp{PE}, \FUNC{shmem\_barrier\_all}
-    ensures completion of all previously issued memory stores and remote memory
+    ensures completion of all previously issued memory accesses and remote memory
     updates issued on the default context via \openshmem \acp{AMO} and
     \ac{RMA} routine calls such
     as \FUNC{shmem\_int\_add}, \FUNC{shmem\_put32},

content/shmem_fence.tex

@@ -1,5 +1,5 @@
 \apisummary{
-    Ensures ordering of delivery of operations on symmetric data objects.
+    Ensures ordering of delivery of operations on symmetric data objects, as well as ordering of prior memory accesses.
 }
 
 \begin{apidefinition}
@@ -17,7 +17,7 @@
 
 \apidescription{
     This routine ensures ordering of delivery of operations on symmetric data
-    objects.
+    objects and ordering of prior memory accesses.
     Table~\ref{mem-order} lists the operations that are ordered
     by the \FUNC{shmem\_fence} routine.
     All operations on symmetric data objects issued to a particular
@@ -36,8 +36,10 @@
 }
 
 \apinotes{
-    \FUNC{shmem\_fence} only provides per-\ac{PE} ordering guarantees and does not
-    guarantee completion of delivery.
+    \FUNC{shmem\_fence} orders prior remote operations with subsequent remote operations to the same \ac{PE}.
+    It also orders all prior normal memory accesses with subsequent remote observable accesses to any \ac{PE}.
+    For ordering of remote operations, \FUNC{shmem\_fence} does not guarantee the completion of prior remote operations;
+    only that their delivery will be ordered with subsequent operations.
     \FUNC{shmem\_fence} also does not have an effect on the ordering between memory
     accesses issued by the target \ac{PE}. \FUNC{shmem\_wait\_until}, \FUNC{shmem\_test},
     \FUNC{shmem\_barrier}, \FUNC{shmem\_barrier\_all} routines can be called by the target \ac{PE} to guarantee
@@ -55,8 +57,8 @@
     In an \openshmem program with multithreaded \acp{PE}, it is the
     user's responsibility to ensure ordering between operations issued by the threads
     in a \ac{PE} that target symmetric memory and calls by threads in that \ac{PE} to
-    \FUNC{shmem\_fence}. The \FUNC{shmem\_fence} routine can enforce memory store ordering only for the
-    calling thread. Thus, to ensure ordering for memory stores performed by a thread that is
+    \FUNC{shmem\_fence}. The \FUNC{shmem\_fence} routine can enforce memory access ordering only for the
+    calling thread. Thus, to ensure ordering for memory accesses performed by a thread that is
     not the thread calling \FUNC{shmem\_fence}, the update must be made visible to the
     calling thread according to the rules of the memory model associated with
     the threading environment.

content/shmem_quiet.tex

@@ -1,6 +1,6 @@
 \apisummary{
     Waits for completion of outstanding operations on symmetric data objects
-    issued by a \ac{PE}.
+    issued by a \ac{PE}, as well as prior memory accesses.
 }
 
 \begin{apidefinition}
@@ -34,7 +34,9 @@
 \apinotes{
     \FUNC{shmem\_quiet} is most useful as a way of ensuring completion of
     several operations on symmetric data objects initiated by the calling
-    \ac{PE}. For example, one might use \FUNC{shmem\_quiet} to await delivery
+    \ac{PE}. 
+    It also ensures completion prior memory accesses.
+    For example, one might use \FUNC{shmem\_quiet} to await delivery
     of a block of data before issuing another \PUT{} or nonblocking
     \PUT{} routine, which sets a completion flag on another \ac{PE}.
     \FUNC{shmem\_quiet} is not usually needed if
@@ -46,8 +48,8 @@
     user's responsibility to ensure ordering between operations issued by the
     threads in a \ac{PE} that target symmetric memory and calls by threads in
     that \ac{PE} to \FUNC{shmem\_quiet}. The \FUNC{shmem\_quiet} routine can
-    enforce memory store ordering only for the calling thread. Thus, to ensure
-    ordering for memory stores performed by a thread that is not the thread
+    enforce memory access ordering only for the calling thread. Thus, to ensure
+    ordering for memory accesses performed by a thread that is not the thread
     calling \FUNC{shmem\_quiet}, the update must be made visible to the calling
     thread according to the rules of the memory model associated with the
     threading environment.
@@ -61,6 +63,8 @@
     when using POSIX Threads, the user may call the
     \FUNC{pthread\_barrier\_wait} routine to ensure that all threads have issued
     operations before a thread calls \FUNC{shmem\_quiet}.
+    Section~\ref{subsubsec:api_relations} provides further details about
+    establishing ordering with accesses and operations in other threads.
 
     \FUNC{shmem\_quiet} does not have an effect on the ordering between memory
     accesses issued by the target \ac{PE}. \FUNC{shmem\_wait\_until},

main_spec.tex

@@ -19,6 +19,9 @@ \section{Programming Model Overview}\label{subsec:programming_model}
 \section{Memory Model}\label{subsec:memory_model}
 \input{content/memory_model}
 
+\subsection{Formal API Memory Model}\label{subsec:api_mem_model}
+\input{content/api_mem_model}
+
 \section{Execution Model}\label{subsec:execution_model}
 \input{content/execution_model}
 
@@ -431,10 +434,11 @@ \subsection{Memory Ordering Routines}\label{subsec:memory_order}
 \begin{longtable}{|l|c|c|}
  \hline
   Operations & Fence & Quiet \\ \hline
-  Memory Store \footnote{Ordering and/or delivery of memory store operations are
+  Memory Store \footnote{Ordering and/or delivery of prior memory accesses are
   ensured only on contexts created with certain options. For details, refer the
-  description of context options in Section~\ref{subsec:shmem_ctx_create}.}
+	description of context options in Section~\ref{subsec:shmem_ctx_create}\label{fnst}.}
                                      & X & X \\
+  Memory Load \footref{fnst}         & X & X \\
   Blocking \OPR{Put}                 & X & X \\
   Blocking \OPR{Get}                 &   &   \\
   Blocking \OPR{\acs{AMO}}           & X & X \\

utils/defs.tex

@@ -69,6 +69,22 @@
 \newcommand{\jth}{${\textit{j}^{\text{\tiny th}}}$}
 \newcommand{\kth}{${\textit{k}^{\text{\tiny th}}}$}
 \newcommand{\lth}{${\textit{l}^{\text{\tiny th}}}$}
+% formal mem model
+\newcommand{\EVENT}[1]{\textit{#1}}
+\newcommand{\REL}[1]{\textit{#1}}
+\newcommand{\relSB}{\textit{sequenced-before}}
+\newcommand{\relMO}{\textit{modification-order}}
+\newcommand{\relRF}{\textit{reads-from}}
+\newcommand{\relSW}{\textit{synchronizes-with}}
+\newcommand{\relHB}{\textit{happens-before}}
+\newcommand{\relDR}{\textit{data race}}
+\newcommand{\relILV}{\textit{implicit local visibility}}
+\newcommand{\relLCO}{\textit{local completion order}}
+\newcommand{\relRDO}{\textit{remote delivery order}}
+\newcommand{\relRCO}{\textit{remote completion order}}
+\newcommand{\relASW}{\textit{API synchronizes with}}
+\newcommand{\relAHB}{\textit{API happens-before}}
+\newcommand{\relADR}{\textit{API data race}}
 
 %% Generate indexed reference.
 \newcommand{\EnvVarIndex}[1]{\index{#1}}

utils/packages.tex

@@ -51,6 +51,7 @@
 \usepackage{draftcopy}
 \usepackage{draftwatermark}
 \usepackage{wrapfig}
+\usepackage{fancyvrb}
 \usepackage{longtable}
 \usepackage{caption}
 \usepackage{subcaption}