1 \documentclass{article}
3 \usepackage{proof}
4 \usepackage{code}
6 \sloppy
7 \setlength{\parskip}{0.5\baselineskip plus 0.2\baselineskip minus 0.1\baselineskip}
8 \setlength{\parsep}{\parskip}
9 \setlength{\topsep}{0cm}
10 \setlength{\parindent}{0cm}
11 \renewcommand{\textfraction}{0}
12 \renewcommand{\topfraction}{1}
13 \renewcommand{\floatpagefraction}{0.8}
14 \renewcommand{\dblfloatpagefraction}{0.8}
17 \newcommand{\NS}{{\cal N}}
18 % NS: set of native threads
19 \newcommand{\HS}{{\cal H}}
21 \newcommand{\hcall}{H}
22 \newcommand{\fcall}{F^{#1}~#2}
23 \newcommand{\ret}{R~#1}
26 \begin{document}
29 \title{A semantics for foreign threads}
31 \author{Simon Peyton Jones \and Simon Marlow}
34 \makeatactive
36 \section{Introduction}
38 \emph{Insert the foreign-thread justification here.}
40 Simon and I are confused by what it means. This is our attempt to specify it precisely.
42 We do not claim that the system accurately describes either of the two proposals on
43 the table, but we think that it can be adjusted until it is. Our main goal is to
44 provide a precise framework in which to discuss teh design tradeoffs.
48 \section{State}
50 The state of the system is represented by a pair
51 $$\NS ; \HS$$
52 where
53 \begin{itemize}
54 \item $\NS = \{t_1, \ldots ,t_n\}$ is a set of \emph{native threads}.
55 A native thread is directly supported by the underlying operating
56 system, and may have some thread-local state. It may therefore
57 be important which native thread executes foreign
60 \item $\HS = \{h_1, \ldots ,h_n\}$ is a set of \emph{Haskell threads}.
62 can be created very cheaply. A Haskell thread can only make progress
63 if a native thread acts as its execution engine.
64 \end{itemize}
66 The syntax of a native thread is this:
67 $$68 \begin{array}{lrcll} 69 \mbox{Native thread} & t & ::= & N[S] \\ 70 \\ 71 \mbox{Native thread stack} & S & ::= & \epsilon & \mbox{Empty}\\ 72 & & | & \hcall : S & \mbox{Executing Haskel} \\ 73 & & | & \fcall{si}{h} : S & \mbox{Executing foreign code}\\ 74 & & | & \bullet & \mbox{Unknown}\\ 75 \\ 76 \mbox{Safety indicator} & si & ::= & u & \mbox{Unsafe} \\ 77 & & | & s & \mbox{Safe} \\ 78 & & | & t & \mbox{Thread-safe} \\ 79 \end{array} 80$$
81 A native thread of form $N[S]$ has thread-id $N$, while $S$ is
82 an abstraction of its call stack. If $\hcall$ is on top of the stack,
83 the thread is willing to execute a Haskell thread. If $\fcall{si}{h}$ is
84 on top of the stack, the thread is in the process of dealing with a call
85 to a foreign function, which will return its result to the Haskell thread
86 $h$. The safety-indicator $si$ is from teh FFI spec.
89 $$90 \begin{array}{lrcll} 91 \mbox{Haskell thread} & h & ::= & (a)_{bt} \\ 92 \\ 93 \mbox{Haskell action} & a & ::= & p ~@>>@~ a & \mbox{Sequence} \\ 94 & & | & \ret{N} & \mbox{Return to native thread N} \\ 95 \\ 96 \mbox{Primitive action} & p & ::= & \tau & \mbox{Internal action} \\ 97 & & | & \fcall{si}{f} & \mbox{Foreign call} \\ 98 \\ 99 \mbox{Bound thread id} & bt & ::= & \epsilon & \mbox{Not bound} \\ 100 & & | & N & \mbox{Bound to native thread N} 101 \end{array} 102$$
103 A Haskell thread $h$ of form $(a)_{bt}$ has action $a$. The indicator
104 $bt$ tells whether the Haskell thread is \emph{bound to} a native
105 thread. If $bt$ is $\epsilon$, the Haskell thread is not bound to a
106 native thread; if $bt$ is $N$, the Haskell thread is bound to native
107 thread $N$. Specifing exactly what it means for a Haskell thread to
108 be bound to a native thread is the main purpose of this document.
110 An action $a$ is a sequence of primitive actions, finishing with a
111 return of some kind. A primitive action is either some internal Haskell
112 thing (such as performing a bit of evaluation, or operating on an @MVar@),
113 or else it is a call to a foreign function $f$.
115 We do not model the data passed to, or returned from, a foreign call, nor
116 any details of what internal Haskell'' operations are.
118 \section{Evolution}
120 We describe how the system evolves in a very standard way, using
121 transition rules, of form
122 $$123 \NS ; \HS ~\Rightarrow~ \NS' ; \HS' 124$$
125 The structural rules are these:
126 $$127 \begin{array}{c} 128 \infer{\NS \cup \{t\} ; \HS ~\Rightarrow~ \NS' \cup \{t\}; \HS'} 129 {\NS ; \HS ~\Rightarrow~ \NS' ; \HS'} 130 \qquad 131 \infer{\NS ; \HS \cup \{h\} ~\Rightarrow~ \NS'; \HS' \cup \{h\}} 132 {\NS ; \HS ~\Rightarrow~ \NS' ; \HS'} 133 \end{array} 134$$
135 These standard rules allow us to write the interesting transitions with less cluter.
136 $$137 \begin{array}{rcll} 138 N[\hcall:S]; (\tau~@>>@~a)_{bt} 139 & \Rightarrow 140 & N[\hcall:S]; (a)_{bt} & (INT) \\ 141 \\ 142 N[\hcall]; (\fcall{si}{f}~@>>@~a)_{\epsilon} 143 & \Rightarrow 144 & N[\fcall{si}{a_\epsilon},\hcall]; & (FCALL1) \\ 146 \\ 147 N[\hcall:S]; (\fcall{si}{f}@>>@~a)_N 148 & \Rightarrow 149 & N[\fcall{si}{a_N}:S]; & (FCALL2) \\ 150 \\ 151 N[\fcall{si}{a_{bt}}:S]; 152 & \Rightarrow 153 & N[S]; a_{bt} & (FRET) \\ 154 \\ 155 N[\bullet]; 156 & \Rightarrow 157 & N[\hcall:\bullet]; (f ~@>>@~ \ret{N})_{bt} & (HCALL1) \\ 158 & \multicolumn{2}{l}{\mbox{where}~ bt \begin{array}[t]{ll} 159 = \epsilon & \mbox{if f is a non-bound foreign export} \\ 160 = N & \mbox{if f is a bound foreign export} 161 \end{array}} \\ 162 \\ 163 N[\fcall{si}{a_{bt}} : S]; 164 & \Rightarrow 165 & N[\hcall : \fcall{si}{a_{bt}} : S]; ~ (f ~@>>@~ \ret{N})_{bt} & (HCALL2) \\ 166 & \multicolumn{2}{l}{\mbox{where}~si \in \{s,t\}} \\ 167 & \multicolumn{2}{l}{\mbox{and}~ bt \begin{array}[t]{ll} 168 = \epsilon & \mbox{if f is a non-bound foreign export} \\ 170 = N & \mbox{if f is a bound foreign export} 171 \end{array}} \\ 172 \\ 173 N[\hcall : S]; \ret{N} 174 & \Rightarrow 175 & N[S]; & (HRET) \\ 176 \\ 177 (nothing) 178 & \Rightarrow 179 & N[\hcall]; & (WKR) \\ 180 & \multicolumn{2}{l}{\mbox{where N is fresh}} \\ 181 \\ 182 (nothing) 183 & \Rightarrow 184 & N[\bullet]; & (EXT) \\ 185 & \multicolumn{2}{l}{\mbox{where N is fresh}} \\ 186 \end{array} 187$$
188 Here is what the rules mean:
189 \begin{itemize}
190 \item (INT) says that an internal action of a Haskell thread
191 can be executed by any native thread that
192 is in the Haskell state; that is, has $H$ on top of its stack. This is true
193 even if the native thread has called a bound foreign export, and that
194 Haskell function is still running.
196 \item On the other hand, (FCALL1) says that only a vanilla worker thread $N[H]$ (i.e. with
197 nothing on its stack except $H$) can execute an unbound foreign call. Similarly (FCALL2) says
198 that only native thread $N$ can execute a foreign call from a Haskell thread bound to $N$.
199 (This is under the proposal that foriegn imports are not labelled bound/unbound.)
201 \item In either (FCALL) case, the Haskell thread is removed from the pool, and captured in the
203 when the native thread decides to return from the call.
205 \item Rules (HCALL1) and (HCALL2) deal with foreign code calling Haskell. (HCALL1)
206 starts with a native thread that comes out of the blue'' with an unknown stack $\bullet$.
207 It just puts a new Haskell thread into the pool, bound or otherwise depending on
208 whether the foreign export being called is labelled as bound.
210 (HCALL2) is similar, except that we aren't allowed to make such a call if
211 the native thread is in the middle of an unsafe foreign call. The difference
212 between (HCALL1) and (HCALL2) looks very unsavoury.
214 \item (HRET) deals with returning from a completed Haskell thread to the appropriate
216 to the right calling native thread, hence the return action'' $\ret{t}$ tacked onto