There is a sentence that uses term `thread 1` to point `P0` in sample
PPCMEM litmus test. Because all other sentences uses term `P0` for the
thread, it would be natural to use the term consistently. This commit
fixes the sentence to use the consistent term.
Signed-off-by: SeongJae Park <sj38.park@xxxxxxxxx>
---
formal/ppcmem.tex | 2 +-
1 file changed, 1 insertion(+), 1 deletion(-)
diff --git a/formal/ppcmem.tex b/formal/ppcmem.tex
index 5dfddd8..e33ba2f 100644
--- a/formal/ppcmem.tex
+++ b/formal/ppcmem.tex
@@ -185,7 +185,7 @@ and line~11 is equivalent to the C statement \co{r3=x}.
which in turn is tested by the \co{bne} instruction. Because actually
modeling the loop would result in state-space explosion, we
instead branch to the Fail: label, terminating the model with
- the initial value of 2 in thread~1's \co{r3} register, which
+ the initial value of 2 in P0's \co{r3} register, which
will not trigger the exists assertion.
There is some debate about whether this trick is universally
--
2.10.0
--
To unsubscribe from this list: send the line "unsubscribe perfbook" in
the body of a message to majordomo@xxxxxxxxxxxxxxx
More majordomo info at http://vger.kernel.org/majordomo-info.html
