process more todos
authorMart Lubbers <mart@martlubbers.net>
Tue, 7 Mar 2023 15:47:03 +0000 (16:47 +0100)
committerMart Lubbers <mart@martlubbers.net>
Tue, 7 Mar 2023 15:47:03 +0000 (16:47 +0100)
thesis.tex
top/4iot.tex
top/blinktree1.tex [new file with mode: 0644]
top/blinktree2.tex [moved from top/blinktree.tex with 70% similarity]
top/green.tex
top/imp.tex
top/int.tex
top/lang.tex
top/lst/example.icl
top/lst/nitrile-lock.json

index 4712e6c..d0fcd9b 100644 (file)
@@ -8,7 +8,7 @@
 \input{preamble}
 
 % To show hboxes even when in non-draft mode
-\setlength{\overfullrule}{20pt}
+%\setlength{\overfullrule}{20pt}
 
 % Just for the todonotes, can go when it's finished
 \usepackage{todonotes}
index 3bdaf18..931522e 100644 (file)
@@ -6,7 +6,7 @@
 
 \begin{document}
 \input{subfileprefix}
-\chapter{Task-oriented programming for the internet of things}%
+\chapter{An introduction to edge device programming}%
 \label{chp:top4iot}
 \begin{chapterabstract}
        This chapter introduces the monograph. It compares traditional edge device programming to \gls{TOP} by:
@@ -216,26 +216,16 @@ blinktask =
 \end{lstClean}
 % VimTeX: SynIgnore off
 
-\section{Conclusion and reading guide}
-\todo[inline]{Reading guide noemen ipv conclusion omdat:
-Veel van wat hier staat is geen conclusie van het voorgaande.  Kun je dit niet beter reading guide noemen?}
+\section{Reading guide}
 This chapter introduced traditional edge device programming and programming edge devices using \gls{MTASK}.
-\todo[inline]{Anders dan de titel van dit hoofdstuk suggereert, geeft dit maar een heel beperkt overzicht van TOP in mTask.
-
-       Zou je niet expliciet noemen dat je task resulten kunt gebruiken, conditionals en een step combinator hebt etc. Voorbeelden van alles lijkt me niet nodig.
-
-Ook zou ik de SDS en integratie met iTask nog eens noemen te verwijzen naar de introductie.
-Iets over semantiek zeggen?}
 The edge layer of \gls{IOT} systems is powered by microcontrollers.
 Microcontrollers have significantly different characteristics to regular computers.
 Programming them happens through compiled firmwares using low-level imperative programming languages.
 Due to the lack of an \gls{OS}, writing applications that perform multiple tasks at the same time is error-prone, becomes complex, and requires a lot of boilerplate such as manual scheduling code.
 With the \gls{MTASK} system, a \gls{TOP} programming language for \gls{IOT} edge devices, this limitation can be overcome.
 Since a lot domain-specific knowledge is built into the language and \gls{RTS}, the hardware requirements can be kept relatively low while maintaining a high abstraction level.
-Furthermore, the programs are automatically integrated with \gls{ITASK}, a \gls{TOP} system for creating interactive distributed web applications, allowing for data sharing, task coordination, and dynamic construction of tasks.
-\todo[inline]{
-This makes it easy to create interactive applications modelling collaboration between end-users and edge devices.
-}
+Tasks in \gls{MTASK} are high-level specifications of the work that needs to be done, they can be combined using task combinators, and share data using \glspl{SDS}.
+Furthermore, the programs are automatically integrated with \gls{ITASK}, a \gls{TOP} system for creating interactive distributed web applications, allowing for data sharing, task coordination, and dynamic construction of tasks over all layers of an \gls{IOT} system.
 
 The following chapters of this monograph thoroughly introduce all aspects of the \gls{MTASK} system.
 First, the language setup and interface are shown in \cref{chp:mtask_dsl}.
diff --git a/top/blinktree1.tex b/top/blinktree1.tex
new file mode 100644 (file)
index 0000000..8f0eaa1
--- /dev/null
@@ -0,0 +1,13 @@
+\documentclass[tikz]{standalone}
+\usepackage{stmaryrd}
+\usetikzlibrary{arrows.meta,shapes.symbols,matrix,positioning}
+\begin{document}
+\begin{tikzpicture}[node distance=1em]
+       \node (s1) {\verb#>>|.#};
+       \node (d1) [left=of s1.north,yshift=-3em] {\verb#delay 500#};
+       \node (s2) [right=of s1.south,xshift=-3em,yshift=-3em,fill=gray!15,label={[xshift=1em,label distance=-5pt]above:{\tiny interpreter}}] {\verb#writeD D3 st >>=.# $\lambda x\shortrightarrow$};
+       \node (s3) [node distance=-.25em,below=of s2.south,fill=gray!15] {\verb#blink (Not x)#};
+       \draw (s1.south) -- (d1.north);
+       \draw (s1.south) -- ([xshift=-1em]s2.north);
+\end{tikzpicture}
+\end{document}
similarity index 70%
rename from top/blinktree.tex
rename to top/blinktree2.tex
index da5a6f7..202d129 100644 (file)
@@ -3,13 +3,9 @@
 \usetikzlibrary{arrows.meta,shapes.symbols,matrix,positioning}
 \begin{document}
 \begin{tikzpicture}[node distance=1em]
-       \node (s1) {\verb#>>|.#};
-       \node (d1) [left=of s1.north,yshift=-3em] {\verb#delay 500#};
-       \node (s2) [right=of s1.north,yshift=-3em] {\verb#>>=.# $\lambda x\shortrightarrow$};
+       \node (s2) {\verb#>>=.# $\lambda x\shortrightarrow$};
        \node (wd) [left=of s2.north,yshift=-3em] {\verb#writeD D3 st#};
        \node (rec) [right=of s2.north,yshift=-3em,fill=gray!15,label={[xshift=1em,label distance=-5pt]above:{\tiny interpreter}}] {\verb#blink (Not x)#};
-       \draw (s1.south) -- (d1.north);
-       \draw (s1.south) -- (s2.north);
        \draw (s2.south) -- (wd.north);
        \draw (s2.south) -- ([xshift=-1.5em]rec.north);
 %      \draw [->,dashed] ([xshift=-1.5em]rec.north) to [out=25,in=25] (s1.east);
index 2687f61..e86f0b2 100644 (file)
@@ -68,8 +68,7 @@ A deeper sleep mode saves more energy, but also requires more work to restore th
 A processor like the ESP8266 driving the \gls{WEMOS} D1 mini loses the content of its \gls{RAM} in deep sleep mode.
 As a result, after waking up, the program itself is preserved, since it is stored in flash memory, but the program state is lost.
 When there is a program state to be preserved, we must either store it elsewhere, limit us to light sleep, or use a microcontroller that keeps the \gls{RAM} intact during deep sleep.
-\todo[inline]{Na de voorgaande hoofdstukken kun je dit makkelijk expliciet maken voor mtask.
-For mTasks this implies that the mTask OS is preserved during deep sleep, but all shipped tasks and their states will be lost.}
+For mTasks this implies that the \gls{MTASK} \gls{RTS} is preserved during deep sleep, but all shipped tasks and their states are lost.
 
 For edge devices executing a single task, explicit sleeping to save energy can be achieved without too much hassle.
 This becomes much more challenging as soon as multiple independent tasks run on the same device.
@@ -451,12 +450,8 @@ In the current \gls{MTASK} \gls{RTS}, the thresholds are determined by experimen
 On systems that lose the content of their \gls{RAM} it is not possible to go to deep sleep mode.
 
 \section{Interrupts}\label{lst:interrupts}
-\todo[inline]{
-Ik zou hier een klein algemeen verhaal over interrupts schrijven om te zorgen dat de lezer weet waarom dit de moeite van het lezen waard is. B.v.
-An interrupt is a request for the processor to interrupt the currently exected code or its sleep, to handle the event.  It is typically much more energy efficient and accurate when a sensor interrupts the processor to notify that something interresting is happening than when the processor repeatedly checks that sensor's state.
-}
 Most microcontrollers have built-in support for processor interrupts.
-These interrupts are hard-wired signals that interrupts the normal flow of the program in order to execute a small piece of code, the \gls{ISR}.
+These interrupts are hard-wired signals that interrupts the normal flow of the program or sleep state in order to execute a small piece of code, the \gls{ISR}.
 While the \glspl{ISR} look like regular functions, they do come with some limitations.
 For example, they must be very short, in order not to miss future interrupts; can only do very limited \gls{IO}; cannot reliably check the clock; and they operate in their own stack, and thus communication must happen via global variables.
 After the execution of the \gls{ISR}, the normal program flow is resumed.
index 5fc3c22..af54add 100644 (file)
@@ -47,6 +47,8 @@ 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 designed to generate code that runs on resource-constrained edge devices.
+There is no heap avaliable for expressions, only for tasks
 \todo[inline]{Zou je hier niet een prargraafje schrijven over dat dit een beetje speciale compiler is.  Alle type checks worden al door Clean gedaan. Dat is voordat deze compiler ooit uitgevoerd gaat worden. Bovendien kan het Clean programma de te compileren byte code dynamisch maken. Dat staat natuurlijk al eerder een keer, maar je make niet aannemen dat iedereen alles leest (en nu nog weet)}
 \todo[inline]{Dit gaat wel hard de diepte in.  Zou je niet een kort stukje schrijven over hoe je bytecode machine er uit ziet?
        Heap: voor de huidige task tree die herschreven wordt.
@@ -422,7 +424,6 @@ 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}$.
-\todo[inline]{Beter uitleggen?}
 
 \begin{figure}
        \begin{subfigure}{.5\textwidth}
@@ -433,7 +434,7 @@ Then, the right-hand side list of continuations is converted to an expression us
                \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}
 
@@ -636,13 +637,13 @@ There are several possible messages that can be received from the server:
 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.
-\todo[inline]{ik denk dat die rewriter een paar woorden uitleg kan gebruiken.
-The rewriter scans the current task tree and tries to reqrite it. Expressions in the tree are evaluated by the interpreter.\  o.i.d.}
+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 always produces a task tree.\todo[inline]{note dat mtask programmas altijd taken zijn, je kunt niet een niet-taak expressie opsturen naar een device}
+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.
@@ -662,20 +663,29 @@ 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.
-\todo[inline]{Beter uitleggen dat \cleaninline{>>\|.} eigenlijk een step is en dat het natuurlijk eigenlijk twee trees zijn.}
+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 for a blink task in \cref{lst:blink_code} in \gls{MTASK}.}%
        \label{fig:blink_tree}
 \end{figure}
 
@@ -712,7 +722,7 @@ This is possible because there is no sharing or cycles in task trees and nodes c
 
 
 \section{C code generation for communication}\label{sec:ccodegen}
-All communication between the \gls{ITASK} server and the \gls{MTASK} server is type parametrised.
+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.
index 1a4eb01..f2ff46e 100644 (file)
@@ -7,7 +7,7 @@
 
 \begin{document}
 \input{subfileprefix}
-\chapter{Integration of mTask and iTask}%
+\chapter{The integration of mTask and iTask}%
 \label{chp:integration_with_itask}
 \begin{chapterabstract}
        This chapter shows the integration of \gls{MTASK} and \gls{ITASK} by showing:
@@ -32,10 +32,11 @@ The entire system is written as a single \gls{CLEAN} specification where multipl
 Tasks can access \glspl{SDS} according to many-to-many communication and multiple clients can work on the same task.
 The diagram contains three labelled arrows that denote the integration functions between \gls{ITASK} and \gls{MTASK}.
 Devices are connected to the system using the \cleaninline{withDevice} function (see \cref{sec:withdevice}).
+There can be multiple devices connected to a single \gls{ITASK} host at the same time.
 Using \cleaninline{liftmTask}, \gls{MTASK} tasks are lifted to a device (see \cref{sec:liftmtask}).
+It is possible to execute multiple tasks on a single device.
 \glspl{SDS} from \gls{ITASK} are lowered to the \gls{MTASK} device using \cleaninline{lowerSds} (see \cref{sec:liftsds}).
 \todo[inline]{mTask device\textsubscript{n} naar hfstk 5? Uitleg over taken en sensoren en \ldots? evt.\ zelfs naar intro hmmm?}
-\todo[inline]{Benoem dat er meerdere devices kunnen zijn en meerdere tasks op één device, en verwijs naar 6.5}
 
 \begin{figure}
        \centering
@@ -238,7 +239,7 @@ The following section contains an elaborate example using all integration functi
 \newpage
 
 \section{Home automation}
-\todo[inline]{Meer uitleg over de applicatie? ADT ipv strings voor keuze?}
+\todo[inline]{Meer uitleg over de applicatie? lijst ipv strings voor keuze?}
 This section presents an interactive home automation program (\cref{lst:example_home_automation}) to illustrate the integration of the \gls{MTASK} language and the \gls{ITASK} system.
 It consists of a web interface for the user to control which tasks are executed on either one of two connected devices: an \gls{ARDUINO} UNO, connected via a serial port; and an ESP8266 based prototyping board called NodeMCU, connected via \gls{TCP}\slash{}\gls{WIFI}.
 \Crefrange{lst:example:spec1}{lst:example:spec2} show the specification for the devices.
index a248aa5..5b7fddc 100644 (file)
@@ -29,14 +29,10 @@ Furthermore, this particular type of embedding has the property that it is exten
 Adding a language construct is as simple as adding a type class.
 Adding an interpretation is done by creating a new data type and providing implementations for the various type classes.
 
-\todo[inline]{Is dit niet de plek om uit te leggen welke restricties we aan mTask opleggen om het op een edge device te kunnen draaien?
-       1 onderscheid tussen mTask en de rest van het programma
-       2 mTask uit kunnen voeren zonder heap gebruik anders dan de task expressie. Dus: 
-       a geen recursieve data types
-       b geen hogere orde functies
-       c strict evaluation
-       d functies en objecten alleen op topniveau
-Nu lijkt het af en toe dat mTask onnodig primitief is, terwijl we het ook algemener hadden kunnen doen.}
+In order to reduce the hardware requirements for devices running \gls{MTASK} programs, several measures have been taken.
+Programs in \gls{MTASK} are written in the \gls{MTASK} \gls{DSL}, separating them from the host \gls{ITASK} program.
+This allows the tasks to be constructed at compile time in order to tailor-make them for the specific work requirements.
+Furthermore, the \gls{MTASK} language is restricted: there are no recursive data structures, no higher-order functions, strict evaluation, and functions and objects can only be declared at the top level.
 
 \section{Class-based shallow embedding}
 Let us illustrate this technique by taking the very simple language of literal values.
@@ -291,8 +287,7 @@ Splitting out the function definition for each single arity means that for every
 Many of the often used functions are already bundled in the \cleaninline{mtask} class constraint collection.
 The \cleaninline{factorial} functions shows a recursive version of the factorial function.
 The \cleaninline{factorialtail} function is a tail-call optimised version of the factorial function.
-It contains a manually added class constraint.
-\todo[inline]{Uitleggen waarom je dit doet}
+It also illustrates a manually added class constraint, as they are required when functions are used that have signatures not present in the \cleaninline{mtask} class collection.
 Zero-arity functions are always called with unit as an argument.
 An illustration of this is seen in the \cleaninline{zeroarity} expression.
 Finally, \cleaninline{swapTuple} shows an example of a tuple being swapped.
@@ -367,8 +362,9 @@ A task is an expression of the type \cleaninline{TaskValue a} in interpretation
 
 \subsection{Basic tasks}
 The \gls{MTASK} language contains interactive and non-interactive basic tasks.
-As \gls{MTASK} is integrated in \gls{ITASK}, the same notion of stability is applied to the observable task value (see \cref{fig:taskvalue}).
-\todo[inline]{Stability beter uitleggen?}
+As \gls{MTASK} is integrated in \gls{ITASK}, the same notion of stability is applied to the task values.
+Task values have either \emph{no value}, or are \emph{unstable} or \emph{stable} (see \cref{fig:taskvalue}).
+Once a task yields a stable value, it does not change anymore.
 The most rudimentary non-interactive basic tasks in the task language of \gls{MTASK} are \cleaninline{rtrn} and \cleaninline{unstable}.
 They lift the value from the \gls{MTASK} expression language to the task domain either as a stable or unstable value.
 There is also a special type of basic task for delaying execution.
@@ -635,10 +631,10 @@ task =
 \end{lstClean}
 
 \section{Interpretations}
-\todo[inline]{Iets meer uitleg over waarom dit zo handig is}
-This section describes all the interpretations that the \gls{MTASK} language has to offer.
+The nature of the \gls{MTASK} \gls{DSL} embedding allows for multiple interpretations of the terms in the language.
+The \gls{MTASK} language has interpretations to pretty print, simulate, and generate byte code for terms in the language.
+There are many other interpretations possible such as static analyses or optimisation.
 Not all these interpretations are necessarily \gls{TOP} engines, i.e.\ not all the interpretations execute the resulting tasks.
-Some may perform an analysis over the program or typeset the program.
 
 \subsection{Pretty printer}
 The pretty printer interpretation converts an \gls{MTASK} term to a string representation.
@@ -666,7 +662,8 @@ blinkTask =
 \end{lstClean}
 
 \subsection{Simulator}
-The simulator converts the expression to a ready-for-work \gls{ITASK} simulation.
+In a real microprocessor, it is hard to observe the state and to control the sensors in such a way that the behaviour of interest can be observed.
+The simulator converts the expression to a ready-for-work \gls{ITASK} simulation to bridge this gap.
 There is one entry point for this interpretation (see \cref{lst:simulatemain}).
 The task resulting from the \cleaninline{simulate} function presents the user with an interactive simulation environment (see \cref{fig:sim}).
 The simulation allows the user to (partially) execute tasks, control the simulated peripherals, inspect the internal state of the tasks, and interact with \glspl{SDS}.
index 242b2a0..d6bb86c 100644 (file)
@@ -62,10 +62,10 @@ blink d =
                >>|. delay (lit d)
                >>|. bl (Not st))
        In {main=bl true}
-lightswitch :: (Shared sds Bool) -> Main (MTask v ()) | liftsds, mtask v & RWShared sds & TC (sds () Bool Bool)
+lightswitch :: (Shared sds Bool) -> Main (MTask v ()) | lowerSds, mtask v & RWShared sds & TC (sds () Bool Bool)
 lightswitch sh =
        declarePin D13 PMOutput \d13->
-       liftsds \ls=sh
+       lowerSds \ls=sh
        In fun \f=(\st->
                     getSds ls
                >>*. [IfValue ((!=.)st) (\v->writeD d13 v)]
index ebd8e50..7af0449 100644 (file)
                          ,{"name":"base-stdenv"
                           ,"version":"1.0.0"}
                          ,{"name":"clean-platform"
-                          ,"version":"0.3.4"}
+                          ,"version":"0.3.22"}
                          ,{"name":"gast"
-                          ,"version":"0.2.1"}
+                          ,"version":"0.2.3"}
                          ,{"name":"gentype"
                           ,"version":"1.1.0"}
                          ,{"name":"graph-copy"
                           ,"version":"2.0.1"}
                          ,{"name":"itasks"
-                          ,"version":"0.2.0"}
+                          ,"version":"0.2.12"}
                          ,{"name":"itasks-mqttclient"
                           ,"version":"1.0.2"}
                          ,{"name":"itasks-serial"
                           ,"version":"0.1.0"}
-                         ,{"name":"lib-compiler-itasks"
-                          ,"version":"2.0.1"}
+                         ,{"name":"lib-compiler"
+                          ,"version":"3.0.2"}
                          ,{"name":"mtask-server"
-                          ,"version":"0.1.0"}
+                          ,"version":"0.1.2"}
                          ,{"name":"serial"
-                          ,"version":"0.1.1"}
+                          ,"version":"0.1.2"}
                          ,{"name":"tcpip"
-                          ,"version":"2.0.1"}]}}
\ No newline at end of file
+                          ,"version":"2.0.1"}]}}