Fix minor typos in the operational model. (#277)

1 files changed, 8 insertions, 8 deletions

diff --git a/src/memory-model-operational.tex b/src/memory-model-operational.tex
index d0ce212..a94c8d4 100644
--- a/src/memory-model-operational.tex
+++ b/src/memory-model-operational.tex
@@ -30,7 +30,7 @@ An interactive version of the model, together with a library of litmus tests,
 is provided online: \url{http://www.cl.cam.ac.uk/~pes20/rmem}.
 This is integrated with a fragment of the RISC-V ISA semantics
 (RV64I and A) expressed explicitly in Sail
-(\url{https://github.com/rems-project/sail})).
+(\url{https://github.com/rems-project/sail}).
 % TODO: compare with the herd and alloy versions
 
 
@@ -42,8 +42,8 @@ Terminology: In contrast to the axiomatic presentation, here every memory operat
 Hence, AMOs give rise to two distinct memory operations, a load and a store.
 When used in conjunction with ``instruction'', the terms ``load'' and ``store'' refer to instructions that give rise to such memory operations.
 As such, both include AMO instructions.
-The term ``acquire'' refers to instruction (or its memory operation) with the acquire-RCpc or acquire-RCsc annotation.
-The term ``release'' refers to instruction (or its memory operation) with the release-RCpc or release-RCsc annotation.
+The term ``acquire'' refers to an instruction (or its memory operation) with the acquire-RCpc or acquire-RCsc annotation.
+The term ``release'' refers to an instruction (or its memory operation) with the release-RCpc or release-RCsc annotation.
 
 \paragraph{Model states}
 A model state consists of a shared memory and a tuple of hart states.
@@ -327,9 +327,9 @@ The condition is followed by an action that is applied to that state when the tr
 A possible program-order-successor of instruction instance $i$ can be fetched from address {\it loc} if:
 \begin{enumerate}
 \item it has not already been fetched, i.e., none of the immediate successors of $i$ in the hart's {\it instruction\_tree} are from {\it loc}; and
-\item if $i$'s pseudocode has already wrote an address to {\em pc}, then {\it loc} must be that address, otherwise {\it loc} is:
+\item if $i$'s pseudocode has already written an address to {\em pc}, then {\it loc} must be that address, otherwise {\it loc} is:
   \begin{itemize}
-  \item for a conditional branch, the successor address and the branch target address;
+  \item for a conditional branch, the successor address or the branch target address;
   \item for a (direct) jump and link instruction ({\tt jal}), the target address;
   \item for an indirect jump instruction ({\tt jalr}), any address; and
   \item for any other instruction, $i.\textit{program\_loc}+4$.
@@ -385,7 +385,7 @@ For a non-AMO load instruction instance $i$ in state {\sc Pending\_mem\_loads}({
 \item all program-order-previous store-acquire-release instructions are finished;
 \end{enumerate}
 
-Let $msoss$ be the set of all unpropagated memory store operation slices from non-{\tt sc} store instruction instances that are program-order-before $i$ and have already calculated the value to be stored, that overlap with the unsatisfied slices of $mlo$, and which are not superseded by intervening stores operations or store operations that are read from by an intervening loads.
+Let $msoss$ be the set of all unpropagated memory store operation slices from non-{\tt sc} store instruction instances that are program-order-before $i$ and have already calculated the value to be stored, that overlap with the unsatisfied slices of $mlo$, and which are not superseded by intervening store operations or store operations that are read from by an intervening load.
 The last condition requires, for each memory store operation slice $msos$ in $msoss$ from instruction $i'$:
 \begin{tightlist}
 \item that there is no store instruction program-order-between $i$ and $i'$ with a memory store operation overlapping $msos$; and
@@ -402,8 +402,8 @@ Where, the {\em restart-dependents} of instruction $j$ are:
 \item program-order-successors of $j$ that have data-flow dependency on a register write of $j$;
 \item program-order-successors of $j$ that have a memory load operation that reads from a memory store operation of $j$ (by forwarding);
 \item if $j$ is a load-acquire, all the program-order-successors of $j$;
-\item if $j$ is a load, for every {\tt fence}, $f$, with {\tt .sr} and {\tt .pr} set, and {\tt .pw} not set, that is program-order-successors of $j$, all the load instructions that are program-order-successors of $f$;
-\item if $j$ is a load, for every {\tt fence.tso}, $f$, that is program-order-successors of $j$, all the load instructions that are program-order-successors of $f$;
+\item if $j$ is a load, for every {\tt fence}, $f$, with {\tt .sr} and {\tt .pr} set, and {\tt .pw} not set, that is a program-order-successor of $j$, all the load instructions that are program-order-successors of $f$;
+\item if $j$ is a load, for every {\tt fence.tso}, $f$, that is a program-order-successor of $j$, all the load instructions that are program-order-successors of $f$;
 and \item (recursively) all the restart-dependents of all the instruction instances above.
 \end{tightlist}