errata
[phd-thesis.git] / top / imp.tex
index ce38d1d..6231b4b 100644 (file)
@@ -32,7 +32,7 @@ First, the source code is compiled to a byte code specification, this specificat
 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.
 In order to execute a task, first the main expression is evaluated in the interpreter, resulting in a task tree.
-Using small-step reduction, this task tree is continuously rewritten by the rewrite engine of the \gls{RTS}.
+Then, using small-step reduction, the task tree is continuously rewritten by the rewrite engine of the \gls{RTS}.
 At times, the reduction requires the evaluation of expressions, using the interpreter.
 During every rewrite step, a task value is produced.
 On the device, the \gls{RTS} may have multiple tasks at the same time active.
@@ -47,6 +47,17 @@ The design, architecture and implementation of the \gls{RTS} is shown in \cref{s
 \end{figure}
 
 \section{Compiler}\label{sec:compiler_imp}
+The byte code compiler for \gls{MTASK} is an interpretation of the \gls{MTASK} language.
+In order to compile terms, instances for all \gls{MTASK} type classes are required for the \cleaninline{:: BCInterpret a} type.
+Terms in \gls{MTASK} are constructed and compiled at run time, but type checked at compile time in the host language \gls{CLEAN}.
+The compiled tasks are sent to the device for interpretation.
+The result of the compilation is the byte code and some metadata regarding the used peripherals and \glspl{SDS}.
+The compilation target is the interpreter of the \gls{MTASK} \gls{RTS}.
+In order to keep the hardware requirements down, all expressions are evaluated on a stack.
+Rewriting of tasks uses the same stack and also a heap.
+The heap usage is minimised by applying aggressive memory management.
+A detailed overview of the \gls{RTS} including the interpreter and rewriter is found in \cref{sec:compiler_rts}.
+
 \subsection{Compiler infrastructure}
 The byte code 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.
@@ -83,7 +94,7 @@ After compilation, several post-processing steps are applied to make the code su
 First, in all tail call \cleaninline{BCReturn} instructions are replaced by \cleaninline{BCTailCall} instructions to optimise the tail calls.
 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 \numrange{0}{2} and can be replaced by the \numrange[parse-numbers=false]{\cleaninline{BCArg0}}{\cleaninline{BCArg2}} shorthands.
+For example, the \cleaninline{BCArg} instruction is often called with argument \numrange{0}{2} and can be replaced by the \cleaninline{BCArg0} to \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 lowered \glspl{SDS} are resolved to provide an initial value for them.
@@ -158,15 +169,14 @@ More information is given in the schemes requiring such arguments.
 
 \begin{table}
        \centering
-       \caption{An overview of the compilation schemes.}
+       \caption{An overview of the compilation rules.}
        \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.\\
+               $\cschemeE{e}{r}$ & Generates code for expressions given the context $r$\\
+               $\cschemeF{e}$ & Generates the code for functions.\\
+               $\cschemeS{e}{r}{w} $ & Generates the code for the step continuations given the context $r$ and the width $w$ of the left-hand side task value.\\
                \bottomrule
        \end{tabularx}
 \end{table}
@@ -177,6 +187,8 @@ 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.
 
+\begingroup
+\allowdisplaybreaks%
 \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};
@@ -208,6 +220,7 @@ Function calls, function arguments and tasks are also compiled using $\mathcal{E
                {} & \text{\emph{Where $w_l$ is the width of the left and, $w_r$ of the right value}}\\
                {} & \text{\emph{similar for other unboxed compound data types}}\\
 \end{align*}
+\endgroup
 
 Translating $\mathcal{E}$ to \gls{CLEAN} code is very straightforward, it basically means writing the instructions to the writer monad.
 Almost always, the type of the interpretation is not used, i.e.\ it is a phantom type.
@@ -322,6 +335,8 @@ Task trees are created with the \cleaninline{BCMkTask} instruction that allocate
 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}).
 
+\begingroup
+\allowdisplaybreaks%
 \begin{align*}
        \cschemeE{\text{\cleaninline{rtrn}}~e}{r} & =
                        \cschemeE{e}{r};
@@ -358,13 +373,14 @@ The following extension of $\mathcal{E}$ shows this compilation scheme (except f
                        \cschemeE{e_2}{r};
                        \text{\cleaninline{BCMkTask BCAnd}};\\
 \end{align*}
+\endgroup%
 
-This translates to Clean code by writing the correct \cleaninline{BCMkTask} instruction as exemplified in \cref{lst:imp_ret}.
+This compilation scheme translates to Clean code by first writing the arguments and then the correct \cleaninline{BCMkTask} instruction.
+This is shown for the \cleaninline{.&&.} task in \cref{lst:imp_ret}.
 
 \begin{lstClean}[caption={The byte code interpretation implementation for \cleaninline{rtrn}.},label={lst:imp_ret}]
-instance rtrn BCInterpret
-where
-       rtrn m = m >>| tell` [BCMkTask (bcstable m)]
+instance .&&. BCInterpret where
+       (.&&.) l r = l >>| r >>| tell` [BCMkTask BCTAnd]
 \end{lstClean}
 
 \subsection{Sequential combinator}\label{ssec:step}
@@ -379,10 +395,10 @@ The resulting function is basically a list of if-then-else constructions to chec
 Some optimisation is possible here but has currently not been implemented.
 
 \begin{align*}
-       \cschemeE{t_1\text{\cleaninline{>>*.}}t_2}{r} & =
+       \cschemeE{t_1\text{\cleaninline{>>*.}}e_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}}));\\
+       {} & \mathbin{\phantom{=}} \text{\cleaninline{BCMkTask}}~\text{\cleaninline{BCAnd}}; \text{\cleaninline{BCMkTask}}~(\text{\cleaninline{BCStep}}~(\cschemeS{e_2}{(r + [\langle l_s, i\rangle])}{\stacksize{t_1}}));\\
 \end{align*}
 
 \begin{align*}
@@ -403,10 +419,14 @@ Some optimisation is possible here but has currently not been implemented.
        {} & \text{\emph{Similar for \cleaninline{IfStable} and \cleaninline{IfUnstable}}}\\
 \end{align*}
 
-First the context is evaluated.
+The step combinator has a task as the left-hand side and a list of continuations at the right-hand side.
+First the context is evaluated ($\cschemeE{a_{f^i}}{r}$).
 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.
+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 step.
 This means that the task tree is transformed as seen in \cref{lst:context_tree}.
+In this figure, the expression \cleaninline{t1 >>=. \\v1->t2 >>=. \\v2->...} is shown\footnote{%
+       \cleaninline{t >>=. e} is a shorthand combinator for \cleaninline{t >>* [OnStable (\\_->true) e].}}.
+Then, the right-hand side list of continuations is converted to an expression using $\mathcal{S}$.
 
 \begin{figure}
        \begin{subfigure}{.5\textwidth}
@@ -417,7 +437,7 @@ This means that the task tree is transformed as seen in \cref{lst:context_tree}.
                \includestandalone{contexttree2}
                \caption{With the embedded context.}
        \end{subfigure}
-       \caption{Context embedded in a task tree.}%
+       \caption{Context embedded in a virtual task tree.}%
        \label{lst:context_tree}
 \end{figure}
 
@@ -449,8 +469,7 @@ instance step BCInterpret where
                                //Return width (always 1, a task pointer)
                                (Just one)
                >>| modify (\s->{s & bcs_context=ctx})
-               >>| tell` [BCMkTask (instr rhswidth funlab)]
-
+               >>| tell` [BCMkTask (instr rhswidth funlab)][+\pagebreak+]
 toContFun :: JumpLabel UInt8 -> BCInterpret a
 toContFun steplabel contextwidth
        = foldr tcf (tell` [BCPush fail]) cont
@@ -464,33 +483,29 @@ where
 \end{lstClean}
 
 \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*}
-       \cschemeF{\text{\cleaninline{sds}}~x=i~\text{\cleaninline{In}}~m} & =
-               \cschemeF{m};\\
-\end{align*}
-
+The compilation scheme for \gls{SDS} definitions is a trivial extension to $\mathcal{F}$.
+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.
+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.
 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 \pgls{SDS} set node.
 
 \begin{align*}
+       \cschemeF{\text{\cleaninline{sds}}~x=i~\text{\cleaninline{In}}~m} & =
+               \cschemeF{m};\\
+       \\
        \cschemeE{\text{\cleaninline{getSds}}~s}{r} & =
-               \text{\cleaninline{BCMkTask}} (\text{\cleaninline{BCSdsGet}} s);\\
+               \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);\\
+       {} & \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 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.
-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.
@@ -522,9 +537,9 @@ The \cleaninline{MTLens} is a type synonym for \pgls{SDS} that represents the ty
 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 read function transforms 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.
+It tries to decode the serialised value, if that succeeds, it is written to the underlying \gls{SDS}, otherwise, an error is thrown otherwise.
 \Cref{lst:mtask_itasksds_lens} shows the implementation for this.
 
 % VimTeX: SynIgnore on
@@ -557,7 +572,8 @@ Once a device is programmed with the \gls{MTASK} \gls{RTS}, it can continuously
 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.
+Most microcontroller 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.
@@ -619,13 +635,16 @@ There are several possible messages that can be received from the server:
 
 \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.
+Tasks are placed in a priority queue orderd 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 always produces a task tree.
+The main expression of \gls{MTASK} programs sent to the device before 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.
@@ -639,24 +658,35 @@ The host is notified if a task value is changed after a rewrite step by sending
 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}]
-fun \blink=(\st->delay (lit 500) >>|. writeD d3 st >>=. blink o Not)
+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_tree}.
+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.
+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.
-This will call the interpreter to evaluate the expression, now that the argument of the function is known.
-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.
+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
-       \includestandalone{blinktree}
-       \caption{The task tree for a blink task in \cref{lst:blink_code} in \gls{MTASK}.}%
+       \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}
 
@@ -676,7 +706,7 @@ The self-managed memory uses a similar layout as the memory layout for \gls{C} p
        \caption{Memory layout in the \gls{MTASK} \gls{RTS}.}\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.
+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.
@@ -692,8 +722,8 @@ For task trees---stored in the heap---the \gls{RTS} already marks tasks and task
 This is possible because there is no sharing or cycles in task trees and nodes contain pointers to their parent.
 
 
-\section{C code generation}\label{sec:ccodegen}
-All communication between the \gls{ITASK} server and the \gls{MTASK} server is type parametrised.
+\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.
 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.