5 files changed, 252 insertions, 10 deletions
diff --git a/src/hypervisor.tex b/src/hypervisor.tex
index e93b803..129d14d 100644
--- a/src/hypervisor.tex
+++ b/src/hypervisor.tex
@@ -270,8 +270,8 @@ instruction exception.
 When VTW=1 (and assuming {\tt mstatus}.TW=0), an attempt in VS-mode to
 execute WFI raises a virtual instruction exception if the WFI does not
 complete within an implementation-specific, bounded time limit.
-When VTVM=1, an attempt in VS-mode to execute SFENCE.VMA or to access CSR
-{\tt satp} raises a virtual instruction exception.
+When VTVM=1, an attempt in VS-mode to execute SFENCE.VMA or SINVAL.VMA or to
+access CSR {\tt satp} raises a virtual instruction exception.
 
 The VGEIN (Virtual Guest External Interrupt Number) field selects a guest
 external interrupt source for VS-level external interrupts.
@@ -2043,8 +2043,8 @@ not in VS-mode.
 The TW field affects execution in all modes except M-mode.
 
 Setting TVM=1 prevents HS-mode from accessing {\tt hgatp} or executing
-HFENCE.GVMA, but has no effect on accesses to {\tt vsatp} or instruction
-HFENCE.VVMA.
+HFENCE.GVMA or HINVAL.GVMA, but has no effect on accesses to {\tt vsatp} or
+instructions HFENCE.VVMA or HINVAL.VVMA.
 
 The hypervisor extension changes the behavior of the the Modify Privilege
 field, MPRV, of {\tt mstatus}.
@@ -2696,8 +2696,8 @@ implementation-specific, bounded time;
 in VS-mode, attempts to execute SRET when {\tt hstatus}.VTSR=1; or
 
 \item
-in VS-mode, attempts to execute an SFENCE instruction or to access
-{\tt satp}, when {\tt hstatus}.VTVM=1.
+in VS-mode, attempts to execute an SFENCE.VMA or SINVAL.VMA instruction or to
+access {\tt satp}, when {\tt hstatus}.VTVM=1.
 
 \end{itemize}
 
diff --git a/src/machine.tex b/src/machine.tex
index 6b82746..c133985 100644
--- a/src/machine.tex
+++ b/src/machine.tex
@@ -818,8 +818,8 @@ example by swapping byte order after loads and before stores.
 
 The TVM (Trap Virtual Memory) bit is a \warl\ field that supports intercepting
 supervisor virtual-memory management operations.  When TVM=1,
-attempts to read or write the {\tt satp} CSR or execute the SFENCE.VMA
-instruction while executing in S-mode will raise an illegal instruction
+attempts to read or write the {\tt satp} CSR or execute an SFENCE.VMA or
+SINVAL.VMA instruction while executing in S-mode will raise an illegal instruction
 exception.  When TVM=0, these operations are permitted in S-mode.
 TVM is hard-wired to 0 when S-mode is not supported.
 
@@ -829,8 +829,8 @@ operating systems to execute in S-mode, rather than classically virtualizing
 them in U-mode.  This approach obviates the need to trap accesses to most
 S-mode CSRs.
 
-Trapping {\tt satp} accesses and the SFENCE.VMA instruction provides the
-hooks necessary to lazily populate shadow page tables.
+Trapping {\tt satp} accesses and the SFENCE.VMA and SINVAL.VMA instructions
+provides the hooks necessary to lazily populate shadow page tables.
 \end{commentary}
 
 The TW (Timeout Wait) bit is a \warl\ field that supports intercepting the WFI
diff --git a/src/priv-instr-table.tex b/src/priv-instr-table.tex
index 5603d7b..b424ae3 100644
--- a/src/priv-instr-table.tex
+++ b/src/priv-instr-table.tex
@@ -111,6 +111,36 @@
   
 
 &
+\multicolumn{4}{|c|}{0001011} &
+\multicolumn{2}{c|}{rs2} &
+\multicolumn{1}{c|}{rs1} &
+\multicolumn{1}{c|}{000} &
+\multicolumn{1}{c|}{00000} &
+\multicolumn{1}{c|}{1110011} & SINVAL.VMA \\
+\cline{2-11}
+  
+
+&
+\multicolumn{4}{|c|}{0001100} &
+\multicolumn{2}{c|}{00000} &
+\multicolumn{1}{c|}{00000} &
+\multicolumn{1}{c|}{000} &
+\multicolumn{1}{c|}{00000} &
+\multicolumn{1}{c|}{1110011} & SFENCE.W.INVAL \\
+\cline{2-11}
+  
+
+&
+\multicolumn{4}{|c|}{0001100} &
+\multicolumn{2}{c|}{00001} &
+\multicolumn{1}{c|}{00000} &
+\multicolumn{1}{c|}{000} &
+\multicolumn{1}{c|}{00000} &
+\multicolumn{1}{c|}{1110011} & SFENCE.INVAL.IR \\
+\cline{2-11}
+  
+
+&
 \multicolumn{10}{c}{} & \\
 &
 \multicolumn{10}{c}{\bf Hypervisor Memory-Management Instructions} & \\
@@ -138,6 +168,26 @@
   
 
 &
+\multicolumn{4}{|c|}{0010011} &
+\multicolumn{2}{c|}{rs2} &
+\multicolumn{1}{c|}{rs1} &
+\multicolumn{1}{c|}{000} &
+\multicolumn{1}{c|}{00000} &
+\multicolumn{1}{c|}{1110011} & HINVAL.VVMA \\
+\cline{2-11}
+  
+
+&
+\multicolumn{4}{|c|}{0110011} &
+\multicolumn{2}{c|}{rs2} &
+\multicolumn{1}{c|}{rs1} &
+\multicolumn{1}{c|}{000} &
+\multicolumn{1}{c|}{00000} &
+\multicolumn{1}{c|}{1110011} & HINVAL.GVMA \\
+\cline{2-11}
+  
+
+&
 \multicolumn{10}{c}{} & \\
 &
 \multicolumn{10}{c}{\bf Hypervisor Virtual-Machine Load and Store Instructions} & \\
diff --git a/src/priv-preface.tex b/src/priv-preface.tex
index 34b4124..108f04d 100644
--- a/src/priv-preface.tex
+++ b/src/priv-preface.tex
@@ -16,6 +16,7 @@ modules:
     \em Supervisor ISA    & \em 1.12 & \em Draft \\
     \em Svnapot Extension & \em 0.1  & \em Draft \\
     \em Svpbmt Extension  & \em 0.1  & \em Draft \\
+    \em Svinval Extension & \em 0.1  & \em Draft \\
     \em Hypervisor ISA    & \em 0.6  & \em Draft \\
     \em N Extension       & \em 1.1 & \em Draft \\
     \hline
@@ -71,6 +72,7 @@ Additionally, the following compatible changes have been made since version
   Sv39, Sv48, and Sv57 PTEs
 \item Added the Svpbmt Standard Extension draft, along with the PBMT bits
   in Sv39, Sv48, and Sv57 PTEs.
+\item Added the Svinval Standard Extension draft
 \item Described the behavior of address-translation caches a little more
   explicitly.
 \item Slightly relaxed the atomicity requirement for A and D bit updates
diff --git a/src/supervisor.tex b/src/supervisor.tex
index 7d62c75..fc523d6 100644
--- a/src/supervisor.tex
+++ b/src/supervisor.tex
@@ -2350,3 +2350,193 @@ Otherwise, the PMAs serve as the intermediate attributes.  Second, if
 to the intermediate attributes to produce the final set of attributes used by
 accesses to the page in question.  Otherwise, the intermediate attributes are
 used as the final set of attributes.
+
+\chapter{``Svinval'' Standard Extension for Fine-Grained Address-Translation Cache Invalidation, Version 0.1}
+\label{svinval}
+
+The Svinval extension splits SFENCE.VMA, HFENCE.VVMA, and HFENCE.GVMA
+instructions into finer-grained invalidation and ordering operations that can
+be more efficiently batched or pipelined on certain classes of high-performance
+implementation.
+
+\vspace{-0.2in}
+\begin{center}
+\begin{tabular}{O@{}R@{}R@{}F@{}R@{}S}
+\\
+\instbitrange{31}{25} &
+\instbitrange{24}{20} &
+\instbitrange{19}{15} &
+\instbitrange{14}{12} &
+\instbitrange{11}{7} &
+\instbitrange{6}{0} \\
+\hline
+\multicolumn{1}{|c|}{funct7} &
+\multicolumn{1}{c|}{rs2} &
+\multicolumn{1}{c|}{rs1} &
+\multicolumn{1}{c|}{funct3} &
+\multicolumn{1}{c|}{rd} &
+\multicolumn{1}{c|}{opcode} \\
+\hline
+7 & 5 & 5 & 3 & 5 & 7 \\
+SINVAL.VMA & asid & vaddr & PRIV & 0 & SYSTEM \\
+\end{tabular}
+\end{center}
+
+The SINVAL.VMA instruction invalidates any address-translation cache entries
+that an SFENCE.VMA instruction with the same values of {\em rs1} and {\em rs2}
+would invalidate.  However, unlike SFENCE.VMA, SINVAL.VMA instructions are only
+ordered with respect to SFENCE.VMA, SFENCE.W.INVAL, and SFENCE.INVAL.IR
+instructions as defined below.
+
+\vspace{-0.2in}
+\begin{center}
+\begin{tabular}{O@{}R@{}R@{}F@{}R@{}S}
+\\
+\instbitrange{31}{25} &
+\instbitrange{24}{20} &
+\instbitrange{19}{15} &
+\instbitrange{14}{12} &
+\instbitrange{11}{7} &
+\instbitrange{6}{0} \\
+\hline
+\multicolumn{1}{|c|}{funct7} &
+\multicolumn{1}{c|}{rs2} &
+\multicolumn{1}{c|}{rs1} &
+\multicolumn{1}{c|}{funct3} &
+\multicolumn{1}{c|}{rd} &
+\multicolumn{1}{c|}{opcode} \\
+\hline
+7 & 5 & 5 & 3 & 5 & 7 \\
+SFENCE.W.INVAL & 0 & 0 & PRIV & 0 & SYSTEM \\
+\end{tabular}
+\end{center}
+
+\vspace{-0.2in}
+\begin{center}
+\begin{tabular}{O@{}R@{}R@{}F@{}R@{}S}
+\\
+\instbitrange{31}{25} &
+\instbitrange{24}{20} &
+\instbitrange{19}{15} &
+\instbitrange{14}{12} &
+\instbitrange{11}{7} &
+\instbitrange{6}{0} \\
+\hline
+\multicolumn{1}{|c|}{funct7} &
+\multicolumn{1}{c|}{rs2} &
+\multicolumn{1}{c|}{rs1} &
+\multicolumn{1}{c|}{funct3} &
+\multicolumn{1}{c|}{rd} &
+\multicolumn{1}{c|}{opcode} \\
+\hline
+7 & 5 & 5 & 3 & 5 & 7 \\
+SFENCE.INVAL.IR & 1 & 0 & PRIV & 0 & SYSTEM \\
+\end{tabular}
+\end{center}
+
+The SFENCE.W.INVAL instruction guarantees that any previous stores already
+visible to the current RISC-V hart are ordered before subsequent SINVAL.VMA
+instructions issued by the same hart.  The SFENCE.INVAL.IR instruction
+guarantees that any previous SINVAL.VMA instructions issued by the current hart
+are ordered before subsequent implicit references by that hart to the
+memory-management data structures.
+
+When issued in order (but not necessarily consecutively) by a single hart, the
+sequence SFENCE.W.INVAL, SINVAL.VMA, and SFENCE.INVAL.IR has the same effect as
+a hypothetical SFENCE.VMA instruction in which:
+\begin{itemize}
+  \item the values of {\em rs1} and {\em rs2} for the SFENCE.VMA are the same
+    as those used in the SINVAL.VMA,
+  \item reads and writes prior to the SFENCE.W.INVAL are considered to be those
+    prior to the SFENCE.VMA, and
+  \item reads and writes following the SFENCE.INVAL.IR are considered to be
+    those subsequent to the SFENCE.VMA.
+\end{itemize}
+
+\vspace{-0.2in}
+\begin{center}
+\begin{tabular}{O@{}R@{}R@{}F@{}R@{}S}
+\\
+\instbitrange{31}{25} &
+\instbitrange{24}{20} &
+\instbitrange{19}{15} &
+\instbitrange{14}{12} &
+\instbitrange{11}{7} &
+\instbitrange{6}{0} \\
+\hline
+\multicolumn{1}{|c|}{funct7} &
+\multicolumn{1}{c|}{rs2} &
+\multicolumn{1}{c|}{rs1} &
+\multicolumn{1}{c|}{funct3} &
+\multicolumn{1}{c|}{rd} &
+\multicolumn{1}{c|}{opcode} \\
+\hline
+7 & 5 & 5 & 3 & 5 & 7 \\
+HINVAL.VVMA & asid & vaddr & PRIV & 0 & SYSTEM \\
+\end{tabular}
+\end{center}
+
+\vspace{-0.2in}
+\begin{center}
+\begin{tabular}{O@{}R@{}R@{}F@{}R@{}S}
+\\
+\instbitrange{31}{25} &
+\instbitrange{24}{20} &
+\instbitrange{19}{15} &
+\instbitrange{14}{12} &
+\instbitrange{11}{7} &
+\instbitrange{6}{0} \\
+\hline
+\multicolumn{1}{|c|}{funct7} &
+\multicolumn{1}{c|}{rs2} &
+\multicolumn{1}{c|}{rs1} &
+\multicolumn{1}{c|}{funct3} &
+\multicolumn{1}{c|}{rd} &
+\multicolumn{1}{c|}{opcode} \\
+\hline
+7 & 5 & 5 & 3 & 5 & 7 \\
+HINVAL.GVMA & vmid & gaddr & PRIV & 0 & SYSTEM \\
+\end{tabular}
+\end{center}
+
+If the hypervisor extension is enabled, the Svinval extension also provides two
+additional instructions: HINVAL.VVMA and HINVAL.GVMA.  These have the same
+semantics as SINVAL.VMA, except that they combine with SFENCE.W.INVAL and
+SFENCE.INVAL.IR to replace HFENCE.VVMA and HFENCE.GVMA, respectively, instead
+of SFENCE.VMA.  In addition, HINVAL.GVMA uses VMIDs instead of ASIDs.
+
+SINVAL.VMA, HINVAL.VVMA, and HINVAL.GVMA require the same permissions and raise
+the same exceptions as SFENCE.VMA, HFENCE.VVMA, and HFENCE.GVMA, respectively.
+In particular, an attempt to execute SINVAL.VMA when {\tt mstatus}.TVM=1 while
+executing in S-mode or HS-mode will raise an illegal instruction exception, and
+an attempt to execute SINVAL.VMA when {\tt hstatus}.VTVM=1 while executing in
+VS-mode raises a virtual instruction exception.  Likewise, an attempt to
+execute HINVAL.GVMA in HS-mode when {\tt mstatus}.TVM=1 raises an illegal
+instruction exception.  An attempt to execute HINVAL.VVMA or HINVAL.GVMA when
+V=1 raises a virtual instruction exception, and an attempt to execute any of
+the above in U-mode raises an illegal instruction exception.
+
+\begin{commentary}
+  SFENCE.W.INVAL and SFENCE.INVAL.IR instructions do not need to be trapped when
+  {\tt mstatus}.TVM=1 or when {\tt hstatus}.VTVM=1, as they only have ordering
+  effects but no visible side effects.  Trapping of the SINVAL.VMA instruction
+  is sufficient to enable emulation of the intended overall TLB maintenance
+  functionality.
+
+  In typical usage, software will invalidate a range of virtual addresses in
+  the address-translation caches by executing an SFENCE.W.INVAL instruction,
+  executing a series of SINVAL.VMA, HINVAL.VVMA, or HINVAL.GVMA instructions to
+  the addresses (and optionally ASIDs or VMIDs) in question, and then executing
+  an SFENCE.INVAL.IR instruction.
+
+  High-performance implementations will be able to pipeline the
+  address-translation cache invalidation operations, and will defer any
+  pipeline stalls or other memory ordering enforcement until an SFENCE.W.INVAL,
+  SFENCE.INVAL.IR, SFENCE.VMA, HFENCE.GVMA, or HFENCE.VVMA instruction is
+  executed.
+
+  Simpler implementations may implement SINVAL.VMA, HINVAL.VVMA, and
+  HINVAL.GVMA identically to SFENCE.VMA, HFENCE.VVMA, and HFENCE.GVMA,
+  respectively, while implementing SFENCE.W.INVAL and SFENCE.INVAL.IR
+  instructions as no-ops.
+\end{commentary}