Updates

Author: madeline-underwood

content/learning-paths/servers-and-cloud-computing/memory_consistency/examples.md

@@ -20,7 +20,7 @@ Though these other atomic instructions are outside the scope of this Learning Pa
 
 ## Litmus7 Switches
 
-As `litmus7` executes code on a machine, it first needs to build the assembly snippets into executable code. By default, `litmus7` compiles with GCC's standard options. When you run on an Arm Neoverse platform however, it is strongly recommend that you use the switch `-ccopts="-mcpu=native"`. This is the simplest way to avoid all possible runtime failures. 
+As `litmus7` executes code on a machine, it first needs to build the assembly snippets into executable code. By default, `litmus7` compiles with GCC's standard options. When you run on an Arm Neoverse platform however, it is strongly recommended that you use the switch `-ccopts="-mcpu=native"`. This is the simplest way to avoid all possible runtime failures. 
 
 For example, if you execute the Compare and Swap example below without this switch, it will fail to run because GCC by default, does not emit the Compare and Swap (`CAS`) instruction. Although `CAS` is supported in Armv8.1 of the Arm architecture, GCC still defaults to Armv8.0. In the future, if  GCC updates its default to target a newer version of the Arm architecture (for example, Armv9.0), the `-ccopts` switch will no longer be necessary for tests that use atomic instructions like `CAS`.
 
@@ -62,7 +62,7 @@ States 2
 ```
 You should see the outcome of `(1,0)`. 
 
-Now let's try to run this same test with `litmus7` on your Arm Neoverse instance to see if you get the same outcomes:
+Now try to run this same test with `litmus7` on your Arm Neoverse instance to see if you get the same outcomes:
 
 ```bash
 litmus7 ./test1.litmus
@@ -244,7 +244,7 @@ Histogram (1 states)
 ```
 Only an outcome of `(1,1)` has been observed. More test iterations can be executed to build confidence that this is the only possible result.
 
- Note that when we you ran `litmus7`, you used the switch `-ccopts="-mcpu=native"`. If you didn't, `litmus7` would fail with a message saying that the `CASA` instruction cannot be emitted by the compiler.
+ Note that when you ran `litmus7`, you used the switch `-ccopts="-mcpu=native"`. If you didn't, `litmus7` would fail with a message saying that the `CASA` instruction cannot be emitted by the compiler.
 
 Try changing the `CASA` to a `CAS` (Compare and Swap with no ordering) to see what happens.
 
@@ -272,7 +272,7 @@ AArch64 MP+Loop+ACQ_REL2
 exists
 (1:X0=1 /\ (1:X2=0 \/ 1:X5=0))
 ```
-On `P0`, you are writing to both `w` and `x` before the store-release on address `y`. This ensures that the writes to both `x` and `w` (the payloads) will be ordered before the write to address `y` (the flag). On `P1`, you loop with a load-acquire on address `y` (the flag). Once it is observed to be set, you load the two payload addresses. The load-acquire ensures that you do not read the payload addresses `w` and `x` until the flag is observe to be set. The condition at the bottom has been updated to check for any cases where either `w` or `x` are 0. Either of these being observed as 0 will be an indication of reading the payload before the ready flag is observed to be set (not what we want). Overall, this code should result in only the outcome `(1,1,1)`.
+On `P0`, you are writing to both `w` and `x` before the store-release on address `y`. This ensures that the writes to both `x` and `w` (the payloads) will be ordered before the write to address `y` (the flag). On `P1`, you loop with a load-acquire on address `y` (the flag). Once it is observed to be set, you load the two payload addresses. The load-acquire ensures that you do not read the payload addresses `w` and `x` until the flag is observe to be set. The condition at the bottom has been updated to check for any cases where either `w` or `x` are 0. Either of these being observed as 0 will be an indication of reading the payload before the ready flag is observed to be set (not what you want). Overall, this code should result in only the outcome `(1,1,1)`.
 
 Run this test with `herd7`:
 

content/learning-paths/servers-and-cloud-computing/memory_consistency/litmus_syntax.md

@@ -73,7 +73,9 @@ Now inspect this litmus file to gain a better understanding of the assembly code
     - Addresses need to be stored as 64-bit values, hence the need to use `X` registers for the addresses because they are 64-bit. `W` registers are 32-bit. In fact, register `Wn` is the lower 32-bits of register `Xn`.
     - Writing the litmus tests this way is simpler than using all `X` registers. If all `X` registers are used, the data type of each register needs to be declared on additional lines. For this reason, most tests are written as shown above. The way this is done may be changed in the future to reduce potential confusion around the mixed use of `W` and `X` registers, but all of this is functionally correct.
 
-Before you run this test with `herd7` and `litmus7`, you can hypothesize on what might be observed in registers `X0` (flag) and `X2` (payload) on thread `P1`. Even though Arm machines are not Sequentially Consistent (modern machines usually aren't), start by assuming this to be the case anyway. To reason on the execution of these threads in a Sequentially Consistent way, means to imagine the instructions on `P0` and `P1` are executed in some interleaved order. Further, if you interleave these instructions in all possible permutations, you can figure out all of the possible valid outcomes of registers `X0` (flag) and `X2` (payload) on `P1`. For the example test above, the possible valid outcomes of `(X0,X2)` (or `(flag,data)`) are `(0,0)`, `(0,1)`, & `(1,1)`. Shown below are some permutations that result in these valid outcomes. These are not all the possible instruction permutations for this test. Listing them all would make this section needlessly long.
+Before you run this test with `herd7` and `litmus7`, you can hypothesize on what might be observed in registers `X0` (flag) and `X2` (payload) on thread `P1`. Even though Arm machines are not Sequentially Consistent (modern machines usually aren't), start by assuming this to be the case anyway. To reason on the execution of these threads in a Sequentially Consistent way, means to imagine the instructions on `P0` and `P1` are executed in some interleaved order. 
+
+Further, if you interleave these instructions in all possible permutations, you can figure out all of the possible valid outcomes of registers `X0` (flag) and `X2` (payload) on `P1`. For the example test above, the possible valid outcomes of `(X0,X2)` (or `(flag,data)`) are `(0,0)`, `(0,1)`, & `(1,1)`. Some permutations that result in these valid outcomes are shown below. These are not all the possible instruction permutations for this test. Listing them all would make this section needlessly long.
 
 #### A Permutation That Results in `(0,0)`: