Zap the old proposals, leave only Proposal 4.
authorWolfgang Thaller <wolfgang.thaller@gmx.net>
Fri, 13 Jun 2003 13:10:32 +0000 (13:10 +0000)
committerWolfgang Thaller <wolfgang.thaller@gmx.net>
Fri, 13 Jun 2003 13:10:32 +0000 (13:10 +0000)
ffi/threads.tex

index 7f6c02a..d16ab59 100644 (file)
@@ -77,805 +77,11 @@ should be used to execute Haskell code. It should be possible to
 implement it with e.g. a Haskell interpreter running in one OS thread
 that just uses other OS threads for foreign calls.
 
-\item There should be no unexpected blocking. Especially, threadsafe calls
-should never cause other threads to block.
+\item There should be no unexpected blocking. Safe Foreign calls (i.e. calls not
+marked as unsafe) should not cause other threads to block.
 \end{itemize}
 
 \newpage
-\part{First Proposal}
-\section{Proposed design}
-
-The key extension is the ability to create a ``bound'' foreign export,
-that can be called from a foreign language.
-The intuitive idea is that ``@bound@'' means that the native OS thread that makes
-the call into Haskell is also guaranteed to run any @foreign@ calls that the
-Haskell thread makes.  
-
-\subsection{Extension to the FFI Syntax}
-
-A bound foreign export is declared by adding the specialid \texttt{bound}
-after the calling convention (before the exported entity string).
-
-The bound attribute can also apply to thunks created by foreign imported
-"wrapper" functions. These stub factories are the only situation where the
-\texttt{bound} attribute applies. 
-
-Example:
-\begin{quote}
-\begin{verbatim}
-foreign export ccall bound "CFoo" haskellFoo
-    :: IO ()
-foreign import ccall bound "wrapper" wrapHaskellFoo
-    :: IO () -> IO (FunPtr (IO ())) 
-\end{verbatim}
-\end{quote}
-
-The \texttt{bound} attribute should only be valid for exported entities
-that are in the IO monad.
-
-
-\subsection{Library Addition}
-
-A function named \texttt{forkBoundThread} should be added to the library
-(somewhere in \texttt{Foreign} or \texttt{Concurrent}).
-A possible implementation for POSIX systems is given below.
-
-\begin{quote}
-\begin{verbatim}
-forkBoundThread :: IO () -> IO ()
-
--- pthread_create(thread, attr, start_routine, arg)
-foreign import ccall pthread_create
-    :: Ptr (Ptr ())
-    -> Ptr ()
-    -> FunPtr (Ptr () -> IO (Ptr ()))
-    -> Ptr ()
-    -> IO CInt
-
-foreign export ccall bound "wrapper" wrapHaskell
-    :: (Ptr () -> IO (Ptr ()))
-    -> IO (FunPtr (Ptr () -> IO (Ptr ())))
-    
-forkBoundThread action =
-    wrapHaskell (\ptr -> do
-            freeHaskellFunPtr thunk
-            action
-            return nullPtr
-        )
-    >>= \thunk -> alloca
-    >>= \thread -> pthread_create thread nullPtr thunk nullPtr
-    >> return ()
-
-\end{verbatim}
-\end{quote}
-
-\section{Operational semantics}
-
-While the intuition is clear, it is quite difficult to say \emph{precisely} what a ``@bound@'' export means.
-The purpose of this section is to give a precise description, using a simple operational semantics.
-
-
-\subsection{State}
-
-The state of the system is represented by a pair
-$$\NS ; \HS$$
-where 
-\begin{itemize}
-\item $\NS = \{t_1, \ldots ,t_n\}$ is a set of \emph{native threads}.
-A native thread is directly supported by the underlying operating
-system, and may have some thread-local state. It may therefore
-be important which native thread executes foreign
-(non-Haskell) code.
-
-\item $\HS = \{h_1, \ldots ,h_n\}$ is a set of \emph{Haskell threads}.
-Haskell threads are supposed to be extremely lightweight, and
-can be created very cheaply. A Haskell thread can only make progress
-if a native thread acts as its execution engine.
-\end{itemize}
-
-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}{h} : S & \mbox{Executing foreign code}\\
-        & & | & \bullet & \mbox{Unknown}\\
-\\
-\mbox{Safety indicator} &  si & ::= & u & \mbox{Unsafe} \\
-        & & | & s & \mbox{Safe} \\
-        & & | & t & \mbox{Thread-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.
-\emph{(What about referring to the $\hcall$ state as
-``inside the Haskell runtime system''? It includes things like GC and other
-``administrative tasks''. A native thread might be in the $\hcall$ state 
-without ever really executing Haskell code.)}
-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)_{bt} \\
-\\
-\mbox{Haskell action} &  a & ::= & p ~@>>@~ a  & \mbox{Sequence} \\
-        & & | & \ret{N}  & \mbox{Return to native thread $N$} \\
-\\
-\mbox{Primitive action} &  p & ::= & \tau & \mbox{Internal action} \\
-        & & | & \fcall{si}{f} & \mbox{Foreign call} \\
-\\
-\mbox{Bound thread id} & bt & ::= & \epsilon & \mbox{Not bound} \\
-        & & | & N & \mbox{Bound to native thread N}
-\end{array}
-$$
-A Haskell thread $h$ of form $(a)_{bt}$ has action $a$.  The indicator
-$bt$ tells whether the Haskell thread is \emph{bound to} a native
-thread.  If $bt$ is $\epsilon$, the Haskell thread is not bound to a
-native thread; if $bt$ is $N$, the Haskell thread is bound to native
-thread $N$.  Specifing exactly what it means for a Haskell thread to
-be bound to a native thread is the main purpose of this document.
-
-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)_{bt} 
-        & \Rightarrow 
-        & N[\hcall:S]; (a)_{bt} & (INT) \\
-\\
-N[\hcall]; (\fcall{si}{f}~@>>@~a)_{\epsilon} 
-        & \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) \\
-\\
-N[\fcall{si}{a_{bt}}:S];  
-        & \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}} \\
-\\
-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} \\
-
-                = N & \mbox{if $f$ is a bound foreign export}
-           \end{array}} \\
-\\
-N[\hcall : S]; \ret{N} 
-        & \Rightarrow 
-        & N[S]; & (HRET) \\
-\\
-(nothing)
-        & \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}} \\
-\end{array}
-$$
-Here is what the rules mean:
-\begin{itemize}
-\item (INT) says that an internal action of a Haskell thread 
-can be executed by any native thread that 
-is in the Haskell state; that is, has $H$ on top of its stack.  This is true
-even if the native thread has called a bound foreign export, and that 
-Haskell function is still running.
-
-\item On the other hand, (FCALL1) says that only a vanilla worker thread $N[H]$ (i.e. with
-nothing on its stack except $H$) can execute an unbound foreign call.  Similarly (FCALL2) says
-that only native thread $N$ can execute a foreign call from a Haskell thread bound to $N$.
-(This is under the proposal that foreign imports are not labelled bound/unbound.)
-
-\item In either (FCALL) case, the Haskell thread is removed from the pool, and captured in the
-native thread's stack.  The rule (FRET) reinstates the Haskell thread (bound or otherwise)
-when the native thread decides to return from the call.
-
-\item Rules (HCALL1) and (HCALL2) deal with foreign code calling Haskell. (HCALL1) 
-starts with a native thread that comes ``out of the blue'' with an unknown stack $\bullet$.
-It just puts a new Haskell thread into the pool, bound or otherwise depending on 
-whether the foreign export being called is labelled as bound.
-
-(HCALL2) is similar, except that we aren't allowed to make such a call if
-the native thread is in the middle of an unsafe foreign call.  The difference
-between (HCALL1) and (HCALL2) looks very unsavoury.
-
-\item (HRET) deals with returning from a completed Haskell thread to the appropriate
-calling native thread.  Notice that even an unbound Haskell thread must return its result
-to the right calling native thread, hence the ``return action'' $\ret{t}$ tacked onto
-the end of the Haskell thread.
-
-\item (WKR) and (EXT) allow new native threads to enter the system.
-
-\end{itemize}
-
-\section{Issues}
-
-\begin{itemize}
-
-\item Somebody suggested labelling foreign imports as bound or unbound,
-and allowing the RTS to choose any thread it wants for executing unbound
-foreign imports.
-
-However, we need top performance for \emph{all} foreign imports, not just
-unbound ones. HOpenGL applications make hundreds and thousands of unsafe calls,
-all of which have to be bound to a specific native thread.
-Now if bound foreign imports need to be as fast as unbound foreign imports
-\footnote{This will be the case in GHC}, we don't need the additional
-complexity.
-
-\item The meaning of "\texttt{bound}" in the FFI declarations is probably
-rather unobvious to people who haven't been following this discussion. Can
-somebody think of something that is more meaningful?
-
-\item Some very broken libraries (Apple's GUI libraries) seem to have
-initialization routines (that run prior to main) which initialize thread local
-state for the "main thread" (the OS thread that the C language \texttt{main()}
-function runs in). Some routines can then only be run in that main thread. Some
-way is needed to allow the programmer to specify that the haskell thread that
-the \texttt{main} action runs in should be bound to the main OS thread.
-
-\item In which module in the libraries should the \texttt{forkBoundThread}
-function go?
-
-\end{itemize}
-
-\newpage
-\part{Second Proposal}
-
-This proposal avoids introducing yet another language extension, and it allows
-foreign calls to be bound to the main thread (which is required to use Apple's
-libraries).
-
-The main idea is that Haskell threads are at first only ``associated'' with
-native threads. There is a combinator @threadbound :: IO() -> IO()@ (somebody
-\emph{please} think of a better name) that ``binds'' a Haskell thread to its
-associated native thread, or to a new native thread if there is no associated
-native thread.
-
-Foreign calls from inside the @threadbound@ combinator are guaranteed to be all
-executed in the same thread, which is guaranteed not to be used for other
-foreign calls from other Haskell threads.
-
-A Haskell thread created by calling-in from Foreign Land is automatically
-associated with the native thread that called the foreign exported function.
-There is no performance penalty if the @threadbound@ combinator is never used.
-
-\section{Operational semantics}
-
-\subsection{State}
-
-The state of the system is represented by a pair
-$$\NS ; \HS$$
-where 
-\begin{itemize}
-\item $\NS = \{t_1, \ldots ,t_n\}$ is a set of \emph{native threads}.
-A native thread is directly supported by the underlying operating
-system, and may have some thread-local state. It may therefore
-be important which native thread executes foreign
-(non-Haskell) code.
-
-\item $\HS = \{h_1, \ldots ,h_n\}$ is a set of \emph{Haskell threads}.
-Haskell threads are supposed to be extremely lightweight, and
-can be created very cheaply. A Haskell thread can only make progress
-if a native thread acts as its execution engine.
-\end{itemize}
-
-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}{h} : S & \mbox{Executing foreign code}\\
-        & & | & \bullet & \mbox{Unknown}\\
-\\
-\mbox{Safety indicator} &  si & ::= & u & \mbox{Unsafe} \\
-        & & | & s & \mbox{Safe} \\
-        & & | & t & \mbox{Thread-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 ``inside the Haskell runtime system'' (that includes, but
-is not limited to, executing Haskell code).
-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)_{at} \\
-\\
-\mbox{Haskell action} &  a & ::= & p ~@>>@~ a  & \mbox{Sequence} \\
-        & & | & \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} \\
-\\
-\mbox{Associated thread id} & at & ::= & \epsilon & \mbox{Not associated} \\
-        & & | & N & \mbox{Associated with native thread N} \\
-\\
-\mbox{Bound thread id} & bt & ::= & N & \mbox{Bound to native thread N}
-
-\end{array}
-$$
-
-Note that $\bound{a}_{bt}$, the ``@threadbound@'' combinator with an explicitly
-specified native thread, is only an ``intermediate result'' of the rules below.
-There will be no way to directly specify this action in a Haskell program
-(or if there will be, it will be a separate extension to the FFI).
-
-In the other proposal (and in a previous version of this one), there was a
-$\ret{N}$ action for returning to foreign land after a call-in. This is not
-necessary here, as Haskell threads always return to their associated native
-threads.
-Threads forked using forkIO do not return anywhere, they just terminate.
-
-\subsection{Initial State}
-
-A program starts with a single Haskell thread that is associated with the
-native thread that executes the C language @main()@ function. This Haskell
-thread executes the Haskell @main@ action.\footnote{This resolves the issue
-that some broken libraries initialize thread-local state for the main thread
-from places like C++ static initializers and therefore insist on other
-functions to be called from the main thread and not from any other thread.}
-
-A Haskell thread spawned using @forkIO@ is not associated with any native
-thread.
-
-\subsection{Evolution}
-
-$$
-\begin{array}{rcll}
-N[\hcall:S]; (\bound{a}~@>>@~b)_{N} 
-        & \Rightarrow 
-        & N[\hcall:S]; (\bound{a}_N~@>>@~b)_{N} & (BIND1) \\
-\\
-; (\bound{a}~@>>@~b)_{\epsilon} 
-        & \Rightarrow 
-        & N[\hcall]; (\bound{a}_N~@>>@~b)_{\epsilon} & (BIND2) \\
-\\
-N[\hcall:S]; (\bound{\epsilon}_N~@>>@~b)_N 
-        & \Rightarrow 
-        & N[\hcall:S]; (b)_N & (UNBIND1) \\
-\\
-N[\hcall]; (\bound{\epsilon}_N~@>>@~b)_{\epsilon} 
-        & \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) \\
-\\
-; (\tau~@>>@~a)_{at} 
-        & \Rightarrow 
-        & ; (a)_{at} & (INT1) \\
-\\
-; (\bound{\tau~@>>@~a}_{bt}~@>>@~b)_{at} 
-        & \Rightarrow 
-        & ; (\bound{a}_{bt}~@>>@~b)_{at} & (INT2) \\
-\\
-N[\hcall]; (\fcall{si}{f}~@>>@~a)_{\epsilon} 
-        & \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) \\
-\\
-M[\hcall]; (\fcall{si}{f}~@>>@~a)_N
-        & \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) \\
-\\
-N[\fcall{si}{a_{at}}:S];  
-        & \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}} \\
-\\
-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\}} \\
-\\
-N[\hcall : S]; (\epsilon)_N 
-        & \Rightarrow 
-        & N[S]; & (HRET) \\
-\\
-; (\forkio{a}~@>>@~b)_{at}
-        & \Rightarrow
-        & ; (b)_{at}, (a)_\epsilon & (FORK1) \\
-\\
-; (\bound{\forkio{a}~@>>@~b}_{bt}~@>>@~c)_{at}
-        & \Rightarrow
-        & ; (\bound{b}_{bt}~@>>@~c)_{at}, (a)_\epsilon & (FORK2) \\
-\\
-; (\epsilon)_\epsilon
-        & \Rightarrow
-        & (nothing) & (END) \\
-\\
-(nothing)
-        & \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}} \\
-\end{array}
-$$
-
-Here is what the rules mean:
-\begin{itemize}
-\item (BIND1) states that a Haskell thread associated with a native thread $N$
-becomes bound to the thread $N$ when the @threadbound@ combinator is used (The
-@threadbound@ combinator is annotated with the thread id it binds to).
-
-\item (BIND2) states that an unassociated Haskell thread becomes bound to a new
-native thread when the @threadbound@ combinator is used.
-
-\item A Haskell thread becomes unbound again when
-the action inside the @threadbound@ combinator is finished (UNBIND1). If the
-Haskell thread is not associated with the native thread, the native thread,
-which was spawned by (BIND2), terminates (UNBIND2).
-
-\item (NEST) says that nested invocations of the @threadbound@ combinator are
-legal, but have no effect.
-
-\item Internal actions are simply executed. For the purposes of this proposal,
-it doesn't matter which native thread is used to execute them, so (INT1)
-doesn't mention any native thread. Internal actions inside a @threadbound@
-combinator are no different from other actions (INT2).
-
-\item (FCALL1) says that only a vanilla worker thread $N[H]$ (i.e. with
-nothing on its stack except $H$) can execute a foreign call from an
-unassociated, unbound thread.
-\item Foreign calls from a Haskell thread associated with a native thread $N$
-can either be executed by the native thread $N$ (FCALL2) or by any vanilla
-worker thread $M[H]$ (FCALL3).
-This is left to the discretion of the runtime system - the fact that a Haskell
-thread is associated with a native thread has no effect by itself.
-
-\item (FCALL4) says that a foreign call from a bound Haskell thread (i.e. from
-inside the @threadbound@ combinator) must be executed by the native thread that
-the Haskell thread is bound to.
-
-\item In all (FCALL) cases, the Haskell thread is removed from the pool, and
-captured in the native thread's stack.  The rule (FRET) reinstates the Haskell
-thread (bound or otherwise) when the native thread decides to return from the
-call.
-
-\item Rules (HCALL1) and (HCALL2) deal with foreign code calling Haskell.
-(HCALL1) starts with a native thread that comes ``out of the blue'' with an
-unknown stack $\bullet$. It just puts a new Haskell thread into the pool and
-associates it with the native thread.
-
-(HCALL2) is similar, except that we aren't allowed to make such a call if
-the native thread is in the middle of an unsafe foreign call.  The difference
-between (HCALL1) and (HCALL2) looks very unsavoury\footnote{Maybe we shouldn't
-be modeling the safety levels here at all --- after all, they are independent
-of the issue at hand.}.
-
-\item (HRET) deals with returning from a completed Haskell thread to the
-appropriate calling native thread, which happens to be the associated native
-thread.
-
-\item (FORK1) and (FORK2) say that threads forked using @forkIO@ are not
-associated with any native thread.
-
-\item A thread that is not associated to a native thread (one spawned using
-@forkIO@) just vanishes when it's finished (END).
-
-\item (WKR) and (EXT) allow new native threads to enter the system.
-
-\end{itemize}
-
-From these rules follows an invariant that is very useful from an implementor's
-point of view:
-
-\begin{quote}
-  At any one time, there is at most one Haskell thread
-  associated with, or bound to, any given native thread.
-\end{quote}
-
-\section{Issues}
-
-\begin{itemize}
-\item @threadbound@ is a terrible name.
-\item In which library module should @threadbound@ go?
-\item Shound the threadbound combinator, when used from an unassociated Haskell thread,
-always create a fresh native thread, or may the native thread be reused?
-
-Rule (BIND2) implies that it is a new native thread, and rule (UNBIND2) says that the
-native thread dies after being used. An alternative might be to allow pooling of
-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') \\
-\\
-; (\bound{\epsilon}_N~@>>@~b)_{at}
-        & \Rightarrow 
-        & ; (b)_{at} & (UNBIND') \\
-\end{array}
-$$
-
-The obvious advantage of pooling is, of course, a possible performance gain;
-However, a "fresh" thread has well-defined thread-local state, but for a 
-reused (pooled) thread, thread-local state is unknown. There shouldn't be
-any libraries that rely on threads being ``fresh''\footnote{but of course,
-you can never know what strange ideas people can come up with}, but having old
-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}:\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.
-They are very much simpler than the Second Proposal.
-
-\newpage
-\part{Fourth Proposal}
-
-This proposal is a variant of the Second and Third Proposals; simpler than the Second,
-but addressing concerns about the Third.
-
 \section{Informal semantics}
 
 Here's the basic idea:
@@ -893,7 +99,9 @@ In particular, @forkIO@ forks a new unbound Haskell thread.
 
 \item[Foreign interface.] \mbox{}\\
 \begin{itemize}
-\item No @safe@ vs @threadsafe@ distinction. But we retain the @safe@/@unsafe@ distinction.
+\item No @safe@ vs @threadsafe@ distinction\footnote{``@threadsafe@'' has already
+been removed from the current Release Candidate of the FFI addendum}. 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, if
 any.
 
@@ -907,18 +115,8 @@ run by a Haskell thread bound to the OS thread that made the call.
 
 \item[Open questions and notes.] \mbox{}\\
 \begin{itemize}
-\item Notice that, unlike the Third Proposal, there can be a 1-1 mapping between Haskell threads
+\item Notice that, there \emph{can} be a 1-1 mapping between Haskell threads
 and OS threads.  Furthermore, we can run efficiently on an SMP.
-
-\item The Second Proposal allows a Haskell thread to temporarily bind itself to an OS thread, using the
-@threadBound@ primitive.  The Fourth Proposal simplifies by making that decision when the Haskell
-thread is spawned.  But it would be possible to modify the Fourth Proposal to allow an unbound Haskell
-thread to bind itself to a new OS thread, either for the remainder of its life (@bindToOS@ @::@ @IO ()@),
-or for some nested action (@bindToOS@ @::@ @IO a -> IO a@).  But it's not clear if either of these are really
-necessary.  They can always be simulated with @forkOS@.
-
-\item There is no notion of an ``associated''' OS thread, a complication of the Second Proposal that we
-do not yet fully understand.
 \end{itemize}
 \end{description}