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]
\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}).
-> 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}.
}\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.
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.
\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}
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}*/
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?"
>>- \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"
repositories / phd-thesis.git / commitdiff