\begin{frame}[fragile]
\frametitle{Adding a View}
\begin{lstlisting}[language=Clean]
+
:: ByteCode a p = BC (RWS () [BC] BCState ())
+
+:: RWS r w s a = RWS (r s -> (a, s, w))
:: BC = BCNop | BCPush BCValue | ...
:: BCValue = E.e: BCValue e & mTaskType, TC e
:: BCShare = { sdsi :: Int, sdsval :: BCValue, sdsname :: String }
:: BCState = { freshl :: Int, freshs :: Int, sdss :: [BCShare] }
+class mTaskType a | toByteCode, fromByteCode, iTask, TC a
+class toByteCode a :: a -> String
+class fromByteCode a :: String -> a
+
instance ByteCode arith, boolExpr, ...
\end{lstlisting}
\end{frame}
\begin{frame}[fragile]
\frametitle{Implementation}
\begin{itemize}
- \item Writing instruction
- \item Carrying state
+ \item Reader Write State Transformer Monad
+ \item Write instruction
+ \item Carry state
\item Hand-crafted helpers
\end{itemize}
\begin{lstlisting}[language=Clean]
\frametitle{Control flow}
\begin{itemize}
\item Use labels
- \item Label resolving
+ \item Label are resolved
\pause{}
\item Thus no reuse
\end{itemize}
freshlabel = get >>= \st=:{freshl}->put {st & freshl=freshl+1} >>| pure freshl
-instance If ByteCode Stmt Stmt Stmt where If b t e = BCIfStmt b t e
-...
+instance IF ByteCode
+where
+ IF b t e = BCIfStmt b t e
+ (?) b t = BCIfStmt b t (tell` [])
+
BCIfStmt (BC b) (BC t) (BC e) = BC (
freshlabel >>= \else->freshlabel >>= \endif->
b >>| tell [BCJmpF else] >>|
instance assign ByteCode where
(=.) (BC v) (BC e) = BC (e >>| censor makeStore v)
-instance sdspub ByteCode where
- pub (BC x) = BC (censor (\[BCSdsFetch s]->[BCSdsPublish s]) x)
+addSDS sds v s = {s & sdss=[{sds & sdsval=BCValue v}:s.sdss]}
makeStore [BCSdsFetch i] = [BCSdsStore i]
makeStore [BCDigitalRead i] = [BCDigitalWrite i]
\begin{lstlisting}
class sdspub v where
pub :: (v t Upd) -> (v () Stmt)
+
instance sdspub ByteCode where
- pub (BC x) = BC (censor (\[BCSdsFetch s]->[BCSdsPublish s]) x)
+ pub (BC x)
+ = BC (censor (\[BCSdsFetch s]->[BCSdsPublish s]) x)
\end{lstlisting}
\end{frame}
\begin{frame}[fragile]
\frametitle{Task scheduling}
- \begin{block}{Old}
+ \begin{block}{Arduino C++ system}
\begin{itemize}
\item Task server
\item Tasks start other tasks
\end{itemize}
\end{block}
\pause{}
- \begin{block}{New}
- \begin{itemize}
- \item Old system, taskserver, tasks start tasks
- \item New system, task+strategy
- \pause{}
- \begin{itemize}
- \item \CI{OnShot}
- \item \CI{OnInterval}
- \item \CI{OnInterrupt}
- \end{itemize}
- \pause{}
- \item How to handle termination
+ \begin{block}{Interpreted Bytecode system}
+ \begin{itemize}[<+->]
+ \item Task accompanied with strategy
+ \item \CI{OnShot}, \CI{OnInterval}, \CI{OnInterrupt}
+ \item How to handle termination?
\end{itemize}
\pause{}
\begin{lstlisting}[language=Clean]
\end{block}
\end{frame}
-\subsection{Interpretation}
+\subsection{Devices}
\begin{frame}[fragile]
- \frametitle{mTask implementation}
- %TODO
+ \frametitle{Devices}
+ \begin{itemize}[<+->]
+ \item Standard C client software
+ \item Modular implementation
+ \item Specification generated from the macros
+ \end{itemize}
+ \pause{}
+ \begin{lstlisting}[language=C,caption={interface.h}]
+...
+#elif defined TARGET_STM32F767ZI
+#define APINS 128
+...
+#define HAVELED 1
+#define HAVEHB 1
+
+#elif defined ARDUINO_ESP8266_NODEMCU
+...
+bool input_available(void);
+uint8_t read_byte(void);
+void write_byte(uint8_t b);
+
+#if DPINS > 0
+void write_dpin(uint8_t i, bool b);
+...
+ \end{lstlisting}
\end{frame}
-\subsection{Devices}
-\begin{frame}
- \frametitle{Devices}
- \begin{itemize}
- \item Standard C
- \item Implement some classes in interface
- \pause{}
- \item How to handle termination
+\begin{frame}[fragile]
+ \frametitle{Storage}
+ \begin{itemize}[<+->]
+ \item Heap is there, but inefficient
+ \item Allocate space in global data
+ \item Selfmanage it
+ \item Tasks grow up
+ \item SDSs grow down
+ \item Compacting on removal
\end{itemize}
+ \pause{}
+ \begin{lstlisting}[language=C]
+struct task {
+ uint16_t tasklength;
+ uint16_t interval;
+ unsigned long lastrun;
+ uint8_t taskid;
+ uint8_t *bc;
+};
+ \end{lstlisting}
+\end{frame}
+
+\begin{frame}[fragile]
+ \frametitle{Interpreter}
+ Stack machine, modular
+ \pause{}
+ \begin{lstlisting}[language=C]
+#define f16(p) program[pc]*265+program[pc+1]
+
+void run_task(struct task *t){
+ uint8_t *program = t->bc;
+ int plen = t->tasklength, pc = 0, sp = 0;
+ while(pc < plen){
+ switch(program[pc++]){
+ case BCPUSH:
+ stack[sp++] = pc++ //Simplified
+ break;
+ case BCADD:
+ stack[sp-2] = stack[sp-2] + stack[sp-1];
+ sp -= 1;
+ break;
+ case BCJMPT:
+ pc = stack[--sp] ? program[pc]-1 : pc+1;
+ break;
+#if APINS > 0
+ case BCANALOGREAD:
+ ...
+ \end{lstlisting}
\end{frame}
\subsection{Server}
+\begin{frame}[fragile]
+ \frametitle{Device storage}
+ \begin{lstlisting}[language=Clean]
+:: Channels :== ([MTaskMSGRecv], [MTaskMSGSend], Bool)
+:: MTaskResource
+ = TCPDevice TCPSettings
+ | SerialDevice TTYSettings
+ | ...
+:: MTaskDevice =
+ { deviceTask :: Maybe TaskId , deviceError :: Maybe String
+ , deviceChannels :: String , deviceName :: String
+ , deviceState :: BCState , deviceTasks :: [MTaskTask]
+ , deviceResource :: MTaskResource
+ , deviceSpec :: Maybe MTaskDeviceSpec
+ , deviceShares :: [MTaskShare]
+ }
+
+channels :: MTaskDevice -> Shared Channels
+
+class MTaskDuplex a where
+ synFun :: a (Shared Channels) -> Task ()
+ \end{lstlisting}
+\end{frame}
+
+\begin{frame}
+ \frametitle{SDS storage}
+ \begin{block}{Approaches}
+ \begin{itemize}[<+->]
+ \item One SDS per SDS
+ \item One SDS per Device and map
+ \item One SDS in the entire system and map
+ \end{itemize}
+ \end{block}
+
+ \pause{}
+
+ \begin{block}{Notifications}
+ \begin{itemize}[<+->]
+ \item Tasks monitoring the SDSs
+ \item Parametric lenses!
+ \end{itemize}
+ \end{block}
+\end{frame}
+
\begin{frame}[fragile]
\frametitle{SDS (2)}
\framesubtitle{Parametric Lenses}
\item Used for notifications
\item On write the SDS returns \CI{p -> Bool}
\end{itemize}
+ \pause{}
\end{block}
-%
-% \begin{lstlisting}
-%sdsFocus :: p1 (RWShared p1 r w) -> RWShared p2 r w | iTask p
-%
-%:: SDSNotifyPred p :== p -> Bool
-%:: SDSLensRead p r rs = SDSRead (p -> rs -> MaybeError TaskException r)
-% | SDSReadConst (p -> r)
-%:: SDSLensWrite p w rs ws = SDSWrite (p -> rs -> w -> MaybeError TaskException (Maybe ws))
-% | SDSWriteConst (p -> w -> MaybeError TaskException (Maybe ws))
-%:: SDSLensNotify p w rs = SDSNotify (p -> rs -> w -> SDSNotifyPred p)
-% | SDSNotifyConst (p -> w -> SDSNotifyPred p)
-%
-%sdsLens :: String (p -> ps) (SDSLensRead p r rs) (SDSLensWrite p w rs ws)
-% (SDSLensNotify p w rs) (RWShared ps rs ws) -> RWShared p r w | iTask ps
-% \end{lstlisting}
-\end{frame}
-\subsection{Examples}
+ \begin{lstlisting}[language=Clean]
+sdsFocus :: p1 (RWShared p1 r w) -> RWShared p2 r w | iTask p
+ \end{lstlisting}
+\end{frame}
+
+\begin{frame}[fragile]
+ \frametitle{Solve the notification problem and how to relay information?}
+ \begin{itemize}
+ \item Tailor made share
+ \item The read and write functions have the World
+ \end{itemize}
+
+ \pause{}
+
+ \begin{onlyenv}<2>
+ \begin{lstlisting}[language=Clean]
+:: P :== Maybe (MTaskDevice, Int)
+deviceStore :: RWShared P [MTaskDevice] [MTaskDevice]
+deviceStore = SDSSource {SDSSource
+ | name="deviceStore", read=realRead, write=realWrite}
+where
+ realDeviceStore :: Shared [MTaskDevice]
+ realDeviceStore = sharedStore "mTaskDevices" []
+
+ realRead :: P *IWorld -> (MaybeError TaskException [MTaskDevice], *IWorld)
+ realRead p iw = read realDeviceStore iw
+ \end{lstlisting}
+ \end{onlyenv}
+
+ \begin{onlyenv}<3>
+ \begin{lstlisting}[language=Clean]
+realWrite :: P [MTaskDevice] *IWorld
+ -> (MaybeError TaskException (SDSNotifyPred P), *IWorld)
+realWrite mi w iw
+# (merr, iw) = write w realDeviceStore iw
+| isNothing mi = (Ok $ gEq{|*|} mi, iw)
+# (Just (dev, ident)) = mi
+| ident == -1 = (Ok $ gEq{|*|} mi, iw)
+= case find ((==)dev) w of
+ Nothing = (Error $ exception "Device lost", iw)
+ Just {deviceShares} = case find (\d->d.identifier == ident) deviceShares of
+ Nothing = (Error $ exception "Share lost", iw)
+ Just s = case sendMessagesIW [MTUpd ident s.MTaskShare.value] dev iw of
+ (Error e, iw) = (Error e, iw)
+ (Ok _, iw) = (Ok $ gEq{|*|} mi, iw)
+ \end{lstlisting}
+ \end{onlyenv}
+\end{frame}
+
+\begin{frame}[fragile]
+ \frametitle{Specific SDS functions}
+ \begin{lstlisting}
+deviceStoreNP :: Shared [MTaskDevice]
+deviceStoreNP = sdsFocus Nothing deviceStore
+
+deviceShare :: MTaskDevice -> Shared MTaskDevice
+deviceShare d = mapReadWriteError
+ ( \ds->case find ((==)d) ds of
+ Nothing = exception "Device lost"
+ Just d = Ok d)
+ , \w ds->case splitWith ((==)d) ds of
+ ([], _) = Error $ exception "Device lost"
+ ([_], ds) = Ok $ Just [w:ds])
+ $ sdsFocus (Just (d, -1)) deviceStore
+
+shareShare :: MTaskDevice MTaskShare -> Shared BCValue
+...
+\end{lstlisting}
+\end{frame}
+
+\subsection{Communication}
+\begin{frame}
+ \frametitle{The glue of the system}
+ \pause{}
+ \begin{block}{Communication}
+ \begin{itemize}
+ \item Compile, send and interact with Tasks
+ \item Interact with SDSs
+ \item All communication via channels
+ \end{itemize}
+ \end{block}
+\end{frame}
+
+\begin{frame}[fragile]
+ \frametitle{Messages}
+ \begin{lstlisting}[language=Clean]
+:: MTaskId :== Int
+:: MSDSId :== Int
+:: MTaskFreeBytes :== Int
+:: MTaskMSGRecv
+ = MTTaskAck MTaskId MTaskFreeBytes | MTTaskDelAck MTaskId
+ | MTSDSAck MSDSId | MTSDSDelAck MSDSId
+ | MTPub MSDSId BCValue | MTMessage String
+ | MTDevSpec MTaskDeviceSpec | MTEmpty
+
+:: MTaskMSGSend
+ = MTTask MTaskInterval String | MTTaskDel MTaskId
+ | MTShutdown | MTSds MSDSId BCValue
+ | MTUpd MSDSId BCValue | MTSpec
+ \end{lstlisting}
+\end{frame}
+
+\begin{frame}[fragile]
+ \frametitle{Connecting with a device}
+ \begin{lstlisting}[language=Clean]
+process :: MTaskDevice (Shared Channels) -> Task ()
+process ...
+
+makeDevice :: String MTaskResource -> MTaskDevice
+
+connectDevice :: MTaskDevice -> Task MTaskDevice
+connectDevice device = set ([], [], False) ch
+ >>| appendTopLevelTask newMap True
+ ( process device ch -||- catchAll (getSynFun device.deviceData ch) errHdl)
+ >>= \tid->upd (\d->{d&deviceTask=Just tid,deviceError=Nothing}) (deviceShare device)
+ >>| set (r,[MTSpec],ss) ch
+ >>| treturn device
+where
+ errHdl e = upd (\d->{d & deviceTask=Nothing, deviceError=Just e}) (deviceShare device) @! ()
+ ch = channels device
+ \end{lstlisting}
+\end{frame}
+
+\begin{frame}
+ \frametitle{Compilation}
+ \begin{itemize}[<+->]
+ \item Get device's compiler state
+ \item Run the RWS
+ \item Resolve labels
+ \item Instantiate shares
+ \item Convert to messages
+ \item Update state
+ \item Send the messages
+ \end{itemize}
+\end{frame}
+
+\begin{frame}[fragile]
+ \frametitle{Interaction with devices}
+ \begin{block}{Send task}
+ \begin{lstlisting}[language=Clean]
+sendTaskToDevice :: String (Main (ByteCode a Stmt)) (MTaskDevice, MTaskInterval)
+ -> Task (MTaskTask, [MTaskShare])
+ \end{lstlisting}
+ \end{block}
+\end{frame}
+
+\begin{frame}[fragile]
+ \frametitle{Example, blink}
+ \begin{lstlisting}[language=Clean]
+blink :: Task ()
+blink = addDevice
+ >>= connectDevice
+ >>= \stm->sendTaskToDevice "blink" blinkTask (stm, OnInterval 1000)
+ >>= \(st, [_,t])->forever (
+ updateSharedInformation "Which led to blink" [] (shareShare stm t)
+ ) >>* [OnAction (Action "Shutdown") $ always
+ $ deleteDevice stm >>| shutDown 0
+ ]
+where
+ blinkTask = sds \led=LED1 In sds \x=True In {main =
+ ledOff led1 :. ledOff led2 :. ledOff led3 :.
+ IF x (ledOff led) (ledOn led) :.
+ x =. Not x}
+ \end{lstlisting}
+\end{frame}
repositories / msc-thesis1617.git / blobdiff