Provide non-normative guidance on HFENCE.GVMA TLB flushing

See #793

1 files changed, 18 insertions, 0 deletions

diff --git a/src/hypervisor.tex b/src/hypervisor.tex
index b46fd62..b8c1994 100644
--- a/src/hypervisor.tex
+++ b/src/hypervisor.tex
@@ -2000,6 +2000,24 @@ address, shifted right by 2~bits, and if operand {\em rs2}$\neq${\tt x0}, it
 specifies a single virtual machine identifier (VMID).
 
 \begin{commentary}
+Conceptually, an implementation might contain two address-translation caches:
+one that maps guest virtual addresses to guest physical addresses, and another
+that maps guest physical addresses to supervisor physical addresses.
+HFENCE.GVMA need not flush the former cache, but it must flush entries from
+the latter cache that match the HFENCE.GVMA's address and VMID arguments.
+
+More commonly, implementations contain address-translation caches that map
+guest virtual addresses directly to supervisor physical addresses, removing
+a level of indirection.
+For such implementations, any entry that was populated using a G-stage
+translation that is ordered by an HFENCE.GVMA instruction must be flushed.
+Because it is often impractical to determine which such entries match the
+HFENCE.GVMA's address argument, a common technique is to flush all entries
+that match the HFENCE.GVMA's VMID argument, regardless of the address
+argument.
+\end{commentary}
+
+\begin{commentary}
 Like for a guest physical address written to {\tt htval} on a
 trap, a guest physical address specified in {\em rs1} is shifted
 right by 2~bits to accommodate addresses wider than the current XLEN.