028bb5e71936fe89b4755a38ae0e181feebf3c38
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}{HCALL}
22 \newcommand{\fcall}{FCALL^{#1}~#2}
23 \newcommand{\ret}{RET~#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 \section{State}
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
54 \item $\HS = \{h_1, \ldots ,h_n\}$ is a set of \emph{Haskell threads}.
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}
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.
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.
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$.
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.
111 \section{Evolution}
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) \\ 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} \\ 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}