Specify SFENCE/HFENCE requirements when changing PBMTE (#1111)

src/hypervisor.adoc

@@ -1635,6 +1635,7 @@ VS-stage address translation, a nonzero guest physical address written
 to `mtval2`/`htval` shall correspond to the exact virtual address
 written to `mtval`/`stval`.
 
+[[hyp-mm-fences]]
 ==== Memory-Management Fences
 
 The behavior of the SFENCE.VMA instruction is affected by the current
@@ -1672,6 +1673,24 @@ address-translation cache entries that have cached PMP settings
 corresponding to the final translated supervisor physical address. An
 HFENCE.VVMA instruction is not required.
 
+Similarly, if the setting of the PBMTE bit in `menvcfg` is changed, an
+HFENCE.GVMA instruction with _rs1_=`x0` and _rs2_=`x0` suffices to synchronize
+with respect to the altered interpretation of G-stage and VS-stage PTEs' PBMT
+fields.
+
+By contrast, if the PBMTE bit in `henvcfg` is changed, executing an
+HFENCE.VVMA with _rs1_=`x0` and _rs2_=`x0` suffices to synchronize with
+respect to the altered interpretation of VS-stage PTEs' PBMT fields for the
+currently active VMID.
+
+NOTE: No mechanism is provided to atomically change `vsatp` and `hgatp`
+together.  Hence, to prevent speculative execution causing one guest's
+VS-stage translations to be cached under another guest's VMID, world-switch
+code should zero `vsatp`, then swap `hgatp`, then finally write the new
+`vstap` value.  Similarly, if `henvcfg`.PBMTE need be world-switched, it
+should be switched after zeroing `vsatp` but before writing the new `vsatp`
+value, obviating the need to execute an HFENCE.VVMA instruction.
+
 === Traps
 
 ==== Trap Cause Codes

src/machine.adoc

@@ -2013,6 +2013,12 @@ implemented, PBMTE is read-only zero. Furthermore, for implementations
 with the hypervisor extension, `henvcfg`.PBMTE is read-only zero if
 `menvcfg`.PBMTE is zero.
 
+After changing `menvcfg`.PBMTE, executing an SFENCE.VMA instruction with
+_rs1_=`x0` and _rs2_=`x0` suffices to synchronize address-translation caches
+with respect to the altered interpretation of page-table entries' PBMT fields.
+See <<hyp-mm-fences>> for additional synchronization requirements when the
+hypervisor extension is implemented.
+
 The definition of the STCE field will be furnished by the forthcoming
 Sstc extension. Its allocation within `menvcfg` may change prior to the
 ratification of that extension.
@@ -3098,6 +3104,8 @@ are modified, M-mode software must synchronize the PMP settings with the
 virtual memory system and any PMP or address-translation caches. This is
 accomplished by executing an SFENCE.VMA instruction with _rs1_=`x0` and
 _rs2_=`x0`, after the PMP CSRs are written.
+See <<hyp-mm-fences>> for additional synchronization requirements when the
+hypervisor extension is implemented.
 
 If page-based virtual memory is not implemented, memory accesses check
 the PMP settings synchronously, so no SFENCE.VMA is needed.

src/priv-preface.adoc

@@ -36,6 +36,8 @@ version 1.12:
 
 * Defined the `misa`.V field to reflect that the V extension has been
 implemented.
+* Specified synchronization requirements when changing the PBMTE fields
+in `menvcfg` and `henvcfg`.
 * Clarified semantics of explicit accesses to CSRs wider than XLEN bits.
 * Clarified that MXLEN≥SXLEN, and added the constraint that
 SXLEN≥UXLEN.