methods.mtask.tex

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