-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}
+\subsection{Implementation}
+\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}