methods.mtask.tex

   1 The \gls{mTask}-\gls{EDSL} is the basis on which the system is built. The
   2 \gls{mTask}-\gls{EDSL} was created by Koopman et al.\ to support several views
   3 such as an \gls{iTasks} simulation and a \gls{C}-code generator. The \gls{EDSL}
   4 was designed to generate a ready to compile \gls{TOP}-like system for
   5 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 given classes. The following sections show the details of the \gls{EDSL}
  11 that are used in this extension. The parts of the \gls{EDSL} that are not used
  12 will 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, solely be phantom types. A view is of
  19 the form \CI{v t r}. The first type variable will be the type of the view, the
  20 second type variable will be the type of the \gls{EDSL}-expression and the
  21 third type variable represents the role of the expression. Currently the role
  22 of the expressions form a hierarchy. The three roles and their hierarchy are
  23 shown in Listing~\ref{lst:exprhier}. This implies that everything is a
  24 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 in to 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 funcitons. 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 task or even
  66 themselves. Therefore there is no need for loop control flow functionality such
  67 as \emph{while} or \emph{for} constructions. The main control flow operators
  68 are the sequence operator and the \emph{if} statement. Both are shown in
  69 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
  72 statement. The listing includes examples of implementations that illustrate
  73 this dependency.
  74
  75 The sequence operator is very straightforward and just ties
  76 the two expressions 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 builtin \glspl{LED}.
  96 The classes facilitating this are shown in Listing~\ref{lst:sdsio}. In this way
  97 the assignment is the same for every assignable entity.
  98
  99 \begin{lstlisting}[%
 100         label={lst:sdsio},caption={Input/Output classes}]
 101 :: DigitalPin = D0 | D1 | D2 | D3 | D4 | D5 |D6 | D7 | D8 | D9 | D10 | D11 | D12 | D13
 102 :: AnalogPin  = A0 | A1 | A2 | A3 | A4 | A5
 103 :: UserLED = LED1 | LED2 | LED3
 104
 105 class dIO v where dIO :: DigitalPin -> v Bool Upd
 106 class aIO v where aIO :: AnalogPin -> v Int Upd
 107 class analogRead v where
 108   analogRead :: AnalogPin -> v Int Expr
 109   analogWrite :: AnalogPin (v Int p) -> v Int Expr
 110 class digitalRead v where
 111   digitalRead :: DigitalPin -> v Bin Expr
 112   digitalWrite :: DigitalPin (v Bool p) -> v Int Expr
 113
 114 :: UserLED = LED1 | LED2 | LED3
 115 class userLed v where
 116   ledOn  :: (v UserLED q) -> (v () Stmt)
 117   ledOff :: (v UserLED q) -> (v () Stmt)
 118
 119 class assign v where
 120   (=.) infixr 2 :: (v t Upd) (v t p) -> v t Expr | ...
 121 \end{lstlisting}
 122
 123 A way of storing data in \glspl{mTask} is using \glspl{SDS}. \glspl{SDS} serve
 124 as variables in the \gls{mTask} and maintain their value across executions.
 125 The classes associated with \glspl{SDS} are listed in
 126 Listing~\ref{lst:sdsclass}. The \CI{Main} type is introduced to box an
 127 \gls{mTask} and make it recognizable by the type system.
 128
 129 \begin{lstlisting}[%
 130         label={lst:sdsclass},caption={\glspl{SDS} in \gls{mTask}}]
 131 :: In a b = In infix 0 a b
 132 :: Main a = {main :: a}
 133
 134 class sds v where
 135   sds :: ((v t Upd)->In t (Main (v c s))) -> (Main (v c s)) | ...
 136 \end{lstlisting}
 137
 138 \section{Semantics}
 139 The \gls{C}-backend of the \gls{mTask}-system has an engine that is generated
 140 alongside the code for the \glspl{Task}. This engine will execute the
 141 \glspl{mTask} according to certain rules and semantics.
 142 \glspl{mTask} do not behave like functions but more like
 143 \gls{iTasks}-\glspl{Task}. An \gls{mTask} is queued when either his timer runs
 144 out or when it is started by another \gls{mTask}. When an \gls{mTask} is
 145 queued it does not block the execution but it will return immediately while
 146 the actual \gls{Task} will be executed some time in the future.
 147
 148 The \gls{iTasks}-backend simulates the \gls{C}-backend and thus uses the same
 149 semantics. This engine expressed in pseudocode is listed as
 150 Algorithm~\ref{lst:engine}. All the \glspl{Task} are inspected on their waiting
 151 time. When the waiting time has not passed; the delta is subtracted and the
 152 task gets pushed to the end of the queue. When the waiting has surpassed they are
 153 executed. When an \gls{mTask} wants to queue another \gls{mTask} it can just
 154 append it to the queue.
 155
 156 \begin{algorithm}[H]
 157         \KwData{\textbf{queue} queue, \textbf{time} $t, t_p$}
 158
 159         $t\leftarrow\text{now}()$\;
 160         \Begin{
 161                 \While{true}{
 162                         $t_p\leftarrow t$\;
 163                         $t\leftarrow\text{now}()$\;
 164                         \If{notEmpty$($queue$)$}{
 165                                 $task\leftarrow \text{queue.pop}()$\;
 166                                 $task$.wait $\leftarrow task$.wait $-(t-t_p)$\;
 167                                 \eIf{$task.wait>t_0$}{
 168                                         queue.append$(task)$\;
 169                                 }{
 170                                         run\_task$(task)$\;
 171                                 }
 172                         }
 173                 }
 174         }
 175         \caption{Engine pseudocode for the \gls{C}- and
 176                 \gls{iTasks}-backend}\label{lst:engine}
 177 \end{algorithm}
 178
 179 To achieve this in the \gls{EDSL} a \gls{Task} clas are added that work in a
 180 similar fashion as the \texttt{sds} class. This class is listed in
 181 Listing~\ref{lst:taskclass}. \glspl{Task} can have an argument and always have
 182 to specify a delay or waiting time. The type signature of the \CI{mtask} is
 183 complex and therefore an example is given. The aforementioned Listing
 184 shows a simple specification containing one task that increments a value
 185 indefinitely every one seconds.
 186
 187 \begin{lstlisting}[label={lst:taskclass},%
 188         caption={The classes for defining tasks}]
 189 class mtask v a where
 190   task :: (((v delay r) a->v MTask Expr)->In (a->v u p) (Main (v t q))) -> Main (v t q) | ...
 191
 192 count = task \count = (\n.count (lit 1000) (n +. One)) In {main = count (lit 1000) Zero}
 193 \end{lstlisting}
 194
 195 \section{Example mTask}
 196 Some example \glspl{mTask} using almost all of the functionality are shown in
 197 Listing~\ref{lst:exmtask}. The \glspl{mTask} shown in the example do not belong
 198 to a particular view and therefore are of the type \CI{View t r}. The
 199 \CI{blink} \gls{mTask} show the classic \gls{Arduino} \emph{Hello World!}
 200 application that blinks a certain \gls{LED} every second. The \CI{thermostat}
 201 expression will enable a digital pin powering a cooling fan when the analog pin
 202 representing a temperature sensor is too high. \CI{thermostat`} shows the same
 203 expression but now using the assignment style \gls{GPIO} technique.
 204
 205 \begin{lstlisting}[%
 206         label={lst:exmtask},caption={Some example \glspl{mTask}}]
 207 blink = task \blink=(\x.
 208                 IF (x ==. lit True) (ledOn led) (ledOff led) :.
 209                 blink (lit 1000) (Not x)
 210         In {main=blink (lit 1000) True}
 211
 212 thermostat :: Main (View () Stmt)
 213 thermostat = {main =
 214   IF (analogRead A0 >. lit 50)
 215         ( digitalWrite D0 (lit True)  )
 216     ( digitalWrite D0 (lit False) )
 217   }
 218
 219 thermostat` :: Main (View () Stmt)
 220 thermostat` = let
 221   a0 = aIO A0
 222   d0 = dIO D0 in {main = IF (a0 >. lit 50) (d0 =. lit True) (d0 =. lit False) }
 223 \end{lstlisting}