Fix HFENCE definitions to include all stores, not just local ones

1 files changed, 7 insertions, 7 deletions

diff --git a/src/hypervisor.tex b/src/hypervisor.tex
index 3ab9102..e8cf7c2 100644
--- a/src/hypervisor.tex
+++ b/src/hypervisor.tex
@@ -858,10 +858,10 @@ controlled by the foreground {\tt satp}.
 If an HFENCE.BVMA instruction executes without trapping, its effect is much the
 same as temporarily entering VS-mode (with the usual swapping of foreground and
 background supervisor registers) and executing SFENCE.VMA.
-Executing an HFENCE.BVMA guarantees that any explicit stores in the instruction
-stream prior to the HFENCE.BVMA are ordered before implicit reads of VS-level
-memory-management data structures when those implicit reads are for
-instructions that
+Executing an HFENCE.BVMA guarantees that any previous stores already visible
+to the current hart are ordered before all subsequent implicit reads by that
+hart of the VS-level memory-management data structures, when those implicit
+reads are for instructions that
 \begin{compactitem}
 \item
 are subsequent to the HFENCE.BVMA, and
@@ -895,9 +895,9 @@ virtual machines, or even a global fence for all memory-management data
 structures.
 \end{commentary}
 
-Executing an HFENCE.GVMA instruction guarantees that any explicit stores in the
-instruction stream prior to the HFENCE.GVMA are ordered before all implicit
-reads of guest-physical memory-management data structures done for instructions
+Executing an HFENCE.GVMA instruction guarantees that any previous stores
+already visible to the current hart are ordered before all subsequent implicit
+reads by that hart of guest-physical memory-management data structures done for instructions
 that follow the HFENCE.GVMA.
 If operand {\em rs1}$\neq${\tt x0}, it specifies a single guest physical
 address, shifted right by 2~bits, and if operand {\em rs2}$\neq${\tt x0}, it