From e36fac1dc27e8fda89f7970d4e1eb1d49d73f47f Mon Sep 17 00:00:00 2001 From: Mart Lubbers Date: Fri, 2 Dec 2022 15:19:12 +0100 Subject: [PATCH] updates --- top/imp.tex | 5 +-- top/int.tex | 75 +++++++++++++++++++++++++++++++++------------ top/lst/example.icl | 45 +++++++++++++++++---------- 3 files changed, 88 insertions(+), 37 deletions(-) diff --git a/top/imp.tex b/top/imp.tex index 0955b46..a8f451c 100644 --- a/top/imp.tex +++ b/top/imp.tex @@ -11,10 +11,11 @@ This chapter shows the implementation of the \gls{MTASK} system. It is threefold: first it shows the implementation of the byte code compiler for \gls{MTASK}'s \gls{TOP} language, then is details of the implementation of \gls{MTASK}'s \gls{TOP} engine that executes the \gls{MTASK} tasks on the microcontroller, and finally it shows how the integration of \gls{MTASK} tasks and \glspl{SDS} is implemented both on the server and on the device. \end{chapterabstract} + +\section{Byte code compiler} IFL19 paper, bytecode instructieset~\cref{chp:bytecode_instruction_set} -\section{Integration with \texorpdfstring{\gls{ITASK}}{iTask}} -IFL18 paper stukken +\section{Run time system} \input{subfilepostamble} \end{document} diff --git a/top/int.tex b/top/int.tex index 7921a9b..1b310cd 100644 --- a/top/int.tex +++ b/top/int.tex @@ -83,9 +83,9 @@ withDevice spec deviceTask = 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 >>* [ifStable: issueShutdown] @@ -117,17 +117,32 @@ 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} +\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 just 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 can be destroyed when for example a task executed in parallel 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 lifted \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 upstroam \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} \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}). @@ -143,6 +158,30 @@ class liftsds v where -> Main (MTask v u) | RWShared sds \end{lstClean} +As an example, \cref{lst:mtask_liftsds_ex} shows a lightswitch function producing an \gls{ITASK}\slash\gls{MTASK} task. +Given an \cleaninline{MTDevice} type, a device handle, 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. +An \gls{ITASK} task that runs in parallel allows interactive updating of this state. + +\todo{dit voorbeeld aanhouden of alleen die grote gebruiken} +\begin{lstClean}[label={lst:mtask_liftsds_ex},caption={Interactive light switch program.}] +lightswitch dev = + withShared False \sh-> + liftmTask (mtask sh) dev + -|| updateSharedInformation [] sh + <<@ Hint "Light switch" +where + mtask sh = + 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} +\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}. @@ -180,8 +219,6 @@ This identifier is then used to provide a reference to the \cleaninline{def} def }\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. @@ -205,7 +242,7 @@ Using the helper function \cleaninline{mkTask}, the actual task is selected from 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. +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{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. @@ -232,8 +269,8 @@ If it is different from the current state, the new value is written to the digit \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}] + \cleaninputlisting[firstline=12,lastline=50,numbers=left,belowskip=0pt,escapeinside={/*}{*/}]{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{figure} diff --git a/top/lst/example.icl b/top/lst/example.icl index 4391c86..8e90646 100644 --- a/top/lst/example.icl +++ b/top/lst/example.icl @@ -7,7 +7,7 @@ import mTask.Interpret import mTask.Interpret.Device.TCP import mTask.Interpret.Device.Serial -Start w = doTasks autoHome w +//Start w = doTasks autoHome w arduino = {TTYSettings | zero & devicePath="/dev/ttyACM0"}/*\label{lst:example:spec1}*/ nodeMCU = {TCPSettings | host="192.168.0.1", port=8123, pingTimeout= ?None}/*\label{lst:example:spec2}*/ @@ -34,24 +34,15 @@ where tasks :: [(String, MTDevice -> Task ())]/*\label{lst:example:tasks1}*/ tasks = [ ("temp", \dev-> - liftmTask ( - DHT (DHT_DHT (DigitalPin D6) DHT22) \dht-> - {main=temperature dht} + 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-> /*\label{lst:example:ls1}*/ withShared False \sh-> - 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 + liftmTask (lightswitch sh) dev -|| updateSharedInformation [] sh <<@ Hint "Switch")/*\label{lst:example:ls2}*/ , ("factorial", \dev-> updateInformation [] 5 <<@ Hint "Factorial of what?" @@ -59,6 +50,28 @@ tasks = >>- \r->viewInformation [] r <<@ Hint "Result" @! ()) ] -factorial i = {main=rtrn (lit i)} -blink d = {main=writeD (lit d) (lit True)} -lightswitch sh = {main=rtrn (lit ())} +factorial :: Int -> Main (MTask v Int) | mtask v +factorial i = + fun \fac=(\i->If (i ==. lit 0) (lit 1) (i *. fac (i -. lit 1))) + In {main=rtrn (fac (lit i))} +blink :: Int -> Main (MTask v ()) | mtask v +blink d = + declarePin D13 PMOutput \d13-> + fun \bl=(\st-> + writeD d13 st + >>|. delay (lit d) + >>|. bl (Not st)) + In {main=bl true} +lightswitch :: (Shared sds Bool) -> Main (MTask v ()) | liftsds, mtask v & RWShared sds & TC (sds () Bool Bool) +lightswitch sh = + 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} + +Start w = doTasks t w +t = withShared True \sh-> + updateSharedInformation [] sh <<@ Hint "Light switch" -- 2.20.1