diff options
| author | Bill Traynor <wmat@riscv.org> | 2023-01-08 11:13:35 -0500 |
|---|---|---|
| committer | Bill Traynor <wmat@riscv.org> | 2023-01-08 11:13:35 -0500 |
| commit | 0552f9c837e8b0e3a397a66e4ed82fc99d13a4a1 (patch) | |
| tree | 228a35eb9a4d9f9ae7d863d836d5108a9b810809 /src/mm-formal.adoc | |
| parent | d0fa7fb97bf6dfc304cb31b68c4e635cefc25430 (diff) | |
| download | riscv-isa-manual-0552f9c837e8b0e3a397a66e4ed82fc99d13a4a1.zip riscv-isa-manual-0552f9c837e8b0e3a397a66e4ed82fc99d13a4a1.tar.gz riscv-isa-manual-0552f9c837e8b0e3a397a66e4ed82fc99d13a4a1.tar.bz2 | |
Deleted the word souce on blocks where it's implied.
Adding a source type to a block implies it's source.
So the source indicator isn't required. My put it back
for easier understanding.
Diffstat (limited to 'src/mm-formal.adoc')
| -rw-r--r-- | src/mm-formal.adoc | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/src/mm-formal.adoc b/src/mm-formal.adoc index 4625eaa..2ff0bf2 100644 --- a/src/mm-formal.adoc +++ b/src/mm-formal.adoc @@ -25,7 +25,7 @@ The online material also contains some litmus tests and some examples of how Alloy can be used to model check some of the mappings in <<memory_porting>>. .The RVWMO memory model formalized in Alloy (1/5: PPO) -[source%linenums,c] +[%linenums,c] ---- // =RVWMO PPO= @@ -58,7 +58,7 @@ fact { ppo in ^gmo } ---- .The RVWMO memory model formalized in Alloy (2/5: Axioms) -[source%linenums,io] +[%linenums,io] .... // =RVWMO axioms= @@ -91,7 +91,7 @@ pred RISCV_mm { LoadValue and Atomicity /* and Progress */ } .The RVWMO memory model formalized in Alloy (3/5: model of memory) -[source%linenums,sml] +[%linenums,sml] .... //Basic model of memory |