diff options
| author | Daniel Lustig <dlustig@nvidia.com> | 2018-07-05 15:53:50 -0700 |
|---|---|---|
| committer | Daniel Lustig <dlustig@nvidia.com> | 2018-07-05 16:01:52 -0700 |
| commit | 1d39eabb487a6da5d164f0248a154ffbc3ed6e7b (patch) | |
| tree | 67f8f6459b7e6a917b120e3d47d085d0a04ca93a /src/memory.tex | |
| parent | b170645fa6f8143b5927cccb27a740064589ba35 (diff) | |
| download | riscv-isa-manual-1d39eabb487a6da5d164f0248a154ffbc3ed6e7b.zip riscv-isa-manual-1d39eabb487a6da5d164f0248a154ffbc3ed6e7b.tar.gz riscv-isa-manual-1d39eabb487a6da5d164f0248a154ffbc3ed6e7b.tar.bz2 | |
Version the appendices.
Also, clarify that they should be considered commentary.
Diffstat (limited to 'src/memory.tex')
| -rw-r--r-- | src/memory.tex | 14 |
1 files changed, 9 insertions, 5 deletions
diff --git a/src/memory.tex b/src/memory.tex index 8af6330..fcaa9c6 100644 --- a/src/memory.tex +++ b/src/memory.tex @@ -9,10 +9,13 @@ \selectfont} \makeatother -\chapter{RVWMO Explanatory Material} +\chapter{RVWMO Explanatory Material, Version 0.1} \label{sec:memorymodelexplanation} -This section provides more explanation for the RVWMO (Chapter~\ref{ch:memorymodel}), using more informal language and concrete examples. +This section provides more explanation for RVWMO (Chapter~\ref{ch:memorymodel}), using more informal language and concrete examples. These are intended to clarify the meaning and intent of the axioms and preserved program order rules. +This appendix should be treated as commentary; all normative material is provided in Chapter~\ref{ch:memorymodel} and in the rest of the main body of the ISA specification. +All currently known discrepancies are listed in Section~\ref{sec:memory:discrepancies}. +Any other discrepancies are unintentional. \section{Why RVWMO?} \label{sec:whyrvwmo} @@ -1402,11 +1405,12 @@ In other words, in {\sf herd} syntax, we may choose to add ``{\tt (po-loc \& rsw Many implementations will already enforce this ordering naturally. As such, even though this rule is not official, we recommend that implementers enforce it nevertheless in order to ensure forwards compatibility with the possible future addition of this rule to RVWMO. -\chapter{Formal Memory Model Specifications} - +\chapter{Formal Memory Model Specifications, Version 0.1} To facilitate formal analysis of RVWMO, this chapter presents a set of formalizations using different tools and modeling approaches. Any discrepancies are unintended; the expectation is that the models describe exactly the same sets of legal behaviors. -All currently-known discrepancies are listed in Section~\ref{sec:memory:discrepancies}. +This appendix should be treated as commentary; all normative material is provided in Chapter~\ref{ch:memorymodel} and in the rest of the main body of the ISA specification. +All currently known discrepancies are listed in Section~\ref{sec:memory:discrepancies}. +Any other discrepancies are unintentional. \clearpage \input{memory-model-alloy.tex} |