From: Mart Lubbers Date: Thu, 1 Dec 2022 14:59:42 +0000 (+0100) Subject: updates X-Git-Url: https://git.martlubbers.net/?a=commitdiff_plain;h=a32d07a619a22edaf51648683eedef695d7fb28a;p=phd-thesis.git updates --- diff --git a/top/int.tex b/top/int.tex index 10ce549..7921a9b 100644 --- a/top/int.tex +++ b/top/int.tex @@ -8,12 +8,13 @@ \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} @@ -56,9 +57,8 @@ withDevice :: a (MTDevice -> Task b) -> 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. @@ -78,22 +78,33 @@ Then, it performs the following four tasks in parallel to monitor the edge devic 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}). @@ -102,9 +113,10 @@ This \gls{ITASK} task tethers the \gls{MTASK} task that is executed on the micro 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. @@ -131,6 +143,7 @@ class liftsds v where -> 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}. @@ -146,7 +159,7 @@ It tries to decode the serialised value, if that succeeds, it is written to the \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} @@ -154,7 +167,7 @@ lens sds = mapReadWriteError \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. @@ -164,9 +177,7 @@ This identifier is then used to provide a reference to the \cleaninline{def} def 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} @@ -175,44 +186,64 @@ This identifier is then used to provide a reference to the \cleaninline{def} def 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} diff --git a/top/lst/example.icl b/top/lst/example.icl index 7d15baa..4391c86 100644 --- a/top/lst/example.icl +++ b/top/lst/example.icl @@ -19,10 +19,9 @@ autoHome = withDevice arduino \dev1-> /*\label{lst:example:conn1}*/ >>* [OnAction (Action "Shutdown") (always (shutDown 0))]/*\label{lst:example:task2}\label{lst:example:par2}*/ chooseTask :: MTDevice MTDevice (SharedTaskList ()) -> Task ()/*\label{lst:example:ct1}*/ -chooseTask dev1 dev2 stl = tune (Title "Run a task") - $ enterChoice [] (zip2 [0..] (map fst tasks)) - <<@ Hint "Choose a task" - >>? \(i, n)->enterChoice [] ["arduino", "node"] +chooseTask dev1 dev2 stl = tune (Title "Run a task") $ + enterChoice [] (zip2 [0..] (map fst tasks)) <<@ Hint "Choose a task" + >>? \(i, n)->enterChoice [] ["arduino", "node"]/*\label{lst:example:selectdev}*/ <<@ Hint "Which device?" >>? \device->appendTask Embedded (mkTask n i device) stl >-| chooseTask dev1 dev2 stl @@ -35,21 +34,29 @@ where tasks :: [(String, MTDevice -> Task ())]/*\label{lst:example:tasks1}*/ tasks = [ ("temp", \dev-> - liftmTask ( DHT (DHT_DHT (DigitalPin D6) DHT22) \dht-> - {main=temperature dht}) dev + liftmTask ( + DHT (DHT_DHT (DigitalPin D6) DHT22) \dht-> + {main=temperature dht} + ) dev >&> \t->viewSharedInformation [ViewAs \i->toString (fromMaybe 0.0 i) +++ "C"] t - <<@ Hint "Current Temperature" - @! ()) - , ("lightswitch", \dev-> + <<@ Hint "Current Temperature" @! ()) + , ("lightswitch", \dev-> /*\label{lst:example:ls1}*/ withShared False \sh-> - liftmTask (lightswitch sh) dev - -|| updateSharedInformation [] sh <<@ Hint "Switch") + liftmTask ( + declarePin D13 PMOutput \d13-> + liftsds \ls=sh + In fun \f=(\st-> + getSds ls + >>*. [IfValue ((!=.)st) (\v->writeD d13 v)] + >>|. f (Not st)) + In {main=f true} + ) dev + -|| updateSharedInformation [] sh <<@ Hint "Switch")/*\label{lst:example:ls2}*/ , ("factorial", \dev-> - updateInformation [] 5 <<@ Hint "Factorial of what?" + updateInformation [] 5 <<@ Hint "Factorial of what?" >>? \i->liftmTask (factorial i) dev - >>- \r->viewInformation [] r <<@ Hint "Result" - @! ()) + >>- \r->viewInformation [] r <<@ Hint "Result" @! ()) ] factorial i = {main=rtrn (lit i)}