top/mtask.tex

   1 \documentclass[../thesis.tex]{subfiles}
   2
   3 \begin{document}
   4 \ifSubfilesClassLoaded{
   5         \pagenumbering{arabic}
   6 }{}
   7
   8 \chapter{Introduction to \texorpdfstring{\gls{IOT}}{IoT} programming}%
   9 \label{chp:top4iot}
  10 \todo{betere chapter naam}
  11 \begin{chapterabstract}
  12         This chapter introduces \gls{MTASK} and puts it into perspective compared to traditional microprocessor programming.
  13 \end{chapterabstract}
  14
  15 Traditionally, the first program that one writes when trying a new language is the so called \emph{Hello World!} program.
  16 This program has the single task of printing the text \emph{Hello World!} to the screen and exiting again, useful to become familiarised with the syntax and verify that the toolchain and runtime environment is working.
  17 On microprocessors, there often is no screen for displaying text.
  18 Nevertheless, almost always there is a monochrome $1\times1$ pixel screen, namely an---often builtin---\gls{LED}.
  19 The \emph{Hello World!} equivalent on microprocessors blinks this \gls{LED}.
  20
  21 \Cref{lst:arduinoBlink} shows how the logic of a blink program might look when using \gls{ARDUINO}'s \gls{CPP} dialect.
  22 Every \gls{ARDUINO} program contains a \arduinoinline{setup} and a \arduinoinline{loop} function.
  23 The \arduinoinline{setup} function is executed only once on boot, the \arduinoinline{loop} function is continuously called afterwards and contains the event loop.
  24 After setting the \gls{GPIO} pin to the correct mode, blink's \arduinoinline{loop} function alternates the state of the pin representing the \gls{LED} between \arduinoinline{HIGH} and \arduinoinline{LOW}, turning the \gls{LED} off and on respectively.
  25 In between it waits for 500 milliseconds so that the blinking is actually visible for the human eye.
  26 Compiling this results in a binary firmware that needs to be flashed onto the program memory.
  27
  28 Translating the traditional blink program to \gls{MTASK} can almost be done by simply substituting some syntax as seen in \cref{lst:blinkImp}.
  29 E.g.\ \arduinoinline{digitalWrite} becomes \cleaninline{writeD}, literals are prefixed with \cleaninline{lit} and the pin to blink is changed to represent the actual pin for the builtin \gls{LED} of the device used in the exercises.
  30 In contrast to the imperative \gls{CPP} dialect, \gls{MTASK} is a \gls{TOP} language and therefore there is no such thing as a loop, only task combinators to combine tasks.
  31 To simulate a loop, the \cleaninline{rpeat} task can be used, this task executes the argument task and, when stable, reinstates it.
  32 The body of the \cleaninline{rpeat} contains similarly named tasks to write to the pins and to wait in between.
  33 The tasks are connected using the sequential \cleaninline{>>|.} combinator that for all current intents and purposes executes the tasks after each other.
  34
  35 \begin{figure}[ht]
  36         \begin{subfigure}[b]{.5\linewidth}
  37                 \begin{lstArduino}[caption={Blink program.},label={lst:arduinoBlink}]
  38 void setup() {
  39         pinMode(D2, OUTPUT);
  40 }
  41
  42 void loop() {
  43         digitalWrite(D2, HIGH);
  44         delay(500);
  45         digitalWrite(D2, LOW);
  46         delay(500);
  47 }\end{lstArduino}
  48         \end{subfigure}%
  49         \begin{subfigure}[b]{.5\linewidth}
  50                 \begin{lstClean}[caption={Blink program.},label={lst:blinkImp}]
  51 blink :: Main (MTask v ()) | mtask v
  52 blink =
  53         declarePin D2 PMOutput \d2->
  54         {main = rpeat (
  55                      writeD d2 true
  56                 >>|. delay (lit 500)
  57                 >>|. writeD d2 false
  58                 >>|. delay (lit 500)
  59         )}\end{lstClean}
  60         \end{subfigure}
  61 \end{figure}
  62
  63 \section{Threaded blinking}
  64 Now say that we want to blink multiple blinking patterns on different \glspl{LED} concurrently.
  65 For example, blink three \glspl{LED} connected to \gls{GPIO} pins $1,2$ and $3$ at intervals of $500,300$ and $800$ milliseconds.
  66 Intuitively you want to lift the blinking behaviour to a function and call this function three times with different parameters as done in \cref{lst:blinkthreadno}
  67
  68 \begin{lstArduino}[caption={Naive approach to multiple blinking patterns.},label={lst:blinkthreadno}]
  69 void setup () { ... }
  70
  71 void blink (int pin, int wait) {
  72         digitalWrite(pin, HIGH);
  73         delay(wait);
  74         digitalWrite(pin, LOW);
  75         delay(wait);
  76 }
  77
  78 void loop() {
  79         blink (D1, 500);
  80         blink (D2, 300);
  81         blink (D3, 800);
  82 }\end{lstArduino}
  83
  84 Unfortunately, this does not work because the \arduinoinline{delay} function blocks all further execution.
  85 The resulting program will blink the \glspl{LED} after each other instead of at the same time.
  86 To overcome this, it is necessary to slice up the blinking behaviour in very small fragments so it can be manually interleaved~\citep{feijs_multi-tasking_2013}.
  87 Listing~\ref{lst:blinkthread} shows how three different blinking patterns might be achieved in \gls{ARDUINO} using the slicing method.
  88 If we want the blink function to be a separate parametrizable function we need to explicitly provide all references to the required state.
  89 Furthermore, the \arduinoinline{delay} function can not be used and polling \arduinoinline{millis} is required.
  90 The \arduinoinline{millis} function returns the number of milliseconds that have passed since the boot of the microprocessor.
  91 Some devices use very little energy when in \arduinoinline{delay} or sleep state.
  92 Resulting in \arduinoinline{millis} potentially affects power consumption since the processor is basically busy looping all the time.
  93 In the simple case of blinking three \glspl{LED} on fixed intervals, it might be possible to calculate the delays in advance using static analysis and generate the appropriate \arduinoinline{delay} code.
  94 Unfortunately, this is very hard when for example the blinking patterns are determined at runtime.
  95
  96 \begin{lstArduino}[label={lst:blinkthread},caption={Threading three blinking patterns.}]
  97 long led1 = 0, led2 = 0, led3 = 0;
  98 bool st1 = false, st2 = false, st3 = false;
  99
 100 void blink(int pin, int dlay, long *lastrun, bool *st) {
 101         if (millis() - *lastrun > dlay) {
 102                 digitalWrite(pin, *st = !*st);
 103                 *lastrun += dlay;
 104         }
 105 }
 106
 107 void loop() {
 108         blink(D1, 500, &led1, &st1);
 109         blink(D2, 300, &led2, &st1);
 110         blink(D3, 800, &led3, &st1);
 111 }\end{lstArduino}
 112
 113 This method is very error prone, requires a lot of pointer juggling and generally results into spaghetti code.
 114 Furthermore, it is very difficult to represent dependencies between threads, often state machines have to be explicitly programmed by hand to achieve this.
 115
 116 \section{Blinking in \texorpdfstring{\gls{MTASK}}{mTask}}
 117 The \cleaninline{delay} \emph{task} does not block the execution but \emph{just} emits no value when the target waiting time has not yet passed and emits a stable value when the time is met.
 118 In contrast, the \arduinoinline{delay()} \emph{function} on the \gls{ARDUINO} is blocking which prohibits interleaving.
 119 To make code reuse possible and make the implementation more intuitive, the blinking behaviour is lifted to a recursive function instead of using the imperative \cleaninline{rpeat} construct.
 120 The function is parametrized with the current state, the pin to blink and the waiting time.
 121 Creating recursive functions like this is not possible in the \gls{ARDUINO} language because the program would run out of stack in an instant and nothing can be interleaved.
 122 With a parallel combinator, tasks can be executed in an interleaved fashion.
 123 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}.
 124
 125 % VimTeX: SynIgnore on
 126 \begin{lstClean}[label={lst:blinkthreadmtask},caption={Threaded blinking.}]
 127 blinktask :: MTask v () | mtask v
 128 blinktask =
 129         declarePin D1 PMOutput \d1->
 130         declarePin D2 PMOutput \d2->
 131         declarePin D3 PMOutput \d3->
 132         fun \blink=(\(st, pin, wait)->
 133                      delay wait
 134                 >>|. writeD d13 st
 135                 >>|. blink (Not st, pin, wait)) In
 136         {main =  blink (true, d1, lit 500)
 137                 .||. blink (true, d2, lit 300)
 138                 .||. blink (true, d3, lit 800)
 139         }\end{lstClean}
 140 % VimTeX: SynIgnore off
 141
 142 \chapter{The \texorpdfstring{\gls{MTASK}}{mTask} \texorpdfstring{\gls{DSL}}{DSL}}%
 143 \label{chp:mtask_dsl}
 144 \begin{chapterabstract}
 145 This chapter serves as a complete guide to the \gls{MTASK} language, from an \gls{MTASK} programmer's perspective.
 146 \end{chapterabstract}
 147
 148 The \gls{MTASK} system is a \gls{TOP} programming environment for programming microprocessors.
 149 It is implemented as an \gls{EDSL} in \gls{CLEAN} using class-based---or tagless-final---embedding (See \cref{ssec:tagless}).
 150 Due to the nature of the embedding technique, it is possible to have multiple interpretations of---or views on---programs written in the \gls{MTASK} language.
 151 The following interpretations are available for \gls{MTASK}.
 152
 153 \begin{itemize}
 154         \item Pretty printer
 155
 156                 This interpretation converts the expression to a string representation.
 157         \item Simulator
 158
 159                 The simulator converts the expression to a ready-for-work \gls{ITASK} simulation in which the user can inspect and control the simulated peripherals and see the internal state of the tasks.
 160         \item Compiler
 161
 162                 The compiler compiles the \gls{MTASK} program at runtime to a specialised bytecode.
 163                 Using a handful of integration functions and tasks, \gls{MTASK} tasks can be executed on microprocessors and integrated in \gls{ITASK} as if they were regular \gls{ITASK} tasks.
 164                 Furthermore, with special language constructs, \glspl{SDS} can be shared between \gls{MTASK} and \gls{ITASK} programs.
 165 \end{itemize}
 166
 167 When using the compiler interpretation in conjunction with the \gls{ITASK} integration, \gls{MTASK} is a heterogeneous \gls{DSL}.
 168 I.e.\ some components---e.g.\ the \gls{RTS} on the microprocessor---is largely unaware of the other components in the system.
 169 Furthermore, it is executed on a completely different architecture.
 170 The \gls{MTASK} language consists of a host language---a simply-typed $\lambda$-calculua with support for some basic types, function definition and data types (see \cref{sec:expressions})---enriched with a task language (see \cref{sec:top}).
 171
 172 \section{Types}
 173 To leverage the type checker of the host language, types in the \gls{MTASK} language are expressed as types in the host language, to make the language type safe.
 174 However, not all types in the host language are suitable for microprocessors that may only have \qty{2}{\kibi\byte} of \gls{RAM} so class constraints are therefore added to the \gls{DSL} functions.
 175 The most used class constraint is the \cleaninline{type} class collection containing functions for serialization, printing, \gls{ITASK} constraints etc.
 176 Many of these functions can be derived using generic programming.
 177 An even stronger restriction on types is defined for types that have a stack representation.
 178 This \cleaninline{basicType} class has instances for many \gls{CLEAN} basic types such as \cleaninline{Int}, \cleaninline{Real} and \cleaninline{Bool}.
 179 The class constraints for values in \gls{MTASK} are omnipresent in all functions and therefore often omitted throughout throughout the chapters for brevity and clarity.
 180
 181 \begin{table}[ht]
 182         \centering
 183         \begin{tabular}{lll}
 184                 \toprule
 185                 \gls{CLEAN}/\gls{MTASK} & \gls{CPP} type & \textnumero{}bits\\
 186                 \midrule
 187                 \cleaninline{Bool}             & \cinline{bool}    & 16\\
 188                 \cleaninline{Char}             & \cinline{char}    & 16\\
 189                 \cleaninline{Int}              & \cinline{int16_t} & 16\\
 190                 \cleaninline{:: Long}          & \cinline{int32_t} & 32\\
 191                 \cleaninline{Real}             & \cinline{float}   & 32\\
 192                 \cleaninline{:: T = A \| B \| C} & \cinline{enum}    & 16\\
 193                 \bottomrule
 194         \end{tabular}
 195         \caption{Mapping from \gls{CLEAN}/\gls{MTASK} data types to \gls{CPP} datatypes.}%
 196         \label{tbl:mtask-c-datatypes}
 197 \end{table}
 198
 199 The \gls{MTASK} language consists of a core collection of type classes bundled in the type class \cleaninline{class mtask}.
 200 Every interpretation implements the type classes in the \cleaninline{mtask} class
 201 There are also \gls{MTASK} extensions that not every interpretation implements such as peripherals and integration with \gls{ITASK}.
 202
 203 \Cref{lst:constraints} contains the definitions for the type constraints and shows some example type signatures for typical \gls{MTASK} expressions and tasks.
 204 \todo{uitleggen}
 205
 206 \begin{lstClean}[caption={Classes and class collections for the \gls{MTASK} language.},label={lst:constraints}]
 207 :: Main a = { main :: a }
 208 :: In a b = (In) infix 0 a b
 209
 210 class type t | iTask, ... ,fromByteCode, toByteCode t
 211 class basicType t | type t where ...
 212
 213 class mtask v | expr, ..., int, real, long v
 214
 215 someExpr :: v Int | mtask v
 216 someExpr = ...
 217
 218 someTask :: MTask v Int | mtask v
 219 someTask =
 220         sensor1 config1 \sns1->
 221         sensor2 config2 \sns2->
 222            fun \fun1= ( ... )
 223         In fun \fun2= ( ... )
 224         In {main=mainexpr}
 225 \end{lstClean}
 226
 227 \section{Expressions}\label{sec:expressions}
 228 \Cref{lst:expressions} shows the \cleaninline{expr} class containing the functionality to lift values from the host language to the \gls{MTASK} language (\cleaninline{lit}); perform number and boolean arithmetics; do comparisons; and conditional execution.
 229 For every common arithmetic operator in the host language, an \gls{MTASK} variant is present, suffixed by a period to not clash with \gls{CLEAN}'s builtin operators.
 230
 231 \begin{lstClean}[caption={The \gls{MTASK} class for expressions},label={lst:expressions}]
 232 class expr v where
 233         lit :: t -> v t | type t
 234         (+.) infixl 6 :: (v t) (v t) -> v t | basicType, +, zero t
 235         ...
 236         (&.) infixr 3 :: (v Bool) (v Bool) -> v Bool
 237         (|.) infixr 2 :: (v Bool) (v Bool) -> v Bool
 238         Not           :: (v Bool) -> v Bool
 239         (==.) infix 4 :: (v a) (v a) -> v Bool | Eq, basicType a
 240         ...
 241         If :: (v Bool) (v t) (v t) -> v t | type t
 242 \end{lstClean}
 243
 244 Conversion to-and-fro data types is available through the overloaded functions \cleaninline{int}, \cleaninline{long} and \cleaninline{real}.
 245
 246 \begin{lstClean}[caption={Type conversion functions in \gls{MTASK}.}]
 247 class int  v a :: (v a) -> v Int
 248 class real v a :: (v a) -> v Real
 249 class long v a :: (v a) -> v Long
 250 \end{lstClean}
 251
 252 Finally, values from the host language must be explicitly lifted to the \gls{MTASK} language using the \cleaninline{lit} function.
 253 For convenience, there are many lower-cased macro definitions for often used constants such as \cleaninline{true :== lit True}, \cleaninline{false :== lit False}, \etc.
 254
 255 \Cref{lst:example_exprs} shows some examples of these expressions.
 256 \cleaninline{e0} defines the literal $42$, \cleaninline{e1} calculates the literal $42.0$ using real numbers.
 257 \cleaninline{e2} compares \cleaninline{e0} and \cleaninline{e1} as integers and if they are equal it returns the \cleaninline{e2}$/2$ and \cleaninline{e0} otherwise.
 258 \cleaninline{approxEqual} performs an approximate equality---albeit not taking into account all floating point pecularities---and demonstrates that \gls{CLEAN} can be used as a macro language, i.e.\ maximise linguistic reuse~\cite{krishnamurthi_linguistic_2001}.
 259 \todo{uitzoeken waar dit handig is}
 260 When calling \cleaninline{approxEqual} in an \gls{MTASK} function, the resulting code is inlined.
 261
 262 \begin{lstClean}[label={lst:example_exprs},caption={Example \gls{MTASK} expressions.}]
 263 e0 :: v Int | expr v
 264 e0 = lit 42
 265
 266 e1 :: v Real | expr v
 267 e1 = lit 38.0 + real (lit 4)
 268
 269 e2 :: v Int | expr v
 270 e2 = if' (e0 ==. int e1)
 271         (int e1 /. lit 2) e0
 272
 273 approxEqual :: (v Real) (v Real) (v Real) -> v Real | expr v
 274 approxEqual x y eps = if' (x == y) true
 275         ( if' (x > y)
 276                 (y -. x < eps)
 277                 (x -. y < eps)
 278         )
 279 \end{lstClean}
 280
 281 \subsection{Data Types}
 282 Most of \gls{CLEAN}'s basic types have been mapped on \gls{MTASK} types.
 283 However, it can be useful to have access to compound types as well.
 284 All types in \gls{MTASK} must have a fixed size representation on the stack so sum types are not (yet) supported.
 285 While it is possible to lift types using the \cleaninline{lit} function, you cannot do anything with the types besides passing them around but they are being produced by some parallel task combinators (see \cref{sssec:combinators_parallel}).
 286 To be able to use types as first class citizens, constructors and field selectors are required.
 287 \Cref{lst:tuple_exprs} shows the scaffolding for supporting tuples in \gls{MTASK}.
 288 Besides the constructors and field selectors, there is also a helper function available that transforms a function from a tuple of \gls{MTASK} expressions to an \gls{MTASK} expression of a tuple.
 289
 290 \begin{lstClean}[label={lst:tuple_exprs},caption={Tuple constructor and field selectors in \gls{MTASK}.}]
 291 class tupl v where
 292         tupl :: (v a) (v b) -> v (a, b) | type a & type b
 293         first :: (v (a, b)) -> v a | type a & type b
 294         second :: (v (a, b)) -> v b | type a & type b
 295
 296         tupopen f :== \v->f (first v, second v)
 297 \end{lstClean}
 298
 299 \subsection{Functions}
 300 Adding functions to the language is achieved by one multi-parameter class to the \gls{DSL}.
 301 By using \gls{HOAS}, both the function definition and the calls to the function can be controlled by the \gls{DSL}~\citep{pfenning_higher-order_1988,chlipala_parametric_2008}.
 302 As \gls{MTASK} only supports first-order functions and does not allow partial function application.
 303 Using a type class of this form, this restriction can be enforced on the type level.
 304 Instead of providing one instance for all functions, a single instance per function arity is defined.
 305 Also, \gls{MTASK} only supports top-level functions which is enforced by the \cleaninline{Main} box.
 306 The definition of the type class and the instances for an example interpretation are as follows:
 307 \todo{uitbreiden}
 308
 309 \begin{lstClean}[caption={Functions in \gls{MTASK}.}]
 310 class fun a v :: ((a -> v s) -> In (a -> v s) (Main (MTask v u)))
 311         -> Main (MTask v u)
 312
 313 instance fun () Inter where ...
 314 instance fun (Inter a) Inter | type a where ...
 315 instance fun (Inter a, Inter b) Inter | type a where ...
 316 instance fun (Inter a, Inter b, Inter c) Inter | type a where ...
 317 ...
 318 \end{lstClean}
 319
 320 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}.
 321 \Cref{lst:function_examples} show the factorial function, a tail-call optimised factorial function and a function with zero arguments to demonstrate the syntax.
 322 Splitting out the function definition for each single arity means that that for every function arity and combination of arguments, a separate class constraint must be created.
 323 Many of the often used functions are already bundled in the \cleaninline{mtask} class constraint collection.
 324 \cleaninline{factorialtail} shows a manually added class constraint.
 325 Definiting zero arity functions is shown in the \cleaninline{zeroarity} expression.
 326 Finally, \cleaninline{swapTuple} shows an example of a tuple being swapped.
 327
 328 % VimTeX: SynIgnore on
 329 \begin{lstClean}[label={lst:function_examples},caption={Function examples in \gls{MTASK}.}]
 330 factorial :: Main (v Int) | mtask v
 331 factorial =
 332         fun \fac=(\i->if' (i <. lit 1)
 333                 (lit 1)
 334                 (i *. fac (i -. lit 1)))
 335         In {main = fac (lit 5) }
 336
 337 factorialtail :: Main (v Int) | mtask v & fun (v Int, v Int) v
 338 factorialtail =
 339            fun \facacc=(\(acc, i)->if' (i <. lit 1)
 340                         acc
 341                         (fac (acc *. i, i -. lit 1)))
 342         In fun \fac=(\i->facacc (lit 1, i))
 343         In {main = fac (lit 5) }
 344
 345 zeroarity :: Main (v Int) | mtask v
 346 zeroarity =
 347            fun \fourtytwo=(\()->lit 42)
 348         In fun \add=(\(x, y)->x +. y)
 349         In {main = add (fourtytwo (), lit 9)}
 350
 351 swapTuple :: Main (v (Int, Bool)) | mtask v
 352 swapTuple =
 353            fun \swap=(tupopen \(x, y)->tupl y x)
 354         In {main = swap (tupl true (lit 42)) }
 355 \end{lstClean}
 356 % VimTeX: SynIgnore off
 357
 358 \section{Tasks}\label{sec:top}
 359 \Gls{MTASK}'s task language can be divided into three categories, namely
 360 \begin{enumerate*}
 361         \item Basic tasks, in most \gls{TOP} systems, the basic tasks are called editors, modelling the interactivity with the user.
 362                 In \gls{MTASK}, there are no \emph{editors} in that sense but there is interaction with the outside world through microprocessor peripherals such as sensors and actuators.
 363         \item Task combinators provide a way of describing the workflow.
 364                 They combine one or more tasks into a compound task.
 365         \item \glspl{SDS} in \gls{MTASK} can be seen as references to data that can be shared using many-to-many communication and are only accessible from within the task language to ensure atomicity.
 366 \end{enumerate*}
 367
 368 As \gls{MTASK} is integrated with \gls{ITASK}, the same stability distinction is made for task values.
 369 A task in \gls{MTASK} is denoted by the \gls{DSL} type synonym shown in \cref{lst:task_type}.
 370
 371 \begin{lstClean}[label={lst:task_type},caption={Task type in \gls{MTASK}.}]
 372 :: MTask v a :== v (TaskValue a)
 373 :: TaskValue a
 374         = NoValue
 375         | Value a Bool
 376 \end{lstClean}
 377
 378 \subsection{Basic tasks}
 379 The most rudimentary basic tasks are the \cleaninline{rtrn} and \cleaninline{unstable} tasks.
 380 They lift the value from the \gls{MTASK} expression language to the task domain either as a stable value or an unstable value.
 381 There is also a special type of basic task for delaying execution.
 382 The \cleaninline{delay} task---given a number of milliseconds---yields an unstable value while the time has not passed.
 383 Once the specified time has passed, the time it overshot the planned time is yielded as a stable task value.
 384
 385 \begin{lstClean}[label={lst:basic_tasks},caption={Function examples in \gls{MTASK}.}]
 386 class rtrn v :: (v t) -> MTask v t
 387 class unstable v :: (v t) -> MTask v t
 388 class delay v :: (v n) -> MTask v n | long v n
 389 \end{lstClean}
 390
 391 \subsubsection{Peripherals}\label{sssec:peripherals}
 392 For every sensor or actuator, basic tasks are available that allow interaction with the specific peripheral.
 393 The type classes for these tasks are not included in the \cleaninline{mtask} class collection as not all devices nor all language interpretations have such peripherals connected.
 394 \todo{Historically, peripheral support has been added \emph{by need}.}
 395
 396 \Cref{lst:dht} and \cref{lst:gpio} show the type classes for \glspl{DHT} sensors and \gls{GPIO} access.
 397 Other peripherals have similar interfaces, they are available in the \cref{sec:aux_peripherals}.
 398 For the \gls{DHT} sensor there are two basic tasks, \cleaninline{temperature} and \cleaninline{humidity}, that---will given a \cleaninline{DHT} object---produce a task that yields the observed temperature in \unit{\celcius} or relative humidity as a percentage as an unstable value.
 399 Currently, two different types of \gls{DHT} sensors are supported, the \emph{DHT} family of sensors connect through $1$-wire protocol and the \emph{SHT} family of sensors connected using \gls{I2C} protocol.
 400 Creating such a \cleaninline{DHT} object is very similar to creating functions in \gls{MTASK} and uses \gls{HOAS} to make it type safe.
 401
 402 \begin{lstClean}[label={lst:dht},caption{The \gls{MTASK} interface for \glspl{DHT} sensors.}]
 403 :: DHT //abstract
 404 :: DHTInfo
 405         = DHT_DHT Pin DHTtype
 406         | DHT_SHT I2CAddr
 407 :: DHTtype = DHT11 | DHT21 | DHT22
 408 class dht v where
 409         DHT :: DHTInfo ((v DHT) -> Main (v b)) -> Main (v b) | type b
 410         temperature :: (v DHT) -> MTask v Real
 411         humidity :: (v DHT) -> MTask v Real
 412
 413 measureTemp :: Main (MTask v Real) | mtask v & dht v
 414 measureTemp = DHT (DHT_SHT (i2c 0x36)) \dht->
 415         {main=temperature dht}
 416 \end{lstClean}
 417
 418 \Gls{GPIO} access is divided into three classes: analog, digital and pin modes.
 419 For all pins and pin modes an \gls{ADT} is available that enumerates the pins.
 420 The analog \gls{GPIO} pins of a microprocessor are connected to an \gls{ADC} that translates the voltage to an integer.
 421 Analog \gls{GPIO} pins can be either read or written to.
 422 Digital \gls{GPIO} pins only report a high or a low value.
 423 The type class definition is a bit more complex since analog \gls{GPIO} pins can be used as digital \gls{GPIO} pins as well.
 424 Therefore, if the \cleaninline{p} type implements the \cleaninline{pin} class---i.e.\ either \cleaninline{APin} or \cleaninline{DPin}---the \cleaninline{dio} class can be used.
 425 \Gls{GPIO} pins usually operate according to a certain pin mode that states whether the pin acts as an input pin, an input with an internal pull-up resistor or an output pin.
 426 This setting can be applied using the \cleaninline{pinMode} class by hand or by using the \cleaninline{declarePin} \gls{GPIO} pin constructor.
 427 Setting the pin mode is a task that immediately finisheds and fields a stable unit value.
 428 Writing to a pin is also a task that immediately finishes but yields the written value instead.
 429 Reading a pin is a task that yields an unstable value---i.e.\ the value read from the actual pin.
 430
 431 \begin{lstClean}[label={lst:gpio},caption{The \gls{MTASK} interface for \gls{GPIO} access.}]
 432 :: APin = A0 | A1 | A2 | A3 | A4 | A5
 433 :: DPin = D0 | D1 | D2 | D3 | D4 | D5 | D6 | D7 | D8 | D9 | D10 | D11 | D12 | D13
 434 :: PinMode = PMInput | PMOutput | PMInputPullup
 435 :: Pin = AnalogPin APin | DigitalPin DPin
 436 class pin p :: p -> Pin
 437
 438 class aio v where
 439         writeA :: (v APin) (v Int) -> MTask v Int
 440         readA :: (v APin) -> MTask v Int
 441
 442 class dio p v | pin p where
 443         writeD :: (v p) (v Bool) -> MTask v Bool
 444         readD :: (v p) -> MTask v Bool | pin p
 445
 446 class pinMode v where
 447         pinMode :: (v PinMode) (v p) -> MTask v () | pin p
 448         declarePin :: p PinMode ((v p) -> Main (v a)) -> Main (v a) | pin p
 449 \end{lstClean}
 450
 451 \subsection{Task combinators}
 452 Task combinators are used to combine multiple tasks into one to describe workflows.
 453 There are three main types of task combinators, namely:
 454 \begin{enumerate*}
 455         \item Sequential combinators that execute tasks one after the other, possibly using the result of the left hand side.
 456         \item Parallel combinators that execute tasks at the same time combining the result.
 457         \item Miscellaneous combinators that change the semantics of a task---e.g.\ repeat it or delay execution.
 458 \end{enumerate*}
 459
 460 \subsubsection{Sequential}
 461 Sequential task combination allows the right-hand side task to observe the left-hand side task value.
 462 All seqential task combinators are expressed in the \cleaninline{expr} class and can be---and are by default---derived from the Swiss army knife step combinator \cleaninline{>>*.}.
 463 This combinator has a single task on the left-hand side and a list of \emph{task continuations} on the right-hand side.
 464 The list of task continuations is checked every rewrite step and if one of the predicates matches, the task continues with the result of this combination.
 465 \cleaninline{>>=.} is a shorthand for the bind operation, if the left-hand side is stable, the right-hand side function is called to produce a new task.
 466 \cleaninline{>>|.} is a shorthand for the sequence operation, if the left-hand side is stable, it continues with the right-hand side task.
 467 The \cleaninline{>>~.} and \cleaninline{>>..} combinators are variants of the ones above that ignore the stability and continue on an unstable value as well.
 468
 469 \begin{lstClean}[label={lst:mtask_sequential},caption={Sequential task combinators in \gls{MTASK}.}]
 470 class step v | expr v where
 471         (>>*.) infixl 1 :: (MTask v t) [Step v t u] -> MTask v u
 472         (>>=.) infixl 0 :: (MTask v t) ((v t) -> MTask v u) -> MTask v u
 473         (>>|.) infixl 0 :: (MTask v t)          (MTask v u) -> MTask v u
 474         (>>~.) infixl 0 :: (MTask v t) ((v t) -> MTask v u) -> MTask v u
 475         (>>..) infixl 0 :: (MTask v t)          (MTask v u) -> MTask v u
 476
 477 :: Step v t u
 478         = IfValue    ((v t) -> v Bool) ((v t) -> MTask v u)
 479         | IfStable   ((v t) -> v Bool) ((v t) -> MTask v u)
 480         | IfUnstable ((v t) -> v Bool) ((v t) -> MTask v u)
 481         | Always                                (MTask v u)
 482 \end{lstClean}
 483
 484 \todo{more examples step?}
 485
 486 The following listing shows an example of a step in action.
 487 The \cleaninline{readPinBin} function produces an \gls{MTASK} task that classifies the value of an analogue pin into four bins.
 488 It also shows that the nature of embedding allows the host language to be used as a macro language.
 489 Furthermore
 490
 491 \begin{lstClean}[label={lst:mtask_readpinbin},caption={Read an analog pin and bin the value in \gls{MTASK}.}]
 492 readPinBin :: Int -> Main (MTask v Int) | mtask v
 493 readPinBin lim = declarePin PMInput A2 \a2->
 494         { main = readA a2 >>*.
 495                 [  IfValue (\x->x <. lim) (\_->rtrn (lit bin))
 496                 \\ lim <-[64,128,192,256]
 497                 &  bin <- [0..]]}
 498 \end{lstClean}
 499
 500 \subsubsection{Parallel}\label{sssec:combinators_parallel}
 501 The result of a parallel task combination is a compound that actually executes the tasks at the same time.
 502
 503 There are two types of parallel task combinators (see \cref{lst:mtask_parallel}).
 504 The conjunction combinator (\cleaninline{.&&.}) combines the result by putting the values from both sides in a tuple.
 505 The stability of the task depends on the stability of both children.
 506 If both children are stable, the result is stable, otherwise the result is unstable.
 507 The disjunction combinator (\cleaninline{.\|\|.}) combines the results by picking the leftmost, most stable task.
 508 The semantics are easily described using \gls{CLEAN} functions shown in \cref{lst:semantics_con,lst:semantics_dis}.
 509
 510 \begin{figure}[ht]
 511         \centering
 512         \begin{subfigure}[t]{.5\textwidth}
 513                 \begin{lstClean}[caption={Semantics of the\\conjunction combinator.},label={lst:semantics_con}]
 514 con :: (TaskValue a) (TaskValue b)
 515         -> TaskValue (a, b)
 516 con NoValue r       = NoValue
 517 con l       NoValue = NoValue
 518 con (Value l ls) (Value r rs)
 519         = Value (l, r) (ls && rs)
 520
 521                 \end{lstClean}
 522         \end{subfigure}%
 523         \begin{subfigure}[t]{.5\textwidth}
 524                 \begin{lstClean}[caption={Semantics of the\\disjunction combinator.},label={lst:semantics_dis}]
 525 dis :: (TaskValue a) (TaskValue a)
 526         -> TaskValue a
 527 dis NoValue r       = r
 528 dis l       NoValue = l
 529 dis (Value l ls) (Value r rs)
 530         | rs        = Value r True
 531         | otherwise = Value l ls
 532                 \end{lstClean}
 533         \end{subfigure}
 534 \end{figure}
 535
 536 \begin{lstClean}[label={lst:mtask_parallel},caption={Parallel task combinators in \gls{MTASK}.}]
 537 class (.&&.) infixr 4 v :: (MTask v a) (MTask v b) -> MTask v (a, b)
 538 class (.||.) infixr 3 v :: (MTask v a) (MTask v a) -> MTask v a
 539 \end{lstClean}
 540
 541 \Cref{lst:mtask_parallel_example} gives an example of the parallel task combinator.
 542 This program will read two pins at the same time, returning when one of the pins becomes \arduinoinline{HIGH}.
 543 If the combinator was the \cleaninline{.&&.} instead, the type would be \cleaninline{MTask v (Bool, Bool)} and the task would only return when both pins have been \arduinoinline{HIGH} but not necessarily at the same time.
 544
 545 \begin{lstClean}[label={lst:mtask_parallel_example},caption={Parallel task combinator example in \gls{MTASK}.}]
 546 task :: MTask v Bool
 547 task =
 548         declarePin D0 PMInput \d0->
 549         declarePin D1 PMInput \d1->
 550         let monitor pin = readD pin >>*. [IfValue (\x->x) \x->rtrn x]
 551         In {main = monitor d0 .||. monitor d1}
 552 \end{lstClean}
 553
 554 \subsubsection{Repeat}
 555 The \cleaninline{rpeat} combinator executes the child task.
 556 If a stable value is observed, the task is reinstated.
 557 The functionality of \cleaninline{rpeat} can also be simulated by using functions and sequential task combinators and even made to be stateful as can be seen in \cref{lst:blinkthreadmtask}.
 558
 559 \begin{lstClean}[label={lst:mtask_repeat},caption={Repeat task combinators in \gls{MTASK}.}]
 560 class rpeat v where
 561         rpeat :: (MTask v a) -> MTask v a
 562 \end{lstClean}
 563
 564 To demonstrate the combinator, \cref{lst:mtask_repeat_example} show \cleaninline{rpeat} in use.
 565 This task will mirror the value read from analog \gls{GPIO} pin \cleaninline{A1} to pin \cleaninline{A2} by constantly reading the pin and writing the result.
 566
 567 \begin{lstClean}[label={lst:mtask_repeat_example},caption={Exemplatory repeat task in \gls{MTASK}.}]
 568 task :: MTask v Int | mtask v
 569 task =
 570         declarePin A1 PMInput \a1->
 571         declarePin A2 PMOutput \a2->
 572         {main = rpeat (readA a1 >>~. writeA a2)}
 573 \end{lstClean}
 574
 575 \subsection{\texorpdfstring{\Acrlongpl{SDS}}{Shared data sources}}
 576 \Glspl{SDS} in \gls{MTASK} are by default references to shared memory.
 577 Similar to peripherals (see \cref{sssec:peripherals}), they are constructed at the top level and are accessed through interaction tasks.
 578 The \cleaninline{getSds} task yields the current value of the \gls{SDS} as an unstable value.
 579 This behaviour is similar to the \cleaninline{watch} task in \gls{ITASK}.
 580 Writing a new value to an \gls{SDS} is done using \cleaninline{setSds}.
 581 This task yields the written value as a stable result after it is done writing.
 582 Getting and immediately after setting an \gls{SDS} is not an \emph{atomic} operation.
 583 It is possible that another task accesses the \gls{SDS} in between.
 584 To circumvent this issue, \cleaninline{updSds} is created, this task atomically updates the value of the \gls{SDS}.
 585
 586 \begin{lstClean}[label={lst:mtask_sds},caption={\Glspl{SDS} in \gls{MTASK}.}]
 587 :: Sds a // abstract
 588 class sds v where
 589         sds :: ((v (Sds t)) -> In t (Main (MTask v u))) -> Main (MTask v u)
 590         getSds :: (v (Sds t))                -> MTask v t
 591         setSds :: (v (Sds t))  (v t)         -> MTask v t
 592         updSds :: (v (Sds t)) ((v t) -> v t) -> MTask v t
 593 \end{lstClean}
 594
 595 \todo{examples sdss}
 596
 597 \chapter{Green computing with \texorpdfstring{\gls{MTASK}}{mTask}}%
 598 \label{chp:green_computing_mtask}
 599
 600 \chapter{Integration with \texorpdfstring{\gls{ITASK}}{iTask}}%
 601 \label{chp:integration_with_itask}
 602 The \gls{MTASK} language is a multi-view \gls{DSL}, i.e.\ there are multiple interpretations possible for a single \gls{MTASK} expression.
 603 Using the byte code compiler (\cleaninline{BCInterpret}) \gls{DSL} interpretation, \gls{MTASK} tasks can be fully integrated in \gls{ITASK} and executed as if they were regular \gls{ITASK} tasks, sharing data using \gls{ITASK} \glspl{SDS}.
 604
 605 \Cref{fig:mtask_integration} shows the
 606
 607 \begin{figure}[ht]
 608         \centering
 609         \includestandalone{mtask_integration}
 610         \caption{\Gls{MTASK}'s integration with \gls{ITASK}.}%
 611         \label{fig:mtask_integration}
 612 \end{figure}
 613
 614 \section{Devices}
 615 \Gls{MTASK} tasks in the byte code compiler view are always executed on a certain device.
 616 All communication with this device happens through a so-called \emph{channels} \gls{SDS}.
 617 The channels contain three fields, a queue of messages that are received, a queue of messages to send and a stop flag.
 618 Every communication method that implements the \cleaninline{channelSync} class can provide the communication with an \gls{MTASK} device.
 619 As of now, serial port communication, direct \gls{TCP} communication and \gls{MQTT} over \gls{TCP} are supported as communication providers.
 620 The \cleaninline{withDevice} function transforms a communication provider and a task that does something with this device to an \gls{ITASK} task.
 621 This task sets up the communication, exchanges specifications, handles errors and cleans up after closing.
 622 \Cref{lst:mtask_device} shows the types and interface to connecting devices.
 623
 624 \begin{lstClean}[label={lst:mtask_device},caption={Device communication interface in \gls{MTASK}.}]
 625 :: MTDevice //abstract
 626 :: Channels :== ([MTMessageFro], [MTMessageTo], Bool)
 627
 628 class channelSync a :: a (sds () Channels Channels) -> Task () | RWShared sds
 629
 630 withDevice :: (a (MTDevice -> Task b) -> Task b) | iTask b & channelSync, iTask a
 631
 632 \end{lstClean}
 633
 634 \section{Lifting tasks}
 635 Once the connection with the device is established, \ldots
 636 \begin{lstClean}
 637 liftmTask :: (Main (BCInterpret (TaskValue u))) MTDevice -> Task u | iTask u
 638 \end{lstClean}
 639
 640 \section{Lifting \texorpdfstring{\acrlongpl{SDS}}{shared data sources}}
 641 \begin{lstClean}[label={lst:mtask_itasksds},caption={Lifted \gls{ITASK} \glspl{SDS} in \gls{MTASK}.}]
 642 class liftsds v where
 643         liftsds :: ((v (Sds t))->In (Shared sds t) (Main (MTask v u)))
 644                 -> Main (MTask v u) | RWShared sds
 645 \end{lstClean}
 646
 647 \chapter{Implementation}%
 648 \label{chp:implementation}
 649 IFL19 paper, bytecode instructieset~\cref{chp:bytecode_instruction_set}
 650
 651 \section{Integration with \texorpdfstring{\gls{ITASK}}{iTask}}
 652 IFL18 paper stukken
 653
 654 \chapter{\texorpdfstring{\gls{MTASK}}{mTask} history}
 655 \section{Generating \texorpdfstring{\gls{C}/\gls{CPP}}{C/C++} code}
 656 A first throw at a class-based shallowly \gls{EDSL} for microprocessors was made by \citet{plasmeijer_shallow_2016}.
 657 The language was called \gls{ARDSL} and offered a type safe interface to \gls{ARDUINO} \gls{CPP} dialect.
 658 A \gls{CPP} code generation backend was available together with an \gls{ITASK} simulation backend.
 659 There was no support for tasks or even functions.
 660 Some time later in the 2015 \gls{CEFP} summer school, an extended version was created that allowed the creation of imperative tasks, \glspl{SDS} and the usage of functions~\citep{koopman_type-safe_2019}.
 661 The name then changed from \gls{ARDSL} to \gls{MTASK}.
 662
 663 \section{Integration with \texorpdfstring{\gls{ITASK}}{iTask}}
 664 Mart Lubbers extended this in his Master's Thesis by adding integration with \gls{ITASK} and a bytecode compiler to the language~\citep{lubbers_task_2017}.
 665 \Gls{SDS} in \gls{MTASK} could be accessed on the \gls{ITASK} server.
 666 In this way, entire \gls{IOT} systems could be programmed from a single source.
 667 However, this version used a simplified version of \gls{MTASK} without functions.
 668 This was later improved upon by creating a simplified interface where \glspl{SDS} from \gls{ITASK} could be used in \gls{MTASK} and the other way around~\citep{lubbers_task_2018}.
 669 It was shown by Matheus Amazonas Cabral de Andrade that it was possible to build real-life \gls{IOT} systems with this integration~\citep{amazonas_cabral_de_andrade_developing_2018}.
 670 Moreover, a course on the \gls{MTASK} simulator was provided at the 2018 \gls{CEFP}/\gls{3COWS} winter school in Ko\v{s}ice, Slovakia~\citep{koopman_simulation_2018}.
 671
 672 \section{Transition to \texorpdfstring{\gls{TOP}}{TOP}}
 673 The \gls{MTASK} language as it is now was introduced in 2018~\citep{koopman_task-based_2018}.
 674 This paper updated the language to support functions, tasks and \glspl{SDS} but still compiled to \gls{CPP} \gls{ARDUINO} code.
 675 Later the bytecode compiler and \gls{ITASK} integration was added to the language~\citep{lubbers_interpreting_2019}.
 676 Moreover, it was shown that it is very intuitive to write \gls{MCU} applications in a \gls{TOP} language~\citep{lubbers_multitasking_2019}.
 677 One reason for this is that a lot of design patterns that are difficult using standard means are for free in \gls{TOP} (e.g.\ multithreading).
 678 In 2019, the \gls{CEFP} summer school in Budapest, Hungary hosted a course on developing \gls{IOT} applications with \gls{MTASK} as well~\citep{lubbers_writing_2019}.
 679
 680 \section{\texorpdfstring{\gls{TOP}}{TOP}}
 681 In 2022, the SusTrainable summer school in Rijeka, Croatia hosted a course on developing greener \gls{IOT} applications using \gls{MTASK} as well (the lecture notes are to be written).
 682 Several students worked on extending \gls{MTASK} with many useful features:
 683 Erin van der Veen did preliminary work on a green computer analysis, built a simulator and explored the possibilities for adding bounded datatypes~\citep{veen_van_der_mutable_2020}; Michel de Boer investigated the possibilities for secure communication channels~\citep{boer_de_secure_2020}; and Sjoerd Crooijmans added abstractions for low-power operation to \gls{MTASK} such as hardware interrupts and power efficient scheduling~\citep{crooijmans_reducing_2021}.
 684 Elina Antonova defined a preliminary formal semantics for a subset of \gls{MTASK}~\citep{antonova_MTASK_2022}.
 685 Moreover, plans for student projects and improvements include exploring integrating \gls{TINYML} into \gls{MTASK}; and adding intermittent computing support to \gls{MTASK}.
 686
 687 In 2023, the SusTrainable summer school in Coimbra, Portugal will host a course on \gls{MTASK} as well.
 688
 689 \section{\texorpdfstring{\gls{MTASK}}{mTask} in practise}
 690 Funded by the Radboud-Glasgow Collaboration Fund, collaborative work was executed with Phil Trinder, Jeremy Singer and Adrian Ravi Kishore Ramsingh.
 691 An existing smart campus application was developed using \gls{MTASK} and quantitively and qualitatively compared to the original application that was developed using a traditional \gls{IOT} stack~\citep{lubbers_tiered_2020}.
 692 The collaboration is still ongoing and a journal article is under review comparing four approaches for the edge layer: \gls{PYTHON}, \gls{MICROPYTHON}, \gls{ITASK} and \gls{MTASK}.
 693 Furthermore, power efficiency behaviour of traditional versus \gls{TOP} \gls{IOT} stacks is being compared as well adding a \gls{FREERTOS} implementation to the mix as well
 694
 695 \input{subfilepostamble}
 696 \end{document}