+%chktex-file 17
\documentclass[../thesis.tex]{subfiles}
\input{subfilepreamble}
+\setcounter{chapter}{6}
+
\begin{document}
\input{subfileprefix}
-
-\chapter{Integration with \texorpdfstring{\gls{ITASK}}{iTask}}%
+\chapter{Integration of mTask and iTask}%
\label{chp:integration_with_itask}
\begin{chapterabstract}
- This chapter shows the integration of \gls{MTASK} with \gls{ITASK} by showing:
+ This chapter shows the integration of \gls{MTASK} and \gls{ITASK} by showing:
\begin{itemize}
- \item an architectural overview of \gls{MTASK};
- \item on the interface for connecting devices;
+ \item an architectural overview of \gls{MTASK} applications;
+ \item the interface for connecting devices;
\item the interface for lifting \gls{MTASK} tasks to \gls{ITASK} tasks;
- \item and interface for lifting \gls{ITASK} \glspl{SDS} to \gls{MTASK} \glspl{SDS}.
+ \item the interface for lowering \gls{ITASK} \glspl{SDS} to \gls{MTASK} \glspl{SDS};
+ \item and a non-trivial home automation example application using all integration mechanisms;
\end{itemize}
\end{chapterabstract}
-The \gls{MTASK} language is a multi-view \gls{DSL}, i.e.\ there are multiple interpretations possible for a single \gls{MTASK} term.
-Using the byte code compiler (\cleaninline{BCInterpret}) \gls{DSL} interpretation, \gls{MTASK} tasks can be fully integrated in \gls{ITASK}.
-They are executed as if they are regular \gls{ITASK} tasks and they communicate may access \glspl{SDS} from \gls{ITASK} as well.
-\Gls{MTASK} devices contain a domain-specific \gls{OS} (\gls{RTS}) and are little \gls{TOP} engines in their own respect, being able to execute tasks.
+The \gls{MTASK} system is a \gls{TOP} \gls{DSL} for edge devices.
+It is a multi-view \gls{DSL}, there are multiple interpretations possible for a single \gls{MTASK} term.
+The main interpretation of \gls{MTASK} terms is the byte code compiler, \cleaninline{:: BCInterpret a}.
+When using this interpretation and a few integration functions, \gls{MTASK} tasks are fully integrated in \gls{ITASK}.
+They execute as regular \gls{ITASK} tasks and they can access \glspl{SDS} from \gls{ITASK}.
+Devices in the \gls{MTASK} system are set up with a domain-specific \gls{OS} and become little \gls{TOP} engines in their own respect, being able to execute tasks.
+
\Cref{fig:mtask_integration} shows the architectural layout of a typical \gls{IOT} system created with \gls{ITASK} and \gls{MTASK}.
The entire system is written as a single \gls{CLEAN} specification where multiple tasks are executed at the same time.
Tasks can access \glspl{SDS} according to many-to-many communication and multiple clients can work on the same task.
-Devices are integrated into the system using the \cleaninline{withDevice} function (see \cref{sec:withdevice}).
+The diagram contains three labelled arrows that denote the integration functions between \gls{ITASK} and \gls{MTASK}.
+Devices are connected to the system using the \cleaninline{withDevice} function (see \cref{sec:withdevice}).
Using \cleaninline{liftmTask}, \gls{MTASK} tasks are lifted to a device (see \cref{sec:liftmtask}).
-\Gls{ITASK} \glspl{SDS} are lifted to the \gls{MTASK} device using \cleaninline{liftsds} (see \cref{sec:liftmtask}).
+\glspl{SDS} from \gls{ITASK} are lowered to the \gls{MTASK} device using \cleaninline{lowerSds} (see \cref{sec:liftsds}).
+\todo[inline]{mTask device\textsubscript{n} naar hfstk 5? Uitleg over taken en sensoren en \ldots? evt.\ zelfs naar intro hmmm?}
+\todo[inline]{Benoem dat er meerdere devices kunnen zijn en meerdere tasks op één device, en verwijs naar 6.5}
-\begin{figure}[ht]
+\begin{figure}
\centering
\includestandalone{mtask_integration}
- \caption{\Gls{MTASK}'s integration with \gls{ITASK}.}%
+ \caption{An architectural overview of an \imtask{} application.}%
\label{fig:mtask_integration}
\end{figure}
-\section{Devices}\label{sec:withdevice}
-When interpreted by the byte code compiler view, an \gls{MTASK} task produces a compiler.
-This compiler is exceuted at run time so that the resulting byte code can be sent to an edge device.
-All communication with this device happens through a so-called \emph{channels} \gls{SDS}.
-The channels contain three fields, a queue of messages that are received, a queue of messages to send and a stop flag.
+\section{Connecting edge devices}\label{sec:withdevice}
+Edge devices in an \gls{MTASK} application are always coordinated by a server.
+This means that they wait for a server to take initiative, set up a connection, and send the work.
+The heavy lifting of connecting an \gls{MTASK} device to an \gls{ITASK} server is done with the \cleaninline{withDevice} \gls{ITASK} function.
+This function has two parameters, a communication specification, and a function using a device handle.
+The device handle is required to interact with \gls{MTASK} devices, e.g.\ lift tasks.
+By using \gls{HOAS} like this, setting up and tearing down the connection to the device is fully controlled.
+
+All communication with a device happens through a so-called \emph{channels} \gls{SDS}.
+The channels contain three fields, a queue of messages that are received, a queue of messages to send, and a stop flag.
Every communication method that implements the \cleaninline{channelSync} class can provide the communication with an \gls{MTASK} device.
-As of now, serial port communication, direct \gls{TCP} communication and \gls{MQTT} over \gls{TCP} are supported as communication providers.
-The \cleaninline{withDevice} function transforms a communication provider and a task that does something with this device to an \gls{ITASK} task.
-Internally, the task sets up the communication, exchanges specifications, executes the inner task while handling errors, and finally cleans up after closing.
-\Cref{lst:mtask_device} shows the types and interface to connecting devices.
+At the time of writing, serial port, direct \gls{TCP}, and \gls{MQTT} over \gls{TCP} are supported communication methods (see \cref{lst:connection_types}).
+Internally, the \cleaninline{withDevice} task sets up the communication, exchanges specifications with the device, executes the inner task while handling errors, and finally cleans up after closing.
+\Cref{lst:mtask_device} shows the types and interface for connecting devices.
\begin{lstClean}[label={lst:mtask_device},caption={Device communication interface in \gls{MTASK}.}]
:: MTDevice //abstract
class channelSync a :: a (Shared sds Channels) -> Task () | RWShared sds
-withDevice :: a (MTDevice -> Task b) -> Task b | iTask b & channelSync, iTask a
+withDevice :: a (MTDevice -> Task b)
+ -> Task b | iTask b & channelSync, iTask a
+\end{lstClean}
+
+\subsection{Implementation}
+\Cref{lst:pseudo_withdevice} shows a pseudocode implementation of the \cleaninline{withDevice} function.
+The \cleaninline{MTDevice} abstract type is internally represented as three \gls{ITASK} \gls{SDS} that contain all the current information about the tasks.
+The first \gls{SDS} is the information about the \gls{RTS} of the device, i.e.\ metadata on the tasks that are executing, the hardware specification and capabilities, and a list of fresh task identifiers.
+The second \gls{SDS} is a map storing downstream \gls{SDS} updates.
+When a lowered \gls{SDS} is updated on the device, a message is sent to the server.
+This message is initially queued in the map in order to properly handle multiple updates asynchronously.
+Finally, the \cleaninline{MTDevices} type contains the communication channels.
+
+The \cleaninline{withDevice} task itself first constructs the \glspl{SDS} using the \gls{ITASK} function \cleaninline{withShared}.
+Then, it performs the following four tasks in parallel to monitor the edge device.
+\begin{enumerate}
+ \item The channels are synchronised using the overloaded \cleaninline{channelSync} function.
+ Errors that occur here are converted to the proper \gls{MTASK} or \gls{ITASK} exception.
+ \item The shutdown flag of the channels is watched.
+ If the connection is lost with the device unexpectedly, an \gls{MTASK} exception is thrown.
+ \item The received messages in the channels are watched and processed.
+ Depending on the type of message, either the device information \gls{SDS} is updated, or the \gls{SDS} update is added to the lowered \gls{SDS} updates \gls{SDS}.
+ \item A request for a specification is sent.
+ Once the specification is received, the device task is run.
+ The task value of this device task is then used as the task value of the \cleaninline{withDevice} task.
+\end{enumerate}
+
+\begin{lstClean}[caption={Pseudocode for the \texttt{withDevice} function in \gls{MTASK}.},label={lst:pseudo_withdevice}]
+withDevice :: a (MTDevice -> Task b) -> Task b | ...
+withDevice spec deviceTask =
+ withShared default \dev->
+ withShared newMap \sdsupdates->
+ withShared ([], [MTTSpecRequest], False) \channels->
+ parallel
+ [ channelSync spec channels
+ , watchForShutdown channels
+ , watchChannelMessages dev channels
+ , waitForSpecification
+ >>| deviceTask (MTDevice dev sdsupdates channels)
+ >>* [OnValue $ ifStable $ \_->issueShutdown]
+ ]
+\end{lstClean}
+
+If at any stage an unrecoverable device error occurs, an \gls{ITASK} exception is thrown in the \cleaninline{withDevice} task.
+This exception can be caught in order to devise fail-safe mechanisms.
+For example, if a device fails, the task can be sent to another device as can be seen in \cref{lst:failover}.
+This function executes an \gls{MTASK} task on a pool of devices connected through \gls{TCP}.
+If a device error occurs during execution, the next device in the pool is tried until the pool is exhausted.
+If another type of error occurs, it is re-thrown for a parent task to catch.
+
+\begin{lstClean}[caption={An \gls{MTASK} failover combinator.},label={lst:failover}]
+ failover :: [TCPSettings] (Main (MTask BCInterpret a)) -> Task a
+ failover [] _ = throw "Exhausted device pool"
+ failover [d:ds] mtask = try (withDevice d (liftmTask mtask)) except
+ where except MTEUnexpectedDisconnect = failover ds mtask
+ except e = throw e
\end{lstClean}
-\section{Lifting tasks}\label{sec:liftmtask}
-Once the connection with the device is established, \gls{MTASK} tasks can be lifted to \gls{MTASK} tasks using the \cleaninline{liftmTask} family of functions (see \cref{lst:liftmtask}).
-Given an \gls{MTASK} task in the \cleaninline{BCInterpret} view and a device obtained from \cleaninline{withDevice}, an \gls{ITASK} task is returned.
-This \gls{ITASK} task tethers the \gls{MTASK} task that is executed on the microcontroller.
-Hence, when for example observing the task value, the actual task value from the microcontroller is observed.
+\section{Lifting mTask tasks}\label{sec:liftmtask}
+Once the connection with the device is established, \gls{MTASK} tasks are lifted to \gls{ITASK} tasks using the \cleaninline{liftmTask} function (see \cref{lst:liftmtask}).
+Given an \gls{MTASK} task in the \cleaninline{BCInterpret} view and a device handle obtained from \cleaninline{withDevice}, an \gls{ITASK} task is returned.
+This \gls{ITASK} task proxies the \gls{MTASK} task that is executed on the microcontroller.
+So, when another task observes the task value, the actual task value from the microcontroller is observed.
\begin{lstClean}[label={lst:liftmtask},caption={The interface for lifting \gls{MTASK} tasks to \gls{ITASK} tasks.}]
-liftmTask :: (Main (MTask BCInterpret u)) MTDevice -> Task u | iTask u
+liftmTask :: (Main (MTask BCInterpret a)) MTDevice -> Task a | iTask a
+\end{lstClean}
+
+\subsection{Implementation}
+\Cref{lst:liftmTask_pseudo} shows the pseudocode for the \cleaninline{liftmTask} implementation
+The first argument is the task and the second argument is the device which is an \gls{ADT} containing the \glspl{SDS} referring to the device information, the \gls{SDS} update queue, and the channels.
+First a fresh identifier for the task is generated using the device state.
+With this identifier, the cleanup hook can be installed.
+This is done to assure the task is removed from the edge device if the \gls{ITASK} task coordinating it is destroyed.
+Tasks in \gls{ITASK} are destroyed when for example it is executed in parallel with another task and the parallel combinator terminates, or when the condition to step holds in a sequential task combination.
+Then the \gls{MTASK} compiler is invoked, its only argument besides the task is a function doing something with the results of the compilation, i.e.\ the lowered \glspl{SDS} and the messages containing the compiled and serialised task.
+With the result of the compilation, the task can be executed.
+First the messages are put in the channels, sending them to the device.
+Then, in parallel:
+\begin{enumerate}
+ \item the value is watched by looking in the device state \gls{SDS}, this task also determines the task value of the whole task;
+ \item the downstream \glspl{SDS} are monitored, i.e.\ the \cleaninline{sdsupdates} \gls{SDS} is monitored and updates from the device are applied to the associated \gls{ITASK} \gls{SDS};
+ \item the upstream \glspl{SDS} are monitored by spawning tasks that watch these \glspl{SDS}, if one is updated, the novel value is sent to the edge device.
+\end{enumerate}
+
+\begin{lstClean}[label={lst:liftmTask_pseudo},caption={Pseudocode implementation for \texttt{liftmTask}.}]
+liftmTask :: (Main (MTask BCInterpret a)) MTDevice -> Task a | iTask a
+liftmTask task (MTDevice dev sdsupdates channels)
+ = freshTaskId dev
+ >>= \tid->withCleanupHook (sendmessage [MTTTaskDel tid] channels) (
+ compile task \mrefs msgs->
+ sendMessage msgs channels
+ >>| waitForReturnAndValue tid dev
+ -|| watchSharesDownstream mrefs tid sdsupdates
+ -|| watchSharesUpstream mrefs channels tid)
\end{lstClean}
-Under the hood, \cleaninline{liftmTask} compiler the \gls{MTASK} task to byte code, gathers the initial values for the lifted \glspl{SDS} and sends the data to the device.
-Once acknowledged, the \gls{MTASK} task value and the \glspl{SDS} are monitored.
-If the \gls{ITASK} server updates the value of a lifted \gls{SDS}, the appropriate message is sent to the \gls{MTASK} to notify it of the change.
-Furthermore, the \gls{MTASK} device may update the \gls{SDS}, and in that case the message is picked up by the \cleaninline{liftmTask} task and the \gls{SDS} on the \gls{ITASK} server updated accordingly.
+Sending the complete byte code to the device is not always a suitable option.
+For example, when the device is connected through an unstable or slow connection, sending the entire byte code induces a lot of delay.
+To mitigate this problem, \gls{MTASK} tasks can be preloaded on a device.
+Preloading means that the task is compiled and integrated into the device firmware.
+On receiving a \cleaninline{TaskPrep}, a hashed value of the task to be sent is included.
+The device then checks the preloaded task registry and uses the local preloaded version if the hash matches.
+Of course this only works for tasks that are not tailor-made for the current work specification and not depend on run time information.
+The interface for task preloading can be found in \cref{lst:preload}.
+Given an \gls{MTASK} task, a header file is created that should be placed in the source code directory of the \gls{RTS} before building to include it in the firmware.
-\section{Lifting \texorpdfstring{\glsxtrlongpl{SDS}}{shared data sources}}\label{sec:liftsds}
-\begin{lstClean}[label={lst:mtask_itasksds},caption={Lifted \gls{ITASK} \glspl{SDS} in \gls{MTASK}.}]
-class liftsds v where
- liftsds :: ((v (Sds t)) -> In (Shared sds t) (Main (MTask v u)))
+\begin{lstClean}[label={lst:preload},caption={Preloading tasks in \gls{MTASK}.}]
+preloadTask :: (Main (MTask BCInterpret a)) -> Task String
+\end{lstClean}
+
+\section{Lowering iTask shared data sources}\label{sec:liftsds}
+Lowering \gls{ITASK} \glspl{SDS} to \gls{MTASK} \glspl{SDS} is something that mostly happens at the \gls{DSL} level using the \cleaninline{lowerSds} function (see \cref{lst:mtask_itasksds}).
+Lowering \pgls{SDS} proxies the \gls{ITASK} \gls{SDS} for use in \gls{MTASK}.
+\Glspl{SDS} in \gls{MTASK} always have an initial value.
+For regular \gls{SDS} this value is given in the source code, for lowered \gls{ITASK} \glspl{SDS} this value is obtained by reading the values once just before sending the task to the edge device.
+On the device, there is just one difference between lowered \glspl{SDS} and regular \glspl{SDS}: after changing a lowered \gls{SDS}, a message is sent to the server containing this new value.
+The \cleaninline{withDevice} task (see \cref{sec:withdevice}) receives and processes this message by writing to the \gls{ITASK} \gls{SDS}.
+Tasks watching this \gls{SDS} get notified then through the normal notification mechanism of \gls{ITASK}.
+\Cref{lst:imp_sds} shows the implementation of this type class for the byte code compiler.
+
+\begin{lstClean}[label={lst:mtask_itasksds},caption={Lowered \gls{ITASK} \glspl{SDS} in \gls{MTASK}.}]
+class lowerSds v where
+ lowerSds :: ((v (Sds t)) -> In (Shared sds t) (Main (MTask v u)))
-> Main (MTask v u) | RWShared sds
\end{lstClean}
+As an example, \cref{lst:mtask_liftsds_ex} shows a light switch function producing an \imtask{} task when given a device handle.
+First an \gls{ITASK} \gls{SDS} of the type boolean is created.
+This boolean represents the state of the light.
+The \gls{MTASK} task uses this \gls{SDS} to turn on or off the light.
+The \gls{ITASK} task that runs in parallel allows interactive updating of this state.
+
+\begin{lstClean}[label={lst:mtask_liftsds_ex},caption={Interactive light switch program in \gls{MTASK}.}]
+lightswitch :: MTDevice -> Task Bool
+lightswitch dev = withShared False \sh->
+ liftmTask (mtask sh) dev
+ -|| updateSharedInformation [] sh
+ <<@ Hint "Light switch"
+where
+ mtask :: (Shared sds Bool) -> Main (MTask v Bool)
+ | mtask, lowerSds v & RWShared sds
+ mtask sh =
+ declarePin D13 PMOutput \ledPin->
+ lowerSds \ls=sh
+ In fun \f=(\st->
+ getSds ls
+ >>*. [IfValue (\v->v !=. st) (writeD ledPin)]
+ >>=. f)
+ In {main=getSds ls >>~. f}
+\end{lstClean}
+
\section{Conclusion}
+This chapter explained the integration of \gls{MTASK} programs with \gls{ITASK}.
+Using just three \gls{ITASK} functions, \gls{MTASK} devices are integrated in \gls{ITASK} seamlessly.
+Devices, using any supported type of connection, are integrated in \gls{ITASK} using the \cleaninline{withDevice} function.
+Once connected, \gls{MTASK} tasks are sent to the device for execution using \cleaninline{liftmTask}, lifting them to full-fledged \gls{ITASK} tasks.
+To lower the bandwidth, tasks can also be preloaded.
+Furthermore, the \gls{MTASK} tasks interact with \gls{ITASK} \glspl{SDS} using the \cleaninline{lowerSds} construct.
+All of this together allows programming all layers of an \gls{IOT} system from a single source and in a single paradigm.
+All details regarding interoperation are automatically taken care of.
+The following section contains an elaborate example using all integration functions that has deliberately been placed after the conclusion.
+
+\newpage
+\vspace*{\fill}
+\hfill
+\begin{center}
+ \cleaninline[basewidth=0pt,columns=flexible,basicstyle=\tt\footnotesize]{let p = [['This page would be intentionally blank if I were not telling you that ']:p] in p} % chktex 10
+\end{center}
+\vspace{\fill}
+\newpage
+\section{Home automation}
+\todo[inline]{Meer uitleg over de applicatie? ADT ipv strings voor keuze?}
+This section presents an interactive home automation program (\cref{lst:example_home_automation}) to illustrate the integration of the \gls{MTASK} language and the \gls{ITASK} system.
+It consists of a web interface for the user to control which tasks are executed on either one of two connected devices: an \gls{ARDUINO} UNO, connected via a serial port; and an ESP8266 based prototyping board called NodeMCU, connected via \gls{TCP}\slash{}\gls{WIFI}.
+\Crefrange{lst:example:spec1}{lst:example:spec2} show the specification for the devices.
+The UNO is connected via serial using the UNIX filepath \path{/dev/ttyACM0} and the default serial port settings.
+The NodeMCU is connected via \gls{WIFI} and hence the \cleaninline{TCPSettings} record is used.
+%Both types have \cleaninline{channelSync} instances.
+
+The code consists of an \gls{ITASK} part and several \gls{MTASK} parts.
+\Crefrange{lst:example:task1}{lst:example:task2} contains the \gls{ITASK} task that coordinates the \gls{IOT} application.
+First the devices are connected (\crefrange{lst:example:conn1}{lst:example:conn2}) followed by launching a \cleaninline{parallel} task, visualised as a tabbed window, and a shutdown button to terminate the program (\crefrange{lst:example:par1}{lst:example:par2}).
+This parallel task is the controller of the tasks that run on the edge devices.
+It contains one task that allows adding new tasks (using \cleaninline{appendTask}) and all other tasks in the process list will be \gls{MTASK} tasks once they are added by the user.
+The controller task, \cleaninline{chooseTask} as shown in \crefrange{lst:example:ct1}{lst:example:ct2}, allows the user to pick a task, and sending it to the specified device.
+Tasks are picked by index from the \cleaninline{tasks} list (\crefrange{lst:example:tasks1}{lst:example:tasks2}) using \cleaninline{enterChoice}.
+The interface that is generated for this is seen in \cref{fig:example_screenshots1}.
+After selecting the task, a device is selected (see \cref{fig:example_screenshots2,lst:example:selectdev}).
+When both a task and a device are selected, an \gls{ITASK} task is added to the process list using \cleaninline{appendTask}.
+Using the helper function \cleaninline{mkTask}, the actual task is selected from the \cleaninline{tasks} list and executed by providing it the device argument.
+For example, when selecting the \cleaninline{temperature} task, the current temperature is shown to the user (\cref{fig:example_screenshots3}).
+This task just sends a simple temperature monitoring task to the device using \cleaninline{liftmTask} and provides a view on its task value using the \cleaninline{>\&>} \gls{ITASK} combinator.
+This combinator allows the observation of the left-hand side task's value through \pgls{SDS}.
+The light switch task at \crefrange{lst:example:ls1}{lst:example:ls2} is a task that has bidirectional interaction using the definition of \cleaninline{lightswitch} shown in \cref{lst:mtask_liftsds_ex}.
+Using \cleaninline{lowerSds}, the status of the light switch is synchronised with the user.
+Finally, a task that calculates the factorial of a user-provided number is shown in the list.
+
+\begin{figure}[!ht]
+ \centering
+ \begin{subfigure}[b]{.3\linewidth}
+ \includegraphics[width=\linewidth]{home_auto1}
+ \caption{Select task.}%
+ \label{fig:example_screenshots1}
+ \end{subfigure}
+ \begin{subfigure}[b]{.3\linewidth}
+ \includegraphics[width=\linewidth]{home_auto2}
+ \caption{Select device.}%
+ \label{fig:example_screenshots2}
+ \end{subfigure}
+ \begin{subfigure}[b]{.3\linewidth}
+ \includegraphics[width=\linewidth]{home_auto3}
+ \caption{View result.}%
+ \label{fig:example_screenshots3}
+ \end{subfigure}
+ \caption{Screenshots of the home automation example program in action.}%
+ \label{fig:example_screenshots}
+\end{figure}
+
+\begin{figure}[p]
+ \begin{fullpage}
+ \cleaninputlisting[firstline=12,lastline=50,numbers=left,belowskip=0pt]{lst/example.icl}
+ \begin{lstClean}[numbers=left,firstnumber=40,aboveskip=0pt,caption={An example of a home automation program.},label={lst:example_home_automation}]
+ , ...][+\label{lst:example:tasks2}+]\end{lstClean}
+ \end{fullpage}
+\end{figure}
\input{subfilepostamble}
\end{document}
repositories / phd-thesis.git / blobdiff