Speculative implicit reads, v2 (#724)

* Speculative implicit reads, v2

These constraints are better expressed as PMAs, and so we relax the
unprivileged spec to always allow speculative implicit reads "unless
otherwise specified", then move the constraints into the PMAs.

This proposal piggybacks on the non-idempotence PMA, constraining implicit
reads to within a power-of-2 region of a non-speculative implicit read.
Furthermore, speculative instruction fetch can also access the subsequent
power-of-2 region.

* Add preface entry

1 files changed, 15 insertions, 0 deletions

diff --git a/src/machine.tex b/src/machine.tex
index 28c3dae..76b5f4c 100644
--- a/src/machine.tex
+++ b/src/machine.tex
@@ -3276,6 +3276,21 @@ misaligned access using multiple smaller accesses, which could cause
 unexpected side effects.
 \end{commentary}
 
+For non-idempotent regions, implicit reads and writes must not be performed
+early or speculatively, with the following exceptions.
+When a non-speculative implicit read is performed, an implementation is
+permitted to additionally read any of the bytes within a naturally aligned
+power-of-2 region containing the address of the non-speculative implicit read.
+Furthermore, when a non-speculative instruction fetch is performed, an
+implementation is permitted to additionally read any of the bytes within the
+{\em next} naturally aligned power-of-2 region of the same size (with the
+address of the region taken modulo $2^{\text{XLEN}}$).
+The results of these additional reads may be used to satisfy subsequent early
+or speculative implicit reads.
+The size of these naturally aligned power-of-2 regions is
+implementation-defined, but, for systems with page-based virtual memory, must
+not exceed the smallest supported page size.
+
 \section{Physical Memory Protection}
 \label{sec:pmp}