From 7b0fe8509016c0841d35239dc87150e945cfd960 Mon Sep 17 00:00:00 2001 From: Mart Lubbers Date: Tue, 6 Jun 2017 12:07:17 +0200 Subject: [PATCH] add stuff about assignments, class implementation etc --- methods.dsl.tex | 8 +-- methods.mtask.tex | 14 ++--- methods.top.tex | 6 +-- results.arch.tex | 8 +-- results.mtask.tex | 135 ++++++++++++++++++++++++++++++++++++++++++++-- thesis.pre | 28 +++++----- 6 files changed, 163 insertions(+), 36 deletions(-) diff --git a/methods.dsl.tex b/methods.dsl.tex index be9d7ac..1a153b1 100644 --- a/methods.dsl.tex +++ b/methods.dsl.tex @@ -12,7 +12,7 @@ functions that transform something to the datatype or the other way around. As an example we have the simple arithmetic \gls{EDSL} shown in Listing~\ref{lst:exdeep}. -\begin{lstlisting}[language=Clean,label={lst:exdeep},% +\begin{lstlisting}[label={lst:exdeep},% caption={A minimal deep \gls{EDSL}}] :: DSL = LitI Int @@ -39,7 +39,7 @@ using bimaps or projection pairs\cite{cheney_lightweight_2002}. Unfortunately the lack of extendability remains a problem. If a language construct is added, no compile time guarantee is given that all views support it. -\begin{lstlisting}[language=Clean,label={lst:exdeepgadt},% +\begin{lstlisting}[label={lst:exdeepgadt},% caption={A minimal deep \gls{EDSL} using \glspl{GADT}}] :: DSL a = LitI Int -> DSL Int @@ -57,7 +57,7 @@ the host language. An evaluator view for our example language then looks something like the code shown in Listing~\ref{lst:exshallow}. Note that much of the internals of the language can be hidden using monads. -\begin{lstlisting}[language=Clean,label={lst:exshallow},% +\begin{lstlisting}[label={lst:exshallow},% caption={A minimal shallow \gls{EDSL}}] :: Env = ... // Some environment :: DSL a = DSL (Env -> a) @@ -109,7 +109,7 @@ must be updated accordingly to prevent possible runtime errors. When an extension is added in a new class, this problem does not arise and views can choose to implement only parts of the collection of classes. -\begin{lstlisting}[language=Clean,label={lst:exclassshallow},% +\begin{lstlisting}[label={lst:exclassshallow},% caption={A minimal class based shallow \gls{EDSL}}] :: Env = ... // Some environment :: Evaluator a = Evaluator (Env -> a) diff --git a/methods.mtask.tex b/methods.mtask.tex index 67f4b4e..1662d6d 100644 --- a/methods.mtask.tex +++ b/methods.mtask.tex @@ -26,7 +26,7 @@ restriction describes updatable expressions such as \gls{GPIO} pins and \glspl{SDS}. \begin{lstlisting}[% - language=Clean,label={lst:exprhier},caption={Expression role hierarchy}] + label={lst:exprhier},caption={Expression role hierarchy}] :: Upd = Upd :: Expr = Expr :: Stmt = Stmt @@ -46,7 +46,7 @@ brevity. Moreover, the class restrictions are only shown in the first functions and omitted in subsequent funcitons. Both the boolean expression and arithmetic expression classes are shown in Listing~\ref{lst:arithbool}. -\begin{lstlisting}[language=Clean,label={lst:arithbool}, +\begin{lstlisting}[label={lst:arithbool}, caption={Basic classes for expressions}] class arith v where lit :: t -> v t Expr @@ -76,7 +76,7 @@ The sequence operator is very straightforward and just ties the two expressions together in sequence. \begin{lstlisting}[% - language=Clean,label={lst:control},caption={Control flow operators}] + label={lst:control},caption={Control flow operators}] class If v q r ~s where If :: (v Bool p) (v t q) (v t r) -> v t s | ... @@ -97,7 +97,7 @@ The classes facilitating this are shown in Listing~\ref{lst:sdsio}. In this way the assignment is the same for every assignable entity. \begin{lstlisting}[% - language=Clean,label={lst:sdsio},caption={Input/Output classes}] + label={lst:sdsio},caption={Input/Output classes}] :: DigitalPin = D0 | D1 | D2 | D3 | D4 | D5 |D6 | D7 | D8 | D9 | D10 | D11 | D12 | D13 :: AnalogPin = A0 | A1 | A2 | A3 | A4 | A5 :: UserLED = LED1 | LED2 | LED3 @@ -127,7 +127,7 @@ Listing~\ref{lst:sdsclass}. The \CI{Main} type is introduced to box an \gls{mTask} and make it recognizable by the type system. \begin{lstlisting}[% - language=Clean,label={lst:sdsclass},caption={\glspl{SDS} in \gls{mTask}}] + label={lst:sdsclass},caption={\glspl{SDS} in \gls{mTask}}] :: In a b = In infix 0 a b :: Main a = {main :: a} @@ -184,7 +184,7 @@ complex and therefore an example is given. The aforementioned Listing shows a simple specification containing one task that increments a value indefinitely every one seconds. -\begin{lstlisting}[language=Clean,label={lst:taskclass},% +\begin{lstlisting}[label={lst:taskclass},% caption={The classes for defining tasks}] class mtask v a where task :: (((v delay r) a->v MTask Expr)->In (a->v u p) (Main (v t q))) -> Main (v t q) | ... @@ -203,7 +203,7 @@ representing a temperature sensor is too high. \CI{thermostat`} shows the same expression but now using the assignment style \gls{GPIO} technique. \begin{lstlisting}[% - language=Clean,label={lst:exmtask},caption={Some example \glspl{mTask}}] + label={lst:exmtask},caption={Some example \glspl{mTask}}] blink = task \blink=(\x. IF (x ==. lit True) (ledOn led) (ledOff led) :. blink (lit 1000) (Not x) diff --git a/methods.top.tex b/methods.top.tex index 3acfb17..cb951a1 100644 --- a/methods.top.tex +++ b/methods.top.tex @@ -27,7 +27,7 @@ image all fields are entered and the \CI{TaskValue} transitions to the \caption{The states of a \CI{TaskValue}}\label{fig:taskvalue} \end{figure} -\begin{lstlisting}[language=Clean,label={lst:taskex},% +\begin{lstlisting}[label={lst:taskex},% caption={An example \gls{Task} for entering a name}] :: Name = { firstname :: String , lastname :: String @@ -100,7 +100,7 @@ Listing~\ref{lst:combinators}. dictates. \end{itemize} -\begin{lstlisting}[language=Clean,% +\begin{lstlisting}[% caption={\Gls{Task}-combinators},label={lst:combinators}] //Step combinator (>>*) infixl 1 :: (Task a) [TaskCont a (Task b)] -> Task b | iTask a & iTask b @@ -134,7 +134,7 @@ operations are atomic in the sense that during reading no other tasks are executed. \begin{lstlisting}[% - language=Clean,label={lst:shares},caption={\Gls{SDS} functions}] + label={lst:shares},caption={\Gls{SDS} functions}] get :: (ReadWriteShared r w) -> Task r | iTask r set :: w (ReadWriteShared r w) -> Task w | iTask w upd :: (r -> w) (ReadWriteShared r w) -> Task w | iTask r & iTask w diff --git a/results.arch.tex b/results.arch.tex index 87a25cb..cbef26c 100644 --- a/results.arch.tex +++ b/results.arch.tex @@ -40,7 +40,7 @@ send a request for specification. The client will serialize his specification and send it to the server so that the server knows what the client is capable of. The exact specification is listed in Listing~\ref{lst:devicespec} -\begin{lstlisting}[language=Clean,label={lst:devicespec}, +\begin{lstlisting}[label={lst:devicespec}, caption={Device specification for \glspl{mTask}}] :: MTaskDeviceSpec = {haveLed :: Bool @@ -74,7 +74,7 @@ stores the specification of the device that is received when connecting. All of this is listed in Listing~\ref{lst:mtaskdevice}. The definitions of the message format are explained in the following section. -\begin{lstlisting}[language=Clean,caption={Device type},label={lst:mtaskdevice}] +\begin{lstlisting}[caption={Device type},label={lst:mtaskdevice}] deviceStore :: Shared [MTaskDevice] :: Channels :== ([MTaskMSGRecv], [MTaskMSGSend], Bool) @@ -101,7 +101,7 @@ class MTaskDuplex a where \section{Communication} All \gls{mTask} messages are encoded following the specification given in Appendix~\ref{app:communication-protocol}. Available messages are: -\begin{lstlisting}[language=Clean,caption={Available messages}] +\begin{lstlisting}[caption={Available messages}] :: MTaskMSGRecv = MTTaskAck Int Int | MTTaskDelAck Int | MTSDSAck Int | MTSDSDelAck Int @@ -130,7 +130,7 @@ their channels. This allows you to give an old device record to the function and still update the latest instance. Listing~\ref{lst:connectDevice} shows the connection function. -\begin{lstlisting}[language=Clean,label={lst:connectDevice},% +\begin{lstlisting}[label={lst:connectDevice},% caption={Connect a device}] withDevices :: MTaskDevice (MTaskDevice -> MTaskDevice) -> Task [MTaskDevice] diff --git a/results.mtask.tex b/results.mtask.tex index 8c22015..9580dec 100644 --- a/results.mtask.tex +++ b/results.mtask.tex @@ -5,6 +5,9 @@ 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. +\section{Semantics} +\todo{semantics} + \section{Bytecode compilation} 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 @@ -32,7 +35,7 @@ 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}[language=Clean,label={lst:bcview},caption={Bytecode view}] +\begin{lstlisting}[label={lst:bcview},caption={Bytecode view}] :: ByteCode a p = BC (RWS () [BC] BCState ()) :: BCValue = E.e: BCValue e & mTaskType, TC e :: BCShare = { @@ -58,15 +61,137 @@ 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 a Expr +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 + ... -\subsection{Arithmetics} +instance userLed ByteCode where + ledOn l = op l BCLedOn + ledOff l = op l BCLedOff +\end{lstlisting} \subsection{Control Flow} +\begin{lstlisting}[label={lst:controlflow},% + caption={Bytecode view for \texttt{arith}}] +instance noOp ByteCode where + noOp = tell` [BCNop] +\end{lstlisting} -\subsection{Shared Data Sources} +\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. The exact implementation is shown in +Listing~\ref{lst:shareview}. -\section{Semantics} +\begin{lstlisting}[label={lst:shareview},% + caption={Bytecode view for \texttt{arith}}] +instance sds ByteCode where + sds f = {main = BC (freshs + >>= \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) -\todo{Uitleggen wat het systeem precies doet} +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} +\todo{hulp functies voor compileren} diff --git a/thesis.pre b/thesis.pre index 7e46909..988e6e0 100644 --- a/thesis.pre +++ b/thesis.pre @@ -62,6 +62,7 @@ {\\}{{$\lambda\:$}}1 {A.}{{$\forall\;\,$}}1 {E.}{{$\exists\;\,$}}1 + {*}{{$^*$}}1 % {>}{{$>$}}1 % {<}{{$<$}}1 % {<=}{{$\leq$}}1 @@ -95,19 +96,20 @@ \newcommand{\CI}[1]{\lstinline[language=Clean,basicstyle=\ttfamily\fontseries{l}\normalsize]|#1|} \lstset{% - breakatwhitespace=false, % sets if automatic breaks should only happen at whitespace - breaklines=true, % sets automatic line breaking - captionpos=b, % sets the caption-position to bottom - keepspaces=true, % keeps spaces in text, useful for keeping indentation of code (possibly needs columns=flexible) - basicstyle=\ttfamily\fontseries{l}\footnotesize,% the size of the fonts that are used for the code - commentstyle=\itshape\fontseries{m}, % comment style - keywordstyle=\bfseries\fontseries{b}, % keyword style - stringstyle=\ttfamily, % string literal style - showspaces=false, % show spaces everywhere adding particular underscores; it overrides 'showstringspaces' - showstringspaces=false, % underline spaces within strings only - showtabs=false, % show tabs within strings adding particular underscores - tabsize=4, % sets default tabsize to 2 spaces - frame=L + breakatwhitespace=false, + breaklines=true, + captionpos=b, + keepspaces=true, + basicstyle=\ttfamily\fontseries{l}\footnotesize, + commentstyle=\itshape\fontseries{m}, + keywordstyle=\bfseries\fontseries{b}, + stringstyle=\ttfamily, + showspaces=false, + showstringspaces=false, + showtabs=false, + tabsize=4, + frame=L, + language=Clean } \title{iTasks and the Internet of Things} -- 2.20.1