The execution environment must guarantee harts make progress

1 files changed, 17 insertions, 0 deletions

diff --git a/src/intro.tex b/src/intro.tex
index 929b321..242ee8c 100644
--- a/src/intro.tex
+++ b/src/intro.tex
@@ -165,6 +165,22 @@ time-multiplexed onto real hardware by the execution environment.
 Some EEIs support the creation and destruction of additional harts,
 for example, via environment calls to fork new harts.
 
+The execution environment is responsible for ensuring the eventual forward
+progress of each of its harts.
+For a given hart, that responsibility is suspended while the hart is
+exercising a mechanism that explicitly waits for an event, such as the
+wait-for-interrupt instruction defined in Volume II of this specification; and
+that responsibility ends if the hart is terminated.
+The following events constitute forward progress:
+\vspace{-0.2in}
+\begin{itemize}
+\parskip 0pt
+\itemsep 1pt
+\item The retirement of an instruction.
+\item A trap, as defined in Section~\ref{sec:trap-defn}.
+\item Any other event defined by an extension to constitute forward progress.
+\end{itemize}
+
 \begin{commentary}
 The term hart was introduced in the work on
 Lithe~\cite{lithe-pan-hotpar09,lithe-pan-pldi10} to provide a term to
@@ -636,6 +652,7 @@ instruction format to avoid breaking up opcode fields.
 \end{commentary}
 
 \section{Exceptions, Traps, and Interrupts}
+\label{sec:trap-defn}
 
 We use the term {\em exception} to refer to an unusual condition
 occurring at run time associated with an instruction in the current