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 is 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. Thus,
  19 views are of the form: \CI{:: v t r = ...}.  The first type variable will be
  20 the type of the view. The second type variable will be the type of the
  21 \gls{EDSL}-expression and the third type variable represents the role of the
  22 expression. Currently the role of the expressions form a hierarchy. The three
  23 roles and their hierarchy are shown in Listing~\ref{lst:exprhier}. This implies
  24 that everything is a statement, only a \CI{Upd} and a \CI{Expr} are
  25 expressions. The \CI{Upd} restriction describes updatable expressions such as
  26 \gls{GPIO} pins and \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 are omitted in subsequent functions. Both the boolean expression and
  47 arithmetic 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 straightforward and its only function is to tie
  76 two expressions together. The left expression is executed first, followed by
  77 the right expression.
  78
  79 \begin{lstlisting}[%
  80         label={lst:control},caption={Control flow operators}]
  81 class If v q r ~s where
  82   If :: (v Bool p) (v t q) (v t r) -> v t s | ...
  83
  84 instance If Code Stmt Stmt Stmt
  85 instance If Code e    Stmt Stmt
  86 instance If Code Stmt e    Stmt
  87 instance If Code x    y    Expr
  88
  89 class seq v where
  90   (:.) infixr 0 :: (v t p) (v u q) -> v u Stmt | ...
  91 \end{lstlisting}
  92
  93 \section{Input/Output and class extensions}
  94 Values can be assigned to all expressions that have an \CI{Upd} role. Examples
  95 of such expressions are \glspl{SDS} and \gls{GPIO} pins. Moreover, class
  96 extensions can be created for specific peripherals such as built-in
  97 \glspl{LED}. The classes facilitating this are shown in
  98 Listing~\ref{lst:sdsio}. In this way the assignment is the same for every
  99 assignable entity.
 100
 101 \begin{lstlisting}[%
 102         label={lst:sdsio},caption={Input/Output classes}]
 103 :: DigitalPin = D0 | D1 | D2 | D3 | D4 | D5 |D6 | D7 | D8 | D9 | D10 | D11 | D12 | D13
 104 :: AnalogPin  = A0 | A1 | A2 | A3 | A4 | A5
 105 :: UserLED = LED1 | LED2 | LED3
 106
 107 class dIO v where dIO :: DigitalPin -> v Bool Upd
 108 class aIO v where aIO :: AnalogPin -> v Int Upd
 109 class analogRead v where
 110   analogRead :: AnalogPin -> v Int Expr
 111   analogWrite :: AnalogPin (v Int p) -> v Int Expr
 112 class digitalRead v where
 113   digitalRead :: DigitalPin -> v Bin Expr
 114   digitalWrite :: DigitalPin (v Bool p) -> v Int Expr
 115
 116 :: UserLED = LED1 | LED2 | LED3
 117 class userLed v where
 118   ledOn  :: (v UserLED q) -> (v () Stmt)
 119   ledOff :: (v UserLED q) -> (v () Stmt)
 120
 121 class assign v where
 122   (=.) infixr 2 :: (v t Upd) (v t p) -> v t Expr | ...
 123 \end{lstlisting}
 124
 125 A way of storing data in \glspl{mTask} is using \glspl{SDS}. \glspl{SDS} serve
 126 as variables in \gls{mTask} and maintain their value across executions.
 127 \glspl{SDS} can be used by multiple \glspl{Task} and can be used to share data.
 128 The classes associated with \glspl{SDS} are listed in
 129 Listing~\ref{lst:sdsclass}. The \CI{Main} type is introduced to box an
 130 \gls{mTask} and make it recognizable by the type system by separating programs
 131 and decorations such as \glspl{SDS}.
 132
 133 \begin{lstlisting}[%
 134         label={lst:sdsclass},caption={\glspl{SDS} in \gls{mTask}}]
 135 :: In a b = In infix 0 a b
 136 :: Main a = {main :: a}
 137
 138 class sds v where
 139   sds :: ((v t Upd)->In t (Main (v c s))) -> (Main (v c s)) | ...
 140 \end{lstlisting}
 141
 142 \section{Semantics}
 143 The \gls{C}-backend of the \gls{mTask}-system has an engine that is generated
 144 alongside the code for the \glspl{Task}. This engine will execute the
 145 \glspl{mTask} according to certain rules and semantics.
 146 \glspl{mTask} do not behave like functions but more like
 147 \gls{iTasks}-\glspl{Task}. An \gls{mTask} is queued when either its timer runs
 148 out or when it is launched by another \gls{mTask}. When an \gls{mTask} is
 149 queued it does not block the execution and it will return immediately while
 150 the actual \gls{Task} will be executed anytime in the future.
 151
 152 The \gls{iTasks}-backend simulates the \gls{C}-backend and thus uses the same
 153 semantics. This engine expressed in pseudocode is listed as
 154 Algorithm~\ref{lst:engine}. All the \glspl{Task} are inspected on their waiting
 155 time. When the waiting time has not passed; the delta is subtracted and the
 156 \gls{Task} gets pushed to the end of the queue. When the waiting has surpassed
 157 they are executed. When an \gls{mTask} opts to queue another \gls{mTask} it
 158 can just append it to the queue.
 159
 160 ~\\
 161 \begin{algorithm}[H]
 162         \KwData{\textbf{queue} queue, \textbf{time} $t, t_p$}
 163
 164         $t\leftarrow\text{now}()$\;
 165         \Begin{
 166                 \While{true}{
 167                         $t_p\leftarrow t$\;
 168                         $t\leftarrow\text{now}()$\;
 169                         \If{notEmpty$($queue$)$}{
 170                                 $task\leftarrow \text{queue.pop}()$\;
 171                                 $task$.wait $\leftarrow task$.wait $-(t-t_p)$\;
 172                                 \eIf{$task.wait>t_0$}{
 173                                         queue.append$(task)$\;
 174                                 }{
 175                                         run\_task$(task)$\;
 176                                 }
 177                         }
 178                 }
 179         }
 180         \caption{Engine pseudocode for the \gls{C}- and
 181                 \gls{iTasks}-view}\label{lst:engine}
 182 \end{algorithm}
 183 ~\\
 184
 185 To achieve this in the \gls{EDSL} a \gls{Task} class is added that work in a
 186 similar fashion as the \texttt{sds} class. This class is listed in
 187 Listing~\ref{lst:taskclass}. \glspl{Task} can have an argument and always have
 188 to specify a delay or waiting time. The type signature of the \CI{mtask} is
 189 complex and therefore an example is given. The aforementioned Listing
 190 shows a simple specification containing one \gls{Task} that increments a value
 191 indefinitely every one seconds.
 192
 193 \begin{lstlisting}[label={lst:taskclass},%
 194         caption={The classes for defining \glspl{Task}}]
 195 class mtask v a where
 196   task :: (((v delay r) a->v MTask Expr)->In (a->v u p) (Main (v t q))) -> Main (v t q) | ...
 197
 198 count = task \count = (\n.count (lit 1000) (n +. One)) In {main = count (lit 1000) Zero}
 199 \end{lstlisting}
 200
 201 \section{Example mTask}
 202 Some example \glspl{mTask} using almost all of their functionality are shown in
 203 Listing~\ref{lst:exmtask}. The \glspl{mTask} shown in the example do not belong
 204 to a particular view and therefore are of the type \CI{View t r}. The
 205 \CI{blink} \gls{mTask} show the classic \gls{Arduino} \emph{Hello World!}
 206 application that blinks a certain \gls{LED} every second. The \CI{thermostat}
 207 expression will enable a digital pin powering a cooling fan when the analog pin
 208 representing a temperature sensor is too high. \CI{thermostat`} shows the same
 209 expression but now using the assignment style \gls{GPIO} technique. The
 210 \CI{thermostat} example also shows that it is not necessary to run everything
 211 as a \CI{task}. The main program code can also just consist of the contents of
 212 the root \CI{main} itself.
 213
 214 \begin{lstlisting}[%
 215         label={lst:exmtask},caption={Some example \glspl{mTask}}]
 216 blink = task \blink=(\x.
 217                 IF (x ==. lit True) (ledOn led) (ledOff led) :.
 218                 blink (lit 1000) (Not x)
 219         In {main=blink (lit 1000) True}
 220
 221 thermostat :: Main (View () Stmt)
 222 thermostat = {main =
 223   IF (analogRead A0 >. lit 50)
 224         ( digitalWrite D0 (lit True)  )
 225     ( digitalWrite D0 (lit False) )
 226   }
 227
 228 thermostat` :: Main (View () Stmt)
 229 thermostat` = let
 230   a0 = aIO A0
 231   d0 = dIO D0 in {main = IF (a0 >. lit 50) (d0 =. lit True) (d0 =. lit False) }
 232 \end{lstlisting}