From: Mart Lubbers Date: Thu, 2 Mar 2023 08:18:38 +0000 (+0100) Subject: process the rest of Pieter's comments X-Git-Url: https://git.martlubbers.net/?a=commitdiff_plain;h=26745fe928b2c2d7bb4b6642107e0cd498f08ef7;p=phd-thesis.git process the rest of Pieter's comments --- diff --git a/dsl/class.tex b/dsl/class.tex index 9490d19..bc8dff9 100644 --- a/dsl/class.tex +++ b/dsl/class.tex @@ -58,7 +58,7 @@ with Class'': TFP 2022.\ DANS.\ \url{https://doi.org/10.5281/zenodo.5081386}.} \section{Deep embedding} Pick a \gls{DSL}, any \gls{DSL}, pick the language of literal integers and addition. In deep embedding, terms in the language are represented by data in the host language. -Hence, defining the constructs is as simple as creating the following algebraic data type\footnote{All data types and functions are subscripted to indicate the evolution.}. +Hence, defining the constructs is as simple as creating the following algebraic data type\footnote{All data types and functions are subscripted to indicate the evolution. When definitions are omitted for version $n$, version $n-1$ is assumed.}. \begin{lstHaskellLhstex} data Expr_0 @@ -553,7 +553,7 @@ e3 = neg_4 (Lit_4 42 `sub_4` Lit_4 38) `Add_4` Lit_4 1 Leveraging \glspl{GADT}, deeply embedded \glspl{DSL} can be made statically type safe even when different value types are supported. Even when \glspl{GADT} are not supported natively in the language, they can be simulated using embedding-projection pairs or equivalence types \citep[\citesection{2.2}]{cheney_lightweight_2002}. Where some solutions to the expression problem do not easily generalise to \glspl{GADT} (see \cref{sec:cde:related}), classy deep embedding does. -Generalising the data structure of our \gls{DSL} is fairly straightforward and to spice things up a bit, we add an equality and boolean not language construct. +Generalising the data structure of our \gls{DSL} is fairly straightforward and to spice things up a bit, we add an equality and boolean negation language construct. To make the existing \gls{DSL} constructs more general, we relax the types of those constructors. For example, operations on integers now work on all numerals instead. Moreover, the \haskelllhstexinline{Lit_g} constructor can be used to lift values of any type to the \gls{DSL} domain as long as they have a \haskelllhstexinline{Show} instance, required for the printer. @@ -710,10 +710,10 @@ For example, hybrid embedding requires a transcoding step between the deep synta & \CIRCLE{}\tnote{3}\\ Simple type system & \CIRCLE{} & \CIRCLE{} & \Circle{} & \CIRCLE{} & \CIRCLE{} & \Circle{} - & \LEFTcircle{}\tnote{4}\\ + & \RIGHTcircle{}\tnote{4}\\ Little boilerplate & \CIRCLE{} & \CIRCLE{} & \Circle{} & \CIRCLE{} & \CIRCLE{} & \Circle{} - & \LEFTcircle{}\tnote{4}\\ + & \RIGHTcircle{}\tnote{4}\\ \bottomrule \end{tabular} \begin{tablenotes} diff --git a/dsl/first.tex b/dsl/first.tex index d6e7298..4170a6f 100644 --- a/dsl/first.tex +++ b/dsl/first.tex @@ -589,7 +589,7 @@ unCk d f ) \end{lstHaskell} -The implementation for this is a little elaborate and it heavily uses the \haskellinline{pl} function, a helper function that translates a string literal \haskellinline{s} to \haskellinline{[|printLit \$(lift s)|]}, i.e.\ it lifts the \haskellinline{printLit} function to the \gls{TH} domain. +The implementation for this is a little elaborate and it heavily uses the \haskellinline{pl} function, a helper function that translates a string literal \haskellinline{s} to \haskellinline{[\|printLit \$(lift s)\|]}, i.e.\ it lifts the \haskellinline{printLit} function to the \gls{TH} domain. \begin{lstHaskell} mkDeconstructor :: Name -> [VarBangType] -> Q Dec diff --git a/intro/intro.tex b/intro/intro.tex index 5977fde..6be118d 100644 --- a/intro/intro.tex +++ b/intro/intro.tex @@ -17,6 +17,7 @@ \end{itemize} \end{chapterabstract} +\todo[inline]{Brackets upright in listings?} This dissertation is about orchestrating \gls{IOT} systems harmlessly and efficiently. \todo{beter?} There are at least 13.4 billion devices connected to the internet at the time of writing \citep{transforma_insights_current_2023}. @@ -354,7 +355,7 @@ This task first defines \gls{GPIO} pin 13 to be of the output type (\cref{lst:in Then the \gls{ITASK} \gls{SDS} is lifted to an \gls{MTASK} \gls{SDS} (\cref{lst:intro:liftsds}), enabling the machinery to keep the \gls{SDS} in sync both on the device and the server. The main expression of the program calls the \cleaninline{blink} function with an initial state. This function on \crefrange{lst:intro:blink_fro}{lst:intro:blink_to} first reads the interval \gls{SDS}, waits the specified delay, writes the state to the \gls{GPIO} pin, and calls itself recursively using the inverse of the state in order to run continuously. -The \cleaninline{>>|.} operator denotes the sequencing of tasks in \gls{MTASK}. +The \cleaninline{>>\|.} operator denotes the sequencing of tasks in \gls{MTASK}. \cleaninputlisting[float={!ht},linerange={23-,25-33},numbers=left,caption={The \gls{MTASK} code for the interactive blinking application.},label={lst:intro_blink_mtask}]{lst/blink.icl} %chktex 8 \todo[inline]{Meer wit rondom =jes, doornummeren?} diff --git a/top/4iot.tex b/top/4iot.tex index 435a8c5..3bdaf18 100644 --- a/top/4iot.tex +++ b/top/4iot.tex @@ -20,10 +20,11 @@ The edge layer of \gls{IOT} systems predominantly consists of microcontrollers. Microcontrollers are tiny computers designed specifically for embedded applications. -They differ significantly from regular computers in many aspects, and as a consequence, development for microcontrollers differs also. +They differ significantly from regular computers in many aspects. For example, they are much smaller; only have a fraction of the memory and processor speed; and run on different architectures. Furthermore, they have much more energy-efficient sleep modes, and support connecting and interfacing with peripherals such as sensors and actuators. To illustrate the difference in characteristics, \cref{tbl:mcu_laptop} compares the hardware properties of a typical laptop with two popular microcontrollers. +As a consequence of these differences, development for microcontrollers is also unlike development for traditional computers. Usually, programming microcontrollers requires an elaborate multistep toolchain of compilation, linkage, binary image creation, and burning this image onto the flash memory of the microcontroller in order to run a program. The software is usually a cyclic executive instead of tasks that run in an \gls{OS}. Hence, all tasks must be manually combined into a single program. @@ -63,7 +64,8 @@ An example of a \gls{TOP} system is \gls{ITASK}, a general-purpose \gls{TOP} lan Such web applications often form the core of the topmost two layers of \gls{IOT} applications: the presentation and application layer. Furthermore, \gls{IOT} edge devices are typically programmed with similar workflow-like programs for which \gls{TOP} is very suitable. Directly incorporating the perception layer, and thus edge devices, in \gls{ITASK} however is not straightforward. -The \gls{ITASK} system is targetting relatively fast and hence energy-hungry systems with large amounts of \gls{RAM} and a speedy connection. +All \gls{ITASK} applications carry the weigth of multi-user \gls{TOP} programs that can generically generate webpages, communication, and storage for all data types in the program. +As a result, the \gls{ITASK} system targetting relatively fast and hence energy-hungry systems with large amounts of \gls{RAM} and a speedy connection. Edge devices in \gls{IOT} systems are typically slow but energy efficient and do not have the memory to run the naturally heap-heavy feature-packed functional programs that \gls{ITASK} programs are. The \gls{MTASK} system bridges this gap by providing a domain-specific \gls{TOP} language for \gls{IOT} edge devices. Domain-specific knowledge is embedded in the language and execution platform and unnecessary features for edge devices are removed to drastically lower the hardware requirements. @@ -106,7 +108,7 @@ The task is not the single cyclic executive and therefore consists of just a mai The task resulting from the main expression is continuously executed by the \gls{RTS}. To simulate a loop, the \cleaninline{rpeat} task combinator is used as this task combinator executes the argument task and, when stable, reinstates it. The body of the \cleaninline{rpeat} task contains a task that writes to the pins and waits in between. -The tasks are connected using the sequential \cleaninline{>>|.} combinator that for all current intents and purposes executes the tasks after each other. +The tasks are connected using the sequential \cleaninline{>>\|.} combinator that for all current intents and purposes executes the tasks after each other. \begin{lstClean}[caption={Blinking the \gls{LED} using the \cleaninline{rpeat} combinator.},label={lst:blinkImp}] blinkTask :: Main (MTask v ()) | mtask v @@ -122,7 +124,7 @@ blinkTask = declarePin D2 PMOutput \ledPin-> The \gls{MTASK} \gls{DSL} is hosted in a full-fledged \gls{FP} language. It is therefore also possible to define the blinking behaviour as a function. \Cref{lst:blinkFun} shows this more natural translation. -The \cleaninline{main} expression is a call to the \cleaninline{blink} function parametrised with the state. +The \cleaninline{main} expression is a call to the \cleaninline{blink} \gls{MTASK} function parametrised with the state. The \cleaninline{blink} function first writes the current state to the \gls{LED}, waits for the specific time, and calls itself recursively with the inverse of the state, resulting in the blinking behaviour. Creating recursive functions like this is not possible in the \gls{ARDUINO} language because the program would run out of stack quickly and combining multiple tasks defined like this would be very difficult. @@ -193,18 +195,19 @@ In between these rewrite steps, other tasks are be executed and communication is Consequently, and in contrast to \gls{ARDUINO}, the \cleaninline{delay} task in \gls{MTASK} does not block the execution. It has no observable value until the target waiting time has passed, and is thence \emph{stable}. As there is no global state, the function is parametrised with the current status, the pin to blink and the waiting time. -With a parallel combinator, tasks are executed at the same time. +With a parallel combinator, tasks are executed seamingly at the same time, i.e.\ their very short small-step reduction steps are interleaved. Therefore, blinking three different blinking patterns is as simple as combining the three calls to the \cleaninline{blink} function with their arguments as seen in \cref{lst:blinkthreadmtask}. % VimTeX: SynIgnore on \begin{lstClean}[label={lst:blinkthreadmtask},caption={Threading three blinking patterns.}] blinktask :: MTask v () | mtask v -blinktask = declarePin D1 PMOutput \d1-> +blinktask = + declarePin D1 PMOutput \d1-> declarePin D2 PMOutput \d2-> declarePin D3 PMOutput \d3-> fun \blink=(\(st, pin, wait)-> delay wait - >>|. writeD d13 st + >>|. writeD pin st >>|. blink (Not st, pin, wait)) In {main = blink (true, d1, lit 500) .||. blink (true, d2, lit 300) @@ -214,7 +217,15 @@ blinktask = declarePin D1 PMOutput \d1-> % 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?} 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. @@ -227,7 +238,7 @@ This makes it easy to create interactive applications modelling collaboration be } 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}. +First, the language setup and interface are shown in \cref{chp:mtask_dsl}. \Cref{chp:integration_with_itask} shows the integration of \gls{MTASK} and \gls{ITASK}. Then, \cref{chp:implementation} provides the implementation of the \gls{DSL}, the compilation schemes, instruction set, and details on the interpreter. \Cref{chp:green_computing_mtask} explains all green computing aspects of \gls{MTASK}, i.e.\ task scheduling and processor interrupts. diff --git a/top/finale.tex b/top/finale.tex index 7d90b58..ffbd9f4 100644 --- a/top/finale.tex +++ b/top/finale.tex @@ -204,7 +204,7 @@ In \gls{MTASK}, all work expressed by tasks is already split up in atomic pieces Furthermore, creating checkpoints should be fairly straightforward as \gls{MTASK} tasks do not rely on any global state---all information required to execute a task is stored in the task tree. It is interesting to see what \gls{TOP} abstraction are useful for intermittent computing and what solutions are required to make this work. -Mesh networks allow for communication not only to-and-fro the device and server but also between devices. +Mesh networks allow for communication not only to and fro the device and server but also between devices. The \gls{ITASK} system already contains primitives for distributed operation. For example, it is possible to run tasks or share data with \glspl{SDS} on different machines. It is interesting to investigate how this networking technique can be utilised in \gls{MTASK}. diff --git a/top/imp.tex b/top/imp.tex index f95d69a..ce38d1d 100644 --- a/top/imp.tex +++ b/top/imp.tex @@ -14,7 +14,7 @@ \item showing the compilation and execution toolchain; \item showing the implementation of the byte code compiler for the \gls{MTASK} language; \item elaborating on the implementation and architecture of the \gls{RTS} of \gls{MTASK}; - \item and explaining the machinery used to automatically serialise and deserialise data to-and-fro the device. + \item and explaining the machinery used to automatically serialise and deserialise data to and fro the device. \end{itemize} \end{chapterabstract} diff --git a/top/lang.tex b/top/lang.tex index 7751832..a248aa5 100644 --- a/top/lang.tex +++ b/top/lang.tex @@ -26,7 +26,17 @@ This means that the language interface, i.e.\ the language constructs, are a col Interpretations of this interface are data types implementing these classes. Due to the nature of this embedding technique, it is possible to have multiple interpretations for programs written in the \gls{MTASK} language. Furthermore, this particular type of embedding has the property that it is extensible both in language constructs and in interpretations. -Adding a language construct is as simple as adding a type class and adding an interpretation is done by creating a new data type and providing implementations for the various type classes. +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.} \section{Class-based shallow embedding} Let us illustrate this technique by taking the very simple language of literal values. @@ -124,7 +134,7 @@ class basicType t | type t where ... The \gls{MTASK} language interface consists of a core collection of type classes bundled in the type class \cleaninline{class mtask} (see \cref{lst:collection}). Every interpretation of \gls{MTASK} terms implements the type classes in the \cleaninline{mtask} class collection. -Optional \gls{MTASK} constructs such as peripherals or lowered \gls{ITASK} \glspl{SDS} are not included in this class collection because not all devices or interpretations support this. +%Optional \gls{MTASK} constructs such as peripherals or lowered \gls{ITASK} \glspl{SDS} are not included in this class collection because not all devices or interpretations support this. \begin{lstClean}[caption={Class collection for the \gls{MTASK} language.},label={lst:collection}] class mtask v | expr, ..., int, real, long v @@ -190,7 +200,7 @@ class expr v where If :: (v Bool) (v t) (v t) -> v t | type t \end{lstClean} -Conversion to-and-fro data types is available through the overloaded functions \cleaninline{int}, \cleaninline{long} and \cleaninline{real}. +Conversion to and fro data types is available through the overloaded functions \cleaninline{int}, \cleaninline{long} and \cleaninline{real}. These functions convert the argument to the respective type similar to casting in \gls{C}. For most interpretations, there are instances of these classes for all numeric types. @@ -227,12 +237,10 @@ It performs a simple approximate equality---admittedly not taking into account a When calling \cleaninline{approxEqual} in an \gls{MTASK} expression, the resulting code is inlined. \begin{lstClean}[label={lst:example_macro},caption={Approximate equality as an example of linguistic reuse in \gls{MTASK}.}] -approxEqual :: (v Real) (v Real) (v Real) -> v Real | expr v -approxEqual x y eps = If (x ==. y) true - ( If (x >. y) - (x -. y <. eps) - (y -. x <. eps) - ) +approxEqual :: (v Real) (v Real) (v Real) -> v Bool | expr v +approxEqual x y eps = x ==. y |. If (x >. y) + (x -. y <. eps) + (y -. x <. eps) \end{lstClean} \subsection{Data types} @@ -277,13 +285,14 @@ instance fun (Show a, Show b, Show c) Show | type a, ... where ... ... \end{lstClean} -Deriving how to define and use functions from the type is quite the challenge even though the resulting syntax is made easier using the infix type \cleaninline{In}. +Deriving how to define and use functions from the type is quite a challenge even though the resulting syntax is made easier using the infix type \cleaninline{In}. \Cref{lst:function_examples} show some examples of functions to illustrate the syntax. Splitting out the function definition for each single arity means that for every function arity and combination of arguments, a separate class constraint must be created. 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} 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. @@ -358,6 +367,8 @@ 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?} 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. @@ -538,7 +549,7 @@ dis :: (TaskValue a) (TaskValue a) dis NoValue r = r dis l NoValue = l dis (Value l ls) (Value r rs) - | rs = Value r True + | rs && not ls = Value r rs | otherwise = Value l ls \end{lstClean} \end{subfigure} @@ -553,7 +564,7 @@ task :: MTask v Bool task = declarePin D0 PMInput \d0-> declarePin D1 PMInput \d1-> - let monitor pin = readD pin >>*. [IfValue (\x->x) \x->rtrn x] + let monitor pin = readD pin >>*. [IfValue id rtrn] In {main = monitor d0 .||. monitor d1} \end{lstClean} @@ -611,12 +622,13 @@ Using a sequence of \cleaninline{getSds} and \cleaninline{setSds} would be unsaf \begin{lstClean}[label={lst:mtask_sds_examples},caption={Examples with \glspl{SDS} in \gls{MTASK}.}] task :: MTask v Int | mtask v -task = declarePin D3 PMInput \d3-> +task = + declarePin D3 PMInput \d3-> declarePin D5 PMInput \d5-> sds \share=0 In fun \count=(\pin-> readD pin - >>* [IfValue (\x->x) (\_->updSds (\x->x +. lit 1) share)] + >>* [IfValue id (\_->updSds (\x->x +. lit 1) share)] >>| delay (lit 100) // debounce >>| count pin) In {main=count d3 .||. count d5} @@ -672,15 +684,15 @@ simulate :: (Main (TraceTask a)) -> [String] \subsection{Byte code compiler} The main interpretation of the \gls{MTASK} system is the byte code compiler (\cleaninline{:: BCInterpret a}). +This interpretation compiles the \gls{MTASK} term at run time to byte code. With it, and a handful of integration functions, \gls{MTASK} tasks can be executed on microcontrollers and integrated in \gls{ITASK} as if they were regular \gls{ITASK} tasks. Furthermore, with a special language construct, \glspl{SDS} can be shared between \gls{MTASK} and \gls{ITASK} programs as well. The integration with \gls{ITASK} is explained thoroughly later in \cref{chp:integration_with_itask}. The \gls{MTASK} language together with \gls{ITASK} is a heterogeneous \gls{DSL}. I.e.\ some components---for example the \gls{RTS} on the microcontroller that executes the tasks---is largely unaware of the other components in the system, and it is executed on a completely different architecture. -The \gls{MTASK} language is based on a simply-typed $\lambda$-calculus with support for some basic types, arithmetic operations, and function definitions. -As the language is a \gls{TOP} language, it is also enriched with a task language (see \cref{sec:top}). -\todo[inline]{Duidelijker maken dat het at compile time gebeurt en niet at run time.} +The \gls{MTASK} language is a \gls{TOP} language with basic tasks tailored for \gls{IOT} edge devices (see \cref{sec:top}). +It uses expressions based a simply-typed $\lambda$-calculus with support for some basic types, arithmetic operations, and function definitions. \section{Conclusion} This chapter gave an overview of the complete \gls{MTASK} \gls{DSL}. @@ -689,9 +701,8 @@ The language is implemented as a class-based shallowly \gls{EDSL} in the pure fu The language is an enriched lambda calculus as a host language. It provides language constructs for arithmetic expressions, conditionals, functions, but also non-interactive basic tasks, task combinators, peripheral support, and integration with \gls{ITASK}. Terms in the language are just interfaces and can be interpreted by one or more interpretations. -\todo[inline]{Which can be used to\ldots} -The most important interpretation of the language is the byte code compiler. -\todo[inline]{That compiles the terms to byte code at compiletime and not run time} +When using the byte code compiler, terms in the \gls{MTASK} language are type checked at compile time but are constructed and compiled at run time. +This facilitates tailor-making tasks for the current work requirements. \input{subfilepostamble} \end{document}