\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}
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 not even seven days is guaranteed.
-Hence, for dynamic applications, generating code at run-time for interpretation on the device is necessary.
-This byte code is then interpreted on MCUs with very little memory and processing power and thus save precious write cycles of the program memory.
-precious write cycles of the program memory.
+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.
+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.
\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 $\parallel$, e.g.\ $\parallel{}a_i\parallel{}$, it denotes the number of stack cells required to store it.
+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.
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` :: BCInterpret a}} helper is used.
+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.
e >>| tell` [BCLabel endiflabel]
\end{lstClean}
-\subsection{Functions}
+\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.
\cschemeF{main=m} & =
\cschemeE{m}{[]};\\
\cschemeF{f~a_0 \ldots a_n = b~\text{\cleaninline{In}}~m} & =
- \text{\cleaninline{BCLabel}}~f;\\
- {} & \mathbin{\phantom{=}} \cschemeE{b}{[\langle f, i\rangle, i\in \{(\Sigma^n_{i=0}\parallel{}a_i\parallel{})..0\}]};\\
- {} & \mathbin{\phantom{=}} \text{\cleaninline{BCReturn}}~\parallel{}b\parallel{}~n;\\
- {} & \mathbin{\phantom{=}} \cschemeF{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*}
-%
-%A function call starts by pushing the stack and frame pointer, and making space for the program counter (a) followed by evaluating the arguments in reverse order (b).
-%On executing \Cl{BCJumpSR}, the program counter is set and the interpreter jumps to the function (c).
-%When the function returns, the return value overwrites the old pointers and the arguments.
-%This occurs right after a \Cl{BCReturn} (d).
-%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}
-% \subfigure[\Cl{BCPushPtrs}]{\includegraphics[width=.24\linewidth]{memory1}}
-% \subfigure[Arguments]{\includegraphics[width=.24\linewidth]{memory2}}
-% \subfigure[\Cl{BCJumpSR}]{\includegraphics[width=.24\linewidth]{memory3}}
-% \subfigure[\Cl{BCReturn}]{\includegraphics[width=.24\linewidth]{memory4}}
-% \caption{The stack layout during function calls.}
-% \Description{A visual representation of the stack layout during a function call and a return.}
-%\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 Subsection~\ref{ssec:step}) and therefore the exact location always has to be determined from the context using \Cl{findarg}\footnote{%
-% \lstinline{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{compilationscheme}
-% \cschemeE{f(a_0, \ldots, a_n)}{r} & =
-% \text{\Cl{BCPushPtrs}};\\
-% {} & \mathbin{\phantom{=}} \cschemeE{a_n}{r}; \cschemeE{a_{\ldots}}{r}; \cschemeE{a_0}{r};\\
-% {} & \mathbin{\phantom{=}} \text{\Cl{BCJumpSR}}\enskip n\enskip f;\\
-% \cschemeE{a_{f^i}}{r} & =
-% \text{\Cl{BCArg} findarg}(r, f, i)\enskip \text{for all}\enskip i\in\{w\ldots v\};\\
-% {} & v = \Sigma^{i-1}_{j=0}\|a_{f^j}\|\\
-% {} & w = v + \|a_{f^i}\|\\
-%\end{compilationscheme}
-%
-%Translating the compilation schemes for functions to Clean is not as straightforward as other schemes due to the nature of shallow embedding.
-%The \Cl{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 \Cl{main} and a callable function.
-%To compile this, the argument must be called with a function representing a function call in mTask.
-%Listing~\ref{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 \Cl{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 \Cl{JumpSR} instruction.
-%The resulting structure (\Cl{g In m}) contains a function representing the mTask function (\Cl{g}) and the \Cl{main} structure to continue with.
-%To get the actual function, \Cl{g} must be called with representations for the argument, i.e.\ using \Cl{findarg} for all arguments.
-%The arguments are added to the context and \Cl{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{lstlisting}[language=Clean,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 (byteWidth a) [a]
-% in addToCtx funlabel zero (argwidth def)
-% >>| liftFunction funlabel (argwidth def)
-% (g (findArgs funlabel zero (argwidth def))) Nothing
-% >>| clearCtx >>| m.main
-% }
-%
-%callFunction :: JumpLabel UInt8 [BCInterpret b] -> BCInterpret c | ...
-%liftFunction :: JumpLabel UInt8 (BCInterpret a) (Maybe UInt8) -> BCInterpret ()
-%\end{lstlisting}
-%
-%\subsection{Tasks}\label{ssec:scheme_tasks}
-%Task trees are created with the \Cl{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 Subsection~\ref{ssec:step}).
-%
-%\begin{compilationscheme}
-% \cschemeE{\text{\Cl{rtrn}}\enskip e}{r} & =
-% \cschemeE{e}{r};
-% \text{\Cl{BCMkTask BCStable}}_{\|e\|};\\
-% \cschemeE{\text{\Cl{unstable}}\enskip e}{r} & =
-% \cschemeE{e}{r};
-% \text{\Cl{BCMkTask BCUnstable}}_{\|e\|};\\
-% \cschemeE{\text{\Cl{readA}}\enskip e}{r} & =
-% \cschemeE{e}{r};
-% \text{\Cl{BCMkTask BCReadA}};\\
-% \cschemeE{\text{\Cl{writeA}}\enskip e_1\enskip e_2}{r} & =
-% \cschemeE{e_1}{r};
-% \cschemeE{e_2}{r};
-% \text{\Cl{BCMkTask BCWriteA}};\\
-% \cschemeE{\text{\Cl{readD}}\enskip e}{r} & =
-% \cschemeE{e}{r};
-% \text{\Cl{BCMkTask BCReadD}};\\
-% \cschemeE{\text{\Cl{writeD}}\enskip e_1\enskip e_2}{r} & =
-% \cschemeE{e_1}{r};
-% \cschemeE{e_2}{r};
-% \text{\Cl{BCMkTask BCWriteD}};\\
-% \cschemeE{\text{\Cl{delay}}\enskip e}{r} & =
-% \cschemeE{e}{r};
-% \text{\Cl{BCMkTask BCDelay}};\\
-% \cschemeE{\text{\Cl{rpeat}}\enskip e}{r} & =
-% \cschemeE{e}{r};
-% \text{\Cl{BCMkTask BCRepeat}};\\
-% \cschemeE{e_1\text{\Cl{.||.}}e_2}{r} & =
-% \cschemeE{e_1}{r};
-% \cschemeE{e_2}{r};
-% \text{\Cl{BCMkTask BCOr}};\\
-% \cschemeE{e_1\text{\Cl{.&&.}}e_2}{r} & =
-% \cschemeE{e_1}{r};
-% \cschemeE{e_2}{r};
-% \text{\Cl{BCMkTask BCAnd}};\\
-%\end{compilationscheme}
-%
-%This simply translates to Clean code by writing the correct \Cl{BCMkTask} instruction as exemplified in Listing~\ref{lst:imp_ret}.
-%
-%\begin{lstlisting}[language=Clean,caption={The backend implementation for \Cl{rtrn}.},label={lst:imp_ret}]
-%instance rtrn BCInterpret where rtrn m = m >>| tell` [BCMkTask (bcstable m)]
-%\end{lstlisting}
-%
-%\subsection{Step combinator}\label{ssec:step}
-%The \Cl{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{compilationscheme}
-% \cschemeE{t_1\text{\Cl{>>*.}}t_2}{r} & =
-% \cschemeE{a_{f^i}}{r}, \langle f, i\rangle\in r;
-% \text{\Cl{BCMkTask}}\enskip \text{\Cl{BCStable}}_{\|r\|};\\
-% {} & \mathbin{\phantom{=}} \cschemeE{t_1}{r};\\
-% {} & \mathbin{\phantom{=}} \text{\Cl{BCMkTask}}\enskip \text{\Cl{BCAnd}};\\
-% {} & \mathbin{\phantom{=}} \text{\Cl{BCMkTask}}\\
-% {} & \mathbin{\phantom{=}} \enskip (\text{\Cl{BCStep}}\enskip (\cschemeS{t_2}{(r + [\langle l_s, i\rangle])}{\|t_1\|}));\\
-%%
-% \cschemeS{[]}{r}{w} & =
-% \text{\Cl{BCPush}}\enskip \bot;\\
-% \cschemeS{\text{\Cl{IfValue}}\enskip f\enskip t:cs}{r}{w} & =
-% \text{\Cl{BCArg}} (\|r\| + w);
-% \text{\Cl{BCIsNoValue}};\\
-% {} & \mathbin{\phantom{=}} \cschemeE{f}{r};
-% \text{\Cl{BCAnd}};\\
-% {} & \mathbin{\phantom{=}} \text{\Cl{BCJmpF}}\enskip l_1;\\
-% {} & \mathbin{\phantom{=}} \cschemeE{t}{r};
-% \text{\Cl{BCJmp}}\enskip l_2;\\
-% {} & \mathbin{\phantom{=}} \text{\Cl{BCLabel}}\enskip l_1;
-% \cschemeS{cs}{r}{w};\\
-% {} & \mathbin{\phantom{=}} \text{\Cl{BCLabel}}\enskip l_2;\\
-% {} & \text{\emph{Where $l_1$ and $l_2$ are fresh labels}}\\
-% {} & \text{\emph{Similar for \Cl{IfStable} and \Cl{IfUnstable}}}\\
-% \cschemeS{\text{\Cl{IfNoValue}}\enskip t:cs}{r}{w} & =
-% \text{\Cl{BCArg}} (\|r\|+w);
-% \text{\Cl{BCIsNoValue}};\\
-% {} & \mathbin{\phantom{=}} \text{\Cl{BCJmpF}}\enskip l_1;\\
-% {} & \mathbin{\phantom{=}} \cschemeE{t}{r};
-% \text{\Cl{BCJmp}}\enskip l_2;\\
-% {} & \mathbin{\phantom{=}} \text{\Cl{BCLabel}}\enskip l_1;
-% \cschemeS{cs}{r}{w};\\
-% {} & \mathbin{\phantom{=}} \text{\Cl{BCLabel}}\enskip l_2;\\
-% {} & \text{\emph{Where $l_1$ and $l_2$ are fresh labels}}\\
-% \cschemeS{\text{\Cl{Always}}\enskip f:cs}{r}{w} & =
-% \cschemeE{f}{r};\\
-%\end{compilationscheme}
-%
-%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 \Cl{.&&.} 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{lstlisting}[language=Clean]
-%t1 >>= \v1->t2 >>= \v2->t3 >>= ...
-%//is transformed to
-%t1 >>= \v1->rtrn v1 .&&. t2 >>= \v2->rtrn (v1, v2) .&&. t3 >>= ...
-%\end{lstlisting}
-%
-%The translation to Clean is given in Listing~\ref{lst:imp_seq}.
-%
-%\begin{lstlisting}[language=Clean,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{lstlisting}
-%
-%\subsection{Shared Data Sources}
-%The compilation scheme for SDS definitions is a trivial extension to $\mathcal{F}$ since there is no code generated as seen below.
-%
-%\begin{compilationscheme}
-% \cschemeF{\text{\Cl{sds}}\enskip x=i\enskip \text{\Cl{In}}\enskip m} & =
-% \cschemeF{m};\\
-% \cschemeF{\text{\Cl{liftsds}}\enskip x=i\enskip \text{\Cl{In}}\enskip m} & =
-% \cschemeF{m};\\
-%\end{compilationscheme}
-%
-%The SDS access tasks have a compilation scheme similar to other tasks (see~Subsection~\ref{ssec:scheme_tasks}).
-%The \Cl{getSds} task just pushes a task tree node with the SDS identifier embedded.
-%The \Cl{setSds} task evaluates the value, lifts that value to a task tree node and creates an SDS set node.
-%
-%\begin{compilationscheme}
-% \cschemeE{\text{\Cl{getSds}}\enskip s}{r} & =
-% \text{\Cl{BCMkTask}} (\text{\Cl{BCSdsGet}} s);\\
-% \cschemeE{\text{\Cl{setSds}}\enskip s\enskip e}{r} & =
-% \cschemeE{e}{r};
-% \text{\Cl{BCMkTask BCStable}}_{\|e\|};\\
-% {} & \mathbin{\phantom{=}} \text{\Cl{BCMkTask}} (\text{\Cl{BCSdsSet}} s);\\
-%\end{compilationscheme}
-%
-%While there is no code generated in the definition, the bytecode compiler is storing the SDS data in the \Cl{bcs_sdses} field in the compilation state.
-%The SDSs are typed as functions in the host language so an argument for this function must be created that represents the SDS on evaluation.
-%For this, an \Cl{BCInterpret} is created that emits this identifier.
-%When passing it to the function, the initial value of the SDS is returned.
-%This initial value is stored as a bytecode encoded value in the state and the compiler continues with the rest of the program.
-%
-%Compiling \Cl{getSds} is a matter of executing the \Cl{BCInterpret} representing the SDS, which yields the identifier that can be embedded in the instruction.
-%Setting the 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.
-%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 \Cl{a} from the \Cl{Shared a} to a \Cl{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.
-%
-%\begin{lstlisting}[language=Clean,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{lstlisting}
-%
-%\section{Run time system}
-%
-%The RTS is designed to run on systems with as little as 2kB of RAM.
-%Aggressive memory management is therefore vital.
-%Not all firmwares for MCUs support heaps and---when they do---allocation often leaves holes when not used in a Last In First Out strategy.
-%Therefore the RTS uses a chunk of memory in the global data segment with its own memory manager tailored to the needs of mTask.
-%The size of this block can be changed in the configuration of the RTS if necessary.
-%On an Arduino {UNO} ---equipped with 2kB of RAM--- this size can be about 1500 bytes.
-%
-%In memory, task data grows from the bottom up and an 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, even tuples.
-%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.
-%
-%The event loop of the RTS is executed repeatedly and consists of three distinct phases.
-%
-%%TODO evt subsubsections verwijderen
-%\subsubsection{Communication}
-%In the first phase, the communication channels are processed.
-%The messages announcing SDS updates are applied immediately, the initialization of new tasks is delayed until the next phase.
-%
-%\subsubsection{Execution}
-%The second phase consists of executing tasks.
-%The RTS executes all tasks in a round robin fashion.
-%If a task is not initialized yet, the bytecode of the main function is interpreted to produce the initial task tree.
-%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.
-%
-%\subsubsection{Memory management}
-%The third and final phase is memory management.
-%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 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.
-%\subsection{Memory management}
-%\subsection{Interpreter}
-%\subsection{Rewrite engine}
-%\section{Task rewriting}\label{sec:rewrite}
-%Tasks are rewritten every event loop iteration and one rewrite cycle is generally very fast.
-%This results in seemingly parallel execution of the tasks because the rewrite steps are interleaved.
-%Rewriting is a destructive process that actually modifies the task tree nodes in memory and marks nodes that become garbage.
-%The task value is stored on the stack and therefore only available during rewriting.
-%
-%\subsection{Basic tasks}
-%The \Cl{rtrn} and \Cl{unstable} tasks always rewrite to themselves and have no side effects.
-%The GPIO interaction tasks do have side effects.
-%The \Cl{readA} and \Cl{readD} tasks will query the given pin every rewrite cycle and emit it as an unstable task value.
-%The \Cl{writeA} and \Cl{writeD} tasks write the given value to the given pin and immediately rewrite to a stable task of the written value.
-%
-%\subsection{Delay and repetition}
-%The \Cl{delay} task stabilizes once a certain amount of time has been passed by storing the finish time on initialization.
-%In every rewrite step it checks whether the current time is bigger than the finish time and if so, it rewrites to a \Cl{rtrn} task containing the number of milliseconds that it overshot the target.
-%The \Cl{rpeat} task combinator rewrites the argument until it becomes stable.
-%Rewriting is a destructive process and therefore the original task tree must be saved.
-%As a consequence, on installation, the argument is cloned and the task rewrites the clone.
-%
-%\subsection{Sequential combination}
-%First the left-hand side of the step task is rewritten.
-%The resulting value is passed to the continuation function.
-%If the continuation function returns a pointer to a task tree, the task tree rewrites to that task tree and marks the original left-hand side as trash.
-%If the function returns $\bot$, the step is kept unchanged.
-%The step itself never fields a value.
-%
-%\subsection{Parallel combination}\label{ssec:parallelExecution}
-%There are two parallel task combinators available.
-%A \Cl{.&&.} task only becomes stable when both sides are stable.
-%A \Cl{.||.} task becomes stable when one of the sides is stable.
-%The combinators first rewrite both sides and then merge the task values according to the semantics given in Listing~\ref{lst:parallel_combinators}.
-%
-%\begin{lstlisting}[language=Clean,caption={Task value semantics for the parallel combinators.},label={lst:parallel_combinators}]
-%(.&&.) :: (TaskValue a) (TaskValue b) -> TaskValue (a, b)
-%(.&&.) (Value lhs stab1) (Value rhs stab2) = Value (lhs, rhs) (stab1 && stab2)
-%(.&&.) _ _ = NoValue
-%
-%(.||.) :: (TaskValue a) (TaskValue a) -> TaskValue a
-%(.||.) lhs=:(Value _ True) _ = lhs
-%(.||.) (Value lhs _) rhs=:(Value _ True) = rhs
-%(.||.) NoValue rhs = rhs
-%(.||.) lhs _ = lhs\end{lstlisting}
-%
-%\subsection{Shared Data Source tasks}
-%The \Cl{BCSdsGet} node always rewrites to itself.
-%It will read the actual SDS embedded and emit the value as an unstable task value.
-%
-%Setting an SDS is a bit more involved because after writing, it emits the value written as a stable task value.
-%The \Cl{BCSdsSet} node contains the identifier for the SDS and a task tree that, when rewritten, emits the value to be set as a stable task value.
-%The naive approach would be to just rewrite the \Cl{BCSdsSet} to a node similar to the \Cl{BCSdsGet} but only with a stable value.
-%However, after writing the SDS, its value might have changed due to other tasks writing it, and then the \Cl{setSDS}'s stable value may change.
-%Therefore, the \Cl{BCSdsSet} node is rewritten to the argument task tree which always represents constant stable value.
-%In future rewrites, the constant value node emits the value that was originally written.
-%
-%The client only knows whether an SDS is a lifted SDS, not to which iTasks SDS it is connected.
-%If the SDS is modified on the device, it sends an update to the server.
-%
-%\section{Conclusion}
+
+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{Conclusion}
+%\todo[inline]{conclusion}
\input{subfilepostamble}
\end{document}
repositories / phd-thesis.git / blobdiff