\chapter{Integration with \texorpdfstring{\gls{ITASK}}{iTask}}%
\label{chp:integration_with_itask}
\begin{chapterabstract}
- This chapter shows the integration of \gls{MTASK} with \gls{ITASK} by showing:
+ \noindent This chapter shows the integration of \gls{MTASK} with \gls{ITASK} by showing:
\begin{itemize}
\item an architectural overview \gls{MTASK} applications;
\item on 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 a interface for lifting \gls{ITASK} \glspl{SDS} to \gls{MTASK} \glspl{SDS};
+ \item and finishes with non-trivial home automation example application using all integration mechanisms;
\end{itemize}
\end{chapterabstract}
-> Task b | iTask b & channelSync, iTask a
\end{lstClean}
-\todo{v.b.\ voor withDevice}
-
\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.
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{widthDevice} function},label={lst:pseudo_withdevice}]
+withDevice spec deviceTask =
+ withShared newMap \sdsupdates->
+ withShared ([], [MTTSpecRequest], False) \channels->
+ withShared default \dev->parallel
+ [ channelSync spec
+ , watchForShutdown
+ , watchChannels
+ , waitForSpecification
+ >>| deviceTask
+ >>* [ifStable: issueShutdown]
+ ]
+\end{lstClean}
+
If at any stage an unrecoverable device error occurs, an \gls{ITASK} exception is thrown on the \cleaninline{withDevice} task.
This exception can be caught in order to device some kind of fail-safe mechanism.
-For example, when a device fails, the tasks can be sent to another device.
-\todo[inline]{Example of failsafe?}
-
-%withDevice spec deviceTask
-% withShared newMap \sdsupdates->
-% withShared ([], [MTTSpecRequest], False) \channels->
-% withShared default \dev->parallel
-% [ channelSync spec // unexpected disconnect
-% , watchForShutdown // unexpected disconnect
-% , watchChannels // process messages
-% , waitForSpecification
-% >>| deviceTask
-% >>* [ifStable: issueShutdown]
-% ]
+For example, when a device fails, the tasks 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.
+If an error occurs during execution, the next device in the pool is tried until the pool is exhausted
+
+\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 _ = throw e
+\end{lstClean}
\section{Lifting \texorpdfstring{\gls{MTASK}}{mTask} 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}).
Hence, when for example observing 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}
Under the hood, \cleaninline{liftmTask}:
\begin{itemize}
\item Generates a fresh task identifier for the device.
-> Main (MTask v u) | RWShared sds
\end{lstClean}
+\subsection{Implementation}
The compilation of the code and the serialisation of the data throws away all typing information.
\Glspl{SDS} are stored in the compiler state as a map from identifiers to either an initial value or an \cleaninline{MTLens}.
The \cleaninline{MTLens} is a type synonym for a \gls{SDS} that represents the typeless serialised value of the underlying \gls{SDS}.
\begin{lstClean}[label={lst:mtask_itasksds_lens},caption={Lens applied to lifted \gls{ITASK} \glspl{SDS} in \gls{MTASK}.}]
lens :: (Shared sds a) -> MTLens | type a & RWShared sds
lens sds = mapReadWriteError
- ( \r->Ok (fromString (toByteCode{|*|} r)
+ ( \r-> Ok (fromString (toByteCode{|*|} r)
, \w r-> ?Just <$> iTasksDecode (toString w)
) ?None sds
\end{lstClean}
\Cref{lst:mtask_itasksds_lift} shows the code for the implementation of \cleaninline{liftsds} that uses the \cleaninline{lens} function shown earlier.
First, the \gls{SDS} to be lifted is extracted from the expression by bootstrapping the fixed point with a dummy value.
-This is safe because the expression on the right-hand side of the \cleaninline{In} is never used.
+This is safe because the expression on the right-hand side of the \cleaninline{In} is never evaluated.
Then, using \cleaninline{addSdsIfNotExist}, the identifier for this particular \gls{SDS} is either retrieved from the compiler state or generated freshly.
This identifier is then used to provide a reference to the \cleaninline{def} definition to evaluate the main expression.
let (t In _) = def (abort "liftsds: expression too strict")
in addSdsIfNotExist (Right $ lens t)
>>= \sdsi->let (_ In e) = def (pure (Sds sdsi)) in e.main
- }
- where
-\end{lstClean}
+ }\end{lstClean}
% VimTeX: SynIgnore off
\todo{v.b.\ voor lifted sdss}
This section presents a interactive home automation program (\Cref{lst:example_home_automation}) to illustrate \gls{MTASK}'s integration with \gls{ITASK}.
It consists of a web interface for the user to control which tasks may be executed on either 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} over WiFi.
-\Crefrange{lst:example:spec1}{lst:example:spec2} show the specification for the devices followed by \crefrange{lst:example:task1}{lst:example:task2} containing the actual task.
-This task first connects the devices (\crefrange{lst:example:conn1}{lst:example:conn2}) followed by a \cleaninline{parallel} task that is visualized as a tabbed window with a shutdown button to terminate the program (\crefrange{lst:example:par1}{lst:example:par2}).
-The \cleaninline{chooseTask} task (\crefrange{lst:example:ct1}{lst:example:ct2}) allows the user to pick a task, sending it to the specified device.
-Tasks are picked from the \cleaninline{tasks} list (\crefrange{lst:example:tasks1}{lst:example:tasks2}).
-For example, the \cleaninline{temperature} task shows the current temperature to the user.
-When the temperature changes, the \gls{DHT} sensor reports it and the task value for the \cleaninline{temperature} task changes.
-This change in task value is reflected in the \gls{ITASK} server and the task value of the \cleaninline{liftmTask} task changes accordingly.
-The task is lifted to an \gls{ITASK} task and the \cleaninline{>\&>}\footnotemark{} \gls{ITASK} combinator transforms the task value into an \gls{SDS} that is displayed to the user using \cleaninline{viewSharedInformation}.
+\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 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} containing the \gls{ITASK} task that coordinates the \gls{IOT} application.
+It first connects the devices (\crefrange{lst:example:conn1}{lst:example:conn2}) followed by launching a \cleaninline{parallel} task, visualized 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, 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 can be 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 is 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 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{>\&>}\footnotemark{} \gls{ITASK} combinator.
\footnotetext{\cleaninline{(>\&>) infixl 1 :: (Task a) ((SDSLens () (? a) ()) -> Task b) -> Task b \| iTask a \& iTask b}}
-Screenshots of the application are given in \cref{fig:example_screenshots}.
+The light switch task at \crefrange{lst:example:ls1}{lst:example:ls2} is a task that has bidirectional interaction.
+Using \cleaninline{liftsds}, the status of the light switch is synchronised with the user.
+The task on the edge device continuously monitors the value of the lifted \gls{SDS}.
+If it is different from the current state, the new value is written to the digital \gls{GPIO} pin 13 and the monitoring function is recursively called.
\begin{figure}[ht]
\centering
\begin{subfigure}[b]{.3\linewidth}
\includegraphics[width=\linewidth]{home_auto1}
- \caption{Select task.}
+ \caption{Select task.}%
+ \label{fig:example_screenshots1}
\end{subfigure}
\begin{subfigure}[b]{.3\linewidth}
\includegraphics[width=\linewidth]{home_auto2}
- \caption{Select device.}
+ \caption{Select device.}%
+ \label{fig:example_screenshots2}
\end{subfigure}
\begin{subfigure}[b]{.3\linewidth}
\includegraphics[width=\linewidth]{home_auto3}
- \caption{View result.}
+ \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}
- \cleaninputlisting[firstline=12,lastline=52,numbers=left,belowskip=0pt,escapeinside={/*}{*/}]{lst/example.icl}
- \begin{lstClean}[numbers=left,firstnumber=42,aboveskip=0pt,caption={An example of a home automation program.},label={lst:example_home_automation}]
- , ...][+\label{lst:example:tasks2}+]
- \end{lstClean}
+ \cleaninputlisting[firstline=12,lastline=60,numbers=left,belowskip=0pt,escapeinside={/*}{*/}]{lst/example.icl}
+ \begin{lstClean}[numbers=left,firstnumber=50,aboveskip=0pt,caption={An example of a home automation program.},label={lst:example_home_automation}]
+ , ...][+\label{lst:example:tasks2}+]\end{lstClean}
\end{figure}
\section{Conclusion}
-
+\Gls{MTASK} edge devices run little \gls{TOP} engines of their own.
+Using only a couple of \gls{ITASK} functions, \gls{MTASK} tasks can be 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 can be sent to the device for execution using \cleaninline{liftmTask}, lifting them to full-fledged \gls{ITASK} tasks.
+Furthermore, the \gls{MTASK} tasks can interact with \gls{ITASK} \glspl{SDS} using the \cleaninline{liftsds} construct.
+This together allows entire \gls{IOT} systems to be programmed from a single source.
\input{subfilepostamble}
\end{document}
repositories / phd-thesis.git / commitdiff