PMP changes need an SFENCE when VM is enabled

src/machine.tex

@@ -2905,3 +2905,28 @@ \subsubsection*{Priority and Matching Logic}
 the PMP check.  The same behavior may manifest for floating-point stores wider
 than XLEN bits (e.g., the FSD instruction in RV32D), even when the store
 address is naturally aligned.
+
+\subsection{Physical Memory Protection and Paging}
+
+The Physical Memory Protection mechanism is designed to compose with the
+page-based virtual memory systems described in Chapter~\ref{supervisor}.  When
+paging is enabled, instructions that access virtual memory may result in
+multiple physical-memory accesses, including implicit references to the page
+tables.  The PMP checks apply to all of these accesses.  The effective
+privilege mode for implicit page-table accesses is S.
+
+Implementations with virtual memory are permitted to perform address
+translations speculatively and earlier than required by an explicit
+virtual-memory access.  The PMP settings for the resulting physical address
+may be checked at any point between the address translation and the explicit
+virtual-memory access.  Hence, when the PMP settings are modified in a manner
+that affects either the physical memory that holds the page tables or the
+physical memory to which the page tables point, M-mode software must
+synchronize the PMP settings with the virtual memory system.  This is
+accomplished by executing an SFENCE.VMA instruction with {\em rs1}={\tt x0}
+and {\em rs2}={\tt x0}, after the PMP CSRs are written.  Note, SFENCE.VMA is
+only guaranteed to synchronize the PMP settings with the virtual memory system
+when it is executed in M-mode.
+
+If page-based virtual memory is not implemented, or when it is disabled,
+memory accesses check the PMP settings synchronously, so no fence is needed.