\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}
\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.
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.
The task value of the \cleaninline{liftmTask} task is the task value of the task on the edge device.
+\todo{v.b.\ voor liftmtask}
+
\section{Lifting \texorpdfstring{\gls{ITASK}}{iTask} \texorpdfstring{\glsxtrlongpl{SDS}}{shared data sources}}\label{sec:liftsds}
Lifting \gls{ITASK} \glspl{SDS} to \gls{MTASK} \glspl{SDS} is something that mostly happens at the compiler level using the \cleaninline{liftsds} function (see \cref{lst:mtask_itasksds}).
\Glspl{SDS} in \gls{MTASK} must always have an initial value.
-> 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.
-\Cref{lst:mtask_itasksds_lens} shows a pseudocode implementation of \cleaninline{liftsds}.
\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}.
+This is done so that the \cleaninline{withDevice} task can write the received \gls{SDS} updates to the according \gls{SDS} independently.
+\Gls{ITASK}'s notification mechanism then takes care of the rest.
Such a \gls{SDS} is created by using the \cleaninline{mapReadWriteError} which, given a pair of read and write functions with error handling, produces a \gls{SDS} with the lens embedded.
The read function transforms, the function that converts a typed value to a typeless serialised value, just applies the serialisation.
-The write function, the function that, given the new serialised value and the old typed value, produces a new typed value tries do deserialise the value.
-
-First, in similar fashion to how functions are implemented, using fixed points, the \glspl{SDS} is
+The write function, the function that, given the new serialised value and the old typed value, produces a new typed value.
+It tries to decode the serialised value, if that succeeds, it is written to the underlying \gls{SDS}, an error is thrown otherwise.
+\Cref{lst:mtask_itasksds_lens} provides the implementation for this:
% VimTeX: SynIgnore on
\begin{lstClean}[label={lst:mtask_itasksds_lens},caption={Lens applied to lifted \gls{ITASK} \glspl{SDS} in \gls{MTASK}.}]
-instance liftsds BCInterpret where
+lens :: (Shared sds a) -> MTLens | type a & RWShared sds
+lens sds = mapReadWriteError
+ ( \r-> Ok (fromString (toByteCode{|*|} r)
+ , \w r-> ?Just <$> iTasksDecode (toString w)
+ ) ?None sds
+\end{lstClean}
+% VimTeX: SynIgnore off
+
+\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 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.
+
+% VimTeX: SynIgnore on
+\begin{lstClean}[label={lst:mtask_itasksds_lift},caption={Lens applied to lifted \gls{ITASK} \glspl{SDS} in \gls{MTASK}.}]
liftsds def = {main =
- let (t In e) = def (abort "liftsds: expression too strict")
+ let (t In _) = def (abort "liftsds: expression too strict")
in addSdsIfNotExist (Right $ lens t)
- >>= \sdsi-> let (t In e) = def (pure (Sds sdsi))
- in e.main
- }
- where
- lens :: ((Shared sds a) -> MTLens) | type, iTask a & RWShared sds
- lens = mapReadWriteError
- ( \r->Ok (fromString (toByteCode{|*|} r)
- , \w r-> ?Just <$> iTasksDecode (toString w)
- ) ?None
-\end{lstClean}
+ >>= \sdsi->let (_ In e) = def (pure (Sds sdsi)) in e.main
+ }\end{lstClean}
% VimTeX: SynIgnore off
+\todo{v.b.\ voor lifted sdss}
+
+\section{Home automation}
+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.
+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}}
+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.
-\section{Conclusion}
+\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}
+ \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 / blobdiff