diff options
| -rw-r--r-- | src/mm-formal.adoc | 6 |
1 files changed, 4 insertions, 2 deletions
diff --git a/src/mm-formal.adoc b/src/mm-formal.adoc index e717e22..1f8fe72 100644 --- a/src/mm-formal.adoc +++ b/src/mm-formal.adoc @@ -462,14 +462,16 @@ operation) with the release-RCpc or release-RCsc annotation. A model state consists of a shared memory and a tuple of hart states. + +. Model states [cols="^,^,^",] |=== -| |*…* |Hart latexmath:[$n$] +|Hart 0 |*…* |Hart latexmath:[$n$] |latexmath:[$\big\uparrow$] latexmath:[$\big\downarrow$] | |latexmath:[$\big\uparrow$] latexmath:[$\big\downarrow$] -|Shared Memory | | +2+|Shared Memory |=== The shared memory state records all the memory store operations that |