+Lowered \glspl{SDS} are stored in the compiler state as \cleaninline{Right MTLens} values.
+The compilation of the code and the serialisation of the data throws away all typing information.
+The \cleaninline{MTLens} is a type synonym for \pgls{SDS} that represents the typeless serialised value of the underlying \gls{SDS}.
+This is done so that the \cleaninline{withDevice} task can write the received \gls{SDS} updates to the according \gls{SDS} while the \gls{SDS} is not in scope.
+The \gls{ITASK} notification mechanism then takes care of the rest.
+Such \pgls{SDS} is created by using the \cleaninline{mapReadWriteError} which, given a pair of read and write functions with error handling, produces \pgls{SDS} with the lens embedded.
+The read function transforms converts the typed value to a typeless serialised value.
+The write function will, given a new serialised value and the old typed value, produce a new typed value.
+It tries to decode the serialised value, if that succeeds, it is written to the underlying \gls{SDS}, an error is thrown otherwise.
+\Cref{lst:mtask_itasksds_lens} shows the implementation for this.
+
+% VimTeX: SynIgnore on
+\begin{lstClean}[label={lst:mtask_itasksds_lens},caption={Lens applied to lowered \gls{ITASK} \glspl{SDS} in \gls{MTASK}.}]
+lens :: (Shared sds a) -> MTLens | type a & RWShared sds
+lens sds = mapReadWriteError
+ ( \r-> Ok (fromString (toByteCode{|*|} r)
+ , \w r-> ?Just <$> iTasksDecode (toString w)
+ ) ?None sds
+\end{lstClean}
+% VimTeX: SynIgnore off
+
+\Cref{lst:mtask_itasksds_lift} shows the code for the implementation of \cleaninline{lowerSds} that uses the \cleaninline{lens} function shown earlier.
+It is very similar to the \cleaninline{sds} constructor in \cref{lst:comp_sds}, only now a \cleaninline{Right} value is inserted in the \gls{SDS} administration.
+
+% VimTeX: SynIgnore on
+\begin{lstClean}[label={lst:mtask_itasksds_lift},caption={The implementation for lowering \glspl{SDS} in \gls{MTASK}.}]
+instance lowerSds BCInterpret where
+ lowerSds def = {main =
+ let (t In _) = def (abort "lowerSds: expression too strict")
+ in addSdsIfNotExist (Right $ lens t)
+ >>= \sdsi->let (_ In e) = def (pure (Sds sdsi)) in e.main
+ }\end{lstClean}
+% VimTeX: SynIgnore off
+
+\section{Run-time system}\label{sec:compiler_rts}
+The \gls{RTS} is a customisable domain-specific \gls{OS} that takes care of the execution of tasks.
+Furthermore, it also takes care of low-level mechanisms such as the communication, multitasking, and memory management.
+Once a 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.
+In order to keep the abstraction level high and the hardware requirements low, much of the high-level functionality of the \gls{MTASK} language is implemented not in terms of lower-level constructs from \gls{MTASK} language but in terms of \ccpp{} code.
+
+Most microcontrollers software consists of a cyclic executive instead of an \gls{OS}, this one loop function is continuously executed and all work is performed there.
+In the \gls{RTS} of the \gls{MTASK} system, there is also such an event loop function.
+It is a function with a relatively short execution time that gets called repeatedly.
+The event loop 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} for more details on task scheduling).
+
+\subsection{Communication phase}
+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 kept deliberately simple and consists of two layers: a link interface and a communication interface.
+Besides opening, closing and cleaning up, the link interface has three functions that are shown in \cref{lst:link_interface}.
+Consequently, implementing this link interface is very simple, but it is still possible to implement more advanced link features such as buffering.
+There are implementations for this interface for serial or \gls{WIFI} 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.
+ It is received immediately after connecting.
+ The \gls{RTS} responds with a \texttt{Spec} answer containing the specification.
+ \item[TaskPrep]
+ tells the device a 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 message allows the \gls{RTS} to postpone execution for a while, until the larger task has been received.
+ The server sends the task only after the device acknowledged the preparation by sending a \texttt{TaskPrepAck} message.
+ \item[Task]
+ contains a new task, its peripheral configuration, the \glspl{SDS}, and the byte code.
+ The new task is immediately copied to the task storage but is only initialised during the next phase.
+ The device acknowledges the task by sending a \texttt{TaskAck} message.
+ \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 the deletion by sending a \texttt{TaskDelAck}.
+ \item[Shutdown]
+ tells the device to reset.
+\end{description}
+
+\subsection{Execution phase}
+The second phase performs 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 execute, 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 rewriter.
+The rewriter scans the current task tree and tries to rewrite it using small-step reduction.
+Expressions in the tree are always strictly evaluated by the interpreter.
+
+When a new task is received, the main expression is evaluated to produce a task tree.
+A task tree is a tree structure in which each node represents a task combinator and the leaves are basic tasks.
+If a task is not initialised 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 of \gls{MTASK} programs sent to the device fore execution 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 \glspl{SDS} is done other than \gls{SDS} operations from the task itself.
+The host is notified if a task value is changed after a rewrite step by sending a \texttt{TaskReturn} message.
+
+Take for example a blink task for which the code is shown in \cref{lst:blink_code}.
+
+\begin{lstClean}[caption={Code for a blink program.},label={lst:blink_code}]
+declarePin D13 PMOutput \ledPin->
+fun \blink=(\st->delay (lit 500) >>|. writeD ledPin st >>=. blink o Not)
+In {main = blink true}
+\end{lstClean}
+
+On receiving this task, the task tree is still null and the initial expression \cleaninline{blink true} is evaluated by the interpreter.
+This results in the task tree shown in \cref{fig:blink_tree1}.
+Rewriting always starts at the top of the tree and traverses to the leaves, the basic tasks that do the actual work.
+The first basic task encountered is the \cleaninline{delay} task, that yields no value until the time, \qty{500}{\ms} in this case, has passed.
+When the \cleaninline{delay} task yielded a stable value after a number of rewrites, the task continues with the right-hand side of the \cleaninline{>>\|.} combinator by evaluating the expression (see \cref{fig:blink_tree2})\footnotemark.
+\footnotetext{\cleaninline{t1 >>\|. t2} is a shorthand for \cleaninline{t1 >>*. [IfStable id \\_->t2]}.}
+This combinator has a \cleaninline{writeD} task at the left-hand side that becomes stable after one rewrite step in which it writes the value to the given pin.
+When \cleaninline{writeD} becomes stable, the written value is the task value that is observed by the right-hand side of the \cleaninline{>>=.} combinator.
+Then the interpreter is used again to evaluate the expression, now that the argument of the function is known.
+The result of the call to the function is again a task tree, but now with different arguments to the tasks, e.g.\ the state in \cleaninline{writeD} is inversed.
+
+\begin{figure}
+ \centering
+ \begin{subfigure}[t]{.5\textwidth}
+ \includestandalone{blinktree1}
+ \caption{Initial task tree}%
+ \label{fig:blink_tree1}
+ \end{subfigure}%
+ \begin{subfigure}[t]{.5\textwidth}
+ \includestandalone{blinktree2}
+ \caption{Task tree after the delay passed}%
+ \label{fig:blink_tree2}
+ \end{subfigure}
+ \caption{The task trees during reduction for a blink task in \gls{MTASK}.}%
+ \label{fig:blink_tree}
+\end{figure}
+
+\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 in the \gls{MTASK} \gls{RTS}.}\label{fig:memory_layout}
+\end{figure}
+
+A task is stored below the stack and it consists of 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 to their parent.
+
+
+\section{C code generation for communication}\label{sec:ccodegen}
+All communication between the \gls{ITASK} server and the \gls{MTASK} server is type parametrised and automated.