process many comments

[phd-thesis.git] / top / int.tex

diff --git a/top/int.tex b/top/int.tex
index 41e0dc7..1a4eb01 100644 (file)
--- a/top/int.tex
+++ b/top/int.tex
@@ -15,7 +15,7 @@
                \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 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 lowering \gls{ITASK} \glspl{SDS} to \gls{MTASK} \glspl{SDS};
+               \item the 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}
                \item and a non-trivial home automation example application using all integration mechanisms;
        \end{itemize}
 \end{chapterabstract}


@@ -34,6 +34,8 @@ The diagram contains three labelled arrows that denote the integration functions
 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}).
 \glspl{SDS} from \gls{ITASK} are lowered to the \gls{MTASK} device using \cleaninline{lowerSds} (see \cref{sec:liftsds}).
 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}).
 \glspl{SDS} from \gls{ITASK} are lowered to the \gls{MTASK} device using \cleaninline{lowerSds} (see \cref{sec:liftsds}).

+\todo[inline]{mTask device\textsubscript{n} naar hfstk 5? Uitleg over taken en sensoren en \ldots? evt.\ zelfs naar intro hmmm?}
+\todo[inline]{Benoem dat er meerdere devices kunnen zijn en meerdere tasks op één device, en verwijs naar 6.5}

 
 \begin{figure}
        \centering
 
 \begin{figure}
        \centering


@@ -73,7 +75,7 @@ The \cleaninline{MTDevice} abstract type is internally represented as three \gls
 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 lowered \gls{SDS} is updated on the device, a message is sent to the server.
 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 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.
+This message is initially queued in the map in order to properly handle multiple updates asynchronously.

 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}.
 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}.


@@ -91,17 +93,19 @@ Then, it performs the following four tasks in parallel to monitor the edge devic
 \end{enumerate}
 
 \begin{lstClean}[caption={Pseudocode for the \texttt{withDevice} function in \gls{MTASK}.},label={lst:pseudo_withdevice}]
 \end{enumerate}
 
 \begin{lstClean}[caption={Pseudocode for the \texttt{withDevice} function in \gls{MTASK}.},label={lst:pseudo_withdevice}]

+withDevice :: a (MTDevice -> Task b) -> Task b | ...

 withDevice spec deviceTask =
 withDevice spec deviceTask =

-       withShared default \dev->parallel
+       withShared default \dev->

        withShared newMap \sdsupdates->
        withShared ([], [MTTSpecRequest], False) \channels->
        withShared newMap \sdsupdates->
        withShared ([], [MTTSpecRequest], False) \channels->

-               [ channelSync spec channels
-               , watchForShutdown channels
-               , watchChannelMessages dev channels
-               , waitForSpecification
-                       >>| deviceTask (MTDevice dev sdsupdates channels)
-                       >>* [ifStable: issueShutdown]
-               ]
+               parallel
+                       [ channelSync spec channels
+                       , watchForShutdown channels
+                       , watchChannelMessages dev channels
+                       , waitForSpecification
+                               >>| deviceTask (MTDevice dev sdsupdates channels)
+                               >>* [OnValue $ ifStable $ \_->issueShutdown]
+                       ]

 \end{lstClean}
 
 If at any stage an unrecoverable device error occurs, an \gls{ITASK} exception is thrown in the \cleaninline{withDevice} task.
 \end{lstClean}
 
 If at any stage an unrecoverable device error occurs, an \gls{ITASK} exception is thrown in the \cleaninline{withDevice} task.


@@ -109,14 +113,14 @@ 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.
 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.
+If another type of error occurs, it is re-thrown 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
 
 \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
+             except e                       = throw e

 \end{lstClean}
 
 \section{Lifting mTask tasks}\label{sec:liftmtask}
 \end{lstClean}
 
 \section{Lifting mTask tasks}\label{sec:liftmtask}


@@ -147,11 +151,12 @@ Then, in parallel:
 \end{enumerate}
 
 \begin{lstClean}[label={lst:liftmTask_pseudo},caption={Pseudocode implementation for \texttt{liftmTask}.}]
 \end{enumerate}
 
 \begin{lstClean}[label={lst:liftmTask_pseudo},caption={Pseudocode implementation for \texttt{liftmTask}.}]

+liftmTask :: (Main (MTask BCInterpret a)) MTDevice -> Task a | iTask a

 liftmTask task (MTDevice dev sdsupdates channels)
        = freshTaskId dev
        >>= \tid->withCleanupHook (sendmessage [MTTTaskDel tid] channels) (
                compile task \mrefs msgs->
 liftmTask task (MTDevice dev sdsupdates channels)
        = freshTaskId dev
        >>= \tid->withCleanupHook (sendmessage [MTTTaskDel tid] channels) (
                compile task \mrefs msgs->

-                       sendMessage msgs channels
+                           sendMessage msgs channels

                        >>| waitForReturnAndValue tid dev
                        -|| watchSharesDownstream mrefs tid sdsupdates
                        -|| watchSharesUpstream mrefs channels tid)
                        >>| waitForReturnAndValue tid dev
                        -|| watchSharesDownstream mrefs tid sdsupdates
                        -|| watchSharesUpstream mrefs channels tid)


@@ -163,7 +168,7 @@ 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.
 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.
+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.
 
 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.
 


@@ -203,13 +208,13 @@ where
        mtask :: (Shared sds Bool) -> Main (MTask v Bool)
                | mtask, lowerSds v & RWShared sds
        mtask sh =
        mtask :: (Shared sds Bool) -> Main (MTask v Bool)
                | mtask, lowerSds v & RWShared sds
        mtask sh =

-               declarePin D13 PMOutput \d13->
+               declarePin D13 PMOutput \ledPin->

                lowerSds \ls=sh
                In fun \f=(\st->
                             getSds ls
                lowerSds \ls=sh
                In fun \f=(\st->
                             getSds ls

-                       >>*. [IfValue (\v->v !=. st) (\v->writeD d13 v)]
-                       >>|. f (Not st))
-               In {main=f true}
+                       >>*. [IfValue (\v->v !=. st) (writeD ledPin)]
+                       >>=. f)
+               In {main=getSds ls >>~. f}

 \end{lstClean}
 
 \section{Conclusion}
 \end{lstClean}
 
 \section{Conclusion}


@@ -233,10 +238,11 @@ The following section contains an elaborate example using all integration functi
 \newpage
 
 \section{Home automation}
 \newpage
 
 \section{Home automation}

+\todo[inline]{Meer uitleg over de applicatie? ADT ipv strings voor keuze?}

 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.
 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 UNO is connected via serial using the UNIX filepath \path{/dev/ttyACM0} and the default serial port settings.

 The NodeMCU is connected via \gls{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.