Third proposal, from S&S
authorSimon Peyton Jones <simonpj@microsoft.com>
Thu, 1 May 2003 10:54:32 +0000 (10:54 +0000)
committerSimon Peyton Jones <simonpj@microsoft.com>
Thu, 1 May 2003 10:54:32 +0000 (10:54 +0000)
ffi/threads.tex

index 753d8d8..c38fc8f 100644 (file)
@@ -15,9 +15,9 @@
 
 
 \newcommand{\NS}{{\cal N}}
-%      NS: set of native threads
+%       NS: set of native threads
 \newcommand{\HS}{{\cal H}}
-%      HS: set of Haskell threads
+%       HS: set of Haskell threads
 \newcommand{\hcall}{H}
 \newcommand{\fcall}[2]{F^{#1}~#2}
 \newcommand{\ret}[1]{R~#1}
@@ -179,13 +179,13 @@ $$
 \mbox{Native thread} &  t & ::= & N[S] \\
 \\
 \mbox{Native thread stack} &  S & ::= & \epsilon & \mbox{Empty}\\
-       & & | & \hcall : S  & \mbox{Executing Haskell} \\
-       & & | & \fcall{si}{h} : S & \mbox{Executing foreign code}\\
-       & & | & \bullet & \mbox{Unknown}\\
+        & & | & \hcall : S  & \mbox{Executing Haskell} \\
+        & & | & \fcall{si}{h} : S & \mbox{Executing foreign code}\\
+        & & | & \bullet & \mbox{Unknown}\\
 \\
 \mbox{Safety indicator} &  si & ::= & u & \mbox{Unsafe} \\
-       & & | & s & \mbox{Safe} \\
-       & & | & t & \mbox{Thread-safe} \\
+        & & | & s & \mbox{Safe} \\
+        & & | & t & \mbox{Thread-safe} \\
 \end{array}
 $$
 A native thread of form $N[S]$ has thread-id $N$, while $S$ is
@@ -206,13 +206,13 @@ $$
 \mbox{Haskell thread} &  h & ::= & (a)_{bt} \\
 \\
 \mbox{Haskell action} &  a & ::= & p ~@>>@~ a  & \mbox{Sequence} \\
-       & & | & \ret{N}  & \mbox{Return to native thread $N$} \\
+        & & | & \ret{N}  & \mbox{Return to native thread $N$} \\
 \\
 \mbox{Primitive action} &  p & ::= & \tau & \mbox{Internal action} \\
-       & & | & \fcall{si}{f} & \mbox{Foreign call} \\
+        & & | & \fcall{si}{f} & \mbox{Foreign call} \\
 \\
 \mbox{Bound thread id} & bt & ::= & \epsilon & \mbox{Not bound} \\
-       & & | & N & \mbox{Bound to native thread N}
+        & & | & N & \mbox{Bound to native thread N}
 \end{array}
 $$
 A Haskell thread $h$ of form $(a)_{bt}$ has action $a$.  The indicator
@@ -241,62 +241,62 @@ The structural rules are these:
 $$
 \begin{array}{c}
 \infer{\NS \cup \{t\} ; \HS ~\Rightarrow~ \NS'  \cup \{t\}; \HS'}
-       {\NS ; \HS ~\Rightarrow~ \NS' ; \HS'}
+        {\NS ; \HS ~\Rightarrow~ \NS' ; \HS'}
 \qquad
 \infer{\NS ; \HS  \cup \{h\} ~\Rightarrow~ \NS'; \HS'   \cup \{h\}}
-       {\NS ; \HS ~\Rightarrow~ \NS' ; \HS'}
+        {\NS ; \HS ~\Rightarrow~ \NS' ; \HS'}
 \end{array}
 $$
 These standard rules allow us to write the interesting transitions with less clutter.
 $$
 \begin{array}{rcll}
 N[\hcall:S]; (\tau~@>>@~a)_{bt} 
-       & \Rightarrow 
-       & N[\hcall:S]; (a)_{bt} & (INT) \\
+        & \Rightarrow 
+        & N[\hcall:S]; (a)_{bt} & (INT) \\
 \\
 N[\hcall]; (\fcall{si}{f}~@>>@~a)_{\epsilon} 
-       & \Rightarrow 
-       & N[\fcall{si}{a_\epsilon}:\hcall];  & (FCALL1) \\
+        & \Rightarrow 
+        & N[\fcall{si}{a_\epsilon}:\hcall];  & (FCALL1) \\
 \\
 N[\hcall:S]; (\fcall{si}{f}@>>@~a)_N 
-       & \Rightarrow 
-       & N[\fcall{si}{a_N}:\hcall:S];  & (FCALL2) \\
+        & \Rightarrow 
+        & N[\fcall{si}{a_N}:\hcall:S];  & (FCALL2) \\
 \\
 N[\fcall{si}{a_{bt}}:S];  
-       & \Rightarrow 
-       & N[S]; a_{bt} & (FRET) \\
+        & \Rightarrow 
+        & N[S]; a_{bt} & (FRET) \\
 \\
 N[\bullet];
-       & \Rightarrow 
-       & N[\hcall:\bullet];  (f ~@>>@~ \ret{N})_{bt} & (HCALL1) \\
-       & \multicolumn{2}{l}{\mbox{where}~ bt \begin{array}[t]{ll}
-               = \epsilon & \mbox{if $f$ is a non-bound foreign export} \\
-               = N & \mbox{if $f$ is a bound foreign export}
-          \end{array}} \\
+        & \Rightarrow 
+        & N[\hcall:\bullet];  (f ~@>>@~ \ret{N})_{bt} & (HCALL1) \\
+        & \multicolumn{2}{l}{\mbox{where}~ bt \begin{array}[t]{ll}
+                = \epsilon & \mbox{if $f$ is a non-bound foreign export} \\
+                = N & \mbox{if $f$ is a bound foreign export}
+           \end{array}} \\
 \\
 N[\fcall{si}{a_{bt}} : S]; 
-       & \Rightarrow 
-       & N[\hcall : \fcall{si}{a_{bt}} : S]; ~ (f ~@>>@~ \ret{N})_{bt} & (HCALL2) \\
-       & \multicolumn{2}{l}{\mbox{where}~si \in \{s,t\}} \\
-       & \multicolumn{2}{l}{\mbox{and}~ bt \begin{array}[t]{ll}
-               = \epsilon & \mbox{if $f$ is a non-bound foreign export} \\
+        & \Rightarrow 
+        & N[\hcall : \fcall{si}{a_{bt}} : S]; ~ (f ~@>>@~ \ret{N})_{bt} & (HCALL2) \\
+        & \multicolumn{2}{l}{\mbox{where}~si \in \{s,t\}} \\
+        & \multicolumn{2}{l}{\mbox{and}~ bt \begin{array}[t]{ll}
+                = \epsilon & \mbox{if $f$ is a non-bound foreign export} \\
 
-               = N & \mbox{if $f$ is a bound foreign export}
-          \end{array}} \\
+                = N & \mbox{if $f$ is a bound foreign export}
+           \end{array}} \\
 \\
 N[\hcall : S]; \ret{N} 
-       & \Rightarrow 
-       & N[S]; & (HRET) \\
+        & \Rightarrow 
+        & N[S]; & (HRET) \\
 \\
 (nothing)
-       & \Rightarrow 
-       & N[\hcall]; & (WKR) \\
-       & \multicolumn{2}{l}{\mbox{where $N$ is fresh}} \\
+        & \Rightarrow 
+        & N[\hcall]; & (WKR) \\
+        & \multicolumn{2}{l}{\mbox{where $N$ is fresh}} \\
 \\
 (nothing)
-       & \Rightarrow 
-       & N[\bullet]; & (EXT) \\
-       & \multicolumn{2}{l}{\mbox{where $N$ is fresh}} \\
+        & \Rightarrow 
+        & N[\bullet]; & (EXT) \\
+        & \multicolumn{2}{l}{\mbox{where $N$ is fresh}} \\
 \end{array}
 $$
 Here is what the rules mean:
@@ -412,13 +412,13 @@ $$
 \mbox{Native thread} &  t & ::= & N[S] \\
 \\
 \mbox{Native thread stack} &  S & ::= & \epsilon & \mbox{Empty}\\
-       & & | & \hcall : S  & \mbox{Executing Haskell} \\
-       & & | & \fcall{si}{h} : S & \mbox{Executing foreign code}\\
-       & & | & \bullet & \mbox{Unknown}\\
+        & & | & \hcall : S  & \mbox{Executing Haskell} \\
+        & & | & \fcall{si}{h} : S & \mbox{Executing foreign code}\\
+        & & | & \bullet & \mbox{Unknown}\\
 \\
 \mbox{Safety indicator} &  si & ::= & u & \mbox{Unsafe} \\
-       & & | & s & \mbox{Safe} \\
-       & & | & t & \mbox{Thread-safe} \\
+        & & | & s & \mbox{Safe} \\
+        & & | & t & \mbox{Thread-safe} \\
 \end{array}
 $$
 A native thread of form $N[S]$ has thread-id $N$, while $S$ is
@@ -437,16 +437,16 @@ $$
 \mbox{Haskell thread} &  h & ::= & (a)_{at} \\
 \\
 \mbox{Haskell action} &  a & ::= & p ~@>>@~ a  & \mbox{Sequence} \\
-       & & | & \epsilon & \mbox{End of thread}
+        & & | & \epsilon & \mbox{End of thread}
 \\
 \mbox{Primitive action} &  p & ::= & \tau & \mbox{Internal action} \\
-       & & | & \fcall{si}{f} & \mbox{Foreign call} \\
-       & & | & \bound{a} & \mbox{``@threadbound@'' combinator} \\
-       & & | & \bound{a}_{bt} & \mbox{the same with specified native thread} \\
-       & & | & \forkio{a} & \mbox{@forkIO@: fork a new thread} \\
+        & & | & \fcall{si}{f} & \mbox{Foreign call} \\
+        & & | & \bound{a} & \mbox{``@threadbound@'' combinator} \\
+        & & | & \bound{a}_{bt} & \mbox{the same with specified native thread} \\
+        & & | & \forkio{a} & \mbox{@forkIO@: fork a new thread} \\
 \\
 \mbox{Associated thread id} & at & ::= & \epsilon & \mbox{Not associated} \\
-       & & | & N & \mbox{Associated with native thread N} \\
+        & & | & N & \mbox{Associated with native thread N} \\
 \\
 \mbox{Bound thread id} & bt & ::= & N & \mbox{Bound to native thread N}
 
@@ -481,89 +481,89 @@ thread.
 $$
 \begin{array}{rcll}
 N[\hcall:S]; (\bound{a}~@>>@~b)_{N} 
-       & \Rightarrow 
-       & N[\hcall:S]; (\bound{a}_N~@>>@~b)_{N} & (BIND1) \\
+        & \Rightarrow 
+        & N[\hcall:S]; (\bound{a}_N~@>>@~b)_{N} & (BIND1) \\
 \\
 ; (\bound{a}~@>>@~b)_{\epsilon} 
-       & \Rightarrow 
-       & N[\hcall]; (\bound{a}_N~@>>@~b)_{\epsilon} & (BIND2) \\
+        & \Rightarrow 
+        & N[\hcall]; (\bound{a}_N~@>>@~b)_{\epsilon} & (BIND2) \\
 \\
 N[\hcall:S]; (\bound{\epsilon}_N~@>>@~b)_N 
-       & \Rightarrow 
-       & N[\hcall:S]; (b)_N & (UNBIND1) \\
+        & \Rightarrow 
+        & N[\hcall:S]; (b)_N & (UNBIND1) \\
 \\
 N[\hcall]; (\bound{\epsilon}_N~@>>@~b)_{\epsilon} 
-       & \Rightarrow 
-       & ; (b)_{\epsilon} & (UNBIND2) \\
+        & \Rightarrow 
+        & ; (b)_{\epsilon} & (UNBIND2) \\
 \\
 N[\hcall:S]; (\bound{\bound{a}~@>>@~b}_{bt}~@>>@~c)_{at} 
-       & \Rightarrow 
-       & N[\hcall:S]; (\bound{a~@>>@~b}_{bt}~@>>@~c)_{at} & (NEST) \\
+        & \Rightarrow 
+        & N[\hcall:S]; (\bound{a~@>>@~b}_{bt}~@>>@~c)_{at} & (NEST) \\
 \\
 ; (\tau~@>>@~a)_{at} 
-       & \Rightarrow 
-       & ; (a)_{at} & (INT1) \\
+        & \Rightarrow 
+        & ; (a)_{at} & (INT1) \\
 \\
 ; (\bound{\tau~@>>@~a}_{bt}~@>>@~b)_{at} 
-       & \Rightarrow 
-       & ; (\bound{a}_{bt}~@>>@~b)_{at} & (INT2) \\
+        & \Rightarrow 
+        & ; (\bound{a}_{bt}~@>>@~b)_{at} & (INT2) \\
 \\
 N[\hcall]; (\fcall{si}{f}~@>>@~a)_{\epsilon} 
-       & \Rightarrow 
-       & N[\fcall{si}{a_\epsilon}:\hcall];  & (FCALL1) \\
+        & \Rightarrow 
+        & N[\fcall{si}{a_\epsilon}:\hcall];  & (FCALL1) \\
 \\
 N[\hcall:S]; (\fcall{si}{f}~@>>@~a)_N 
-       & \Rightarrow 
-       & N[\fcall{si}{a_N}:\hcall:S];  & (FCALL2) \\
+        & \Rightarrow 
+        & N[\fcall{si}{a_N}:\hcall:S];  & (FCALL2) \\
 \\
 M[\hcall]; (\fcall{si}{f}~@>>@~a)_N
-       & \Rightarrow 
-       & M[\fcall{si}{a_N}:\hcall];  & (FCALL3) \\
+        & \Rightarrow 
+        & M[\fcall{si}{a_N}:\hcall];  & (FCALL3) \\
 \\
 N[\hcall:S]; (\bound{\fcall{si}{f}~@>>@~a}_N~@>>@~b)_at
-       & \Rightarrow 
-       & N[\fcall{si}{(\bound{a}_N~@>>@~b)_{at}}:\hcall:S];  & (FCALL4) \\
+        & \Rightarrow 
+        & N[\fcall{si}{(\bound{a}_N~@>>@~b)_{at}}:\hcall:S];  & (FCALL4) \\
 \\
 N[\fcall{si}{a_{at}}:S];  
-       & \Rightarrow 
-       & N[S]; a_{at} & (FRET) \\
+        & \Rightarrow 
+        & N[S]; a_{at} & (FRET) \\
 \\
 N[\bullet];
-       & \Rightarrow 
-       & N[\hcall:\bullet];  (f)_{N} & (HCALL1) \\
-       & \multicolumn{2}{l}{\mbox{where $f$ is a foreign export}} \\
+        & \Rightarrow 
+        & N[\hcall:\bullet];  (f)_{N} & (HCALL1) \\
+        & \multicolumn{2}{l}{\mbox{where $f$ is a foreign export}} \\
 \\
 N[\fcall{si}{a_{at}} : S]; 
-       & \Rightarrow 
-       & N[\hcall : \fcall{si}{a_{at}} : S]; ~ (f)_{N} & (HCALL2) \\
-       & \multicolumn{2}{l}{\mbox{where $f$ is a foreign export}} \\
-       & \multicolumn{2}{l}{\mbox{and}~si \in \{s,t\}} \\
+        & \Rightarrow 
+        & N[\hcall : \fcall{si}{a_{at}} : S]; ~ (f)_{N} & (HCALL2) \\
+        & \multicolumn{2}{l}{\mbox{where $f$ is a foreign export}} \\
+        & \multicolumn{2}{l}{\mbox{and}~si \in \{s,t\}} \\
 \\
 N[\hcall : S]; (\epsilon)_N 
-       & \Rightarrow 
-       & N[S]; & (HRET) \\
+        & \Rightarrow 
+        & N[S]; & (HRET) \\
 \\
 ; (\forkio{a}~@>>@~b)_{at}
-       & \Rightarrow
-       & ; (b)_{at}, (a)_\epsilon & (FORK1) \\
+        & \Rightarrow
+        & ; (b)_{at}, (a)_\epsilon & (FORK1) \\
 \\
 ; (\bound{\forkio{a}~@>>@~b}_{bt}~@>>@~c)_{at}
-       & \Rightarrow
-       & ; (\bound{b}_{bt}~@>>@~c)_{at}, (a)_\epsilon & (FORK2) \\
+        & \Rightarrow
+        & ; (\bound{b}_{bt}~@>>@~c)_{at}, (a)_\epsilon & (FORK2) \\
 \\
 ; (\epsilon)_\epsilon
-       & \Rightarrow
-       & (nothing) & (END) \\
+        & \Rightarrow
+        & (nothing) & (END) \\
 \\
 (nothing)
-       & \Rightarrow 
-       & N[\hcall]; & (WKR) \\
-       & \multicolumn{2}{l}{\mbox{where $N$ is fresh}} \\
+        & \Rightarrow 
+        & N[\hcall]; & (WKR) \\
+        & \multicolumn{2}{l}{\mbox{where $N$ is fresh}} \\
 \\
 (nothing)
-       & \Rightarrow 
-       & N[\bullet]; & (EXT) \\
-       & \multicolumn{2}{l}{\mbox{where $N$ is fresh}} \\
+        & \Rightarrow 
+        & N[\bullet]; & (EXT) \\
+        & \multicolumn{2}{l}{\mbox{where $N$ is fresh}} \\
 \end{array}
 $$
 
@@ -654,12 +654,12 @@ the threads by replacing rules (BIND2), (UNBIND1) and (UNBIND2) by:
 $$
 \begin{array}{rcll}
 N[\hcall]; (\bound{a}~@>>@~b)_{\epsilon} 
-       & \Rightarrow 
-       & N[\hcall]; (\bound{a}_N~@>>@~b)_{\epsilon} & (BIND2') \\
+        & \Rightarrow 
+        & N[\hcall]; (\bound{a}_N~@>>@~b)_{\epsilon} & (BIND2') \\
 \\
 ; (\bound{\epsilon}_N~@>>@~b)_{at}
-       & \Rightarrow 
-       & ; (b)_{at} & (UNBIND') \\
+        & \Rightarrow 
+        & ; (b)_{at} & (UNBIND') \\
 \end{array}
 $$
 
@@ -672,4 +672,201 @@ thread-local state lying around could make bugs harder to reproduce.
 
 \end{itemize}
 
+\newpage
+\part{Third Proposal}
+
+This proposal, from Simon Marlow and Simon Peyton Jones, is another attempt to simplify
+the bound-threads design.  We think that it's more or less what Daan proposed, only he never wrote it up.
+
+We have a growing feeling that the First Proposal including
+'bound' foreign exports and so forth is too complicated - especially
+when OS designers are already trying to solve similar problems.
+c.f. the arguments about 1:1 vs. M:N threading in Linux and other OSs.
+If both the OS and the Haskell RTS are doing dynamic M:N style thread
+allocation, it seems like overkill, and we don't have a lot of
+confidence that we would be able to tune this kind of system
+effectively.
+
+
+\section{Informal semantics}
+
+Here's the basic idea:
+\begin{description}
+\item[Haskell threads and OS threads.] \mbox{}\\
+\begin{itemize}
+\item Every Haskell thread is bound to a exactly one OS thread.  
+
+\item Many Haskell threads 
+may be bound to the same OS thread.
+In particular, @forkIO@ forks a new Haskell thread bound to the same OS thread as the call of @forkIO@.
+
+\item A Haskell thread, bound to a new OS thread, can be created with @forkOS@.
+
+\end{itemize}
+
+\item[Foreign interface.] \mbox{}\\
+\begin{itemize}
+\item No @safe@ vs @threadsafe@ distinction. But we retain the @safe@/@unsafe@ distinction.
+\item A foreign call made by a Haskell thread is (guaranteed to be) made by its bound OS thread.
+\item If that foreign call blocks, then so do all the Haskell threads bound to that OS thread.
+\item A foreign call \emph{into Haskell} (via @foreign export@ or @foreign import wrapper@) is 
+run by a Haskell thread bound to the OS thread that made the call.
+\end{itemize}
+
+\item[Non-blocking calls.] \mbox{}\\
+\begin{itemize}
+\item 
+To make a foreign call from Haskell which does not block other Haskell threads bound to the
+same OS thread, it's easy to hand off to a new OS thread:
+\begin{verbatim}
+  nonBlocking :: IO a -> IO a
+  nonBlocking a = do { r <- newEmptyMVar ;
+                       forkOS (do { v <- a; putMVar r v }) ;
+                       takeMVar r }
+
+  foreign import foo :: Int -> IO Int
+
+  ....do { x <- .... ; 
+           r <- nonBlocking (foo x) ; 
+           ... }...
+\end{verbatim}
+\item
+The @nonBlocking@ function looks expensive, because it starts a new OS thread, but it's easy
+to make a more efficient version that keeps a pool of Haskell threads, each with a dedicated 
+OS thread, ready to execute any IO actions passed to @nonBlocking@.  This allows us to write in Haskell
+what we would otherwise have to implement in the runtime system
+
+\item If the programmer knows that the Haskell thread will have its own dedicated OS thread (e.g.
+it's a thread born from a call into Haskell) then he can avoid the @nonBlocking@ wrapper and the
+consequent OS-thread-switch costs.  Let
+the programmer decide!
+\end{itemize}
+
+\item[Open questions and notes.] \mbox{}\\
+\begin{itemize}
+\item We lose out by not being able to take advantage of SMP automatically 
+for existing Concurrent Haskell programs.  But:
+  (a) running multithreaded Haskell programs on SMP is an open research
+      problem anyway, and
+
+  (b) Assuming we solve (a), and your OS has a pretty good threading
+      implementation, then you can just use forkOS everywhere (i.e. get a 1:1
+      Haskell to OS thread mapping).
+
+\item 
+It'd be possible to allow any OS thread to run a Haskell thread (not just its bound OS thread),
+provided it didn't make any foreign calls.  
+\end{itemize}
+\end{description}
+
+
+\section{Formal semantics}
+
+The syntax of a native thread is this:
+$$
+\begin{array}{lrcll}
+\mbox{Native thread} &  t & ::= & N[S] \\
+\\
+\mbox{Native thread stack} &  S & ::= & \epsilon & \mbox{Empty}\\
+        & & | & \hcall : S  & \mbox{Executing Haskell} \\
+        & & | & \fcall{si}{a} : S & \mbox{Executing foreign code} \\
+        & & | & \bullet & \mbox{Unknown}\\
+\\
+\mbox{Safety indicator} &  si & ::= & u & \mbox{Unsafe} \\
+        & & | & s & \mbox{Safe}
+\end{array}
+$$
+A native thread of form $N[S]$ has thread-id $N$, while $S$ is
+an abstraction of its call stack.  If $\hcall$ is on top of the stack,
+the thread is willing to execute a Haskell thread.
+If $\fcall{si}{h}$ is
+on top of the stack, the thread is in the process of dealing with a call
+to a foreign function, which will return its result to the Haskell thread
+$h$.  The safety-indicator $si$ is from the FFI spec.
+
+The syntax of a Haskell thread is this:
+$$
+\begin{array}{lrcll}
+\mbox{Haskell thread} &  h & ::= & (a)_{N} & \mbox{Bound to native thread N} \\
+\\
+\mbox{Haskell action} &  a & ::= & p ~@>>@~ a  & \mbox{Sequence} \\
+        & & | & \ret  & \mbox{Return from a call into Haskell} \\
+\\
+\mbox{Primitive action} &  p & ::= & \tau & \mbox{Internal action} \\
+        & & | & @forkIO@~a & \mbox{Fork a thread} \\
+        & & | & @forkOS@~a & \mbox{Fork a native thread} \\
+        & & | & \fcall{si}{f} & \mbox{Foreign call} 
+\end{array}
+$$
+A Haskell thread $h$ of form $(a)_{N}$ has action $a$.  The indicator
+$N$ identifies the native thread $N$ to which the Haskell thread is \emph{bound}.
+
+An action $a$ is a sequence of primitive actions, finishing with a 
+return of some kind.  A primitive action is either some internal Haskell
+thing (such as performing a bit of evaluation, or operating on an @MVar@),
+or else it is a call to a foreign function $f$.
+
+We do not model the data passed to, or returned from, a foreign call, nor
+any details of what ``internal Haskell'' operations are.  
+
+\subsection{Evolution}
+
+We describe how the system evolves in a very standard way, using 
+transition rules, of form
+$$
+\NS ; \HS ~\Rightarrow~ \NS' ; \HS'
+$$
+The structural rules are these:
+$$
+\begin{array}{c}
+\infer{\NS \cup \{t\} ; \HS ~\Rightarrow~ \NS'  \cup \{t\}; \HS'}
+        {\NS ; \HS ~\Rightarrow~ \NS' ; \HS'}
+\qquad
+\infer{\NS ; \HS  \cup \{h\} ~\Rightarrow~ \NS'; \HS'   \cup \{h\}}
+        {\NS ; \HS ~\Rightarrow~ \NS' ; \HS'}
+\end{array}
+$$
+These standard rules allow us to write the interesting transitions with less clutter.
+$$
+\begin{array}{rcll}
+N[\hcall:S]; (\tau~@>>@~a)_{M} 
+        & \Rightarrow 
+        & N[\hcall:S]; (a)_{M} & (INT) \\
+\\
+N[\hcall:S]; (\fcall{si}{f}@>>@~a)_N 
+        & \Rightarrow 
+        & N[\fcall{si}{a_N}:\hcall:S];  & (FCALL) \\
+\\
+N[\hcall:S]; (@forkIO@~b~@>>@~a)_N 
+        & \Rightarrow 
+        & N[\hcall:S]; (a)_{N}, (b)_N & (FORKIO) \\
+N[\hcall:S]; (@forkOS@~b~@>>@~a)_N 
+        & \Rightarrow 
+        & N[\hcall:S], M[\hcall]; (a)_{N}, (b)_M & (FORKOS) \\
+\\
+N[\fcall{si}{a}:S];  
+        & \Rightarrow 
+        & N[S]; a_{N} & (FRET) \\
+\\
+N[\bullet];
+        & \Rightarrow 
+        & N[\hcall:\bullet];  (f ~@>>@~ \ret{})_{N} & (HCALL1) \\
+\\
+N[\fcall{s}{a} : S]; 
+        & \Rightarrow 
+        & N[\hcall : \fcall{s}{a} : S]; ~ (f ~@>>@~ \ret{})_{N} & (HCALL2) \\
+ \\
+N[\hcall : S]; (\ret{})_N
+        & \Rightarrow 
+        & N[S]; & (HRET) \\
+\\
+(nothing)
+        & \Rightarrow 
+        & N[\bullet]; & (EXT) \\
+        & \multicolumn{2}{l}{\mbox{where $N$ is fresh}} \\
+\end{array}
+$$
+
+The pattern of these rules is exactly as for the First Proposal, but they are noticeably simpler.
+
 \end{document}