\chapter[chap:future]{Future work}
\section{Improved notation for hierarchical state}
-The hierarchic state model requires quite some boilerplate code for unpacking
+The hierarchical state model requires quite some boilerplate code for unpacking
and distributing the input state and collecting and repacking the output
state.
boilerplate away. This would incur no flexibility cost at all, since there are
no other ways that would work.
-One particular notation in Haskell that seemed promising, whas he \hs{do}
+One particular notation in Haskell that seems promising, is the \hs{do}
notation. This is meant to simplify Monad notation by hiding away some
details. It allows one to write a list of expressions, which are composited
using the monadic \emph{bind} operator, written in Haskell as \hs{>>}. For
will be desugared into:
\starthaskell
-(somefunc a b) >> (otherfunc b c)
+(somefunc a) >> (otherfunc b)
\stophaskell
-There is also the \hs{>>=} operator, which allows for passing variables from
-one expression to the next. If we could use this notation to compose a
-stateful computation from a number of other stateful functions, this could
-move all the boilerplate code into the \hs{>>} operator. Perhaps the compiler
-should be taught to always inline the \hs{>>} operator, but after that there
-should be no further changes required to the compiler.
+The main reason to have the monadic notation, is to be able to wrap
+results of functions in a datatype (the \emph{monad}) that can contain
+extra information, and hide extra behaviour in the binding operators.
-This is highlights an important aspect of using a functional language for our
+The \hs{>>=} operator allows extracting the actual result of a function
+and passing it to another function. Let's try to illustrate this from an
+example. The following snippet:
+
+\starthaskell
+do
+ x <- somefunc a
+ otherfunc x
+\stophaskell
+
+will be desugared into:
+
+\starthaskell
+(somefunc a) >>= (\x -> otherfunc x)
+\stophaskell
+
+The \hs{\x -> ...} notation creates a lambda abstraction in Haskell,
+that binds the \hs{x} variable. Here, the \hs{>>=} operator is supposed
+to extract whatever result somefunc has and pass it to the lambda
+expression created. This will probably not make the monadic notation
+completely clear to a reader without prior experience with Haskell, but
+it should serve to understand the following discussion.
+
+The monadic notation could perhaps be used to compose a number of
+stateful functions into another stateful computation. Perhaps this could
+move all the boilerplate code into the \hs{>>} and \hs{>>=} operators.
+Because the boilerplate is still there (it's not magically disappeared,
+just moved into these functions), the compiler should still be able to compile
+these descriptions without any special magic (though perhaps it should
+always inline the binding operators to reveal the flow of values).
+
+This highlights an important aspect of using a functional language for our
descriptions: We can use the language itself to provide abstractions of common
-patterns, making our code smaller.
+patterns, making our code smaller and easier to read.
-\subsection{Outside the Monad}
+\subsection{Breaking out of the Monad}
However, simply using the monad notation is not as easy as it sounds. The main
problem is that the Monad type class poses a number of limitations on the
bind operator \hs{>>}. Most importantly, it has the following type signature:
(>>) :: Stateful s1 r1 -> Stateful s2 r2 -> Stateful (s1, s2) r2
\stophaskell
-What we see here, is that when we compose two stateful functions (whose inputs
-have already been applied, leaving just the state argument to be applied), the
-result is again a stateful function whose state is composed of the two
-\emph{substates}. The return value is simply the return value of the second
-function, discarding the first (to preserve that one, the \hs{>>=} operator
-can be used).
+What we see here, is that when we compose two stateful functions (that
+have already been applied to their inputs, leaving just the state
+argument to be applied to), the result is again a stateful function
+whose state is composed of the two \emph{substates}. The return value is
+simply the return value of the second function, discarding the first (to
+preserve that result, the \hs{>>=} operator can be used).
There is a trick we can apply to change the signature of the \hs{>>} operator.
\small{GHC} does not require the bind operators to be part of the \hs{Monad}
this is not a big problem. We might even be able to replace some of the
Prelude with hardware-translateable versions by doing this.
-We can now define the following binding operators. For completeness, we also
-supply the return function, which is not called by \small{GHC} implicitely,
-but can be called explicitely by a hardware description.
+The binding operators can now be defined exactly as they are needed. For
+completeness, the \hs{return} function is also defined. It is not called
+by \small{GHC} implicitely, but can be called explicitely by a hardware
+description. \in{Example}[ex:StateMonad] shows these definitions.
-\starthaskell
+\startbuffer[StateMonad]
(>>) :: Stateful s1 r1 -> Stateful s2 r2 -> Stateful (s1, s2) r2
f1 >> f2 = f1 >>= \_ -> f2
return :: r -> Stateful () r
return r = \s -> (s, r)
-\stophaskell
+\stopbuffer
+\placeexample[here][ex:StateMonad]{Binding operators to compose stateful computations}
+ {\typebufferhs{StateMonad}}
-As you can see, this closely resembles the boilerplate of unpacking state,
+These definitions closely resemble the boilerplate of unpacking state,
passing it to two functions and repacking the new state. With these
definitions, we could have writting \in{example}[ex:NestedState] a lot
shorter, see \in{example}[ex:DoState]. In this example the type signature of
foo is the same (though it is now written using the \hs{Stateful} type
-synonym, it is still completel equivalent to the original: \hs{foo :: Word ->
+synonym, it is still completely equivalent to the original: \hs{foo :: Word ->
FooState -> (FooState, Word)}.
Note that the \hs{FooState} type has changed (so indirectly the type of
stateful functions at a time, the final state consists of nested two-tuples.
The final \hs{()} in the state originates from the fact that the \hs{return}
function has no real state, but is part of the composition. We could have left
-out the return statement (and the \hs{outb <-} part) to make \hs{foo}'s return
+out the return expression (and the \hs{outb <-} part) to make \hs{foo}'s return
value equal to \hs{funcb}'s, but this approach makes it clearer what is
happening.
type FooState = ( AState, (BState, ()) )
foo :: Word -> Stateful FooState Word
foo in = do
- outa <- funca in sa
- outb <- funcb outa sb
+ outa <- funca in
+ outb <- funcb outa
return outb
\stopbuffer
-\placeexample[here][ex:DoState]{Simple function composing two stateful
+\placeexample[][ex:DoState]{Simple function composing two stateful
functions, using do notation.}
{\typebufferhs{DoState}}
two functions (components) in two directions. For most Monad instances, this
is a requirement, but here it could have been different.
+\todo{Add examples or reference for state synonyms}
+
\subsection{Alternative syntax}
-Because of the above issues, misusing Haskell's do notation is probably not
+Because of these typing issues, misusing Haskell's do notation is probably not
the best solution here. However, it does show that using fairly simple
abstractions, we could hide a lot of the boilerplate code. Extending
\small{GHC} with some new syntax sugar similar to the do notation might be a
feasible.
+\subsection{Arrows}
+Another abstraction mechanism offered by Haskell are arrows. Arrows are
+a generalisation of monads \cite[hughes98], for which \GHC also supports
+some syntax sugar \cite[paterson01]. Their use for hiding away state
+boilerplate is not directly evident, but since arrows are a complex
+concept further investigation is appropriate.
+
\section[sec:future:pipelining]{Improved notation or abstraction for pipelining}
Since pipelining is a very common optimization for hardware systems, it should
-be easy to specify a pipelined system. Since it involves quite some registers
+be easy to specify a pipelined system. Since it introduces quite some registers
into an otherwise regular combinatoric system, we might look for some way to
abstract away some of the boilerplate for pipelining.
This problem is slightly more complex than the problem we've seen before. One
significant difference is that each variable that crosses a stage boundary
-needs a registers. However, when a variable crosses multiple stage boundaries,
+needs a register. However, when a variable crosses multiple stage boundaries,
it must be stored for a longer period and should receive multiple registers.
Since we can't find out from the combinator code where the result of the
combined values is used (at least not without using Template Haskell to
This produces cumbersome code, where there is still a lot of explicitness
(though this could be hidden in syntax sugar).
+ \todo{The next sentence is unclear}
\item Scope each variable over every subsequent pipeline stage and allocate
the maximum amount of registers that \emph{could} be needed. This means we
will allocate registers that are never used, but those could be optimized
\section{Recursion}
The main problems of recursion have been described in
\in{section}[sec:recursion]. In the current implementation, recursion is
-therefore not possible, instead we rely on a number of implicit list-recursive
+therefore not possible, instead we rely on a number of implicitly list-recursive
builtin functions.
Since recursion is a very important and central concept in functional
programming, it would very much improve the flexibility and elegance of our
-hardware descriptions if we could support full recursion.
+hardware descriptions if we could support (full) recursion.
For this, there are two main problems to solve:
possible, though it will still stay a challenge. Further advances in
dependent typing support for Haskell will probably help here as well.
-TODO: Reference Christiaan and other type-level work
-(http://personal.cis.strath.ac.uk/conor/pub/she/)
+\todo{Reference Christiaan and other type-level work
+(http://personal.cis.strath.ac.uk/conor/pub/she/)}
\item For all recursion, there is the obvious challenge of deciding when
recursion is finished. For list recursion, this might be easier (Since the
base case of the recursion influences the type signatures). For general
recursion, this requires a complete set of simplification and evaluation
transformations to prevent infinite expansion. The main challenge here is how
to make this set complete, or at least define the constraints on possible
-recursion which guarantee it will work.
+recursion that guarantee it will work.
-TODO: Loop unrolling
+\todo{Reference Christian for loop unrolling?}
\stopitemize
\section{Multiple clock domains and asynchronicity}
Cλash, currently). Since every function in Cλash describes the behaviour on
each cycle boundary, we really can't fit in asynchronous behaviour easily.
-Due to the same reason, multiple clock domains cannot be supported. There is
+Due to the same reason, multiple clock domains cannot be easily supported. There is
currently no way for the compiler to know in which clock domain a function
should operate and since the clock signal is never explicit, there is also no
way to express circuits that synchronize various clock domains.
functions more generic event handlers, where the system generates a stream of
events (Like \quote{clock up}, \quote{clock down}, \quote{input A changed},
\quote{reset}, etc.). When working with multiple clock domains, each domain
-could get its own events.
+could get its own clock events.
-As an example, we would have something like the following:
-
-\starthaskell
+\startbuffer[AsyncDesc]
data Event = ClockUp | Reset | ...
type MainState = State Word
-- func is some combinatoric expression
func :: Word -> Event -> Word
func inp _ = inp * 2 + 3
-\stophaskell
+\stopbuffer
-TODO: Picture
+\placeexample[][ex:AsyncDesc]{Hardware description using asynchronous events.}
+ {\typebufferhs{AsyncDesc}}
-In this example, we see that every function takes an input of type
-\hs{Event}. The function \hs{main} that takes the output of
-\hs{func} and accumulates it on every clock cycle. On a reset signal, the
-accumulator is reset. The function \hs{func} is just a combinatoric
-function, with no synchronous elements. We can see this because there is no
-state and the event input is completely ignored. If the compiler is smart
-enough, we could even leave the event input out for functions that don't use
-it, either because they are completely combinatoric (like in this example), or
-because they rely on the the caller to select the clock signal.
+\todo{Picture}
+
+\in{Example}[ex:AsyncDesc] shows a simple example of this event-based
+approach. In this example we see that every function takes an input of
+type \hs{Event}. The function \hs{main} that takes the output of
+\hs{func} and accumulates it on every clock cycle. On a reset signal,
+the accumulator is reset. The function \hs{func} is just a combinatoric
+function, with no synchronous elements. We can see this because there
+is no state and the event input is completely ignored. If the compiler
+is smart enough, we could even leave the event input out for functions
+that don't use it, either because they are completely combinatoric (like
+in this example), or because they rely on the the caller to select the
+clock signal.
This structure is similar to the event handling structure used to perform I/O
-in languages like Amanda. TODO: Ref. There is a top level case expression that
+in languages like Amanda. \todo{ref} There is a top level case expression that
decides what to do depending on the current input event.
-A slightly more complex example that shows a system with two clock domains.
-There is no real integration between the clock domains (there is one input and
-one output for each clock domain), but it does show how multiple clocks can be
-distinguished.
+A slightly more complex example is show in
+\in{example}[ex:MulticlockDesc]. It shows a system with two clock
+domains. There is no real integration between the clock domains in this
+example (there is one input and one output for each clock domain), but
+it does show how multiple clocks can be distinguished.
-\starthaskell
+\startbuffer[MulticlockDesc]
data Event = ClockUpA | ClockUpB | ...
type MainState = State (SubAState, SubBState)
type SubBState = State ...
subb :: Word -> SubAState -> (SubAState, Word)
subb = ...
-\stophaskell
+\stopbuffer
-Note that in the above example the \hs{suba} and \hs{subb} functions are
-\emph{always} called, to get at their combinatoric outputs. The new state
-is calculated as well, but only saved when the right clock has an up
-transition.
+\placeexample[][ex:MulticlockDesc]{Hardware description with multiple clock domains through events.}
+ {\typebufferhs{MulticlockDesc}}
-As you can see, there is some code duplication in the case statement that
+Note that in \in{example}[ex:MulticlockDesc] the \hs{suba} and \hs{subb}
+functions are \emph{always} called, to get at their combinatoric
+outputs. The new state is calculated as well, but only saved when the
+right clock has an up transition.
+
+As you can see, there is some code duplication in the case expression that
selects the right clock. One of the advantages of an explicit approach like
this, is that some of this duplication can be extracted away into helper
functions. For example, we could imagine a \hs{select_clock} function, which
takes a stateful function that is not aware of events, and changes it into a
-function that only updates its state on a specific (clock) event.
+function that only updates its state on a specific (clock) event. Such a
+function is shown in \in{example}[ex:SelectClock].
-\starthaskell
+\startbuffer[SelectClock]
select_clock :: Event
-> (input -> State s -> (State s, output))
-> (input -> State s -> Event -> (State s, output))
where
(sa'', outa) = (select_clock ClockUpA suba) inpa sa event
(sb'', outb) = (select_clock ClockUpB subb) inpb sb event
-\stophaskell
+\stopbuffer
+\placeexample[][ex:SelectClock]{A function to filter clock events.}
+ {\typebufferhs{SelectClock}}
As you can see, this can greatly reduce the length of the main function, while
increasing the readability. As you might also have noted, the select\_clock
The main cost of this approach will probably be extra complexity in the
compiler: The paths (state) data can take become very non-trivial, and it
-is probably hard to properly analyze these paths and produce the intended VHDL
-description.
+is probably hard to properly analyze these paths and produce the
+intended \VHDL description.
\section{Multiple cycle descriptions}
In the current Cλash prototype, every description is a single-cycle
state value. Since we can use higher order values anywhere, why not in the
state?
-As a (contrived) example, consider the following accumulator:
-
-\starthaskell
+\startbuffer[HigherAccum]
-- The accumulator function that takes a word and returns a new accumulator
-- and the result so far. This is the function we want to put inside the
-- state.
main :: Word -> State Acc -> (State Acc, Word)
main a s = (State s', out)
where (s', out) = s a
-\stophaskell
-
-This code uses a function as its state, which implicitely contains the value
-accumulated so far. This is a fairly trivial example, that is more easy to
-write with a simple \hs{Word} state value, but for more complex descriptions
-this style might pay off. Note that in a way we are using the
-\emph{continuation passing style} of writing functions, where we pass a
-sort of \emph{continuation} from one cycle to the next.
+\stopbuffer
+\placeexample[][ex:HigherAccum]{An accumulator using a higher order state.}
+ {\typebufferhs{HigherAccum}}
+
+As a (contrived) example, consider the accumulator in
+\in{example}[ex:HigherAccum]. This code uses a function as its state,
+which implicitely contains the value accumulated so far. This is a
+fairly trivial example, that is more easy to write with a simple
+\hs{Word} state value, but for more complex descriptions this style
+might pay off. Note that in a way we are using the \emph{continuation
+passing style} of writing functions, where we pass a sort of
+\emph{continuation} from one cycle to the next.
Our normalization process completely removes higher order values inside a
function by moving applications and higher order values around so that every
particular state variable. This separation is probably a non-trivial problem,
though.
-TODO: Reference "Definitional interpreters for higher-order programming
+\todo{Reference "Definitional interpreters for higher-order programming
languages":
-http://portal.acm.org/citation.cfm?id=805852\&dl=GUIDE\&coll=GUIDE\&CFID=58835435\&CFTOKEN=81856623
+http://portal.acm.org/citation.cfm?id=805852\&dl=GUIDE\&coll=GUIDE\&CFID=58835435\&CFTOKEN=81856623}
\section{New language}
During the development of the prototype, it has become clear that Haskell is
This is of course a very intrusive solution. Every type must become member
of this typeclass, and there is now some member in every type that is a
special don't care value. Guaranteeing the obvious don't care semantics
- also becomes harder, since every pattern match or case statement must now
+ also becomes harder, since every pattern match or case expressions must now
also take care of the don't care value (this might actually be an
advantage, since it forces designers to specify how to handle don't care
for different operations).
These options should be explored further to see if they provide feasible
methods for describing don't care conditions. Possibly there are completely
other methods which work better.
+
+\section{Correctness proofs of the normalization system}
+As stated in \in{section}[sec:normalization:properties], there are a
+number of properties we would like to see verified about the
+normalization system. In particular, the \emph{termination} and
+\emph{completeness} of the system would be a good candidate for future
+research. Specifying formal semantics for the Core language in
+order to verify the \emph{soundness} of the system would be an even more
+challenging task.
+% vim: set sw=2 sts=2 expandtab:
projects / matthijs / master-project / report.git / blobdiff