more updates, slight restructure
[phd-thesis.git] / mtask / mtask.tex
1 \documentclass[../thesis.tex]{subfiles}
2
3 \begin{document}
4 \ifSubfilesClassLoaded{
5 \pagenumbering{arabic}
6 }{}
7
8 \mychapter{chp:top4iot}{Introduction to \gls{IOT} programming}
9 \todo{betere chapter naam}
10 \begin{chapterabstract}
11 This chapter introduces \gls{MTASK} and puts it into perspective compared to traditional microprocessor programming.
12 \end{chapterabstract}
13
14 Traditionally, the first program that one writes when trying a new language is the so called \emph{Hello World!} program.
15 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.
16 On microprocessors, there often is no screen for displaying text.
17 Nevertheless, almost always there is a monochrome $1\times1$ pixel screen, namely an---often builtin---\gls{LED}.
18 The \emph{Hello World!} equivalent on microprocessors blinks this \gls{LED}.
19
20 \Cref{lst:arduinoBlink} shows how the logic of a blink program might look when using \gls{ARDUINO}'s \gls{CPP} dialect.
21 Every \gls{ARDUINO} program contains a \arduinoinline{setup} and a \arduinoinline{loop} function.
22 The \arduinoinline{setup} function is executed only once on boot, the \arduinoinline{loop} function is continuously called afterwards and contains the event loop.
23 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.
24 In between it waits for 500 milliseconds so that the blinking is actually visible for the human eye.
25 Compiling this results in a binary firmware that needs to be flashed onto the program memory.
26
27 Translating the traditional blink program to \gls{MTASK} can almost be done by simply substituting some syntax as seen in \cref{lst:blinkImp}.
28 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.
29 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.
30 To simulate a loop, the \cleaninline{rpeat} task can be used, this task executes the argument task and, when stable, reinstates it.
31 The body of the \cleaninline{rpeat} contains similarly named tasks to write to the pins and to wait in between.
32 The tasks are connected using the sequential \cleaninline{>>|.} combinator that for all current intents and purposes executes the tasks after each other.
33
34 \begin{figure}[ht]
35 \begin{subfigure}[b]{.5\linewidth}
36 \begin{lstArduino}[caption={Blink program.},label={lst:arduinoBlink}]
37 void setup() {
38 pinMode(D2, OUTPUT);
39 }
40
41 void loop() {
42 digitalWrite(D2, HIGH);
43 delay(500);
44 digitalWrite(D2, LOW);
45 delay(500);
46 }\end{lstArduino}
47 \end{subfigure}%
48 \begin{subfigure}[b]{.5\linewidth}
49 \begin{lstClean}[caption={Blink program.},label={lst:blinkImp}]
50
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 (1, 500);
80 blink (2, 300);
81 blink (3, 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~\cite{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 delay, long *lastrun, bool *st) {
101 if (millis() - *lastrun > delay) {
102 digitalWrite(pin, *st = !*st);
103 *lastrun += delay;
104 }
105 }
106
107 void loop() {
108 blink(1, 500, &led1, &st1);
109 blink(2, 300, &led2, &st1);
110 blink(3, 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 \gls{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 \cleaninline{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 \begin{lstClean}[label={lst:blinkthreadmtask},caption={Threaded blinking.}]
126 blinktask :: MTask v () | mtask v
127 blinktask =
128 declarePin D1 PMOutput \d1->
129 declarePin D2 PMOutput \d2->
130 declarePin D3 PMOutput \d3->
131 fun \blink=(\(st, pin, wait)->
132 delay wait
133 >>|. writeD d13 st
134 >>|. blink (Not st, pin, wait)) In
135 {main = blink (true, d1, lit 500)
136 .||. blink (true, d2, lit 300)
137 .||. blink (true, d3, lit 800)
138 }\end{lstClean}
139
140 \mychapter{chp:mtask_dsl}{The \gls{MTASK} \gls{DSL}}
141 \begin{chapterabstract}
142 This chapter serves as a complete guide to the \gls{MTASK} language, from an \gls{MTASK} programmer's perspective.
143 \end{chapterabstract}
144
145 The \gls{MTASK} system is a \gls{TOP} programming environment for programming microprocessors.
146 It is implemented as an \gls{EDSL} in \gls{CLEAN} using class-based---or tagless-final---embedding (See \cref{ssec:tagless}).
147 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.
148
149 \begin{itemize}
150 \item Pretty printer
151
152 This interpretation converts the expression to a string representation.
153 \item Simulator
154
155 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.
156 \item Compiler
157
158 The compiler compiles the \gls{MTASK} program at runtime to a specialised bytecode.
159 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.
160 Furthermore, with special language constructs, \glspl{SDS} can be shared between \gls{MTASK} and \gls{ITASK} programs.
161 \end{itemize}
162
163 \section{Types}
164 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.
165 However, not all types in the host language are suitable for microprocessors that may only have 2KiB of \gls{RAM} so class constraints are therefore added to the \gls{DSL} functions.
166 The most used class constraint is the \cleaninline{type} class collection containing functions for serialization, printing, \gls{ITASK} constraints etc.
167 Many of these functions can be derived using generic programming.
168 An even stronger restriction on types is defined for types that have a stack representation.
169 This \cleaninline{basicType} class has instances for many \gls{CLEAN} basic types such as \cleaninline{Int}, \cleaninline{Real} and \cleaninline{Bool}.
170 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.
171
172 \begin{table}[ht]
173 \centering
174 \begin{tabular}{lll}
175 \toprule
176 \gls{CLEAN}/\gls{MTASK} & \gls{CPP} type & \textnumero{}bits\\
177 \midrule
178 \cleaninline{Bool} & \cinline{bool} & 16\\
179 \cleaninline{Char} & \cinline{char} & 16\\
180 \cleaninline{Int} & \cinline{int16_t} & 16\\
181 \cleaninline{:: Long} & \cinline{int32_t} & 32\\
182 \cleaninline{Real} & \cinline{float} & 32\\
183 \cleaninline{:: T = A \| B \| C} & \cinline{enum} & 16\\
184 \bottomrule
185 \end{tabular}
186 \caption{Mapping from \gls{CLEAN}/\gls{MTASK} data types to \gls{CPP} datatypes.}%
187 \label{tbl:mtask-c-datatypes}
188 \end{table}
189
190 The \gls{MTASK} language consists of a core collection of type classes bundled in the type class \cleaninline{class mtask}.
191 Every interpretation implements the type classes in the \cleaninline{mtask} class
192 There are also \gls{MTASK} extensions that not every interpretation implements such as peripherals and integration with \gls{ITASK}.
193
194 \Cref{lst:constraints} contains the definitions for the type constraints and shows some example type signatures for typical \gls{MTASK} expressions and tasks.
195
196 \begin{lstClean}[caption={Classes and class collections for the \gls{MTASK} language.},label={lst:constraints}]
197 class type t | iTask, ... ,fromByteCode, toByteCode t
198 class basicType t | type t where ...
199
200 class mtask v | expr, ..., int, real, long v
201
202 someExpr :: v Int | mtask v
203 someExpr = ...
204
205 someTask :: MTask v Int | mtask v
206 someTask =
207 sensor1 config1 \sns1->
208 sensor2 config2 \sns2->
209 fun \fun1= ( ... )
210 In fun \fun2= ( ... )
211 In {main=mainexpr}
212 \end{lstClean}
213
214 \section{Expressions}
215 \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.
216 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.
217
218 \begin{lstClean}[caption={The \gls{MTASK} class for expressions},label={lst:expressions}]
219 class expr v where
220 lit :: t -> v t | type t
221 (+.) infixl 6 :: (v t) (v t) -> v t | basicType, +, zero t
222 ...
223 (&.) infixr 3 :: (v Bool) (v Bool) -> v Bool
224 (|.) infixr 2 :: (v Bool) (v Bool) -> v Bool
225 Not :: (v Bool) -> v Bool
226 (==.) infix 4 :: (v a) (v a) -> v Bool | Eq, basicType a
227 ...
228 If :: (v Bool) (v t) (v t) -> v t | type t
229 \end{lstClean}
230
231 Conversion to-and-fro data types is available through the overloaded functions \cleaninline{int}, \cleaninline{long} and \cleaninline{real}.
232
233 \begin{lstClean}
234 class int v a :: (v a) -> v Int
235 class real v a :: (v a) -> v Real
236 class long v a :: (v a) -> v Long
237 \end{lstClean}
238
239 Finally, values from the host language must be explicitly lifted to the \gls{MTASK} language using the \cleaninline{lit} function.
240 For convenience, there are many lower-cased macro definitions for often used constants as can be seen in \cref{lst:convenience_lits}
241
242 \begin{lstClean}[label={lst:convenience_lits}]
243 // Booleans
244 true :== lit True
245 false :== lit False
246 \end{lstClean}
247
248 \subsection{Functions}
249 Functions in \gls{MTASK} are defined
250
251 \section{Tasks}
252 \subsection{Basic tasks}
253 \subsubsection{Peripherals}
254 \subsection{Task combinators}
255 \subsubsection{Parallel}
256 \subsubsection{Sequential}
257 \subsubsection{Miscellaneous}
258 \subsection{\glspl{SDS}}
259
260 \mychapter{chp:green_computing_mtask}{Green computing with \gls{MTASK}}
261
262 \mychapter{chp:integration_with_itask}{Integration with \gls{ITASK}}
263 \section{Devices}
264 \section{Lift tasks}
265 \section{Lift \glspl{SDS}}
266
267 \mychapter{chp:implementation}{Implementation}
268 IFL19 paper, bytecode instructieset~\cref{chp:bytecode_instruction_set}
269
270 \section{Integration with \gls{ITASK}}
271 IFL18 paper stukken
272
273 \chapter{\gls{MTASK} history}
274 \section{Generating \glsentrytext{C}/\glsentrytext{CPP} code}
275 A first throw at a class-based shallowly \gls{EDSL} for microprocessors was made by Pieter Koopman and Rinus Plasmijer in 2016~\cite{plasmeijer_shallow_2016}.
276 The language was called \gls{ARDSL} and offered a type safe interface to \gls{ARDUINO} \gls{CPP} dialect.
277 A \gls{CPP} code generation backend was available together with an \gls{ITASK} simulation backend.
278 There was no support for tasks or even functions.
279 Some time later in the 2015 CEFP summer school, an extended version was created that allowed the creation of imperative tasks, \glspl{SDS} and the usage of functions~\cite{koopman_type-safe_2019}.
280 The name then changed from \gls{ARDSL} to \gls{MTASK}.
281
282 \section{Integration with \glsentrytext{ITASK}}
283 Mart Lubbers extended this in his Master's Thesis by adding integration with \gls{ITASK} and a bytecode compiler to the language~\cite{lubbers_task_2017}.
284 \Gls{SDS} in \gls{MTASK} could be accessed on the \gls{ITASK} server.
285 In this way, entire \gls{IOT} systems could be programmed from a single source.
286 However, this version used a simplified version of \gls{MTASK} without functions.
287 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~\cite{lubbers_task_2018}.
288 It was shown by Matheus Amazonas Cabral de Andrade that it was possible to build real-life \gls{IOT} systems with this integration~\cite{amazonas_cabral_de_andrade_developing_2018}.
289 Moreover, a course on the \gls{MTASK} simulator was provided at the 2018 CEFP/3COWS winter school in Ko\v{s}ice, Slovakia~\cite{koopman_simulation_2018}.
290
291 \section{Transition to \glsentrytext{TOP}}
292 The \gls{MTASK} language as it is now was introduced in 2018~\cite{koopman_task-based_2018}.
293 This paper updated the language to support functions, tasks and \glspl{SDS} but still compiled to \gls{CPP} \gls{ARDUINO} code.
294 Later the bytecode compiler and \gls{ITASK} integration was added to the language~\cite{lubbers_interpreting_2019}.
295 Moreover, it was shown that it is very intuitive to write \gls{MCU} applications in a \gls{TOP} language~\cite{lubbers_multitasking_2019}.
296 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).
297 In 2019, the CEFP summer school in Budapest, Hungary hosted a course on developing \gls{IOT} applications with \gls{MTASK} as well~\cite{lubbers_writing_2019}.
298
299 \section{\glsentrytext{TOP}}
300 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).
301 Several students worked on extending \gls{MTASK} with many useful features:
302 Erin van der Veen did preliminary work on a green computer analysis, built a simulator and explored the possibilities for adding bounded datatypes~\cite{veen_van_der_mutable_2020}; Michel de Boer investigated the possibilities for secure communication channels~\cite{boer_de_secure_2020}; and Sjoerd Crooijmans added abstractions for low-power operation to \gls{MTASK} such as hardware interrupts and power efficient scheduling~\cite{crooijmans_reducing_2021}.
303 Elina Antonova defined a preliminary formal semantics for a subset of \gls{MTASK}~\cite{antonova_MTASK_2022}.
304 Moreover, plans for student projects and improvements include exploring integrating \gls{TINYML} into \gls{MTASK}; and adding intermittent computing support to \gls{MTASK}.
305
306 In 2023, the SusTrainable summer school in Coimbra, Portugal will host a course on \gls{MTASK} as well.
307
308 \section{\glsentrytext{MTASK} in practise}
309 Funded by the Radboud-Glasgow Collaboration Fund, collaborative work was executed with Phil Trinder, Jeremy Singer and Adrian Ravi Kishore Ramsingh.
310 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~\cite{lubbers_tiered_2020}.
311 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}.
312 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
313
314 \input{subfilepostamble}
315 \end{document}