upiates
[phd-thesis.git] / top / imp.tex
index a8f451c..fb0a597 100644 (file)
 
 \input{subfilepreamble}
 
+\setcounter{chapter}{5}
+
 \begin{document}
 \input{subfileprefix}
-
 \chapter{Implementation}%
 \label{chp:implementation}
 \begin{chapterabstract}
-       This chapter shows the implementation of the \gls{MTASK} system.
-       It is threefold: first it shows the implementation of the byte code compiler for \gls{MTASK}'s \gls{TOP} language, then is details of the implementation of \gls{MTASK}'s \gls{TOP} engine that executes the \gls{MTASK} tasks on the microcontroller, and finally it shows how the integration of \gls{MTASK} tasks and \glspl{SDS} is implemented both on the server and on the device.
+       \noindent This chapter shows the implementation of the \gls{MTASK} system by:
+       \begin{itemize}
+               \item gives details of the implementation of \gls{MTASK}'s \gls{TOP} engine that executes the \gls{MTASK} tasks on the microcontroller;
+               \item shows the implementation of the byte code compiler for \gls{MTASK}'s \gls{TOP} language;
+               \item explains the machinery used to automatically serialise and deserialise data to-and-fro the device.
+       \end{itemize}
 \end{chapterabstract}
 
-\section{Byte code compiler}
-IFL19 paper, bytecode instructieset~\cref{chp:bytecode_instruction_set}
+Microcontrollers usually have flash-based program memory which wears out fairly quick.
+For example, the atmega328p in the \gls{ARDUINO} UNO is rated for 10000 write cycles.
+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.
+Hence, for dynamic applications, interpretation on the device is necessary, saving precious write cycles of the program memory.
+
+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.
+Once the device is programmed with the \gls{MTASK} \gls{RTS}, it can continuously receive new tasks without the need for reprogramming.
+The \gls{OS} is written in portable \ccpp{} and only contains a small device-specific portion.
+
+\section{\texorpdfstring{\Glsxtrlong{RTS}}{Run time system}}
+The event loop of the \gls{RTS} is executed repeatedly and consists of three distinct phases.
+After doing the three phases, the devices goes to sleep for as long as possible (see \cref{chp:green_computing_mtask}).
+
+\subsection{Communication}
+In the first phase, the communication channels are processed.
+The exact communication method is a customisable device-specific option baked into the \gls{RTS}.
+The interface is deliberately kept simple and consists of a two layer interface: a link interface and a communication interface.
+Besides opening, closing and cleaning up, the link interface has only three functions that are shown in \cref{lst:link_interface}.
+Consequently, implementing this link interface is very simple but allows for many more advanced link settings such as buffering.
+There are implementations for this interface for serial or Wi-Fi connections using \gls{ARDUINO} and \gls{TCP} connections for Linux.
+
+\begin{lstArduino}[caption={Link interface of the \gls{MTASK} \gls{RTS}.},label={lst:link_interface}]
+bool link_input_available(void);
+uint8_t link_read_byte(void);
+void link_write_byte(uint8_t b);
+\end{lstArduino}
+
+The communication interface abstracts away from this link interface and is typed instead.
+It contains only two functions as seen in \cref{lst:comm_interface}.
+There are implementations for direct communication, or communication using an \gls{MQTT} broker.
+Both use the automatic serialisation and deserialisation shown in \cref{sec:ccodegen}.
+
+\begin{lstArduino}[caption={Communication interface of the \gls{MTASK} \gls{RTS}.},label={lst:comm_interface}]
+struct MTMessageTo receive_message(void);
+void send_message(struct MTMessageFro msg);
+\end{lstArduino}
+
+Processing the received messages from the communication channels happens synchronously and the channels are exhausted completely before moving on to the next phase.
+There are several possible messages that can be received from the server:
+
+\begin{description}
+       \item[SpecRequest]
+               is a message instructing the device to send its specification and is sent usually immediately after connecting.
+               The \gls{RTS} responds with a \texttt{Spec} answer containing the specification.
+       \item[TaskPrep]
+               tells the device a (big) task is on its way.
+               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.
+               This allows the \gls{RTS} to postpone execution for a while, until the big task has been received.
+               The server sends the big task when the device acknowledges (by sending a \texttt{TaskPrepAck} message) the preparation.
+       \item[Task]
+               contains a new task, its peripheral configuration, the \glspl{SDS}, and the bytecode.
+               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.
+               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.
+       \item[SdsUpdate]
+               notifies the device of the new value for a lowered \gls{SDS}.
+               The old value of the lowered \gls{SDS} is immediately replaced with the new one.
+               There is no acknowledgement required.
+       \item[TaskDel]
+               instructs the device to delete a running task.
+               Tasks are automatically deleted when they become stable.
+               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.
+               The device acknowledges by sending a \texttt{TaskDelAck}.
+       \item[Shutdown]
+               tells the device to reset.
+\end{description}
+
+\subsection{Execution}
+The second phase consists of performing one execution step for all tasks that wish for it.
+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.
+Execution of a task is always an interplay between the interpreter and the \emph{rewriter}.
+
+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.
+The main expression always produces a task tree.
+Execution of a task consists of continuously rewriting the task until its value is stable.
+Rewriting is a destructive process, i.e.\ the rewriting is done in place.
+The rewriting engine uses the interpreter when needed, e.g.\ to calculate the step continuations.
+The rewriter and the interpreter use the same stack to store intermediate values.
+Rewriting steps are small so that interleaving results in seemingly parallel execution.
+In this phase new task tree nodes may be allocated.
+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.
+The host is notified if a task value is changed after a rewrite step.
+
+\subsection{Memory management}
+The third and final phase is memory management.
+The \gls{MTASK} \gls{RTS} is designed to run on systems with as little as \qty{2}{\kibi\byte} of \gls{RAM}.
+Aggressive memory management is therefore vital.
+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.
+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}.
+The size of this block can be changed in the configuration of the \gls{RTS} if necessary.
+On an \gls{ARDUINO} UNO---equipped with \qty{2}{\kibi\byte} of \gls{RAM}---the maximum viable size is about \qty{1500}{\byte}.
+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}).
+
+\begin{figure}
+       \centering
+       \includestandalone{memorylayout}
+       \caption{Memory layout}\label{fig:memory_layout}
+\end{figure}
+
+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.
+
+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.
+As a consequence, the stack moves when a new task is received.
+This never happens within execution because communication is always processed before execution.
+Values in the interpreter are always stored on the stack.
+Compound data types are stored unboxed and flattened.
+Task trees grow from the top down as in a heap.
+This approach allows for flexible ratios, i.e.\ many tasks and small trees or few tasks and big trees.
+
+Stable tasks, and unreachable task tree nodes are removed.
+If a task is to be removed, tasks with higher memory addresses are moved down.
+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.
+This is possible because there is no sharing or cycles in task trees and nodes contain pointers pointers to their parent.
+
+\todo{plaa\-tje van me\-mo\-ry hier uitbreiden}
+
+\section{Compiler}
+\subsection{Instruction set}
+The instruction set is a fairly standard stack machine instruction set extended with special \gls{TOP} instructions.
+
+\Cref{lst:instruction_type} shows the \gls{CLEAN} type representing the instruction set of which \cref{tbl:instr_task} gives detailed semantics.
+Type synonyms are used to provide insight on the arguments of the instructions.
+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.
+
+\begin{lstClean}[caption={The type housing the instruction set.},label={lst:instruction_type}]
+:: ArgWidth    :== UInt8         :: ReturnWidth :== UInt8
+:: Depth       :== UInt8         :: Num         :== UInt8
+:: SdsId       :== UInt8         :: JumpLabel   =: JL UInt16
+
+//** Datatype housing all instructions
+:: BCInstr
+       //Return instructions
+       //Jumps
+       = BCJumpF JumpLabel | BCJump JumpLabel | BCLabel JumpLabel | BCJumpSR ArgWidth JumpLabel
+       | BCReturn ReturnWidth ArgWidth | BCTailcall ArgWidth ArgWidth JumpLabel
+       //Arguments
+       | BCArgs ArgWidth ArgWidth
+       //Task node creation and refinement
+       | BCMkTask BCTaskType | BCTuneRateMs | BCTuneRateSec
+       //Task value ops
+       | BCIsStable | BCIsUnstable | BCIsNoValue | BCIsValue
+       //Stack ops
+       | BCPush String255 | BCPop Num | BCRot Depth Num | BCDup | BCPushPtrs
+       //Casting
+       | BCItoR | BCItoL | BCRtoI | ...
+       // arith
+       | BCAddI | BCSubI | ...
+       ...
+
+//** Datatype housing all task types
+:: BCTaskType
+       = BCStableNode ArgWidth | ArgWidth
+       // Pin io
+       | BCReadD | BCWriteD | BCReadA | BCWriteA | BCPinMode
+       // Interrupts
+       | BCInterrupt
+       // Repeat
+       | BCRepeat
+       // Delay
+       | BCDelay | BCDelayUntil //* Only for internal use
+       // Parallel
+       | BCTAnd | BCTOr
+       //Step
+       | BCStep ArgWidth JumpLabel
+       //Sds ops
+       | BCSdsGet SdsId | BCSdsSet SdsId | BCSdsUpd SdsId JumpLabel
+       // Rate limiter
+       | BCRateLimit
+       ////Peripherals
+       //DHT
+       | BCDHTTemp UInt8 | BCDHTHumid UInt8
+       ...
+\end{lstClean}
+
+\subsection{Compiler}
+The bytecode compiler interpretation for the \gls{MTASK} language is implemented as a monad stack containing a writer monad and a state monad.
+The writer monad is used to generate code snippets locally without having to store them in the monadic values.
+The state monad accumulates the code, and stores the stateful data the compiler requires.
+\Cref{lst:compiler_state} shows the data type for the state, storing:
+function the compiler currently is in;
+code of the main expression;
+context (see \todo{insert ref to compilation rules step here});
+code for the functions;
+next fresh label;
+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};
+and finally there is a list of peripherals used.
+
+\begin{lstClean}[label={lst:compiler_state},caption={\Gls{MTASK}'s byte code compiler type}]
+:: BCInterpret a :== StateT BCState (WriterT [BCInstr] Identity) a
+:: BCState =
+       { bcs_infun        :: JumpLabel
+       , bcs_mainexpr     :: [BCInstr]
+       , bcs_context      :: [BCInstr]
+       , bcs_functions    :: Map JumpLabel BCFunction
+       , bcs_freshlabel   :: JumpLabel
+       , bcs_sdses        :: [Either String255 MTLens]
+       , bcs_hardware     :: [BCPeripheral]
+       }
+:: BCFunction =
+       { bcf_instructions :: [BCInstr]
+       , bcf_argwidth     :: UInt8
+       , bcf_returnwidth  :: UInt8
+       }
+\end{lstClean}
+
+Executing the compiler is done by providing an initial state.
+After compilation, several post-processing steps are applied to make the code suitable for the microprocessor.
+First, in all tail call \cleaninline{BCReturn}'s are replaced by \cleaninline{BCTailCall} to implement tail call elimination.
+Furthermore, all byte code is concatenated, resulting in one big program.
+Many instructions have commonly used arguments so shorthands are introduced to reduce the program size.
+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.
+Furthermore, redundant instructions (e.g.\ pop directly after push) are removed as well in order not to burden the code generation with these intricacies.
+Finally the labels are resolved to represent actual program addresses instead of freshly generated identifiers.
+After the byte code is ready, the lifted \glspl{SDS} are resolved to provide an initial value for them.
+The result---byte code, \gls{SDS} specification and perpipheral specifications---are the result of the process, ready to be sent to the device. 
+
+\section{Compilation rules}
+This section describes the compilation rules, the translation from abstract syntax to byte code.
+The compilation scheme consists of three schemes\slash{}functions.
+When something is surrounded by double vertical bars, e.g.\ $\stacksize{a_i}$, it denotes the number of stack cells required to store it.
+
+Some schemes have a \emph{context} $r$ as an argument which contains information about the location of the arguments in scope.
+More information is given in the schemes requiring such arguments.
+
+\newcommand{\cschemeE}[2]{\mathcal{E}\llbracket#1\rrbracket~#2}
+\newcommand{\cschemeF}[1]{\mathcal{F}\llbracket#1\rrbracket}
+\newcommand{\cschemeS}[3]{\mathcal{S}\llbracket#1\rrbracket~#2~#3}
+\begin{table}
+       \centering
+       \begin{tabularx}{\linewidth}{l X}
+               \toprule
+               Scheme & Description\\
+               \midrule
+               $\cschemeE{e}{r}$ & Produces the value of expression $e$ given the context $r$ and pushes it on the stack.
+                       The result can be a basic value or a pointer to a task.\\
+               $\cschemeF{e}$ & Generates the bytecode for functions.\\
+               $\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.\\
+               \bottomrule
+       \end{tabularx}
+\end{table}
+
+\subsection{Expressions}
+Almost all expression constructions are compiled using $\mathcal{E}$.
+The argument of $\mathcal{E}$ is the context (see \cref{ssec:functions}).
+Values are always placed on the stack; tuples and other compound data types are unpacked.
+Function calls, function arguments and tasks are also compiled using $\mathcal{E}$ but their compilations is explained later.
+
+\begin{align*}
+       \cschemeE{\text{\cleaninline{lit}}~e}{r} & = \text{\cleaninline{BCPush (bytecode e)}};\\
+       \cschemeE{e_1\mathbin{\text{\cleaninline{+.}}}e_2}{r} & = \cschemeE{e_1}{r};
+                       \cschemeE{e_2}{r};
+                       \text{\cleaninline{BCAdd}};\\
+               {} & \text{\emph{Similar for other binary operators}}\\
+       \cschemeE{\text{\cleaninline{Not}}~e}{r} & =
+                       \cschemeE{e}{r};
+                       \text{\cleaninline{BCNot}};\\
+               {} & \text{\emph{Similar for other unary operators}}\\
+       \cschemeE{\text{\cleaninline{If}}~e_1~e_2~e_3}{r} & =
+                       \cschemeE{e_1}{r};
+                       \text{\cleaninline{BCJmpF}}\enskip l_{else}; \mathbin{\phantom{=}} \cschemeE{e_2}{r}; \text{\cleaninline{BCJmp}}\enskip l_{endif};\\
+               {} & \mathbin{\phantom{=}} \text{\cleaninline{BCLabel}}\enskip l_{else}; \cschemeE{e_3}{r}; \mathbin{\phantom{=}} \text{\cleaninline{BCLabel}}\enskip l_{endif};\\
+               {} & \text{\emph{Where $l_{else}$ and $l_{endif}$ are fresh labels}}\\
+       \cschemeE{\text{\cleaninline{tupl}}~e_1~e_2}{r} & =
+                       \cschemeE{e_1}{r};
+                       \cschemeE{e_2}{r};\\
+               {} & \text{\emph{Similar for other unboxed compound data types}}\\
+       \cschemeE{\text{\cleaninline{first}}~e}{r} & =
+                       \cschemeE{e}{r};
+                       \text{\cleaninline{BCPop}}\enskip w;\\
+               {} & \text{\emph{Where $w$ is the width of the left value and}}\\
+               {} & \text{\emph{similar for other unboxed compound data types}}\\
+       \cschemeE{\text{\cleaninline{second}}\enskip e}{r} & =
+                       \cschemeE{e}{r};
+                       \text{\cleaninline{BCRot}}\enskip w_1\enskip (w_1+w_2);
+                       \text{\cleaninline{BCPop}}\enskip w_2;\\
+               {} & \text{\emph{Where $w_1$ is the width of the left and, $w_2$ of the right value}}\\
+               {} & \text{\emph{similar for other unboxed compound data types}}\\
+\end{align*}
+
+Translating $\mathcal{E}$ to \gls{CLEAN} code is very straightforward, it basically means executing the monad.
+Almost always, the type of the interpretation is not used, i.e.\ it is a phantom type.
+To still have the functions return the correct type, the \cleaninline{tell`}\footnote{\cleaninline{tell` :: [BCInstr] -> BCInterpret a}} helper is used.
+This function is similar to the writer monad's \cleaninline{tell} function but is casted to the correct type.
+\Cref{lst:imp_arith} shows the implementation for the arithmetic and conditional expressions.
+Note that $r$, the context, is not an explicit argument but stored in the state.
+
+\begin{lstClean}[caption={Interpretation implementation for the arithmetic and conditional classes.},label={lst:imp_arith}]
+instance expr BCInterpret where
+       lit   t   = tell` [BCPush (toByteCode{|*|} t)]
+       (+.)  a b = a >>| b >>| tell` [BCAdd]
+       ...
+       If c t e = freshlabel >>= \elselabel->freshlabel >>= \endiflabel->
+               c >>| tell` [BCJumpF elselabel] >>|
+               t >>| tell` [BCJump endiflabel,BCLabel elselabel] >>|
+               e >>| tell` [BCLabel endiflabel]
+\end{lstClean}
+
+\subsection{Functions}\label{ssec:functions}
+Compiling functions occurs in $\mathcal{F}$, which generates bytecode for the complete program by iterating over the functions and ending with the main expression.
+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.
+The main expression is a special case of $\mathcal{F}$ since it neither has arguments nor something to continue.
+Therefore, it is just compiled using $\mathcal{E}$.
+
+\begin{align*}
+       \cschemeF{main=m} & =
+               \cschemeE{m}{[]};\\
+       \cschemeF{f~a_0 \ldots a_n = b~\text{\cleaninline{In}}~m} & =
+               \text{\cleaninline{BCLabel}}~f; \cschemeE{b}{[\langle f, i\rangle, i\in \{(\Sigma^n_{i=0}\stacksize{a_i})..0\}]};\\
+               {} & \mathbin{\phantom{=}} \text{\cleaninline{BCReturn}}~\stacksize{b}~n; \cschemeF{m};\\
+\end{align*}
+
+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}).
+On executing \cleaninline{BCJumpSR}, the program counter is set and the interpreter jumps to the function (\cref{lst:funcall_jumpsr}).
+When the function returns, the return value overwrites the old pointers and the arguments.
+This occurs right after a \cleaninline{BCReturn} (\cref{lst:funcall_ret}).
+Putting the arguments on top of pointers and not reserving space for the return value uses little space and facilitates tail call optimization.
+
+\begin{figure}
+       \begin{subfigure}{.24\linewidth}
+               \centering
+               \includestandalone{memory1}
+               \caption{\cleaninline{BCPushPtrs}}\label{lst:funcall_pushptrs}
+       \end{subfigure}
+       \begin{subfigure}{.24\linewidth}
+               \centering
+               \includestandalone{memory2}
+               \caption{Arguments}\label{lst:funcall_args}
+       \end{subfigure}
+       \begin{subfigure}{.24\linewidth}
+               \centering
+               \includestandalone{memory3}
+               \caption{\cleaninline{BCJumpSR}}\label{lst:funcall_jumpsr}
+       \end{subfigure}
+       \begin{subfigure}{.24\linewidth}
+               \centering
+               \includestandalone{memory4}
+               \caption{\cleaninline{BCReturn}}\label{lst:funcall_ret}
+       \end{subfigure}
+       \caption{The stack layout during function calls.}%
+\end{figure}
+
+Calling a function and referencing function arguments are an extension to $\mathcal{E}$ as shown below.
+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)}}.
+Compiling argument $a_{f^i}$, the $i$th argument in function $f$, consists of traversing all positions in the current context.
+Arguments wider than one stack cell are fetched in reverse to preserve the order.
+
+\begin{align*}
+       \cschemeE{f(a_0, \ldots, a_n)}{r} & =
+               \text{\cleaninline{BCPushPtrs}}; \cschemeE{a_n}{r}; \cschemeE{a_{\ldots}}{r}; \cschemeE{a_0}{r}; \text{\cleaninline{BCJumpSR}}~n~f;\\
+       \cschemeE{a_{f^i}}{r} & =
+               \text{\cleaninline{BCArg}~findarg}(r, f, i)~\text{for all}~i\in\{w\ldots v\};\\
+               {} & v = \Sigma^{i-1}_{j=0}\stacksize{a_{f^j}}~\text{ and }~ w = v + \stacksize{a_{f^i}}\\
+\end{align*}
+
+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}
+The \cleaninline{fun} class has a single function with a single argument.
+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.
+To compile this, the argument must be called with a function representing a function call in mTask.
+\Cref{lst:fun_imp} shows the implementation for this as Clean code.
+To uniquely identify the function, a fresh label is generated.
+The function is then called with the \cleaninline{callFunction} helper function that generates the instructions that correspond to calling the function.
+That is, it pushes the pointers, compiles the arguments, and writes the \cleaninline{JumpSR} instruction.
+The resulting structure (\cleaninline{g In m}) contains a function representing the mTask function (\cleaninline{g}) and the \cleaninline{main} structure to continue with.
+To get the actual function, \cleaninline{g} must be called with representations for the argument, i.e.\ using \cleaninline{findarg} for all arguments.
+The arguments are added to the context and \cleaninline{liftFunction} is called with the label, the argument width and the compiler.
+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.
+After lifting the function, the context is cleared again and compilation continues with the rest of the program.
+
+\begin{lstClean}[label={lst:fun_imp},caption={The backend implementation for functions.}]
+instance fun (BCInterpret a) BCInterpret | type a where
+       fun def = {main=freshlabel >>= \funlabel->
+               let (g In m) = def \a->callFunction funlabel (toByteWidth a) [a]
+                   argwidth = toByteWidth (argOf g)
+               in  addToCtx funlabel zero argwidth
+               >>| infun funlabel
+                       (liftFunction funlabel argwidth
+                               (g (retrieveArgs funlabel zero argwidth)
+                               ) ?None)
+               >>| clearCtx >>| m.main
+               }
+
+argOf :: ((m a) -> b) a -> UInt8 | toByteWidth a
+callFunction :: JumpLabel UInt8 [BCInterpret b] -> BCInterpret c | ...
+liftFunction :: JumpLabel UInt8 (BCInterpret a) (?UInt8) -> BCInterpret ()
+\end{lstClean}
+
+\subsection{Tasks}\label{ssec:scheme_tasks}
+Task trees are created with the \cleaninline{BCMkTask} instruction that allocates a node and pushes it to the stack.
+It pops arguments from the stack according to the given task type.
+The following extension of $\mathcal{E}$ shows this compilation scheme (except for the step combinator, explained in \cref{ssec:step}).
+
+\begin{align*}
+       \cschemeE{\text{\cleaninline{rtrn}}~e}{r} & =
+                       \cschemeE{e}{r};
+                       \text{\cleaninline{BCMkTask BCStable}}_{\stacksize{e}};\\
+       \cschemeE{\text{\cleaninline{unstable}}~e}{r} & =
+                       \cschemeE{e}{r};
+                       \text{\cleaninline{BCMkTask BCUnstable}}_{\stacksize{e}};\\
+       \cschemeE{\text{\cleaninline{readA}}~e}{r} & =
+                       \cschemeE{e}{r};
+                       \text{\cleaninline{BCMkTask BCReadA}};\\
+       \cschemeE{\text{\cleaninline{writeA}}~e_1~e_2}{r} & =
+                       \cschemeE{e_1}{r};
+                       \cschemeE{e_2}{r};
+                       \text{\cleaninline{BCMkTask BCWriteA}};\\
+       \cschemeE{\text{\cleaninline{readD}}~e}{r} & =
+                       \cschemeE{e}{r};
+                       \text{\cleaninline{BCMkTask BCReadD}};\\
+       \cschemeE{\text{\cleaninline{writeD}}~e_1~e_2}{r} & =
+                       \cschemeE{e_1}{r};
+                       \cschemeE{e_2}{r};
+                       \text{\cleaninline{BCMkTask BCWriteD}};\\
+       \cschemeE{\text{\cleaninline{delay}}~e}{r} & =
+                       \cschemeE{e}{r};
+                       \text{\cleaninline{BCMkTask BCDelay}};\\
+       \cschemeE{\text{\cleaninline{rpeat}}~e}{r} & =
+                       \cschemeE{e}{r};
+                       \text{\cleaninline{BCMkTask BCRepeat}};\\
+       \cschemeE{e_1\text{\cleaninline{.\|\|.}}e_2}{r} & =
+                       \cschemeE{e_1}{r};
+                       \cschemeE{e_2}{r};
+                       \text{\cleaninline{BCMkTask BCOr}};\\
+       \cschemeE{e_1\text{\cleaninline{.&&.}}e_2}{r} & =
+                       \cschemeE{e_1}{r};
+                       \cschemeE{e_2}{r};
+                       \text{\cleaninline{BCMkTask BCAnd}};\\
+\end{align*}
+
+This simply translates to Clean code by writing the correct \cleaninline{BCMkTask} instruction as exemplified in \cref{lst:imp_ret}.
+
+\begin{lstClean}[caption={The backend implementation for \cleaninline{rtrn}.},label={lst:imp_ret}]
+instance rtrn BCInterpret
+where
+       rtrn m = m >>| tell` [BCMkTask (bcstable m)]
+\end{lstClean}
+
+\subsection{Step combinator}\label{ssec:step}
+The \cleaninline{step} construct is a special type of task because the task value of the left-hand side may change over time.
+Therefore, the continuation tasks on the right-hand side are \emph{observing} this task value and acting upon it.
+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.
+This function either returns a pointer to a task tree or fails (denoted by $\bot$).
+It is special because in the generated function, the task value of a task can actually be inspected.
+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).
+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.
+The resulting function is basically a list of if-then-else constructions to check all predicates one by one.
+Some optimization is possible here but has currently not been implemented.
+
+\begin{align*}
+       \cschemeE{t_1\text{\cleaninline{>>*.}}t_2}{r} & =
+               \cschemeE{a_{f^i}}{r}, \langle f, i\rangle\in r;
+               \text{\cleaninline{BCMkTask}}~\text{\cleaninline{BCStable}}_{\stacksize{r}}; \cschemeE{t_1}{r};\\
+       {} & \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}}));\\
+\end{align*}
+
+\begin{align*}
+       \cschemeS{[]}{r}{w} & =
+               \text{\cleaninline{BCPush}}~\bot;\\
+       \cschemeS{\text{\cleaninline{IfValue}}~f~t:cs}{r}{w} & =
+               \text{\cleaninline{BCArg}} (\stacksize{r} + w);
+               \text{\cleaninline{BCIsNoValue}};\\
+       {} & \mathbin{\phantom{=}} \cschemeE{f}{r};
+               \text{\cleaninline{BCAnd}};\\
+       {} & \mathbin{\phantom{=}} \text{\cleaninline{BCJmpF}}~l_1;\\
+       {} & \mathbin{\phantom{=}} \cschemeE{t}{r};
+               \text{\cleaninline{BCJmp}}~l_2;\\
+       {} & \mathbin{\phantom{=}} \text{\cleaninline{BCLabel}}~l_1;
+               \cschemeS{cs}{r}{w};\\
+       {} & \mathbin{\phantom{=}} \text{\cleaninline{BCLabel}}~l_2;\\
+       {} & \text{\emph{Where $l_1$ and $l_2$ are fresh labels}}\\
+       {} & \text{\emph{Similar for \cleaninline{IfStable} and \cleaninline{IfUnstable}}}\\
+\end{align*}
+
+First the context is evaluated.
+The context contains arguments from functions and steps that need to be preserved after rewriting.
+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.
+This means that the task tree is be transformed as follows:
+
+\begin{lstClean}
+t1 >>= \v1->t2 >>= \v2->t3 >>= ...
+//is transformed to
+t1 >>= \v1->rtrn v1 .&&. t2 >>= \v2->rtrn (v1, v2) .&&. t3 >>= ...
+\end{lstClean}
+
+The translation to \gls{CLEAN} is given in \cref{lst:imp_seq}.
+
+\begin{lstClean}[caption={Backend implementation for the step class.},label={lst:imp_seq}]
+instance step BCInterpret where
+       (>>*.) lhs cont
+               //Fetch a fresh label and fetch the context
+               =   freshlabel >>= \funlab->gets (\s->s.bcs_context)
+               //Generate code for lhs
+               >>= \ctx->lhs
+               //Possibly add the context
+               >>| tell` (if (ctx =: []) []
+                               //The context is just the arguments up till now in reverse
+                               (  [BCArg (UInt8 i)\\i<-reverse (indexList ctx)]
+                               ++ map BCMkTask (bcstable (UInt8 (length ctx)))
+                               ++ [BCMkTask BCTAnd]
+                               ))
+               //Increase the context
+               >>| addToCtx funlab zero lhswidth
+               //Lift the step function
+               >>| liftFunction funlab
+                               //Width of the arguments is the width of the lhs plus the
+                               //stability plus the context
+                               (one + lhswidth + (UInt8 (length ctx)))
+                               //Body     label  ctx width            continuations
+                               (contfun funlab (UInt8 (length ctx)))
+                               //Return width (always 1, a task pointer)
+                               (Just one)
+               >>| modify (\s->{s & bcs_context=ctx})
+               >>| tell` [BCMkTask (instr rhswidth funlab)]
+
+toContFun :: JumpLabel UInt8 -> BCInterpret a
+toContFun steplabel contextwidth
+       = foldr tcf (tell` [BCPush fail]) cont
+where
+       tcf (IfStable f t)
+               = If ((stability >>| tell` [BCIsStable]) &. f val)
+                       (t val >>| tell` [])
+       ...
+       stability = tell` [BCArg (lhswidth + contextwidth)]
+       val = retrieveArgs steplabel zero lhswidth
+\end{lstClean}
+
+\subsection{\texorpdfstring{\Glspl{SDS}}{Shared data sources}}
+The compilation scheme for \gls{SDS} definitions is a trivial extension to $\mathcal{F}$ since there is no code generated as seen below.
+
+\begin{align*}
+       \cschemeF{\text{\cleaninline{sds}}~x=i~\text{\cleaninline{In}}~m} & =
+               \cschemeF{m};\\
+\end{align*}
+
+The \gls{SDS} access tasks have a compilation scheme similar to other tasks (see \cref{ssec:scheme_tasks}).
+The \cleaninline{getSds} task just pushes a task tree node with the \gls{SDS} identifier embedded.
+The \cleaninline{setSds} task evaluates the value, lifts that value to a task tree node and creates an \gls{SDS} set node.
+
+\begin{align*}
+       \cschemeE{\text{\cleaninline{getSds}}~s}{r} & =
+               \text{\cleaninline{BCMkTask}} (\text{\cleaninline{BCSdsGet}} s);\\
+       \cschemeE{\text{\cleaninline{setSds}}~s~e}{r} & =
+               \cschemeE{e}{r};
+               \text{\cleaninline{BCMkTask BCStable}}_{\stacksize{e}};\\
+       {} & \mathbin{\phantom{=}} \text{\cleaninline{BCMkTask}} (\text{\cleaninline{BCSdsSet}} s);\\
+\end{align*}
+
+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.
+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.
+For this, an \cleaninline{BCInterpret} is created that emits this identifier.
+When passing it to the function, the initial value of the \gls{SDS} is returned.
+This initial value is stored as a byte code encoded value in the state and the compiler continues with the rest of the program.
+
+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.
+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.
+Lifted SDSs are compiled in a very similar way.\todo{deze \P{} moet naar integration?}
+The only difference is that there is no initial value but an iTasks SDS when executing the Clean function.
+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.
+The encoding and decoding itself is unsafe when used directly but the type system of the language and the abstractions make it safe.
+Upon sending the mTask task to the device, the initial values of the lifted SDSs are fetched to complete the SDS specification.
+
+% VimTeX: SynIgnore on
+\begin{lstClean}[caption={Backend implementation for the SDS classes.},label={lst:comp_sds}]
+:: Sds a = Sds Int
+instance sds BCInterpret where
+       sds def = {main = freshsds >>= \sdsi->
+                       let sds = modify (\s->{s & bcs_sdses=put sdsi
+                                               (Left (toByteCode t)) s.bcs_sdses})
+                                       >>| pure (Sds sdsi)
+                           (t In e) = def sds
+                       in e.main}
+       getSds f   = f >>= \(Sds i)-> tell` [BCMkTask (BCSdsGet (fromInt i))]
+       setSds f v = f >>= \(Sds i)->v >>| tell`
+               (  map BCMkTask (bcstable (byteWidth v))
+               ++ [BCMkTask (BCSdsSet (fromInt i))])
+\end{lstClean}
+% VimTeX: SynIgnore off
+
+\section{C code generation}\label{sec:ccodegen}
+All communication between the \gls{ITASK} server and the \gls{MTASK} server is type-parametrised.
+From the structural representation of the type, a \gls{CLEAN} parser and printer is constructed using generic programming.
+Furthermore, a \ccpp{} parser and printer is generated for use on the \gls{MTASK} device.
+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.
 
-\section{Run time system}
+\section{Conclusion}
+%\todo[inline]{conclusion}
 
 \input{subfilepostamble}
 \end{document}