X-Git-Url: https://git.martlubbers.net/?a=blobdiff_plain;f=results.mtask.tex;h=c32f7acf318e05ad9d6a03f3404b136458d6b089;hb=7694dfaa240c6dd9af2f1ac8880f0fb1d7f38324;hp=aaa2515b6c8c1af92b47aceec4d320b07dda4dd9;hpb=a3a00cd9df798eda92291a2f3f6c922bdfdfdac2;p=msc-thesis1617.git

diff --git a/results.mtask.tex b/results.mtask.tex
index aaa2515..c32f7ac 100644
--- a/results.mtask.tex
+++ b/results.mtask.tex
@@ -1,16 +1,290 @@
-\section{mTask}
-\subsection{Semantics}
-\todo{Uitleggen wat het systeem precies doet}
+Some functionality of the original \gls{mTask}-\gls{EDSL} will not be used in
+this extension \gls{EDSL}. Conversely, some functionality needed was not
+available in the existing \gls{EDSL}. Due to the nature of class based shallow
+embedding this obstacle is very easy to solve. A type housing the \gls{EDSL}
+does not have to implement all the available classes. Moreover, classes can be
+added at will without interfering with the existing views.
 
-\subsection{Extension on the \gls{mTask}-\gls{EDSL}}
-\todo{Aanpassingen aan de mTask DSL}
+\section{Semantics}
+\subsection{\glspl{mTask}}
+The current \gls{mTask} engine for devices does not support \glspl{Task} in the
+sense that the \gls{C}-view it does. \glspl{Task} in the new system are are
+\CI{Main} objects with a program inside. A \gls{Task} runs periodically, on
+interrupt or one-shot. 
+\todo{elaborate}
 
-\section{iTasks}
-\subsection{Shares}
-\todo{Semantiek van shares, hoe ze in iTasks zijn, hoe typering}
+\subsection{\glspl{SDS}}
+\glspl{SDS} behave a little bit differently on an \gls{mTask} device than in
+the \gls{iTasks} system. In an \gls{iTasks} system, when the \gls{SDS} is
+updated, a broadcast to everyone in the system watching is made to notify them
+of an update. \glspl{SDS} on the device can update very often and the update
+might not be the final value it will get. Therefore a device must publish the
+\gls{SDS} explicitly to save bandwidth. This means that an extra function is
+added to the \CI{sds} class that adds the \CI{pub} function.
+\todo{elaborate}
 
-\subsection{Lifting}
-\todo{Lift mTask taken naar echte taken, hoe werkt dat?}
+\section{Bytecode compilation}\label{sec:compiler}
+The \glspl{mTask} are sent to the device in bytecode and are saved in the
+memory of the device. To compile the \gls{EDSL} code to bytecode, a view is
+added to the \gls{mTask}-system called \CI{ByteCode}. As shown in
+Listing~\ref{lst:bcview}, the \CI{ByteCode} view is a boxed \gls{RWST} that
+writes bytecode instructions (\CI{BC}) while carrying around a \CI{BCState}.
+The state is kept between devices and contains fresh variable names and a
+register of shares used.
 
-\section{Demo}
-\todo{Wat voorbeeld code}
+Types implementing the \gls{mTask} classes must have two free type variables.
+Therefore the \gls{RWST} is wrapped with a constructor and two phantom type
+variables are added. This means that the programmer has to unbox the
+\CI{ByteCode} object to be able to use return values for the monad. Tailor made
+access functions are used to achieve this with ease. The fresh variable stream
+in a compiler using an \gls{RWST} is often put in to the \emph{Reader} part of
+the monad. However, not all code is compiled immediately and later on the fresh
+variable stream can not contain variables that were used before. Therefore this
+information is put in the state which is kept between compilations.
+
+Not all types are suitable for usage in bytecode compiled programs. Every value
+used in the bytecode view must fit in the \CI{BCValue} type which restricts
+the content. Most notably, the type must be bytecode encodable.  A \CI{BCValue}
+must be encodable and decodable without losing type or value information. At
+the moment a simple encoding scheme is used that uses a single byte prefixes to
+detect which type the value is. The devices know of these prefixes and act
+accordingly.
+
+\begin{lstlisting}[label={lst:bcview},caption={Bytecode view}]
+:: ByteCode a p = BC (RWS () [BC] BCState ())
+:: BCValue = E.e: BCValue e & mTaskType, TC e
+:: BCShare =
+	{ sdsi :: Int
+	, sdsval :: BCValue
+	}
+:: BCState = 
+	{ freshl :: [Int]
+	, freshs :: [Int]
+	, sdss :: [BCShare]
+	}
+
+class toByteCode a :: a -> String
+class fromByteCode a :: String -> a
+class mTaskType a | toByteCode, fromByteCode, iTask, TC a
+
+instance toByteCode Int, ... , UserLED, BCValue
+instance fromByteCode Int, ... , UserLED, BCValue
+
+instance arith ByteCode
+...
+instance serial ByteCode
+\end{lstlisting}
+
+\section{Implementation}
+\subsection{Instruction Set}
+The instruction set is given in Listing~\ref{bc:instr}. The instruction set is
+kept large, but under $255$, to get the highest expressivity for the lowest
+program size. 
+
+The interpreter is a
+stack machine. Therefore the it needs instructions like \emph{Push} and
+\emph{Pop}. The virtual instruction \CI{BCLab} is added to allow for an easy
+implementation. However, this is not a real instruction and the labels are
+resolved to actual addresses in the final step of compilation to save
+instructions.
+
+\begin{lstlisting}[label={bc:instr},%
+	caption={Bytecode instruction set}]
+:: BC = BCNop
+	| BCLab Int          | BCPush BCValue     | BCPop
+	//SDS functions
+	| BCSdsStore BCShare | BCSdsFetch BCShare | BCSdsPublish BCShare
+	//Unary ops
+	| BCNot
+	//Binary Int ops
+	| BCAdd              | BCSub              | BCMul
+	| BCDiv
+	//Binary Bool ops
+	| BCAnd              | BCOr
+	//Binary ops
+	| BCEq               | BCNeq              | BCLes             | BCGre
+	| BCLeq              | BCGeq
+	//Conditionals and jumping
+	| BCJmp Int          | BCJmpT Int         | BCJmpF Int
+	//UserLED
+	| BCLedOn            | BCLedOff
+	//Pins
+	| BCAnalogRead Pin   | BCAnalogWrite Pin  | BCDigitalRead Pin | BCDigitalWrite Pin
+	//Return
+	| BCReturn
+\end{lstlisting}
+
+All instructions are can be converted semi-automatically using the generic
+function \CI{consIndex\{*\}} that gives the index of the constructor. This
+constructor index is the actual byte value for the instruction. The
+\CI{BCValue} type contains existentially quantified types and therefore must
+have a given implementation for all generic functions.
+
+\subsection{Helper functions}
+The \CI{ByteCode} type is just a boxed \gls{RWST} and that gives us access to
+the whole range of \gls{RWST} functions. However, to apply a function the type
+must be unboxed. After application the type must be boxed again. To achieve
+this some helper functions have been created. They are listed in
+Listing~\ref{lst:helpers}. The \CI{op} and \CI{op2} function is crafted to make
+operators that pop one or two values off the stack respectively. The \CI{tell`}
+is a wrapper around the \gls{RWST} function \CI{tell} that appends the argument
+to the \emph{Writer} value.
+
+\begin{lstlisting}[label={lst:helpers},caption={Some helper functions}]
+op2 :: (ByteCode a p1) (ByteCode a p2) BC -> ByteCode b Expr
+op2 (BC x) (BC y) bc = BC (x >>| y >>| tell [bc])
+
+op :: (ByteCode a p) BC -> ByteCode b c
+op (BC x) bc = BC (x >>| tell [bc])
+
+tell` :: [BC] -> (ByteCode a p)
+tell` x = BC (tell x)
+
+unBC :: (ByteCode a p) -> RWS () [BC] BCState ()
+unBC (BC x) = x
+\end{lstlisting}
+
+\subsection{Arithmetics \& Peripherals}
+Almost all of the code from the simple classes use exclusively helper
+functions. Listing~\ref{lst:arithview} shows some implementations. The classes
+\CI{boolExpr} and the classes for the peripherals are implemented in the same
+fashion.
+
+\begin{lstlisting}[label={lst:arithview},caption={%
+	Bytecode view implementation for arithmetic and peripheral classes}]
+instance arith ByteCode where
+	lit x = tell` [BCPush (BCValue x)]
+	(+.) x y = op2 x y BCDiv
+	...
+
+instance userLed ByteCode where
+	ledOn  l = op l BCLedOn
+	ledOff l = op l BCLedOff
+\end{lstlisting}
+
+\subsection{Control Flow}
+Sequence is very straightforward in the bytecode view. The function just
+sequences the two \glspl{RWST}. The \emph{If} statement requires some detailed
+explanation since labels come in to play. The implementation speaks for itself
+in Listing~\ref{lst:controlflow}. First all the labels are gathered and then
+they are placed in the correct order in the bytecode sequence. It can happen
+that multiple labels appear consecutively in the code. This is not a problem
+since the labels are resolved to real addresses later on anyways.
+
+\begin{lstlisting}[label={lst:controlflow},%
+	caption={Bytecode view for \texttt{arith}}]
+freshlabel = get >>= \st=:{freshl=[fr:frs]}->put {st & freshl=frs} >>| pure fr
+
+instance If ByteCode Stmt Stmt Stmt where If b t e = BCIfStmt b t e
+instance If ByteCode e Stmt Stmt    where If b t e = BCIfStmt b t e
+instance If ByteCode Stmt e Stmt    where If b t e = BCIfStmt b t e
+instance If ByteCode x y 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] >>|
+	t >>| tell [BCJmp endif, BCLab else] >>|
+	e >>| tell [BCLab endif]
+	)
+instance noOp ByteCode where
+	noOp = tell` [BCNop]
+\end{lstlisting}
+
+\subsection{Shared Data Sources \& Assignment}
+Shared data sources must be acquired from the state and constructing one
+happens via multiple steps. First a fresh identifier is grabbed from the state.
+Then a \CI{BCShare} record is created with that identifier. A \CI{BCSdsFetch}
+instruction is written and the body is generated to finally add the share to
+the actual state with the value obtained from the function. The exact
+implementation is shown in Listing~\ref{lst:shareview}.
+
+\begin{lstlisting}[label={lst:shareview},%
+	caption={Bytecode view for \texttt{arith}}]
+freshshare = get >>= \st=:{freshl=[fr:frs]}->put {st & freshl=frs} >>| pure fr
+
+instance sds ByteCode where
+	sds f = {main = BC (freshshare
+			>>= \sdsi->pure {BCShare | sdsi=sdsi,sdsval=BCValue 0}
+			>>= \sds->pure (f (tell` [BCSdsFetch sds]))
+			>>= \(v In bdy)->modify (addSDS sds v)
+			>>| unBC (unMain bdy))
+		}
+	pub (BC x) = BC (censor (\[BCSdsFetch s]->[BCSdsPublish s]) x)
+
+addSDS sds v s = {s & sdss=[{sds & sdsval=BCValue v}:s.sdss]}
+\end{lstlisting}
+
+All assignable types compile to an \gls{RWST} that writes one instruction. For
+example, using an \gls{SDS} always results in an expression of the form
+\CI{sds \x=4 In ...}. The actual \CI{x} is the \gls{RWST} that always writes
+one \CI{BCSdsFetch} instruction with the correct \gls{SDS} embedded. When the
+call of the \CI{x} is not a read but an assignment,  the instruction will be
+rewritten as a \CI{BCSdsStore}. The implementation for this is given in
+Listing~\ref{lst:assignmentview}.
+
+\begin{lstlisting}[label={lst:assignmentview},%
+	caption={Bytecode view implementation for assignment.}]
+instance assign ByteCode where
+	(=.) (BC v) (BC e) = BC (e >>| censor makeStore v)
+
+makeStore [BCSdsFetch i]    = [BCSdsStore i]
+makeStore [BCDigitalRead i] = [BCDigitalWrite i]
+makeStore [...]             = [...]
+\end{lstlisting}
+
+\section{Actual Compilation}
+All the previous functions are tied together with the \CI{toMessages} function.
+This function compiles the bytecode and transforms the \gls{Task} in a message.
+The \glspl{SDS} that were not already sent to the device are also placed in
+messages to be sent to the device. This functionality is listed in
+Listing~\ref{lst:compilation}. The compilation process consists of two steps.
+First the \gls{RWST} is executed, secondly the \emph{Jump} statements that jump
+to labels are transformed to jump to addresses. The translation of labels is
+possible in one sweep because no labels are reused. Reusing labels would not
+give a speed improvement since the labels are removed anyways in the end.
+
+\begin{lstlisting}[label={lst:compilation},%
+	caption={Actual compilation.}]
+bclength :: BC -> Int
+bclength (BCPush s) = 1 + size (toByteCode s)
+bclength ... = ...
+bclength x = 1 + consNum{|*|} x
+
+computeGotos :: [BC] Int -> ([BC], Map Int Int)
+computeGotos [] _ = ([], newMap)
+computeGotos [BCLab l:xs] i = appSnd ('DM'.put l i) (computeGotos xs i)
+computeGotos [x:xs] i = appFst (\bc->[x:bc]) (computeGotos xs (i + bclength x))
+
+toRealByteCode :: (ByteCode a b) BCState -> (String, BCState)
+toRealByteCode x s
+# (s, bc) = runBC x s
+# (bc, gtmap) = computeGotos bc 1
+= (concat (map (toString o toByteVal) (map (implGotos gtmap) bc)), s)
+
+toMessages :: MTaskInterval (Main (ByteCode a b)) BCState -> ([MTaskMSGSend], BCState)
+toMessages interval x oldstate
+# (bc, newstate) = toRealByteCode (unMain x) oldstate
+# newsdss = difference newstate.sdss oldstate.sdss 
+= ([MTSds sdsi e\\{sdsi,sdsval=e}<-newsdss] ++ [MTTask interval bc], newstate)
+\end{lstlisting}
+
+\section{Example}
+The heating example given previously in Listing~\ref{lst:exmtask} would be
+compiled to the following code. The left column indicates the
+position in the program memory.
+
+\begin{lstlisting}[caption={Thermostat bytecode},language=c]
+ 1-2 : BCAnalogRead (Analog A0)
+ 3-6 : BCPush (Int 50)
+ 7   : BCGre
+ 8-9 : BCJmpF 17                   //Jump to else
+10-12: BCPush (Bool 1)
+13-14: BCDigitalWrite (Digital D0)
+15-16: BCJmp 21                    //Jump to end of if
+17-19: BCPush (Bool 0)             //Else label
+20   : BCDigitalWrite (Digital D0)
+\end{lstlisting}
+
+\todo{add more elaborate example?}