X-Git-Url: https://git.martlubbers.net/?a=blobdiff_plain;f=top%2Ftop.tex;fp=top%2Ftop.tex;h=6c759fb168a7c95644764de6419e11550674a695;hb=5aa57e0cb31d64685ad4c0624c1047a4b7e77399;hp=913dfc7b16ab9efe09eeec2ef7372cb892f27bca;hpb=2925b1f5ecee47e6d0893e5640323ff694c4cd28;p=phd-thesis.git diff --git a/top/top.tex b/top/top.tex index 913dfc7..6c759fb 100644 --- a/top/top.tex +++ b/top/top.tex @@ -5,716 +5,11 @@ \begin{document} \input{subfileprefix} -\chapter{Edge device programming}% -\label{chp:top4iot} -\begin{chapterabstract} - This chapter: - \begin{itemize} - \item shows how to create the \emph{Hello World!} application for microcontrollers using \gls{ARDUINO}; - \item extends this idea with multithreading, demonstrating the difficulty programming multi-tasking applications; - \item describes a comparative variant in \gls{MTASK} and shows that upgrading to a multi-tasking variant is straightforward - \item demonstrates that the complexity of running multiple tasks; - \item and concludes with the history of \gls{MTASK}'s development. - \end{itemize} -\end{chapterabstract} - -The edge layer of \gls{IOT} system mostly consists of microcontrollers. -Microcontrollers are tiny computers designed specifically for embedded applications. -They therefore only have a soup\c{c}on of memory, have a slow processor, come with many energy efficient sleep modes and have a lot of peripheral support such as \gls{GPIO} pins. -Usually, programming microcontrollers requires an elaborate multi-step toolchain of compilation, linkage, binary image creation, and burning this image onto the flash memory of the microcontroller in order to compile and run a program. -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. -\Cref{tbl:mcu_laptop} compares the hardware properties of a typical laptop with two very popular microcontrollers. - -\begin{table} - \caption{Hardware characteristics of typical microcontrollers and laptops.}% - \label{tbl:mcu_laptop} - \begin{tabular}{llll} - \toprule - & Laptop & Atmega328P & ESP8266\\ - \midrule - CPU speed & \qtyrange{2}{4}{\giga\hertz} & \qty{16}{\mega\hertz} & \qty{80}{\mega\hertz} or \qty{160}{\mega\hertz}\\ - \textnumero{} cores & \numrange{4}{8} & 1 & 1\\ - Storage & \qty{1}{\tebi\byte} & \qty{32}{\kibi\byte} & \qtyrange{0.5}{4}{\mebi\byte}\\ - \gls{RAM} & \qtyrange{4}{16}{\gibi\byte} & \qty{2}{\kibi\byte} & \qty{160}{\kibi\byte}\\ - Power & \qtyrange{50}{100}{\watt} & \qtyrange{0.13}{250}{\milli\watt} & \qtyrange{0.1}{350}{\milli\watt}\\ - Price & \euro{1500} & \euro{3} & \euro{4}\\ - \bottomrule - \end{tabular} -\end{table} - -Each type of microcontrollers 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. -The popular \gls{ARDUINO} \gls{C}\slash\gls{CPP} dialect and accompanying libraries provide an abstraction layer for common microcontroller behaviour allowing the programmer to program multiple types of microcontrollers using a single language. -Originally it was designed for the in-house developed open-source hardware with the same name but the setup allows porting to many architectures. -It provides an \gls{IDE} and toolchain automation to perform all steps of the toolchain with a single command. - -\section{Hello world!} -Traditionally, the first program that one writes when trying a new language is the so called \emph{Hello World!} program. -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. -On microcontrollers, there usually is no screen for displaying text. -Nevertheless, almost always there is a built-in monochrome $1\times1$ pixel screen, namely \pgls{LED}. -The \emph{Hello World!} equivalent on microcontrollers blinks this \gls{LED}. - -\Cref{lst:arduinoBlink} shows how the logic of a blink program might look when using \gls{ARDUINO}'s \gls{C}\slash\gls{CPP} dialect. -Every \gls{ARDUINO} program contains a \arduinoinline{setup} and a \arduinoinline{loop} function. -The \arduinoinline{setup} function is executed only once on boot, the \arduinoinline{loop} function is continuously called afterwards and contains the event loop. -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. -In between it waits for \qty{500}{\ms} so that the blinking is actually visible for the human eye. - -Translating the traditional blink program to \gls{MTASK} can almost be done by simply substituting some syntax as seen in \cref{lst:blinkImp}. -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. -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. -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. -The body of the \cleaninline{rpeat} contains similarly named tasks to write to the pins and to wait in between. -The tasks are connected using the sequential \cleaninline{>>|.} combinator that for all current intents and purposes executes the tasks after each other. - -\begin{figure}[ht] - \begin{subfigure}[b]{.5\linewidth} - \begin{lstArduino}[caption={Blink program.},label={lst:arduinoBlink}] -void setup() { - pinMode(D2, OUTPUT); -} - -void loop() { - digitalWrite(D2, HIGH); - delay(500); - digitalWrite(D2, LOW); - delay(500); -} - \end{lstArduino} - \end{subfigure}% - \begin{subfigure}[b]{.5\linewidth} - \begin{lstClean}[caption={Blink program.},label={lst:blinkImp}] -blink :: Main (MTask v ()) | mtask v -blink = - declarePin D2 PMOutput \d2-> - {main = rpeat ( - writeD d2 true - >>|. delay (lit 500) - >>|. writeD d2 false - >>|. delay (lit 500) - ) -} - \end{lstClean} - \end{subfigure} -\end{figure} - -\section{Threaded blinking} -Now say that we want to blink multiple blinking patterns on different \glspl{LED} concurrently. -For example, blink three \glspl{LED} connected to \gls{GPIO} pins $1,2$ and $3$ at intervals of \qtylist{500;300;800}{\ms}. -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} - -\begin{lstArduino}[caption={Naive approach to multiple blinking patterns.},label={lst:blinkthreadno}] -void setup () { ... } - -void blink (int pin, int wait) { - digitalWrite(pin, HIGH); - delay(wait); - digitalWrite(pin, LOW); - delay(wait); -} - -void loop() { - blink (D1, 500); - blink (D2, 300); - blink (D3, 800); -}\end{lstArduino} - -Unfortunately, this does not work because the \arduinoinline{delay} function blocks all further execution. -The resulting program will blink the \glspl{LED} after each other instead of at the same time. -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}. -Listing~\ref{lst:blinkthread} shows how three different blinking patterns might be achieved in \gls{ARDUINO} using the slicing method. -If we want the blink function to be a separate parametrizable function we need to explicitly provide all references to the required state. -Furthermore, the \arduinoinline{delay} function can not be used and polling \arduinoinline{millis} is required. -The \arduinoinline{millis} function returns the number of milliseconds that have passed since the boot of the microcontroller. -Some devices use very little energy when in \arduinoinline{delay} or sleep state. -Resulting in \arduinoinline{millis} potentially affects power consumption since the processor is basically busy looping all the time. -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. -Unfortunately, this is very hard when for example the blinking patterns are determined at runtime. - -\begin{lstArduino}[label={lst:blinkthread},caption={Threading three blinking patterns.}] -long led1 = 0, led2 = 0, led3 = 0; -bool st1 = false, st2 = false, st3 = false; - -void blink(int pin, int dlay, long *lastrun, bool *st) { - if (millis() - *lastrun > dlay) { - digitalWrite(pin, *st = !*st); - *lastrun += dlay; - } -} - -void loop() { - blink(D1, 500, &led1, &st1); - blink(D2, 300, &led2, &st1); - blink(D3, 800, &led3, &st1); -}\end{lstArduino} - -This method is very error prone, requires a lot of pointer juggling and generally results into spaghetti code. -Furthermore, it is very difficult to represent dependencies between threads, often state machines have to be explicitly programmed by hand to achieve this. - -\section{Blinking in \texorpdfstring{\gls{MTASK}}{mTask}} -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. -In contrast, the \arduinoinline{delay()} \emph{function} on the \gls{ARDUINO} is blocking which prohibits interleaving. -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. -The function is parametrized with the current state, the pin to blink and the waiting time. -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. -With a parallel combinator, tasks can be executed in an interleaved fashion. -Therefore, blinking three different blinking patterns is as simple as combining the three calls to the \cleaninline{blink} function with their arguments as seen in \cref{lst:blinkthreadmtask}. - -% VimTeX: SynIgnore on -\begin{lstClean}[label={lst:blinkthreadmtask},caption={Threaded blinking.}] -blinktask :: MTask v () | mtask v -blinktask = - declarePin D1 PMOutput \d1-> - declarePin D2 PMOutput \d2-> - declarePin D3 PMOutput \d3-> - fun \blink=(\(st, pin, wait)-> - delay wait - >>|. writeD d13 st - >>|. blink (Not st, pin, wait)) In - {main = blink (true, d1, lit 500) - .||. blink (true, d2, lit 300) - .||. blink (true, d3, lit 800) - }\end{lstClean} -% VimTeX: SynIgnore off - -\section{\texorpdfstring{\Gls{MTASK}}{MTask} history} -\subsection{Generating \texorpdfstring{\gls{C}/\gls{CPP}}{C/C++} code} -A first throw at a class-based shallowly \gls{EDSL} for microcontrollers was made by \citet{plasmeijer_shallow_2016}. -The language was called \gls{ARDSL} and offered a type safe interface to \gls{ARDUINO} \gls{CPP} dialect. -A \gls{CPP} code generation backend was available together with an \gls{ITASK} simulation backend. -There was no support for tasks or even functions. -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}. -The name then changed from \gls{ARDSL} to \gls{MTASK}. - -\subsection{Integration with \texorpdfstring{\gls{ITASK}}{iTask}} -\Citet{lubbers_task_2017} extended this in his Master's Thesis by adding integration with \gls{ITASK} and a bytecode compiler to the language. -\Gls{SDS} in \gls{MTASK} could be accessed on the \gls{ITASK} server. -In this way, entire \gls{IOT} systems could be programmed from a single source. -However, this version used a simplified version of \gls{MTASK} without functions. -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}. -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. -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}. - -\section{Transition to \texorpdfstring{\gls{TOP}}{TOP}} -The \gls{MTASK} language as it is now was introduced in 2018 \citep{koopman_task-based_2018}. -This paper updated the language to support functions, tasks and \glspl{SDS} but still compiled to \gls{CPP} \gls{ARDUINO} code. -Later the bytecode compiler and \gls{ITASK} integration was added to the language \citep{lubbers_interpreting_2019}. -Moreover, it was shown that it is very intuitive to write microcontroller applications in a \gls{TOP} language \citep{lubbers_multitasking_2019}. -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). -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}. - -\subsection{\texorpdfstring{\Glsxtrshort{TOP}}{TOP}} -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). -Several students worked on extending \gls{MTASK} with many useful features: -\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}). -\Citet{antonova_mtask_2022} defined a preliminary formal semantics for a subset of \gls{MTASK}. -Moreover, plans for student projects and improvements include exploring integrating \gls{TINYML} into \gls{MTASK}; and adding intermittent computing support to \gls{MTASK}. - -In 2023, the SusTrainable summer school in Coimbra, Portugal will host a course on \gls{MTASK} as well. - -\subsection{\texorpdfstring{\gls{MTASK}}{mTask} in practise} -Funded by the Radboud-Glasgow Collaboration Fund, collaborative work was executed with Phil Trinder, Jeremy Singer, and Adrian Ravi Kishore Ramsingh. -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}. -This research was later extended to include a four-way comparison: \gls{PYTHON}, \gls{MICROPYTHON}, \gls{ITASK} and \gls{MTASK} \citep{lubbers_could_2022}. -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. - -\chapter{The \texorpdfstring{\gls{MTASK}}{mTask} \texorpdfstring{\glsxtrshort{DSL}}{DSL}}% -\label{chp:mtask_dsl} -\begin{chapterabstract} -This chapter introduces the \gls{MTASK} language more technically by: - \begin{itemize} - \item introducing the setup of the \gls{EDSL}; - \item and showing the language interface and examples for: - \begin{itemize} - \item data types - \item expression - \item task and their combinators. - \end{itemize} - \end{itemize} -\end{chapterabstract} - -The \gls{MTASK} system is a complete \gls{TOP} programming environment for programming microcontrollers. -It is implemented as an \gls{EDSL} in \gls{CLEAN} using class-based---or tagless-final---embedding (see \cref{sec:tagless-final_embedding}). - -Due to the nature of the embedding technique, it is possible to have multiple views on-programs written in the \gls{MTASK} language. -The following interpretations are available for \gls{MTASK}. - -\begin{description} - \item[Pretty printer] - - This interpretation converts the expression to a string representation. - \item[Simulator] - - 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. - \item[Byte code compiler] - - The compiler compiles the \gls{MTASK} program at runtime to a specialised byte code. - Using a handful of integration functions and tasks, \gls{MTASK} tasks can be executed on microcontrollers and integrated in \gls{ITASK} as if they were regular \gls{ITASK} tasks. - Furthermore, with special language constructs, \glspl{SDS} can be shared between \gls{MTASK} and \gls{ITASK} programs. -\end{description} - -When using the compiler interpretation in conjunction with the \gls{ITASK} integration, \gls{MTASK} is a heterogeneous \gls{DSL}. -I.e.\ some components---e.g.\ the \gls{RTS} on the microcontroller---is largely unaware of the other components in the system, and it is executed on a completely different architecture. -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}). - -\section{Types} -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. -However, not all types in the host language are suitable for microcontrollers that may only have \qty{2}{\kibi\byte} of \gls{RAM} so class constraints are therefore added to the \gls{DSL} functions. -The most used class constraint is the \cleaninline{type} class collection containing functions for serialization, printing, \gls{ITASK} constraints, \etc. -Many of these functions can be derived using generic programming. -An even stronger restriction on types is defined for types that have a stack representation. -This \cleaninline{basicType} class has instances for many \gls{CLEAN} basic types such as \cleaninline{Int}, \cleaninline{Real} and \cleaninline{Bool}. -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. - -\begin{table}[ht] - \centering - \caption{Mapping from \gls{CLEAN}/\gls{MTASK} data types to \gls{CPP} datatypes.}% - \label{tbl:mtask-c-datatypes} - \begin{tabular}{lll} - \toprule - \gls{CLEAN}/\gls{MTASK} & \gls{CPP} type & \textnumero{}bits\\ - \midrule - \cleaninline{Bool} & \cinline{bool} & 16\\ - \cleaninline{Char} & \cinline{char} & 16\\ - \cleaninline{Int} & \cinline{int16_t} & 16\\ - \cleaninline{:: Long} & \cinline{int32_t} & 32\\ - \cleaninline{Real} & \cinline{float} & 32\\ - \cleaninline{:: T = A \| B \| C} & \cinline{enum} & 16\\ - \bottomrule - \end{tabular} -\end{table} - -\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. -The \gls{MTASK} language interface consists of a core collection of type classes bundled in the type class \cleaninline{class mtask}. -Every interpretation implements the type classes in the \cleaninline{mtask} class -There are also \gls{MTASK} extensions that not every interpretation implements such as peripherals and \gls{ITASK} integration. -\begin{lstClean}[caption={Classes and class collections for the \gls{MTASK} language.},label={lst:constraints}] -class type t | iTask, ... ,fromByteCode, toByteCode t -class basicType t | type t where ... - -class mtask v | expr, ..., int, real, long v - -\end{lstClean} - -Sensors, \glspl{SDS}, functions, \etc{} may only be defined at the top level. -The \cleaninline{Main} type is used that is used to distinguish the top level from the main expression. -Some top level definitions, such as functions, are defined using \gls{HOAS}. -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}). - -\begin{lstClean}[caption={Example task and auxiliary types in the \gls{MTASK} language.},label={lst:mtask_types}] -:: Main a = { main :: a } -:: In a b = (In) infix 0 a b - -someTask :: MTask v Int | mtask v & liftsds v & sensor1 v & ... -someTask = - sensor1 config1 \sns1-> - sensor2 config2 \sns2-> - sds \s1=initial - In liftsds \s2=someiTaskSDS - In fun \fun1= ( ... ) - In fun \fun2= ( ... ) - In { main = mainexpr } -\end{lstClean} - -\section{Expressions}\label{sec:expressions} -\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. -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. - -\begin{lstClean}[caption={The \gls{MTASK} class for expressions},label={lst:expressions}] -class expr v where - lit :: t -> v t | type t - (+.) infixl 6 :: (v t) (v t) -> v t | basicType, +, zero t - ... - (&.) infixr 3 :: (v Bool) (v Bool) -> v Bool - (|.) infixr 2 :: (v Bool) (v Bool) -> v Bool - Not :: (v Bool) -> v Bool - (==.) infix 4 :: (v a) (v a) -> v Bool | Eq, basicType a - ... - If :: (v Bool) (v t) (v t) -> v t | type t -\end{lstClean} - -Conversion to-and-fro data types is available through the overloaded functions \cleaninline{int}, \cleaninline{long} and \cleaninline{real} that will convert the argument to the respective type similar to casting in \gls{C}. - -\begin{lstClean}[caption={Type conversion functions in \gls{MTASK}.}] -class int v a :: (v a) -> v Int -class real v a :: (v a) -> v Real -class long v a :: (v a) -> v Long -\end{lstClean} - -Values from the host language must be explicitly lifted to the \gls{MTASK} language using the \cleaninline{lit} function. -For convenience, there are many lower-cased macro definitions for often used constants such as \cleaninline{true :== lit True}, \cleaninline{false :== lit False}, \etc. - -\Cref{lst:example_exprs} shows some examples of these expressions. -Since they are only expressions, there is no need for a \cleaninline{Main}. -\cleaninline{e0} defines the literal $42$, \cleaninline{e1} calculates the literal $42.0$ using real numbers. -\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. - -\begin{lstClean}[label={lst:example_exprs},caption={Example \gls{MTASK} expressions.}] -e0 :: v Int | expr v -e0 = lit 42 - -e1 :: v Real | expr v -e1 = lit 38.0 + real (lit 4) - -e2 :: v Int | expr v -e2 = if' (e0 ==. int e1) - (int e1 /. lit 2) e0 -\end{lstClean} - -\Gls{MTASK} is shallowly embedded in \gls{CLEAN} and the terms are constructed at runtime. -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} -\cleaninline{approxEqual} in \cref{lst:example_macro} performs an approximate equality---albeit not taking into account all floating point pecularities---. -When calling \cleaninline{approxEqual} in an \gls{MTASK} function, the resulting code is inlined. - -\begin{lstClean}[label={lst:example_macro},caption={Example linguistic reuse in the \gls{MTASK} language.}] -approxEqual :: (v Real) (v Real) (v Real) -> v Real | expr v -approxEqual x y eps = if' (x ==. y) true - ( if' (x >. y) - (y -. x < eps) - (x -. y < eps) - ) -\end{lstClean} - -\subsection{Data types} -Most of \gls{CLEAN}'s basic types have been mapped on \gls{MTASK} types. -However, it can be useful to have access to compound types as well. -All types in \gls{MTASK} must have a fixed size representation on the stack so sum types are not (yet) supported. -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}). -To be able to use types as first class citizens, constructors and field selectors are required (see \cref{chp:first-class_datatypes}). -\Cref{lst:tuple_exprs} shows the scaffolding for supporting tuples in \gls{MTASK}. -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. -Examples for using tuple can be found in \cref{sec:mtask_functions}. - -\begin{lstClean}[label={lst:tuple_exprs},caption={Tuple constructor and field selectors in \gls{MTASK}.}] -class tupl v where - tupl :: (v a) (v b) -> v (a, b) | type a & type b - first :: (v (a, b)) -> v a | type a & type b - second :: (v (a, b)) -> v b | type a & type b - - tupopen f :== \v->f (first v, second v) -\end{lstClean} - -\subsection{Functions}\label{sec:mtask_functions} -Adding functions to the language is achieved by type class to the \gls{DSL}. -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}. -The \gls{MTASK} only allows first-order functions and does not allow partial function application. -This is restricted by using a multi-parameter type class where the first parameter represents the arguments and the second parameter the view. -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. -Also, \gls{MTASK} only supports top-level functions which is enforced by the \cleaninline{Main} box. -The definition of the type class and the instances for an example interpretation (\cleaninline{:: Inter}) are as follows: - -\begin{lstClean}[caption={Functions in \gls{MTASK}.}] -class fun a v :: ((a -> v s) -> In (a -> v s) (Main (MTask v u))) - -> Main (MTask v u) - -instance fun () Inter where ... -instance fun (Inter a) Inter | type a where ... -instance fun (Inter a, Inter b) Inter | type a, type b where ... -instance fun (Inter a, Inter b, Inter c) Inter | type a, ... where ... -... -\end{lstClean} - -Deriving how to define and use functions from the type is quite the challenge even though the resulting syntax is made easier using the infix type \cleaninline{In}. -\Cref{lst:function_examples} show the factorial function, a tail-call optimised factorial function and a function with zero arguments to demonstrate the syntax. -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. -Many of the often used functions are already bundled in the \cleaninline{mtask} class constraint collection. -\cleaninline{factorialtail} shows a manually added class constraint. -Definiting zero arity functions is shown in the \cleaninline{zeroarity} expression. -Finally, \cleaninline{swapTuple} shows an example of a tuple being swapped. - -% VimTeX: SynIgnore on -\begin{lstClean}[label={lst:function_examples},caption={Function examples in \gls{MTASK}.}] -factorial :: Main (v Int) | mtask v -factorial = - fun \fac=(\i->if' (i <. lit 1) - (lit 1) - (i *. fac (i -. lit 1))) - In {main = fac (lit 5) } - -factorialtail :: Main (v Int) | mtask v & fun (v Int, v Int) v -factorialtail = - fun \facacc=(\(acc, i)->if' (i <. lit 1) - acc - (fac (acc *. i, i -. lit 1))) - In fun \fac=(\i->facacc (lit 1, i)) - In {main = fac (lit 5) } - -zeroarity :: Main (v Int) | mtask v -zeroarity = - fun \fourtytwo=(\()->lit 42) - In fun \add=(\(x, y)->x +. y) - In {main = add (fourtytwo (), lit 9)} - -swapTuple :: Main (v (Int, Bool)) | mtask v -swapTuple = - fun \swap=(tupopen \(x, y)->tupl y x) - In {main = swap (tupl true (lit 42)) } -\end{lstClean} -% VimTeX: SynIgnore off - -\section{Tasks and task combinators}\label{sec:top} -\Gls{MTASK}'s task language can be divided into three categories, namely -\begin{enumerate*} - \item Basic tasks, in most \gls{TOP} systems, the basic tasks are called editors, modelling the interactivity with the user. - In \gls{MTASK}, there are no \emph{editors} in that sense but there is interaction with the outside world through microcontroller peripherals such as sensors and actuators. - \item Task combinators provide a way of describing the workflow. - They combine one or more tasks into a compound task. - \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. -\end{enumerate*} - -As \gls{MTASK} is integrated with \gls{ITASK}, the same stability distinction is made for task values. -A task in \gls{MTASK} is denoted by the \gls{DSL} type synonym shown in \cref{lst:task_type}. - -\begin{lstClean}[label={lst:task_type},caption={Task type in \gls{MTASK}.}] -:: MTask v a :== v (TaskValue a) -:: TaskValue a - = NoValue - | Value a Bool -\end{lstClean} - -\subsection{Basic tasks} -The most rudimentary basic tasks are the \cleaninline{rtrn} and \cleaninline{unstable} tasks. -They lift the value from the \gls{MTASK} expression language to the task domain either as a stable value or an unstable value. -There is also a special type of basic task for delaying execution. -The \cleaninline{delay} task---given a number of milliseconds---yields an unstable value while the time has not passed. -Once the specified time has passed, the time it overshot the planned time is yielded as a stable task value. -See \cref{sec:repeat} for an example task using \cleaninline{delay}. - -\begin{lstClean}[label={lst:basic_tasks},caption={Function examples in \gls{MTASK}.}] -class rtrn v :: (v t) -> MTask v t -class unstable v :: (v t) -> MTask v t -class delay v :: (v n) -> MTask v n | long v n -\end{lstClean} - -\subsubsection{Peripherals}\label{sssec:peripherals} -For every sensor or actuator, basic tasks are available that allow interaction with the specific peripheral. -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. -%\todo{Historically, peripheral support has been added \emph{by need}.} - -\Cref{lst:dht,lst:gpio} show the type classes for \glspl{DHT} sensors and \gls{GPIO} access. -Other peripherals have similar interfaces, they are available in the \cref{sec:aux_peripherals}. -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. -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. -Creating such a \cleaninline{DHT} object is very similar to creating functions in \gls{MTASK} and uses \gls{HOAS} to make it type safe. - -\begin{lstClean}[label={lst:dht},caption{The \gls{MTASK} interface for \glspl{DHT} sensors.}] -:: DHT //abstract -:: DHTInfo - = DHT_DHT Pin DHTtype - | DHT_SHT I2CAddr -:: DHTtype = DHT11 | DHT21 | DHT22 -class dht v where - DHT :: DHTInfo ((v DHT) -> Main (v b)) -> Main (v b) | type b - temperature :: (v DHT) -> MTask v Real - humidity :: (v DHT) -> MTask v Real - -measureTemp :: Main (MTask v Real) | mtask v & dht v -measureTemp = DHT (DHT_SHT (i2c 0x36)) \dht-> - {main=temperature dht} -\end{lstClean} - -\Gls{GPIO} access is divided into three classes: analog, digital and pin modes. -For all pins and pin modes an \gls{ADT} is available that enumerates the pins. -The analog \gls{GPIO} pins of a microcontroller are connected to an \gls{ADC} that translates the voltage to an integer. -Analog \gls{GPIO} pins can be either read or written to. -Digital \gls{GPIO} pins only report a high or a low value. -The type class definition is a bit more complex since analog \gls{GPIO} pins can be used as digital \gls{GPIO} pins as well. -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. -\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. -This setting can be applied using the \cleaninline{pinMode} class by hand or by using the \cleaninline{declarePin} \gls{GPIO} pin constructor. -Setting the pin mode is a task that immediately finisheds and fields a stable unit value. -Writing to a pin is also a task that immediately finishes but yields the written value instead. -Reading a pin is a task that yields an unstable value---i.e.\ the value read from the actual pin. - -\begin{lstClean}[label={lst:gpio},caption={The \gls{MTASK} interface for \gls{GPIO} access.}] -:: APin = A0 | A1 | A2 | A3 | A4 | A5 -:: DPin = D0 | D1 | D2 | D3 | D4 | D5 | D6 | D7 | D8 | D9 | D10 | D11 | D12 | D13 -:: PinMode = PMInput | PMOutput | PMInputPullup -:: Pin = AnalogPin APin | DigitalPin DPin -class pin p :: p -> Pin - -class aio v where - writeA :: (v APin) (v Int) -> MTask v Int - readA :: (v APin) -> MTask v Int - -class dio p v | pin p where - writeD :: (v p) (v Bool) -> MTask v Bool - readD :: (v p) -> MTask v Bool | pin p - -class pinMode v where - pinMode :: (v PinMode) (v p) -> MTask v () | pin p - declarePin :: p PinMode ((v p) -> Main (v a)) -> Main (v a) | pin p -\end{lstClean} - -\begin{lstClean}[label={lst:gpio_examples},caption={\Gls{GPIO} example in \gls{MTASK}.}] -task1 :: MTask v Int | mtask v -task1 = declarePin A3 PMInput \a3->{main=readA a3} +%\chapter{\texorpdfstring{\Glsxtrshort{TOP} for the \glsxtrshort{IOT}}{TOP for the IoT}}% +\subfile{4iot} -task2 :: MTask v Int | mtask v -task2 = declarePin D3 PMOutput \d3->{main=writeD d3 true} -\end{lstClean} - -\subsection{Task combinators} -Task combinators are used to combine multiple tasks into one to describe workflows. -There are three main types of task combinators, namely: -\begin{enumerate*} - \item Sequential combinators that execute tasks one after the other, possibly using the result of the left hand side. - \item Parallel combinators that execute tasks at the same time combining the result. - \item Miscellaneous combinators that change the semantics of a task---e.g.\ repeat it or delay execution. -\end{enumerate*} - -\subsubsection{Sequential} -Sequential task combination allows the right-hand side task to observe the left-hand side task value. -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{>>*.}. -This combinator has a single task on the left-hand side and a list of \emph{task continuations} on the right-hand side. -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. -\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. -\cleaninline{>>|.} is a shorthand for the sequence operation, if the left-hand side is stable, it continues with the right-hand side task. -The \cleaninline{>>~.} and \cleaninline{>>..} combinators are variants of the ones above that ignore the stability and continue on an unstable value as well. - -\begin{lstClean}[label={lst:mtask_sequential},caption={Sequential task combinators in \gls{MTASK}.}] -class step v | expr v where - (>>*.) infixl 1 :: (MTask v t) [Step v t u] -> MTask v u - (>>=.) infixl 0 :: (MTask v t) ((v t) -> MTask v u) -> MTask v u - (>>|.) infixl 0 :: (MTask v t) (MTask v u) -> MTask v u - (>>~.) infixl 0 :: (MTask v t) ((v t) -> MTask v u) -> MTask v u - (>>..) infixl 0 :: (MTask v t) (MTask v u) -> MTask v u - -:: Step v t u - = IfValue ((v t) -> v Bool) ((v t) -> MTask v u) - | IfStable ((v t) -> v Bool) ((v t) -> MTask v u) - | IfUnstable ((v t) -> v Bool) ((v t) -> MTask v u) - | Always (MTask v u) -\end{lstClean} - -\todo{more examples step?} - -The following listing shows an example of a step in action. -The \cleaninline{readPinBin} function produces an \gls{MTASK} task that classifies the value of an analogue pin into four bins. -It also shows that the nature of embedding allows the host language to be used as a macro language. -Furthermore - -\begin{lstClean}[label={lst:mtask_readpinbin},caption={Read an analog pin and bin the value in \gls{MTASK}.}] -readPinBin :: Int -> Main (MTask v Int) | mtask v -readPinBin lim = declarePin PMInput A2 \a2-> - { main = readA a2 >>*. - [ IfValue (\x->x <. lim) (\_->rtrn (lit bin)) - \\ lim <-[64,128,192,256] - & bin <- [0..]]} -\end{lstClean} - -\subsubsection{Parallel}\label{sssec:combinators_parallel} -The result of a parallel task combination is a compound that actually executes the tasks at the same time. - -There are two types of parallel task combinators (see \cref{lst:mtask_parallel}). -The conjunction combinator (\cleaninline{.&&.}) combines the result by putting the values from both sides in a tuple. -The stability of the task depends on the stability of both children. -If both children are stable, the result is stable, otherwise the result is unstable. -The disjunction combinator (\cleaninline{.\|\|.}) combines the results by picking the leftmost, most stable task. -The semantics are easily described using \gls{CLEAN} functions shown in \cref{lst:semantics_con,lst:semantics_dis}. - -\begin{figure}[ht] - \centering - \begin{subfigure}[t]{.5\textwidth} - \begin{lstClean}[caption={Semantics of the\\conjunction combinator.},label={lst:semantics_con}] -con :: (TaskValue a) (TaskValue b) - -> TaskValue (a, b) -con NoValue r = NoValue -con l NoValue = NoValue -con (Value l ls) (Value r rs) - = Value (l, r) (ls && rs) - - \end{lstClean} - \end{subfigure}% - \begin{subfigure}[t]{.5\textwidth} - \begin{lstClean}[caption={Semantics of the\\disjunction combinator.},label={lst:semantics_dis}] -dis :: (TaskValue a) (TaskValue a) - -> TaskValue a -dis NoValue r = r -dis l NoValue = l -dis (Value l ls) (Value r rs) - | rs = Value r True - | otherwise = Value l ls - \end{lstClean} - \end{subfigure} -\end{figure} - -\begin{lstClean}[label={lst:mtask_parallel},caption={Parallel task combinators in \gls{MTASK}.}] -class (.&&.) infixr 4 v :: (MTask v a) (MTask v b) -> MTask v (a, b) -class (.||.) infixr 3 v :: (MTask v a) (MTask v a) -> MTask v a -\end{lstClean} - -\Cref{lst:mtask_parallel_example} gives an example of the parallel task combinator. -This program will read two pins at the same time, returning when one of the pins becomes \arduinoinline{HIGH}. -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. - -\begin{lstClean}[label={lst:mtask_parallel_example},caption={Parallel task combinator example in \gls{MTASK}.}] -task :: MTask v Bool -task = - declarePin D0 PMInput \d0-> - declarePin D1 PMInput \d1-> - let monitor pin = readD pin >>*. [IfValue (\x->x) \x->rtrn x] - In {main = monitor d0 .||. monitor d1} -\end{lstClean} - -\subsubsection{Repeat}\label{sec:repeat} -The \cleaninline{rpeat} combinator executes the child task. -If a stable value is observed, the task is reinstated. -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}. - -\begin{lstClean}[label={lst:mtask_repeat},caption={Repeat task combinators in \gls{MTASK}.}] -class rpeat v where - rpeat :: (MTask v a) -> MTask v a -\end{lstClean} - -To demonstrate the combinator, \cref{lst:mtask_repeat_example} show \cleaninline{rpeat} in use. -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. - -\begin{lstClean}[label={lst:mtask_repeat_example},caption={Exemplatory repeat task in \gls{MTASK}.}] -task :: MTask v Int | mtask v -task = - declarePin A1 PMInput \a1-> - declarePin A2 PMOutput \a2-> - {main = rpeat (readA a1 >>~. writeA a2 >>|. delay (lit 1000))} -\end{lstClean} - -\subsection{\texorpdfstring{\Glsxtrlongpl{SDS}}{Shared data sources}} -\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}). -Similar to peripherals (see \cref{sssec:peripherals}), they are constructed at the top level and are accessed through interaction tasks. -The \cleaninline{getSds} task yields the current value of the \gls{SDS} as an unstable value. -This behaviour is similar to the \cleaninline{watch} task in \gls{ITASK}. -Writing a new value to \pgls{SDS} is done using \cleaninline{setSds}. -This task yields the written value as a stable result after it is done writing. -Getting and immediately after setting \pgls{SDS} is not necessarily an \emph{atomic} operation in \gls{MTASK} because it is possible that another task accesses the \gls{SDS} in between. -To circumvent this issue, \cleaninline{updSds} is created, this task atomically updates the value of the \gls{SDS}. -The \cleaninline{updSds} task only guarantees atomicity within \gls{MTASK}. - -\begin{lstClean}[label={lst:mtask_sds},caption={\Glspl{SDS} in \gls{MTASK}.}] -:: Sds a // abstract -class sds v where - sds :: ((v (Sds t)) -> In t (Main (MTask v u))) -> Main (MTask v u) - getSds :: (v (Sds t)) -> MTask v t - setSds :: (v (Sds t)) (v t) -> MTask v t - updSds :: (v (Sds t)) ((v t) -> v t) -> MTask v t -\end{lstClean} - -\Cref{lst:mtask_sds_examples} shows an example using \glspl{SDS}. -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}. -In the \cleaninline{main} expression, this function is called twice and the results are combined using the parallel or combinator (\cleaninline{.||.}). -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} - -\begin{lstClean}[label={lst:mtask_sds_examples},caption={Examples with \glspl{SDS} in \gls{MTASK}.}] -task :: MTask v Int | mtask v -task = declarePin D3 PMInput \d3-> - declarePin D5 PMInput \d5-> - sds \share=0 - In fun \count=(\pin-> - readD pin - >>* [IfValue (\x->x) (\_->updSds (\x->x +. lit 1) share)] - >>| delay (lit 100) // debounce - >>| count pin) - In {main=count d3 .||. count d5} -\end{lstClean} +%\chapter{The \texorpdfstring{\gls{MTASK}}{mTask} \texorpdfstring{\glsxtrshort{DSL}}{DSL}}% +\subfile{lang} \chapter{Integration with \texorpdfstring{\gls{ITASK}}{iTask}}% \label{chp:integration_with_itask} @@ -790,6 +85,7 @@ IFL19 paper, bytecode instructieset~\cref{chp:bytecode_instruction_set} \section{Integration with \texorpdfstring{\gls{ITASK}}{iTask}} IFL18 paper stukken +% Green computing \subfile{green} \input{subfilepostamble}