88c67ca75f8568a455e7f392607a8da456d419b4
[phd-thesis.git] / top / imp.tex
1 \documentclass[../thesis.tex]{subfiles}
2
3 \input{subfilepreamble}
4
5 \setcounter{chapter}{5}
6
7 \begin{document}
8 \input{subfileprefix}
9 \chapter{Implementation}%
10 \label{chp:implementation}
11 \begin{chapterabstract}
12 \noindent This chapter shows the implementation of the \gls{MTASK} system by:
13 \begin{itemize}
14 \item gives details of the implementation of \gls{MTASK}'s \gls{TOP} engine that executes the \gls{MTASK} tasks on the microcontroller;
15 \item shows the implementation of the byte code compiler for \gls{MTASK}'s \gls{TOP} language;
16 \item explains the machinery used to automatically serialise and deserialise data to-and-fro the device.
17 \end{itemize}
18 \end{chapterabstract}
19
20 Microcontrollers usually have flash-based program memory which wears out fairly quick.
21 For example, the atmega328p in the \gls{ARDUINO} UNO is rated for 10000 write cycles.
22 While this sounds like a lot, if new tasks are sent to the device every minute or so, a lifetime of only seven days is guaranteed.
23 Hence, for dynamic applications, interpretation on the device is necessary, saving precious write cycles of the program memory.
24
25 In order to provide the device with the tools to interpret the byte code, it is programmed with a \gls{RTS}, a customisable domain-specific \gls{OS} that takes care of the execution of tasks but also low-level mechanisms such as the communication, multi tasking, and memory management.
26 Once the device is programmed with the \gls{MTASK} \gls{RTS}, it can continuously receive new tasks without the need for reprogramming.
27 The \gls{OS} is written in portable \ccpp{} and only contains a small device-specific portion.
28
29 \section{\texorpdfstring{\Glsxtrlong{RTS}}{Run time system}}
30 The event loop of the \gls{RTS} is executed repeatedly and consists of three distinct phases.
31 After doing the three phases, the devices goes to sleep for as long as possible (see \cref{chp:green_computing_mtask}).
32
33 \subsection{Communication}
34 In the first phase, the communication channels are processed.
35 The exact communication method is a customisable device-specific option baked into the \gls{RTS}.
36 The interface is deliberately kept simple and consists of a two layer interface: a link interface and a communication interface.
37 Besides opening, closing and cleaning up, the link interface has only three functions that are shown in \cref{lst:link_interface}.
38 Consequently, implementing this link interface is very simple but allows for many more advanced link settings such as buffering.
39 There are implementations for this interface for serial or Wi-Fi connections using \gls{ARDUINO} and \gls{TCP} connections for Linux.
40
41 \begin{lstArduino}[caption={Link interface of the \gls{MTASK} \gls{RTS}.},label={lst:link_interface}]
42 bool link_input_available(void);
43 uint8_t link_read_byte(void);
44 void link_write_byte(uint8_t b);
45 \end{lstArduino}
46
47 The communication interface abstracts away from this link interface and is typed instead.
48 It contains only two functions as seen in \cref{lst:comm_interface}.
49 There are implementations for direct communication, or communication using an \gls{MQTT} broker.
50 Both use the automatic serialisation and deserialisation shown in \cref{sec:ccodegen}.
51
52 \begin{lstArduino}[caption={Communication interface of the \gls{MTASK} \gls{RTS}.},label={lst:comm_interface}]
53 struct MTMessageTo receive_message(void);
54 void send_message(struct MTMessageFro msg);
55 \end{lstArduino}
56
57 Processing the received messages from the communication channels happens synchronously and the channels are exhausted completely before moving on to the next phase.
58 There are several possible messages that can be received from the server:
59
60 \begin{description}
61 \item[SpecRequest]
62 is a message instructing the device to send its specification and is sent usually immediately after connecting.
63 The \gls{RTS} responds with a \texttt{Spec} answer containing the specification.
64 \item[TaskPrep]
65 tells the device a (big) task is on its way.
66 Especially on faster connections, it may be the case that the communication buffers overflow because a big message is sent while the \gls{RTS} is busy executing tasks.
67 This allows the \gls{RTS} to postpone execution for a while, until the big task has been received.
68 The server sends the big task when the device acknowledges (by sending a \texttt{TaskPrepAck} message) the preparation.
69 \item[Task]
70 contains a new task, its peripheral configuration, the \glspl{SDS}, and the bytecode.
71 The new task is immediately copied to the task storage but is only initialised during the next phase after which a \texttt{TaskAck} is sent.
72 Tasks are stored below the stack, but since the stack is only used in the middle phase, execution, it is no problem that it moves.
73 \item[SdsUpdate]
74 notifies the device of the new value for a lowered \gls{SDS}.
75 The old value of the lowered \gls{SDS} is immediately replaced with the new one.
76 There is no acknowledgement required.
77 \item[TaskDel]
78 instructs the device to delete a running task.
79 Tasks are automatically deleted when they become stable.
80 However, a task may also be deleted when the surrounding task on the server is deleted, for example when the task is on the left-hand side of a step combinator and the condition to step holds.
81 The device acknowledges by sending a \texttt{TaskDelAck}.
82 \item[Shutdown]
83 tells the device to reset.
84 \end{description}
85
86 \subsection{Execution}
87 The second phase consists of performing one execution step for all tasks that wish for it.
88 Tasks are ordered in a priority queue ordered by the time a task needs to be executed, the \gls{RTS} selects all tasks that can be scheduled, see \cref{sec:scheduling} for more details.
89 A task is stored below the stack and its complete state is a \gls{CLEAN} record contain most importantly the task id, a pointer to the task tree in the heap (null if not initialised yet), the current task value, the configuration of \glspl{SDS}, the configuration of peripherals, the byte code and some scheduling information.
90
91 If a task is not initialized yet, i.e.\ the pointer to the current task tree is still null, the byte code of the main function is interpreted.
92 The main expression always produces a task tree.
93 The rewriting engine uses the interpreter when needed, e.g.\ to calculate the step continuations.
94 The rewriter and the interpreter use the same stack to store intermediate values.
95 Rewriting steps are small so that interleaving results in seemingly parallel execution.
96 In this phase new task tree nodes may be allocated.
97 Both rewriting and initialization are atomic operations in the sense that no processing on SDSs is done other than SDS operations from the task itself.
98 The host is notified if a task value is changed after a rewrite step.
99
100 \subsection{Memory management}
101 The third and final phase is memory management.
102 The \gls{MTASK} \gls{RTS} is designed to run on systems with as little as \qty{2}{\kibi\byte} of \gls{RAM}.
103 Aggressive memory management is therefore vital.
104 Not all firmwares for microprocessors support heaps and---when they do---allocation often leaves holes when not used in a \emph{last in first out} strategy.
105 The \gls{RTS} uses a chunk of memory in the global data segment with its own memory manager tailored to the needs of \gls{MTASK}.
106 The size of this block can be changed in the configuration of the \gls{RTS} if necessary.
107 On an \gls{ARDUINO} UNO---equipped with \qty{2}{\kibi\byte} of \gls{RAM}---the maximum viable size is about \qty{1500}{\byte}.
108 The self-managed memory uses a similar layout as the memory layout for \gls{C} programs only the heap and the stack are switched (see \cref{fig:memory_layout}).
109
110 \begin{figure}
111 \centering
112 \includestandalone{memorylayout}
113 \caption{Memory layout}\label{fig:memory_layout}
114 \end{figure}
115
116 In memory, task data grows from the bottom up and the interpreter stack is located directly on top of it growing in the same direction.
117 As a consequence, the stack moves when a new task is received.
118 This never happens within execution because communication is always processed before execution.
119 Values in the interpreter are always stored on the stack, even tuples.
120 Task trees grow from the top down as in a heap.
121 This approach allows for flexible ratios, i.e.\ many tasks and small trees or few tasks and big trees.
122
123 Stable tasks, and unreachable task tree nodes are removed.
124 If a task is to be removed, tasks with higher memory addresses are moved down.
125 For task trees---stored in the heap---the \gls{RTS} already marks tasks and task trees as trash during rewriting so the heap can be compacted in a single pass.
126 This is possible because there is no sharing or cycles in task trees and nodes contain pointers pointers to their parent.
127
128 \todo{plaa\-tje van me\-mo\-ry hier}
129
130 \section{Compiler}
131 \subsection{Instruction set}
132 The instruction set is a fairly standard stack machine instruction set extended with special \gls{TOP} instructions.
133 \Cref{lst:instruction_type} shows the \gls{CLEAN} type representing the instruction set of which \cref{tbl:instr_task} gives detailed semantics.
134 Type synonyms are used to provide insight on the arguments of the instructions.
135 One notable instruction is the \cleaninline{MkTask} instruction, it allocates and initialises a task tree node and pushes a pointer to it on the stack.
136
137 \begin{lstClean}[caption={The type housing the instruction set.},label={lst:instruction_type}]
138 :: ArgWidth :== UInt8 :: ReturnWidth :== UInt8
139 :: Depth :== UInt8 :: Num :== UInt8
140 :: SdsId :== UInt8 :: JumpLabel =: JL UInt16
141
142 //** Datatype housing all instructions
143 :: BCInstr
144 //Return instructions
145 //Jumps
146 = BCJumpF JumpLabel | BCJump JumpLabel | BCLabel JumpLabel | BCJumpSR ArgWidth JumpLabel
147 | BCReturn ReturnWidth ArgWidth | BCTailcall ArgWidth ArgWidth JumpLabel
148 //Arguments
149 | BCArgs ArgWidth ArgWidth
150 //Task node creation and refinement
151 | BCMkTask BCTaskType | BCTuneRateMs | BCTuneRateSec
152 //Task value ops
153 | BCIsStable | BCIsUnstable | BCIsNoValue | BCIsValue
154 //Stack ops
155 | BCPush String255 | BCPop Num | BCRot Depth Num | BCDup | BCPushPtrs
156 //Casting
157 | BCItoR | BCItoL | BCRtoI | ...
158 // arith
159 | BCAddI | BCSubI | ...
160 ...
161
162 //** Datatype housing all task types
163 :: BCTaskType
164 = BCStableNode ArgWidth | ArgWidth
165 // Pin io
166 | BCReadD | BCWriteD | BCReadA | BCWriteA | BCPinMode
167 // Interrupts
168 | BCInterrupt
169 // Repeat
170 | BCRepeat
171 // Delay
172 | BCDelay | BCDelayUntil //* Only for internal use
173 // Parallel
174 | BCTAnd | BCTOr
175 //Step
176 | BCStep ArgWidth JumpLabel
177 //Sds ops
178 | BCSdsGet SdsId | BCSdsSet SdsId | BCSdsUpd SdsId JumpLabel
179 // Rate limiter
180 | BCRateLimit
181 ////Peripherals
182 //DHT
183 | BCDHTTemp UInt8 | BCDHTHumid UInt8
184 ...
185 \end{lstClean}
186
187 \subsection{Compiler}
188 The bytecode compiler interpretation for the \gls{MTASK} language is implemented as a monad stack containing a writer monad and a state monad.
189 The writer monad is used to generate code snippets locally without having to store them in the monadic values.
190 The state monad accumulates the code, and stores the stateful data the compiler requires.
191 \Cref{lst:compiler_state} shows the data type for the state, storing:
192 function the compiler currently is in;
193 code of the main expression;
194 context (see \todo{insert ref to compilation rules step here});
195 code for the functions;
196 next fresh label;
197 a list of all the used \glspl{SDS}, either local \glspl{SDS} containing the initial value (\cleaninline{Left}) or lifted \glspl{SDS} (see \cref{sec:liftsds}) containing a reference to the associated \gls{ITASK} \gls{SDS};
198 and finally there is a list of peripherals used.
199
200 \begin{lstClean}[label={lst:compiler_state},caption={\Gls{MTASK}'s byte code compiler type}]
201 :: BCInterpret a :== StateT BCState (WriterT [BCInstr] Identity) a
202 :: BCState =
203 { bcs_infun :: JumpLabel
204 , bcs_mainexpr :: [BCInstr]
205 , bcs_context :: [BCInstr]
206 , bcs_functions :: Map JumpLabel BCFunction
207 , bcs_freshlabel :: JumpLabel
208 , bcs_sdses :: [Either String255 MTLens]
209 , bcs_hardware :: [BCPeripheral]
210 }
211 :: BCFunction =
212 { bcf_instructions :: [BCInstr]
213 , bcf_argwidth :: UInt8
214 , bcf_returnwidth :: UInt8
215 }
216 \end{lstClean}
217
218 Executing the compiler is done by providing an initial state.
219 After compilation, several post-processing steps are applied to make the code suitable for the microprocessor.
220 First, in all tail call \cleaninline{BCReturn}'s are replaced by \cleaninline{BCTailCall} to implement tail call elimination.
221 Furthermore, all byte code is concatenated, resulting in one big program.
222 Many instructions have commonly used arguments so shorthands are introduced to reduce the program size.
223 For example, the \cleaninline{BCArg} instruction is often called with argument \qtyrange{0}{2} and can be replaced by the \cleaninline{BCArg0}--\cleaninline{BCArg2} shorthands.
224 Furthermore, redundant instructions (e.g.\ pop directly after push) are removed as well in order not to burden the code generation with these intricacies.
225 Finally the labels are resolved to represent actual program addresses instead of freshly generated identifiers.
226 After the byte code is ready, the lifted \glspl{SDS} are resolved to provide an initial value for them.
227 The result---byte code, \gls{SDS} specification and perpipheral specifications---are the result of the process, ready to be sent to the device.
228
229 \section{Compilation rules}
230 This section describes the compilation rules, the translation from abstract syntax to byte code.
231 The compilation scheme consists of three schemes\slash{}functions.
232 When something is surrounded by double vertical bars, e.g.\ $\stacksize{a_i}$, it denotes the number of stack cells required to store it.
233
234 Some schemes have a \emph{context} $r$ as an argument which contains information about the location of the arguments in scope.
235 More information is given in the schemes requiring such arguments.
236
237 \newcommand{\cschemeE}[2]{\mathcal{E}\llbracket#1\rrbracket~#2}
238 \newcommand{\cschemeF}[1]{\mathcal{F}\llbracket#1\rrbracket}
239 \newcommand{\cschemeS}[3]{\mathcal{S}\llbracket#1\rrbracket~#2~#3}
240 \begin{table}
241 \centering
242 \begin{tabularx}{\linewidth}{l X}
243 \toprule
244 Scheme & Description\\
245 \midrule
246 $\cschemeE{e}{r}$ & Produces the value of expression $e$ given the context $r$ and pushes it on the stack.
247 The result can be a basic value or a pointer to a task.\\
248 $\cschemeF{e}$ & Generates the bytecode for functions.\\
249 $\cschemeS{e}{r}{w} $ & Generates the function for the step continuation given the context $r$ and the width $w$ of the left-hand side task value.\\
250 \bottomrule
251 \end{tabularx}
252 \end{table}
253
254 \subsection{Expressions}
255 Almost all expression constructions are compiled using $\mathcal{E}$.
256 The argument of $\mathcal{E}$ is the context (see \cref{ssec:functions}).
257 Values are always placed on the stack; tuples and other compound data types are unpacked.
258 Function calls, function arguments and tasks are also compiled using $\mathcal{E}$ but their compilations is explained later.
259
260 \begin{align*}
261 \cschemeE{\text{\cleaninline{lit}}~e}{r} & = \text{\cleaninline{BCPush (bytecode e)}};\\
262 \cschemeE{e_1\mathbin{\text{\cleaninline{+.}}}e_2}{r} & = \cschemeE{e_1}{r};
263 \cschemeE{e_2}{r};
264 \text{\cleaninline{BCAdd}};\\
265 {} & \text{\emph{Similar for other binary operators}}\\
266 \cschemeE{\text{\cleaninline{Not}}~e}{r} & =
267 \cschemeE{e}{r};
268 \text{\cleaninline{BCNot}};\\
269 {} & \text{\emph{Similar for other unary operators}}\\
270 \cschemeE{\text{\cleaninline{If}}~e_1~e_2~e_3}{r} & =
271 \cschemeE{e_1}{r};
272 \text{\cleaninline{BCJmpF}}\enskip l_{else}; \mathbin{\phantom{=}} \cschemeE{e_2}{r}; \text{\cleaninline{BCJmp}}\enskip l_{endif};\\
273 {} & \mathbin{\phantom{=}} \text{\cleaninline{BCLabel}}\enskip l_{else}; \cschemeE{e_3}{r}; \mathbin{\phantom{=}} \text{\cleaninline{BCLabel}}\enskip l_{endif};\\
274 {} & \text{\emph{Where $l_{else}$ and $l_{endif}$ are fresh labels}}\\
275 \cschemeE{\text{\cleaninline{tupl}}~e_1~e_2}{r} & =
276 \cschemeE{e_1}{r};
277 \cschemeE{e_2}{r};\\
278 {} & \text{\emph{Similar for other unboxed compound data types}}\\
279 \cschemeE{\text{\cleaninline{first}}~e}{r} & =
280 \cschemeE{e}{r};
281 \text{\cleaninline{BCPop}}\enskip w;\\
282 {} & \text{\emph{Where $w$ is the width of the left value and}}\\
283 {} & \text{\emph{similar for other unboxed compound data types}}\\
284 \cschemeE{\text{\cleaninline{second}}\enskip e}{r} & =
285 \cschemeE{e}{r};
286 \text{\cleaninline{BCRot}}\enskip w_1\enskip (w_1+w_2);
287 \text{\cleaninline{BCPop}}\enskip w_2;\\
288 {} & \text{\emph{Where $w_1$ is the width of the left and, $w_2$ of the right value}}\\
289 {} & \text{\emph{similar for other unboxed compound data types}}\\
290 \end{align*}
291
292 Translating $\mathcal{E}$ to \gls{CLEAN} code is very straightforward, it basically means executing the monad.
293 Almost always, the type of the interpretation is not used, i.e.\ it is a phantom type.
294 To still have the functions return the correct type, the \cleaninline{tell`}\footnote{\cleaninline{tell` :: [BCInstr] -> BCInterpret a}} helper is used.
295 This function is similar to the writer monad's \cleaninline{tell} function but is casted to the correct type.
296 \Cref{lst:imp_arith} shows the implementation for the arithmetic and conditional expressions.
297 Note that $r$, the context, is not an explicit argument but stored in the state.
298
299 \begin{lstClean}[caption={Interpretation implementation for the arithmetic and conditional classes.},label={lst:imp_arith}]
300 instance expr BCInterpret where
301 lit t = tell` [BCPush (toByteCode{|*|} t)]
302 (+.) a b = a >>| b >>| tell` [BCAdd]
303 ...
304 If c t e = freshlabel >>= \elselabel->freshlabel >>= \endiflabel->
305 c >>| tell` [BCJumpF elselabel] >>|
306 t >>| tell` [BCJump endiflabel,BCLabel elselabel] >>|
307 e >>| tell` [BCLabel endiflabel]
308 \end{lstClean}
309
310 \subsection{Functions}\label{ssec:functions}
311 Compiling functions occurs in $\mathcal{F}$, which generates bytecode for the complete program by iterating over the functions and ending with the main expression.
312 When compiling the body of the function, the arguments of the function are added to the context so that the addresses can be determined when referencing arguments.
313 The main expression is a special case of $\mathcal{F}$ since it neither has arguments nor something to continue.
314 Therefore, it is just compiled using $\mathcal{E}$.
315
316 \begin{align*}
317 \cschemeF{main=m} & =
318 \cschemeE{m}{[]};\\
319 \cschemeF{f~a_0 \ldots a_n = b~\text{\cleaninline{In}}~m} & =
320 \text{\cleaninline{BCLabel}}~f; \cschemeE{b}{[\langle f, i\rangle, i\in \{(\Sigma^n_{i=0}\stacksize{a_i})..0\}]};\\
321 {} & \mathbin{\phantom{=}} \text{\cleaninline{BCReturn}}~\stacksize{b}~n; \cschemeF{m};\\
322 \end{align*}
323
324 A function call starts by pushing the stack and frame pointer, and making space for the program counter (\cref{lst:funcall_pushptrs}) followed by evaluating the arguments in reverse order (\cref{lst:funcall_args}).
325 On executing \cleaninline{BCJumpSR}, the program counter is set and the interpreter jumps to the function (\cref{lst:funcall_jumpsr}).
326 When the function returns, the return value overwrites the old pointers and the arguments.
327 This occurs right after a \cleaninline{BCReturn} (\cref{lst:funcall_ret}).
328 Putting the arguments on top of pointers and not reserving space for the return value uses little space and facilitates tail call optimization.
329
330 \begin{figure}
331 \begin{subfigure}{.24\linewidth}
332 \centering
333 \includestandalone{memory1}
334 \caption{\cleaninline{BCPushPtrs}}\label{lst:funcall_pushptrs}
335 \end{subfigure}
336 \begin{subfigure}{.24\linewidth}
337 \centering
338 \includestandalone{memory2}
339 \caption{Arguments}\label{lst:funcall_args}
340 \end{subfigure}
341 \begin{subfigure}{.24\linewidth}
342 \centering
343 \includestandalone{memory3}
344 \caption{\cleaninline{BCJumpSR}}\label{lst:funcall_jumpsr}
345 \end{subfigure}
346 \begin{subfigure}{.24\linewidth}
347 \centering
348 \includestandalone{memory4}
349 \caption{\cleaninline{BCReturn}}\label{lst:funcall_ret}
350 \end{subfigure}
351 \caption{The stack layout during function calls.}%
352 \end{figure}
353
354 Calling a function and referencing function arguments are an extension to $\mathcal{E}$ as shown below.
355 Arguments may be at different places on the stack at different times (see \cref{ssec:step}) and therefore the exact location always has to be determined from the context using \cleaninline{findarg}\footnote{\cleaninline{findarg [l`:r] l = if (l == l`) 0 (1 + findarg r l)}}.
356 Compiling argument $a_{f^i}$, the $i$th argument in function $f$, consists of traversing all positions in the current context.
357 Arguments wider than one stack cell are fetched in reverse to preserve the order.
358
359 \begin{align*}
360 \cschemeE{f(a_0, \ldots, a_n)}{r} & =
361 \text{\cleaninline{BCPushPtrs}}; \cschemeE{a_n}{r}; \cschemeE{a_{\ldots}}{r}; \cschemeE{a_0}{r}; \text{\cleaninline{BCJumpSR}}~n~f;\\
362 \cschemeE{a_{f^i}}{r} & =
363 \text{\cleaninline{BCArg}~findarg}(r, f, i)~\text{for all}~i\in\{w\ldots v\};\\
364 {} & v = \Sigma^{i-1}_{j=0}\stacksize{a_{f^j}}~\text{ and }~ w = v + \stacksize{a_{f^i}}\\
365 \end{align*}
366
367 Translating the compilation schemes for functions to Clean is not as straightforward as other schemes due to the nature of shallow embedding.\todo{deze \P{} moet ge\-\"up\-da\-ted worden}
368 The \cleaninline{fun} class has a single function with a single argument.
369 This argument is a Clean function that---when given a callable Clean function representing the mTask function---will produce \cleaninline{main} and a callable function.
370 To compile this, the argument must be called with a function representing a function call in mTask.
371 \Cref{lst:fun_imp} shows the implementation for this as Clean code.
372 To uniquely identify the function, a fresh label is generated.
373 The function is then called with the \cleaninline{callFunction} helper function that generates the instructions that correspond to calling the function.
374 That is, it pushes the pointers, compiles the arguments, and writes the \cleaninline{JumpSR} instruction.
375 The resulting structure (\cleaninline{g In m}) contains a function representing the mTask function (\cleaninline{g}) and the \cleaninline{main} structure to continue with.
376 To get the actual function, \cleaninline{g} must be called with representations for the argument, i.e.\ using \cleaninline{findarg} for all arguments.
377 The arguments are added to the context and \cleaninline{liftFunction} is called with the label, the argument width and the compiler.
378 This function executes the compiler, decorates the instructions with a label and places them in the function dictionary together with the metadata such as the argument width.
379 After lifting the function, the context is cleared again and compilation continues with the rest of the program.
380
381 \begin{lstClean}[label={lst:fun_imp},caption={The backend implementation for functions.}]
382 instance fun (BCInterpret a) BCInterpret | type a where
383 fun def = {main=freshlabel >>= \funlabel->
384 let (g In m) = def \a->callFunction funlabel (toByteWidth a) [a]
385 argwidth = toByteWidth (argOf g)
386 in addToCtx funlabel zero argwidth
387 >>| infun funlabel
388 (liftFunction funlabel argwidth
389 (g (retrieveArgs funlabel zero argwidth)
390 ) ?None)
391 >>| clearCtx >>| m.main
392 }
393
394 argOf :: ((m a) -> b) a -> UInt8 | toByteWidth a
395 callFunction :: JumpLabel UInt8 [BCInterpret b] -> BCInterpret c | ...
396 liftFunction :: JumpLabel UInt8 (BCInterpret a) (?UInt8) -> BCInterpret ()
397 \end{lstClean}
398
399 \subsection{Tasks}\label{ssec:scheme_tasks}
400 Task trees are created with the \cleaninline{BCMkTask} instruction that allocates a node and pushes it to the stack.
401 It pops arguments from the stack according to the given task type.
402 The following extension of $\mathcal{E}$ shows this compilation scheme (except for the step combinator, explained in \cref{ssec:step}).
403
404 \begin{align*}
405 \cschemeE{\text{\cleaninline{rtrn}}~e}{r} & =
406 \cschemeE{e}{r};
407 \text{\cleaninline{BCMkTask BCStable}}_{\stacksize{e}};\\
408 \cschemeE{\text{\cleaninline{unstable}}~e}{r} & =
409 \cschemeE{e}{r};
410 \text{\cleaninline{BCMkTask BCUnstable}}_{\stacksize{e}};\\
411 \cschemeE{\text{\cleaninline{readA}}~e}{r} & =
412 \cschemeE{e}{r};
413 \text{\cleaninline{BCMkTask BCReadA}};\\
414 \cschemeE{\text{\cleaninline{writeA}}~e_1~e_2}{r} & =
415 \cschemeE{e_1}{r};
416 \cschemeE{e_2}{r};
417 \text{\cleaninline{BCMkTask BCWriteA}};\\
418 \cschemeE{\text{\cleaninline{readD}}~e}{r} & =
419 \cschemeE{e}{r};
420 \text{\cleaninline{BCMkTask BCReadD}};\\
421 \cschemeE{\text{\cleaninline{writeD}}~e_1~e_2}{r} & =
422 \cschemeE{e_1}{r};
423 \cschemeE{e_2}{r};
424 \text{\cleaninline{BCMkTask BCWriteD}};\\
425 \cschemeE{\text{\cleaninline{delay}}~e}{r} & =
426 \cschemeE{e}{r};
427 \text{\cleaninline{BCMkTask BCDelay}};\\
428 \cschemeE{\text{\cleaninline{rpeat}}~e}{r} & =
429 \cschemeE{e}{r};
430 \text{\cleaninline{BCMkTask BCRepeat}};\\
431 \cschemeE{e_1\text{\cleaninline{.\|\|.}}e_2}{r} & =
432 \cschemeE{e_1}{r};
433 \cschemeE{e_2}{r};
434 \text{\cleaninline{BCMkTask BCOr}};\\
435 \cschemeE{e_1\text{\cleaninline{.&&.}}e_2}{r} & =
436 \cschemeE{e_1}{r};
437 \cschemeE{e_2}{r};
438 \text{\cleaninline{BCMkTask BCAnd}};\\
439 \end{align*}
440
441 This simply translates to Clean code by writing the correct \cleaninline{BCMkTask} instruction as exemplified in \cref{lst:imp_ret}.
442
443 \begin{lstClean}[caption={The backend implementation for \cleaninline{rtrn}.},label={lst:imp_ret}]
444 instance rtrn BCInterpret
445 where
446 rtrn m = m >>| tell` [BCMkTask (bcstable m)]
447 \end{lstClean}
448
449 \subsection{Step combinator}\label{ssec:step}
450 The \cleaninline{step} construct is a special type of task because the task value of the left-hand side may change over time.
451 Therefore, the continuation tasks on the right-hand side are \emph{observing} this task value and acting upon it.
452 In the compilation scheme, all continuations are first converted to a single function that has two arguments: the stability of the task and its value.
453 This function either returns a pointer to a task tree or fails (denoted by $\bot$).
454 It is special because in the generated function, the task value of a task can actually be inspected.
455 Furthermore, it is a lazy node in the task tree: the right-hand side may yield a new task tree after several rewrite steps (i.e.\ it is allowed to create infinite task trees using step combinators).
456 The function is generated using the $\mathcal{S}$ scheme that requires two arguments: the context $r$ and the width of the left-hand side so that it can determine the position of the stability which is added as an argument to the function.
457 The resulting function is basically a list of if-then-else constructions to check all predicates one by one.
458 Some optimization is possible here but has currently not been implemented.
459
460 \begin{align*}
461 \cschemeE{t_1\text{\cleaninline{>>*.}}t_2}{r} & =
462 \cschemeE{a_{f^i}}{r}, \langle f, i\rangle\in r;
463 \text{\cleaninline{BCMkTask}}~\text{\cleaninline{BCStable}}_{\stacksize{r}}; \cschemeE{t_1}{r};\\
464 {} & \mathbin{\phantom{=}} \text{\cleaninline{BCMkTask}}~\text{\cleaninline{BCAnd}}; \text{\cleaninline{BCMkTask}}~(\text{\cleaninline{BCStep}}~(\cschemeS{t_2}{(r + [\langle l_s, i\rangle])}{\stacksize{t_1}}));\\
465 \end{align*}
466
467 \begin{align*}
468 \cschemeS{[]}{r}{w} & =
469 \text{\cleaninline{BCPush}}~\bot;\\
470 \cschemeS{\text{\cleaninline{IfValue}}~f~t:cs}{r}{w} & =
471 \text{\cleaninline{BCArg}} (\stacksize{r} + w);
472 \text{\cleaninline{BCIsNoValue}};\\
473 {} & \mathbin{\phantom{=}} \cschemeE{f}{r};
474 \text{\cleaninline{BCAnd}};\\
475 {} & \mathbin{\phantom{=}} \text{\cleaninline{BCJmpF}}~l_1;\\
476 {} & \mathbin{\phantom{=}} \cschemeE{t}{r};
477 \text{\cleaninline{BCJmp}}~l_2;\\
478 {} & \mathbin{\phantom{=}} \text{\cleaninline{BCLabel}}~l_1;
479 \cschemeS{cs}{r}{w};\\
480 {} & \mathbin{\phantom{=}} \text{\cleaninline{BCLabel}}~l_2;\\
481 {} & \text{\emph{Where $l_1$ and $l_2$ are fresh labels}}\\
482 {} & \text{\emph{Similar for \cleaninline{IfStable} and \cleaninline{IfUnstable}}}\\
483 \end{align*}
484
485 First the context is evaluated.
486 The context contains arguments from functions and steps that need to be preserved after rewriting.
487 The evaluated context is combined with the left-hand side task value by means of a \cleaninline{.&&.} combinator to store it in the task tree so that it is available after a rewrite.
488 This means that the task tree is be transformed as follows:
489
490 \begin{lstClean}
491 t1 >>= \v1->t2 >>= \v2->t3 >>= ...
492 //is transformed to
493 t1 >>= \v1->rtrn v1 .&&. t2 >>= \v2->rtrn (v1, v2) .&&. t3 >>= ...
494 \end{lstClean}
495
496 The translation to \gls{CLEAN} is given in \cref{lst:imp_seq}.
497
498 \begin{lstClean}[caption={Backend implementation for the step class.},label={lst:imp_seq}]
499 instance step BCInterpret where
500 (>>*.) lhs cont
501 //Fetch a fresh label and fetch the context
502 = freshlabel >>= \funlab->gets (\s->s.bcs_context)
503 //Generate code for lhs
504 >>= \ctx->lhs
505 //Possibly add the context
506 >>| tell` (if (ctx =: []) []
507 //The context is just the arguments up till now in reverse
508 ( [BCArg (UInt8 i)\\i<-reverse (indexList ctx)]
509 ++ map BCMkTask (bcstable (UInt8 (length ctx)))
510 ++ [BCMkTask BCTAnd]
511 ))
512 //Increase the context
513 >>| addToCtx funlab zero lhswidth
514 //Lift the step function
515 >>| liftFunction funlab
516 //Width of the arguments is the width of the lhs plus the
517 //stability plus the context
518 (one + lhswidth + (UInt8 (length ctx)))
519 //Body label ctx width continuations
520 (contfun funlab (UInt8 (length ctx)))
521 //Return width (always 1, a task pointer)
522 (Just one)
523 >>| modify (\s->{s & bcs_context=ctx})
524 >>| tell` [BCMkTask (instr rhswidth funlab)]
525
526 toContFun :: JumpLabel UInt8 -> BCInterpret a
527 toContFun steplabel contextwidth
528 = foldr tcf (tell` [BCPush fail]) cont
529 where
530 tcf (IfStable f t)
531 = If ((stability >>| tell` [BCIsStable]) &. f val)
532 (t val >>| tell` [])
533 ...
534 stability = tell` [BCArg (lhswidth + contextwidth)]
535 val = retrieveArgs steplabel zero lhswidth
536 \end{lstClean}
537
538 \subsection{\texorpdfstring{\Glspl{SDS}}{Shared data sources}}
539 The compilation scheme for \gls{SDS} definitions is a trivial extension to $\mathcal{F}$ since there is no code generated as seen below.
540
541 \begin{align*}
542 \cschemeF{\text{\cleaninline{sds}}~x=i~\text{\cleaninline{In}}~m} & =
543 \cschemeF{m};\\
544 \end{align*}
545
546 The \gls{SDS} access tasks have a compilation scheme similar to other tasks (see \cref{ssec:scheme_tasks}).
547 The \cleaninline{getSds} task just pushes a task tree node with the \gls{SDS} identifier embedded.
548 The \cleaninline{setSds} task evaluates the value, lifts that value to a task tree node and creates an \gls{SDS} set node.
549
550 \begin{align*}
551 \cschemeE{\text{\cleaninline{getSds}}~s}{r} & =
552 \text{\cleaninline{BCMkTask}} (\text{\cleaninline{BCSdsGet}} s);\\
553 \cschemeE{\text{\cleaninline{setSds}}~s~e}{r} & =
554 \cschemeE{e}{r};
555 \text{\cleaninline{BCMkTask BCStable}}_{\stacksize{e}};\\
556 {} & \mathbin{\phantom{=}} \text{\cleaninline{BCMkTask}} (\text{\cleaninline{BCSdsSet}} s);\\
557 \end{align*}
558
559 While there is no code generated in the definition, the byte code compiler is storing the \gls{SDS} data in the \cleaninline{bcs_sdses} field in the compilation state.
560 The \glspl{SDS} are typed as functions in the host language so an argument for this function must be created that represents the \gls{SDS} on evaluation.
561 For this, an \cleaninline{BCInterpret} is created that emits this identifier.
562 When passing it to the function, the initial value of the \gls{SDS} is returned.
563 This initial value is stored as a byte code encoded value in the state and the compiler continues with the rest of the program.
564
565 Compiling \cleaninline{getSds} is a matter of executing the \cleaninline{BCInterpret} representing the \gls{SDS}, which yields the identifier that can be embedded in the instruction.
566 Setting the \gls{SDS} is similar: the identifier is retrieved and the value is written to put in a task tree so that the resulting task can remember the value it has written.
567 Lifted SDSs are compiled in a very similar way.\todo{deze \P{} moet naar integration?}
568 The only difference is that there is no initial value but an iTasks SDS when executing the Clean function.
569 A lens on this SDS converting \cleaninline{a} from the \cleaninline{Shared a} to a \cleaninline{String255}---a bytecode encoded version---is stored in the state.
570 The encoding and decoding itself is unsafe when used directly but the type system of the language and the abstractions make it safe.
571 Upon sending the mTask task to the device, the initial values of the lifted SDSs are fetched to complete the SDS specification.
572
573 % VimTeX: SynIgnore on
574 \begin{lstClean}[caption={Backend implementation for the SDS classes.},label={lst:comp_sds}]
575 :: Sds a = Sds Int
576 instance sds BCInterpret where
577 sds def = {main = freshsds >>= \sdsi->
578 let sds = modify (\s->{s & bcs_sdses=put sdsi
579 (Left (toByteCode t)) s.bcs_sdses})
580 >>| pure (Sds sdsi)
581 (t In e) = def sds
582 in e.main}
583 getSds f = f >>= \(Sds i)-> tell` [BCMkTask (BCSdsGet (fromInt i))]
584 setSds f v = f >>= \(Sds i)->v >>| tell`
585 ( map BCMkTask (bcstable (byteWidth v))
586 ++ [BCMkTask (BCSdsSet (fromInt i))])
587 \end{lstClean}
588 % VimTeX: SynIgnore off
589
590 \section{C code generation}\label{sec:ccodegen}
591 All communication between the \gls{ITASK} server and the \gls{MTASK} server is type-parametrised.
592 From the structural representation of the type, a \gls{CLEAN} parser and printer is constructed using generic programming.
593 Furthermore, a \ccpp{} parser and printer is generated for use on the \gls{MTASK} device.
594 The technique for generating the \ccpp{} parser and printer is very similar to template metaprogramming and requires a generic programming library or compiler support that includes a lot of metadata in the record and constructor nodes.
595
596
597 \section{Conclusion}
598 \todo[inline]{conclusion}
599
600 \input{subfilepostamble}
601 \end{document}