More stuff
authorSimon Peyton Jones <simonpj@microsoft.com>
Fri, 10 Jan 2003 15:14:16 +0000 (15:14 +0000)
committerSimon Peyton Jones <simonpj@microsoft.com>
Fri, 10 Jan 2003 15:14:16 +0000 (15:14 +0000)
ffi/threads.tex

index dff79be..028bb5e 100644 (file)
@@ -19,7 +19,8 @@
 \newcommand{\HS}{{\cal H}}
 %      HS: set of Haskell threads
 \newcommand{\hcall}{HCALL}
-\newcommand{\fcall}[1]{FCALL~#1}
+\newcommand{\fcall}[2]{FCALL^{#1}~#2}
+\newcommand{\ret}[1]{RET~#1}
 
 
 \begin{document}
@@ -58,19 +59,24 @@ if a native thread acts as its execution engine.
 
 The syntax of a native thread is this:
 $$
-\begin{array}{lrcl}
+\begin{array}{lrcll}
 \mbox{Native thread} &  t & ::= & N[stk] \\
 \\
-\mbox{Native thread stack} &  stk & ::= & \epsilon \\
-       & & | & \hcall : stk \\
-       & & | & \fcall{f} : stk
+\mbox{Native thread stack} &  stk & ::= & \epsilon & \mbox{Empty}\\
+       & & | & \hcall : stk  & \mbox{Executing Haskel} \\
+       & & | & \fcall{si}{h} : stk & \mbox{Executing foreign code}\\
+\\
+\mbox{Safety indicator} &  si & ::= & u & \mbox{Unsafe} \\
+       & & | & s & \mbox{Safe} \\
+       & & | & t & \mbox{Thread-safe} \\
 \end{array}
 $$
 A native thread of form $N[stk]$ has thread-id $N$, while $stk$ 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{f}$ is
+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 the foreign function $f$.  
+to a foreign function, which will return its result to the Haskell thread
+$h$.  The safety-indicator $si$ is from teh FFI spec.
 
 The syntax of a Haskell thread is this:
 $$
@@ -81,7 +87,7 @@ $$
        & & | & @ret@ \\
 \\
 \mbox{Primitive action} &  a & ::= & \tau \\
-       & & | & @fcall@~f \\
+       & & | & \fcall{si}{f} \\
 \\
 \mbox{Bound task id} & bt & ::= & \epsilon \\
        & & | & N
@@ -121,6 +127,52 @@ $$
 $$
 These standard rules allow us to write the interesting transitions with less cluter.
 $$
-\begin{arary}{rcl}
+\begin{array}{rcll}
+T[\hcall:stk]; (\tau~@>>@~a)_{bt} 
+       & \Rightarrow 
+       & T[\hcall:stk]; (a)_{bt} & (INT) \\
+\\
+T[\hcall]; (\fcall{si}{f}~@>>@~a)_{\epsilon} 
+       & \Rightarrow 
+       & T[\fcall{si}{a_\epsilon},\hcall];  & (FCALL1) \\
 
+\\
+T[\hcall:stk]; (@fcall@~f~@>>@~a)_T 
+       & \Rightarrow 
+       & T[\fcall{si}{a_T}:stk];  & (FCALL2) \\
+\\
+T[\fcall{si}{a_{bt}}:stk];  
+       & \Rightarrow 
+       & T[stk]; a_{bt} & (FRET) \\
+\\
+% empty %
+       & \Rightarrow 
+       & \nu(~T[\hcall];  (f ~@>>@~ \ret{T})_{bt}) & (HCALL1) \\
+       & \multicolumn{2}{l}{\mbox{where} bt \begin{array}[t]{ll}
+               \epsilon & \mbox{if $f$ is a non-bound foreign export} \\
+               T & \mbox{if $f$ is a bound foreign export}
+          \end{array}} \\
+\\
+T[\fcall{si}{a_{bt}} : stk]; 
+       & \Rightarrow 
+       & T[\hcall : \fcall{si}{a_{bt}} : stk]; ~ (f ~@>>@~ \ret{T})_{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} \\
+
+               T & \mbox{if $f$ is a bound foreign export}
+          \end{array}} \\
+\\
+T[\hcall : stk]; \ret{T} 
+       & \Rightarrow 
+       & T[stk]; & (HRET) \\
+\\
+% empay $
+       & \Rightarrow 
+       & \nu{ T[\hcall]; ) & (SPAWN) \\
+\end{array}
+$$
+Here is what the rules mean:
+\begin{itemize}
+\item 
 \end{document}