X-Git-Url: https://git.martlubbers.net/?a=blobdiff_plain;f=top%2Fint.tex;h=41e0dc7120679b2c5e136de92737657884364789;hb=382f9709a872c0dfdb86e1184d07224a47c8eff3;hp=7921a9b470897e302714fb648003e07705c28cf5;hpb=a32d07a619a22edaf51648683eedef695d7fb28a;p=phd-thesis.git diff --git a/top/int.tex b/top/int.tex index 7921a9b..41e0dc7 100644 --- a/top/int.tex +++ b/top/int.tex @@ -1,51 +1,61 @@ +%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} - \noindent 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 \gls{MTASK} applications; - \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 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; + \item a 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} 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}). -\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{Connecting edge 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. +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 (see \cref{lst:connection_types}). -The \cleaninline{withDevice} function transforms such 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 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 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 @@ -62,155 +72,193 @@ withDevice :: a (MTDevice -> Task b) 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 lifted \gls{SDS} is updated on the device, a message is sent to the server. -This message is initially queued in the map to allow for asynchronous handling of multiple 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 handly multiple updates asychronously. 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} to create anonymous local \glspl{SDS}. +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 It synchronises the channels using the \cleaninline{channelSync} overloaded function. - Errors that occur here are converted to the proper \gls{MTASK} exception. - \item Watches the channels for the shutdown flag. + \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 Watches the channels for messages and processes them accordingly by changing the device information \gls{SDS} or adding the lifted \gls{SDS} updates to the corresponding \gls{SDS} update queue. - \item Sends a request for a specification. Once the specification is received, the device task is run. + \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{widthDevice} function},label={lst:pseudo_withdevice}] +\begin{lstClean}[caption={Pseudocode for the \texttt{withDevice} function in \gls{MTASK}.},label={lst:pseudo_withdevice}] withDevice spec deviceTask = + withShared default \dev->parallel withShared newMap \sdsupdates-> withShared ([], [MTTSpecRequest], False) \channels-> - withShared default \dev->parallel - [ channelSync spec - , watchForShutdown - , watchChannels + [ channelSync spec channels + , watchForShutdown channels + , watchChannelMessages dev channels , waitForSpecification - >>| deviceTask + >>| deviceTask (MTDevice dev sdsupdates channels) >>* [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 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 +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 rethrown 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 _ = throw e + 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}). -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 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. - \item Compiles the task and fetches the values for the tethered \glspl{SDS}. - \item Sends the task to the device - \item Watches, in parallel: the tethered \glspl{SDS} in \gls{ITASK}, if they are updated, a message is sent to the device; the \gls{SDS} update queue, if there is a downstream update, the \gls{ITASK} \gls{SDS} it references is updated as well; and the task value. -\end{itemize} - -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. -For regular \gls{SDS} this value is given in the source code, for lifted \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 itself, there is just one difference between lifted \glspl{SDS} and regular \glspl{SDS}: after changing \pgls{SDS}, a message is sent to the server containing this new value. +\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 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} + +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. + +\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={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: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} -\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}. -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. -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}.}] -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 +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 \d13-> + lowerSds \ls=sh + In fun \f=(\st-> + getSds ls + >>*. [IfValue (\v->v !=. st) (\v->writeD d13 v)] + >>|. f (Not st)) + In {main=f true} \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 _) = def (abort "liftsds: expression too strict") - in addSdsIfNotExist (Right $ lens t) - >>= \sdsi->let (_ In e) = def (pure (Sds sdsi)) in e.main - }\end{lstClean} -% VimTeX: SynIgnore off - -\todo{v.b.\ voor lifted sdss} +\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} -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. - +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 WiFi and hence the \cleaninline{TCPSettings} record is used. -Both types have \cleaninline{channelSync} instances. +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} 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}). +\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, sending it to the specified device. +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 can be seen in \cref{fig:example_screenshots1}. +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 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. +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{>\&>}\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. - -\begin{figure}[ht] +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} @@ -231,19 +279,13 @@ If it is different from the current state, the new value is written to the digit \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}] +\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} -\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}