top/top.tex

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