many updates
[phd-thesis.git] / top / imp.tex
index 09c2ce7..091adb8 100644 (file)
@@ -6,11 +6,12 @@
 
 \begin{document}
 \input{subfileprefix}
-\chapter{The implementation of \texorpdfstring{\gls{MTASK}}{mTask}}%
+\chapter{The implementation of mTask}%
 \label{chp:implementation}
 \begin{chapterabstract}
        This chapter shows the implementation of the \gls{MTASK} system by:
        \begin{itemize}
+               \item showing the compilation and execution toolchain;
                \item elaborating on the implementation and architecture of the \gls{RTS} of \gls{MTASK};
                \item showing the implementation of the byte code compiler for the \gls{MTASK} language;
                \item and explaining the machinery used to automatically serialise and deserialise data to-and-fro the device.
 The \gls{MTASK} system targets resource-constrained edge devices that have little memory, processor speed, and communication.
 Such edge devices are often powered by microcontrollers, tiny computers specifically designed for embedded applications.
 The microcontrollers usually have flash-based program memory which wears out fairly quickly.
-For example, the flash memory of the popular atmega328p powering the \gls{ARDUINO} UNO is rated for 10000 write cycles.
+For example, the flash memory of the popular atmega328p powering the \gls{ARDUINO} UNO is rated for \num{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, storing the program in the \gls{RAM} of the device and interpreting this code is necessary in order to save precious write cycles of the program memory.
 In the \gls{MTASK} system, the \gls{MTASK} \gls{RTS}, a domain-specific \gls{OS}, is responsible for interpreting the programs.
 
-\section{\texorpdfstring{\Glsxtrlong{RTS}}{Run time system}}
+Programs in \gls{MTASK} are \gls{DSL} terms constructed at run time in an \gls{ITASK} system.
+\Cref{fig:toolchain} shows the compilation and execution toolchain of such programs.
+First, the source code is compiled to a byte code specification, this specification contains the compiled main expression, the functions, and the \gls{SDS} and peripheral configuration.
+How an \gls{MTASK} task is compiled to this specification is shown in \cref{sec:compiler_imp}.
+This package is then sent to the \gls{RTS} of the device for execution, shown in \cref{sec:compiler_rts}.
+On the device, the \gls{RTS} may have multiple tasks at the same time active.
+
+\begin{figure}
+       \centering
+       \centerline{\includestandalone{toolchain}}
+       \caption{Compilation and execution toolchain of \gls{MTASK} programs.}%
+       \label{fig:toolchain}
+\end{figure}
+
+\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}, the \gls{RTS} of the \gls{MTASK} system is implemented as such also.
-It consists of a loop function with a relatively short execution time, similar to the one in \gls{ARDUINO}, that gets called repeatedly.
+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).
 
@@ -124,7 +140,7 @@ When the \cleaninline{delay} task yielded a stable value after a number of rewri
 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.
 This will call the interpreter to evaluate the expression, now that the argument of the function is known.
-The result of the function is the original task tree again, but now with the state inversed.
+The result of 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
@@ -164,7 +180,7 @@ 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.
 
-\section{Compiler}
+\section{Compiler}\label{sec:compiler_imp}
 \subsection{Compiler infrastructure}
 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.
@@ -175,7 +191,7 @@ code of the main expression;
 context (see \cref{ssec:step});
 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};
+a list of all the used \glspl{SDS}, either local \glspl{SDS} containing the initial value (\cleaninline{Left}) or lowered \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={The type for the \gls{MTASK} byte code compiler.}]
@@ -204,7 +220,7 @@ Many instructions have commonly used arguments so shorthands are introduced to r
 For example, the \cleaninline{BCArg} instruction is often called with argument \numrange{0}{2} and can be replaced by the \numrange[parse-numbers=false]{\cleaninline{BCArg0}}{\cleaninline{BCArg2}} shorthands.
 Furthermore, redundant instructions such as 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 the freshly generated identifiers.
-After the byte code is ready, the lifted \glspl{SDS} are resolved to provide an initial value for them.
+After the byte code is ready, the lowered \glspl{SDS} are resolved to provide an initial value for them.
 The byte code, \gls{SDS} specification and perpipheral specifications are the result of the process, ready to be sent to the device.
 
 \subsection{Instruction set}
@@ -266,7 +282,6 @@ One notable instruction is the \cleaninline{MkTask} instruction, it allocates an
        ...
 \end{lstClean}
 
-
 \section{Compilation rules}
 This section describes the compilation rules, the translation from \gls{AST} to byte code.
 The compilation scheme consists of three schemes\slash{}functions.
@@ -525,16 +540,19 @@ Some optimization is possible here but has currently not been implemented.
 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 as
+This means that the task tree is be transformed as seen in \cref{lst:context_tree}.
 
 \begin{figure}
        \begin{subfigure}{.5\textwidth}
                \includestandalone{contexttree1}
-
-       \end{subfigure}
+               \caption{Without the embedded context.}
+       \end{subfigure}%
        \begin{subfigure}{.5\textwidth}
                \includestandalone{contexttree2}
+               \caption{With the embedded context.}
        \end{subfigure}
+       \caption{Context embedded in a task tree.}%
+       \label{lst:context_tree}
 \end{figure}
 
 The translation to \gls{CLEAN} is given in \cref{lst:imp_seq}.
@@ -579,7 +597,7 @@ where
        val = retrieveArgs steplabel zero lhswidth
 \end{lstClean}
 
-\subsection{\texorpdfstring{\Glspl{SDS}}{Shared data sources}}
+\subsection{Shared data sources}\label{lst:imp_sds}
 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*}
@@ -600,18 +618,19 @@ The \cleaninline{setSds} task evaluates the value, lifts that value to a task tr
        {} & \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.
+While there is no code generated in the definition, the byte code compiler is storing all \gls{SDS} data in the \cleaninline{bcs_sdses} field in the compilation state.
+Regular \glspl{SDS} are stored as \cleaninline{Right String255} values.
 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.
+In the case of a local \gls{SDS}, this initial value is stored as a byte code encoded value in the state and the compiler continues with the rest of the program.
 
+\Cref{lst:comp_sds} shows the implementation of the \cleaninline{sds} type class.
 First, the initial \gls{SDS} value is extracted from the expression by bootstrapping the fixed point with a dummy value.
 This is safe because the expression on the right-hand side of the \cleaninline{In} is never evaluated.
 Then, using \cleaninline{addSdsIfNotExist}, the identifier for this particular \gls{SDS} is either retrieved from the compiler state or generated freshly.
 This identifier is then used to provide a reference to the \cleaninline{def} definition to evaluate the main expression.
 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.
-Lifted SDSs are compiled in a very similar way \cref{sec:liftsds}.
 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.
 
 % VimTeX: SynIgnore on
@@ -631,8 +650,42 @@ instance sds BCInterpret where
 \end{lstClean}
 % VimTeX: SynIgnore off
 
-\section{\texorpdfstring{\Gls{C}}{C} code generation}\label{sec:ccodegen}
-All communication between the \gls{ITASK} server and the \gls{MTASK} server is type-parametrised.
+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{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 rich generic programming library or compiler support that includes a lot of metadata in the record and constructor nodes.