Clarify forbidden execution scenarios in A.1 litmus test (#809)

Updates description of forbidden execution where a0=1 in the figure A.1
litmus test by specifying that (c) reads the value written by (a) in
both scenarios.

Signed-off-by: hasheddan <georgedanielmangum@gmail.com>

1 files changed, 1 insertions, 1 deletions

diff --git a/src/memory.tex b/src/memory.tex
index 2cab253..ae3013f 100644
--- a/src/memory.tex
+++ b/src/memory.tex
@@ -108,7 +108,7 @@ This notation is explained in Table~\ref{tab:litmus:key}.
 Of the listed relations, {\sf rf} edges between harts, {\sf co} edges, {\sf fr} edges, and {\sf ppo} edges directly constrain the global memory order (as do {\sf fence}, {\sf addr}, {\sf data}, and some {\sf ctrl} edges, via {\sf ppo}).
 Other edges (such as intra-hart {\sf rf} edges) are informative but do not constrain the global memory order.
 
-For example, in Figure~\ref{fig:litmus:sample}, {\tt a0=1} could occur only if one of the following were true:
+For example, in Figure~\ref{fig:litmus:sample}, {\tt a0=1} could occur only if (c) reads the value written by (a) and one of the following were true:
 \begin{itemize}
   \item (b) appears before (a) in global memory order (and in the coherence order {\sf co}).  However, this violates RVWMO PPO rule~\ref{ppo:->st}.  The {\sf co} edge from (b) to (a) highlights this contradiction.
   \item (a) appears before (b) in global memory order (and in the coherence order {\sf co}).  However, in this case, the Load Value Axiom would be violated, because (a) is not the latest matching store prior to (c) in program order.  The {\sf fr} edge from (c) to (b) highlights this contradiction.