+\subsection{Implementation}
+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.
+When a lifted \gls{SDS} is updated on the device, a message is sent to the server.
+This message is initially queued in the map to allow for asynchronous handling of multiple updates.
+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} to create anonymous local \glspl{SDS}.
+Then, it performs the following four tasks in parallel to monitor the edge device.
+\begin{enumerate}
+ \item It synchronises the channels using the \cleaninline{channelSync} overloaded function.
+ Errors that occur here are converted to the proper \gls{MTASK} exception.
+ \item Watches the channels for the shutdown flag.
+ If the connection is lost with the device unexpectedly, an \gls{MTASK} exception is thrown.
+ \item Watches the channels for messages and processes them accordingly by changing the device information \gls{SDS} or adding the lifted \gls{SDS} updates to the corresponding \gls{SDS} update queue.
+ \item Sends a request for a specification. Once the specification is received, the device task is run.
+ The task value of this device task is then used as the task value of the \cleaninline{withDevice} task.
+\end{enumerate}
+
+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]
+% ]
+
+\section{Lifting \texorpdfstring{\gls{MTASK}}{mTask} tasks}\label{sec:liftmtask}