028bb5e71936fe89b4755a38ae0e181feebf3c38
[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}{HCALL}
22 \newcommand{\fcall}[2]{FCALL^{#1}~#2}
23 \newcommand{\ret}[1]{RET~#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 \section{State}
43
44 The state of the system is represented by a pair
45 $$\NS ; \HS$$
46 where
47 \begin{itemize}
48 \item $\NS = \{t_1, \ldots ,t_n\}$ is a set of \emph{native threads}.
49 A native thread is directly supported by the underlying operating
50 system, and may have some thread-local state. It may therefore
51 be important which native thread executes foreign
52 (non-Haskell) code.
53
54 \item $\HS = \{h_1, \ldots ,h_n\}$ is a set of \emph{Haskell threads}.
55 Haskell threads are supposed to be extremely lightweight, and
56 can be created very cheaply. A Haskell thread can only make progress
57 if a native thread acts as its execution engine.
58 \end{itemize}
59
60 The syntax of a native thread is this:
61 $$
62 \begin{array}{lrcll}
63 \mbox{Native thread} & t & ::= & N[stk] \\
64 \\
65 \mbox{Native thread stack} & stk & ::= & \epsilon & \mbox{Empty}\\
66 & & | & \hcall : stk & \mbox{Executing Haskel} \\
67 & & | & \fcall{si}{h} : stk & \mbox{Executing foreign code}\\
68 \\
69 \mbox{Safety indicator} & si & ::= & u & \mbox{Unsafe} \\
70 & & | & s & \mbox{Safe} \\
71 & & | & t & \mbox{Thread-safe} \\
72 \end{array}
73 $$
74 A native thread of form $N[stk]$ has thread-id $N$, while $stk$ is
75 an abstraction of its call stack. If $\hcall$ is on top of the stack,
76 the thread is willing to execute a Haskell thread. If $\fcall{si}{h}$ is
77 on top of the stack, the thread is in the process of dealing with a call
78 to a foreign function, which will return its result to the Haskell thread
79 $h$. The safety-indicator $si$ is from teh FFI spec.
80
81 The syntax of a Haskell thread is this:
82 $$
83 \begin{array}{lrcl}
84 \mbox{Haskell thread} & h & ::= & (a)_{bt} \\
85 \\
86 \mbox{Haskell action} & a & ::= & pa ~@>>@~ a \\
87 & & | & @ret@ \\
88 \\
89 \mbox{Primitive action} & a & ::= & \tau \\
90 & & | & \fcall{si}{f} \\
91 \\
92 \mbox{Bound task id} & bt & ::= & \epsilon \\
93 & & | & N
94 \end{array}
95 $$
96 A Haskell thread $h$ of form $(a)_{bt}$ has action $a$. The indicator
97 $bt$ tells whether the Haskell thread is \emph{bound to} a native
98 thread. If $bt$ is $\epsilon$, the Haskell thread is not bound to a
99 native thread; if $bt$ is $N$, the Haskell thread is bound to native
100 thread $N$. Specifing exactly what it means for a Haskell thread to
101 be bound to a native thread is the main purpose of this document.
102
103 An action $a$ is a sequence of primitive actions, finishing with a
104 return of some kind. A primitive action is either some internal Haskell
105 thing (such as performing a bit of evaluation, or operating on an @MVar@),
106 or else it is a call to a foreign function $f$.
107
108 We do not model the data passed to, or returned from, a foreign call, nor
109 any details of what ``internal Haskell'' operations are.
110
111 \section{Evolution}
112
113 We describe how the system evolves in a very standard way, using
114 transition rules, of form
115 $$
116 \NS ; \HS ~\Rightarrow~ \NS' ; \HS'
117 $$
118 The structural rules are these:
119 $$
120 \begin{array}{c}
121 \infer{\NS \cup \{t\} ; \HS ~\Rightarrow~ \NS' \cup \{t\}; \HS'}
122 {\NS ; \HS ~\Rightarrow~ \NS' ; \HS'}
123 \qquad
124 \infer{\NS ; \HS \cup \{h\} ~\Rightarrow~ \NS'; \HS' \cup \{h\}}
125 {\NS ; \HS ~\Rightarrow~ \NS' ; \HS'}
126 \end{array}
127 $$
128 These standard rules allow us to write the interesting transitions with less cluter.
129 $$
130 \begin{array}{rcll}
131 T[\hcall:stk]; (\tau~@>>@~a)_{bt}
132 & \Rightarrow
133 & T[\hcall:stk]; (a)_{bt} & (INT) \\
134 \\
135 T[\hcall]; (\fcall{si}{f}~@>>@~a)_{\epsilon}
136 & \Rightarrow
137 & T[\fcall{si}{a_\epsilon},\hcall]; & (FCALL1) \\
138
139 \\
140 T[\hcall:stk]; (@fcall@~f~@>>@~a)_T
141 & \Rightarrow
142 & T[\fcall{si}{a_T}:stk]; & (FCALL2) \\
143 \\
144 T[\fcall{si}{a_{bt}}:stk];
145 & \Rightarrow
146 & T[stk]; a_{bt} & (FRET) \\
147 \\
148 % empty %
149 & \Rightarrow
150 & \nu(~T[\hcall]; (f ~@>>@~ \ret{T})_{bt}) & (HCALL1) \\
151 & \multicolumn{2}{l}{\mbox{where} bt \begin{array}[t]{ll}
152 \epsilon & \mbox{if $f$ is a non-bound foreign export} \\
153 T & \mbox{if $f$ is a bound foreign export}
154 \end{array}} \\
155 \\
156 T[\fcall{si}{a_{bt}} : stk];
157 & \Rightarrow
158 & T[\hcall : \fcall{si}{a_{bt}} : stk]; ~ (f ~@>>@~ \ret{T})_{bt} & (HCALL2) \\
159 & \multicolumn{2}{l}{\mbox{where}~si \in \{s,t\}} \\
160 & \multicolumn{2}{l}{\mbox{and} bt \begin{array}[t]{ll}
161 \epsilon & \mbox{if $f$ is a non-bound foreign export} \\
162
163 T & \mbox{if $f$ is a bound foreign export}
164 \end{array}} \\
165 \\
166 T[\hcall : stk]; \ret{T}
167 & \Rightarrow
168 & T[stk]; & (HRET) \\
169 \\
170 % empay $
171 & \Rightarrow
172 & \nu{ T[\hcall]; ) & (SPAWN) \\
173 \end{array}
174 $$
175 Here is what the rules mean:
176 \begin{itemize}
177 \item
178 \end{document}