methods.mtask.tex

   1 The \gls{mTask}-\gls{EDSL} is the language used in the system. The
   2 \gls{mTask}-\gls{EDSL} was created by Koopman et al.\ and supported several
   3 views such as an \gls{iTasks} simulation and a \gls{C}-code generator. The
   4 \gls{EDSL} was designed to generate a ready-to-compile \gls{TOP}-like program
   5 for microcontrollers such as the \gls{Arduino}~\cite{koopman_type-safe_nodate}%
   6 \cite{plasmeijer_shallow_2016}.
   7
   8 The \gls{mTask}-\gls{EDSL} is a shallowly embedded class based \gls{EDSL} and
   9 therefore it is very suitable to have a new backend that partly implements the
  10 classes given. The following sections show the details of the \gls{EDSL} that
  11 are used in this extension. The parts of the \gls{EDSL} that are not used will
  12 not be discussed and the details of those parts can be found in the cited
  13 literature.
  14
  15 A view for the \gls{mTask}-\gls{EDSL} is a type with kind \CI{*->*->*}%
  16 \footnote{A type with two free type variables.} that implements some of the
  17 classes given. The types do not have to be present as fields in the higher
  18 kinded view and can, and will most often, be exclusively phantom types. A view
  19 is of the form \CI{v t r}. The first type variable will be the type of the
  20 view. The second type variable will be the type of the \gls{EDSL}-expression
  21 and the third type variable represents the role of the expression. Currently
  22 the role of the expressions form a hierarchy. The three roles and their
  23 hierarchy are shown in Listing~\ref{lst:exprhier}. This implies that everything
  24 is a statement, only a \CI{Upd} and a \CI{Expr} are expressions. The \CI{Upd}
  25 restriction describes updatable expressions such as \gls{GPIO} pins and
  26 \glspl{SDS}.
  27
  28 \begin{lstlisting}[%
  29         label={lst:exprhier},caption={Expression role hierarchy}]
  30 :: Upd   = Upd
  31 :: Expr  = Expr
  32 :: Stmt  = Stmt
  33
  34 class isExpr a :: a -> Int
  35 instance isExpr Upd
  36 instance isExpr Expr
  37 \end{lstlisting}
  38
  39 \section{Expressions}
  40 Expressions in the \gls{mTask}-\gls{EDSL} are divided into two types, namely
  41 boolean expressions and arithmetic expressions. The class of arithmetic
  42 language constructs also contains the function \CI{lit} that lifts a
  43 host-language value into the \gls{EDSL} domain. All standard arithmetic
  44 functions are included in the \gls{EDSL} but are omitted in the example for
  45 brevity. Moreover, the class restrictions are only shown in the first functions
  46 and omitted in subsequent functions. Both the boolean expression and arithmetic
  47 expression classes are shown in Listing~\ref{lst:arithbool}.
  48
  49 \begin{lstlisting}[label={lst:arithbool},
  50         caption={Basic classes for expressions}]
  51 class arith v where
  52   lit           :: t -> v t Expr
  53   (+.) infixl 6 :: (v t p) (v t q) -> v t Expr          | +, zero t    & isExpr p & isExpr q
  54   (-.) infixl 6 :: (v t p) (v t q) -> v t Expr          | -, zero t    & ...
  55   ...
  56 class boolExpr v where
  57   Not           :: (v Bool p) -> v Bool Expr            | ...
  58   (&.) infixr 3 :: (v Bool p) (v Bool q) -> v Bool Expr | ...
  59   ...
  60   (==.) infix 4 :: (v a p) (v a q) -> v Bool Expr       | ==, toCode a & ...
  61 \end{lstlisting}
  62
  63 \section{Control flow}
  64 Looping of \glspl{Task} happens because \glspl{Task} are executed after waiting
  65 a specified amount of time or when they are launched by another \gls{Task} or
  66 even themselves. Therefore there is no need for loop control flow functionality
  67 such as \emph{while} or \emph{for} constructions. The main control flow
  68 operators are the sequence operator and the \emph{if} statement. Both are shown
  69 in Listing~\ref{lst:control}. The first class of \emph{If} statements describes
  70 the regular \emph{if} statement. The expressions given can have any role. The
  71 functional dependency on \CI{s} determines the return type of the statement.
  72 The listing includes examples of implementations that illustrate this
  73 dependency.
  74
  75 The sequence operator is very straightforward and its only function is to tie
  76 the together in sequence.
  77
  78 \begin{lstlisting}[%
  79         label={lst:control},caption={Control flow operators}]
  80 class If v q r ~s where
  81   If :: (v Bool p) (v t q) (v t r) -> v t s | ...
  82
  83 instance If Code Stmt Stmt Stmt
  84 instance If Code e    Stmt Stmt
  85 instance If Code Stmt e    Stmt
  86 instance If Code x    y    Expr
  87
  88 class seq v where
  89   (:.) infixr 0 :: (v t p) (v u q) -> v u Stmt | ...
  90 \end{lstlisting}
  91
  92 \section{Input/Output and class extensions}
  93 Values can be assigned to all expressions that have an \CI{Upd} role. Examples
  94 of such expressions are \glspl{SDS} and \gls{GPIO} pins. Moreover, class
  95 extensions can be created for specific peripherals such as built-in
  96 \glspl{LED}. The classes facilitating this are shown in
  97 Listing~\ref{lst:sdsio}. In this way the assignment is the same for every
  98 assignable entity.
  99
 100 \begin{lstlisting}[%
 101         label={lst:sdsio},caption={Input/Output classes}]
 102 :: DigitalPin = D0 | D1 | D2 | D3 | D4 | D5 |D6 | D7 | D8 | D9 | D10 | D11 | D12 | D13
 103 :: AnalogPin  = A0 | A1 | A2 | A3 | A4 | A5
 104 :: UserLED = LED1 | LED2 | LED3
 105
 106 class dIO v where dIO :: DigitalPin -> v Bool Upd
 107 class aIO v where aIO :: AnalogPin -> v Int Upd
 108 class analogRead v where
 109   analogRead :: AnalogPin -> v Int Expr
 110   analogWrite :: AnalogPin (v Int p) -> v Int Expr
 111 class digitalRead v where
 112   digitalRead :: DigitalPin -> v Bin Expr
 113   digitalWrite :: DigitalPin (v Bool p) -> v Int Expr
 114
 115 :: UserLED = LED1 | LED2 | LED3
 116 class userLed v where
 117   ledOn  :: (v UserLED q) -> (v () Stmt)
 118   ledOff :: (v UserLED q) -> (v () Stmt)
 119
 120 class assign v where
 121   (=.) infixr 2 :: (v t Upd) (v t p) -> v t Expr | ...
 122 \end{lstlisting}
 123
 124 A way of storing data in \glspl{mTask} is using \glspl{SDS}. \glspl{SDS} serve
 125 as variables in \gls{mTask} and maintain their value across executions.
 126 \glspl{SDS} can be used by multiple \glspl{Task} and can be used to share data.
 127 The classes associated with \glspl{SDS} are listed in
 128 Listing~\ref{lst:sdsclass}. The \CI{Main} type is introduced to box an
 129 \gls{mTask} and make it recognizable by the type system by separating programs
 130 and decorations such as \glspl{SDS}.
 131
 132 \begin{lstlisting}[%
 133         label={lst:sdsclass},caption={\glspl{SDS} in \gls{mTask}}]
 134 :: In a b = In infix 0 a b
 135 :: Main a = {main :: a}
 136
 137 class sds v where
 138   sds :: ((v t Upd)->In t (Main (v c s))) -> (Main (v c s)) | ...
 139 \end{lstlisting}
 140
 141 \section{Semantics}
 142 The \gls{C}-backend of the \gls{mTask}-system has an engine that is generated
 143 alongside the code for the \glspl{Task}. This engine will execute the
 144 \glspl{mTask} according to certain rules and semantics.
 145 \glspl{mTask} do not behave like functions but more like
 146 \gls{iTasks}-\glspl{Task}. An \gls{mTask} is queued when either its timer runs
 147 out or when it is launched by another \gls{mTask}. When an \gls{mTask} is
 148 queued it does not block the execution and it will return immediately while
 149 the actual \gls{Task} will be executed anytime in the future.
 150
 151 The \gls{iTasks}-backend simulates the \gls{C}-backend and thus uses the same
 152 semantics. This engine expressed in pseudocode is listed as
 153 Algorithm~\ref{lst:engine}. All the \glspl{Task} are inspected on their waiting
 154 time. When the waiting time has not passed; the delta is subtracted and the
 155 \gls{Task} gets pushed to the end of the queue. When the waiting has surpassed
 156 they are executed. When an \gls{mTask} wants to queue another \gls{mTask} it
 157 can just append it to the queue.
 158
 159 \begin{algorithm}[H]
 160         \KwData{\textbf{queue} queue, \textbf{time} $t, t_p$}
 161
 162         $t\leftarrow\text{now}()$\;
 163         \Begin{
 164                 \While{true}{
 165                         $t_p\leftarrow t$\;
 166                         $t\leftarrow\text{now}()$\;
 167                         \If{notEmpty$($queue$)$}{
 168                                 $task\leftarrow \text{queue.pop}()$\;
 169                                 $task$.wait $\leftarrow task$.wait $-(t-t_p)$\;
 170                                 \eIf{$task.wait>t_0$}{
 171                                         queue.append$(task)$\;
 172                                 }{
 173                                         run\_task$(task)$\;
 174                                 }
 175                         }
 176                 }
 177         }
 178         \caption{Engine pseudocode for the \gls{C}- and
 179                 \gls{iTasks}-backend}\label{lst:engine}
 180 \end{algorithm}
 181
 182 To achieve this in the \gls{EDSL} a \gls{Task} class is added that work in a
 183 similar fashion as the \texttt{sds} class. This class is listed in
 184 Listing~\ref{lst:taskclass}. \glspl{Task} can have an argument and always have
 185 to specify a delay or waiting time. The type signature of the \CI{mtask} is
 186 complex and therefore an example is given. The aforementioned Listing
 187 shows a simple specification containing one \gls{Task} that increments a value
 188 indefinitely every one seconds.
 189
 190 \begin{lstlisting}[label={lst:taskclass},%
 191         caption={The classes for defining \glspl{Task}}]
 192 class mtask v a where
 193   task :: (((v delay r) a->v MTask Expr)->In (a->v u p) (Main (v t q))) -> Main (v t q) | ...
 194
 195 count = task \count = (\n.count (lit 1000) (n +. One)) In {main = count (lit 1000) Zero}
 196 \end{lstlisting}
 197
 198 \section{Example mTask}
 199 Some example \glspl{mTask} using almost all of their functionality are shown in
 200 Listing~\ref{lst:exmtask}. The \glspl{mTask} shown in the example do not belong
 201 to a particular view and therefore are of the type \CI{View t r}. The
 202 \CI{blink} \gls{mTask} show the classic \gls{Arduino} \emph{Hello World!}
 203 application that blinks a certain \gls{LED} every second. The \CI{thermostat}
 204 expression will enable a digital pin powering a cooling fan when the analog pin
 205 representing a temperature sensor is too high. \CI{thermostat`} shows the same
 206 expression but now using the assignment style \gls{GPIO} technique. The
 207 \CI{thermostat} example also show that it is not necessary to run everything as
 208 a \CI{task}. The main program code can also just consist of the contents of the
 209 root \CI{main} itself.
 210
 211 \begin{lstlisting}[%
 212         label={lst:exmtask},caption={Some example \glspl{mTask}}]
 213 blink = task \blink=(\x.
 214                 IF (x ==. lit True) (ledOn led) (ledOff led) :.
 215                 blink (lit 1000) (Not x)
 216         In {main=blink (lit 1000) True}
 217
 218 thermostat :: Main (View () Stmt)
 219 thermostat = {main =
 220   IF (analogRead A0 >. lit 50)
 221         ( digitalWrite D0 (lit True)  )
 222     ( digitalWrite D0 (lit False) )
 223   }
 224
 225 thermostat` :: Main (View () Stmt)
 226 thermostat` = let
 227   a0 = aIO A0
 228   d0 = dIO D0 in {main = IF (a0 >. lit 50) (d0 =. lit True) (d0 =. lit False) }
 229 \end{lstlisting}