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 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 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 \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 the \gls{mTask} and maintain their value across executions.
 126 The classes associated with \glspl{SDS} are listed in
 127 Listing~\ref{lst:sdsclass}. The \CI{Main} type is introduced to box an
 128 \gls{mTask} and make it recognizable by the type system.
 129
 130 \begin{lstlisting}[%
 131         label={lst:sdsclass},caption={\glspl{SDS} in \gls{mTask}}]
 132 :: In a b = In infix 0 a b
 133 :: Main a = {main :: a}
 134
 135 class sds v where
 136   sds :: ((v t Upd)->In t (Main (v c s))) -> (Main (v c s)) | ...
 137 \end{lstlisting}
 138
 139 \section{Semantics}
 140 The \gls{C}-backend of the \gls{mTask}-system has an engine that is generated
 141 alongside the code for the \glspl{Task}. This engine will execute the
 142 \glspl{mTask} according to certain rules and semantics.
 143 \glspl{mTask} do not behave like functions but more like
 144 \gls{iTasks}-\glspl{Task}. An \gls{mTask} is queued when either its timer runs
 145 out or when it is launched by another \gls{mTask}. When an \gls{mTask} is
 146 queued it does not block the execution and it will return immediately while
 147 the actual \gls{Task} will be executed anytime in the future.
 148
 149 The \gls{iTasks}-backend simulates the \gls{C}-backend and thus uses the same
 150 semantics. This engine expressed in pseudocode is listed as
 151 Algorithm~\ref{lst:engine}. All the \glspl{Task} are inspected on their waiting
 152 time. When the waiting time has not passed; the delta is subtracted and the
 153 \gls{Task} gets pushed to the end of the queue. When the waiting has surpassed
 154 they are executed. When an \gls{mTask} wants to queue another \gls{mTask} it
 155 can just append it to the queue.
 156
 157 \begin{algorithm}[H]
 158         \KwData{\textbf{queue} queue, \textbf{time} $t, t_p$}
 159
 160         $t\leftarrow\text{now}()$\;
 161         \Begin{
 162                 \While{true}{
 163                         $t_p\leftarrow t$\;
 164                         $t\leftarrow\text{now}()$\;
 165                         \If{notEmpty$($queue$)$}{
 166                                 $task\leftarrow \text{queue.pop}()$\;
 167                                 $task$.wait $\leftarrow task$.wait $-(t-t_p)$\;
 168                                 \eIf{$task.wait>t_0$}{
 169                                         queue.append$(task)$\;
 170                                 }{
 171                                         run\_task$(task)$\;
 172                                 }
 173                         }
 174                 }
 175         }
 176         \caption{Engine pseudocode for the \gls{C}- and
 177                 \gls{iTasks}-backend}\label{lst:engine}
 178 \end{algorithm}
 179
 180 To achieve this in the \gls{EDSL} a \gls{Task} class is added that work in a
 181 similar fashion as the \texttt{sds} class. This class is listed in
 182 Listing~\ref{lst:taskclass}. \glspl{Task} can have an argument and always have
 183 to specify a delay or waiting time. The type signature of the \CI{mtask} is
 184 complex and therefore an example is given. The aforementioned Listing
 185 shows a simple specification containing one \gls{Task} that increments a value
 186 indefinitely every one seconds.
 187
 188 \begin{lstlisting}[label={lst:taskclass},%
 189         caption={The classes for defining \glspl{Task}}]
 190 class mtask v a where
 191   task :: (((v delay r) a->v MTask Expr)->In (a->v u p) (Main (v t q))) -> Main (v t q) | ...
 192
 193 count = task \count = (\n.count (lit 1000) (n +. One)) In {main = count (lit 1000) Zero}
 194 \end{lstlisting}
 195
 196 \section{Example mTask}
 197 Some example \glspl{mTask} using almost all of their functionality are shown in
 198 Listing~\ref{lst:exmtask}. The \glspl{mTask} shown in the example do not belong
 199 to a particular view and therefore are of the type \CI{View t r}. The
 200 \CI{blink} \gls{mTask} show the classic \gls{Arduino} \emph{Hello World!}
 201 application that blinks a certain \gls{LED} every second. The \CI{thermostat}
 202 expression will enable a digital pin powering a cooling fan when the analog pin
 203 representing a temperature sensor is too high. \CI{thermostat`} shows the same
 204 expression but now using the assignment style \gls{GPIO} technique.
 205
 206 \begin{lstlisting}[%
 207         label={lst:exmtask},caption={Some example \glspl{mTask}}]
 208 blink = task \blink=(\x.
 209                 IF (x ==. lit True) (ledOn led) (ledOff led) :.
 210                 blink (lit 1000) (Not x)
 211         In {main=blink (lit 1000) True}
 212
 213 thermostat :: Main (View () Stmt)
 214 thermostat = {main =
 215   IF (analogRead A0 >. lit 50)
 216         ( digitalWrite D0 (lit True)  )
 217     ( digitalWrite D0 (lit False) )
 218   }
 219
 220 thermostat` :: Main (View () Stmt)
 221 thermostat` = let
 222   a0 = aIO A0
 223   d0 = dIO D0 in {main = IF (a0 >. lit 50) (d0 =. lit True) (d0 =. lit False) }
 224 \end{lstlisting}