Add commentary about multi-hit/failing to SFENCE.VMA

src/supervisor.tex

@@ -1073,6 +1073,24 @@ \subsection{Supervisor Memory-Management Fence Instruction}
 memory locations, an SFENCE.VMA instruction must be executed after the writes
 to flush the relevant cached translations.
 
+\begin{commentary}
+A consequence of this specification is that an implementation may use any
+translation for an address that was valid at any time since the most recent
+SFENCE.VMA that subsumes that address.
+In particular, if a leaf PTE is modified but a subsuming SFENCE.VMA is not
+executed, either the old translation or the new translation will be used, but
+the choice is unpredictable.
+The behavior is otherwise well-defined.
+
+In a conventional TLB design, it is possible for multiple entries to match a
+single address if, for example, a page is upgraded to a superpage without first
+clearing the original non-leaf PTE's valid bit and executing an SFENCE.VMA with
+{\em rs1}={\tt x0}.
+In this case, a similar remark applies: it is unpredictable whether the old
+non-leaf PTE or the new leaf PTE is used, but the behavior is otherwise well
+defined.
+\end{commentary}
+
 Implementations must only perform implicit reads of the translation
 data structures pointed to by the current contents of the {\tt satp}
 register, and must only raise exceptions for implicit accesses that are