Threads stuff
[haskell-report.git] / ffi / threads.tex
1 \documentclass{article}
2
3 \usepackage{proof}
4 \usepackage{code}
5
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}
15
16
17 \newcommand{\NS}{{\cal N}}
18 % NS: set of native threads
19 \newcommand{\HS}{{\cal H}}
20 % HS: set of Haskell threads
21 \newcommand{\hcall}{H}
22 \newcommand{\fcall}[2]{F^{#1}~#2}
23 \newcommand{\ret}[1]{R~#1}
24
25
26 \begin{document}
27
28
29 \title{A semantics for foreign threads}
30
31 \author{Simon Peyton Jones \and Simon Marlow}
32
33
34 \makeatactive
35
36 \section{Introduction}
37
38 \emph{Insert the foreign-thread justification here.}
39
40 Simon and I are confused by what it means. This is our attempt to specify it precisely.
41
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.
45
46
47
48 \section{State}
49
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
58 (non-Haskell) code.
59
60 \item $\HS = \{h_1, \ldots ,h_n\}$ is a set of \emph{Haskell threads}.
61 Haskell threads are supposed to be extremely lightweight, and
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}
65
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.
87
88 The syntax of a Haskell thread is this:
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.
109
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$.
114
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.
117
118 \section{Evolution}
119
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) \\
145
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} \\
169
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.
195
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.)
200
201 \item In either (FCALL) case, the Haskell thread is removed from the pool, and captured in the
202 native thread's stack. The rule (FRET) reinstates the Haskell thread (bound or otherwise)
203 when the native thread decides to return from the call.
204
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.
209
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.
213
214 \item (HRET) deals with returning from a completed Haskell thread to the appropriate
215 calling native thread. Notice that even an unbound Haskell thread must return its result
216 to the right calling native thread, hence the ``return action'' $\ret{t}$ tacked onto
217 the end of the Haskell thread.
218
219 \item (WKR) and (EXT) allow new native threads to enter the system.
220
221 \end{itemize}
222
223
224 \end{document}