X-Git-Url: https://git.stderr.nl/gitweb?p=matthijs%2Fmaster-project%2Freport.git;a=blobdiff_plain;f=Chapters%2FNormalization.tex;h=fd62fea830bb20103c8c653ef1ceeb5db745d2da;hp=433871013eced36c05be270707d14eceeed84646;hb=58a5aa7ca5edc07ba1070f4f4ed384b42e36e8f3;hpb=549db3f3ac20300b86403b0aa4320d7bf3945b5c diff --git a/Chapters/Normalization.tex b/Chapters/Normalization.tex index 4338710..fd62fea 100644 --- a/Chapters/Normalization.tex +++ b/Chapters/Normalization.tex @@ -30,13 +30,13 @@ have a direct hardware interpretation. \section{Normal form} - The transformations described here have a well-defined goal: To bring the + The transformations described here have a well-defined goal: to bring the program in a well-defined form that is directly translatable to \VHDL, while fully preserving the semantics of the program. We refer to this form as the \emph{normal form} of the program. The formal definition of this normal form is quite simple: - \placedefinition{}{\startboxed A program is in \emph{normal form} if none of the + \placedefinition[force]{}{\startboxed A program is in \emph{normal form} if none of the transformations from this chapter apply.\stopboxed} Of course, this is an \quote{easy} definition of the normal form, since our @@ -65,26 +65,6 @@ other expression. \stopitemize - \todo{Intermezzo: functions vs plain values} - - A very simple example of a program in normal form is given in - \in{example}[ex:MulSum]. As you can see, all arguments to the function (which - will become input ports in the generated \VHDL) are at the outer level. - This means that the body of the inner lambda abstraction is never a - function, but always a plain value. - - As the body of the inner lambda abstraction, we see a single (recursive) - let expression, that binds two variables (\lam{mul} and \lam{sum}). These - variables will be signals in the generated \VHDL, bound to the output port - of the \lam{*} and \lam{+} components. - - The final line (the \quote{return value} of the function) selects the - \lam{sum} signal to be the output port of the function. This \quote{return - value} can always only be a variable reference, never a more complex - expression. - - \todo{Add generated VHDL} - \startbuffer[MulSum] alu :: Bit -> Word -> Word -> Word alu = λa.λb.λc. @@ -125,13 +105,33 @@ ncline(add)(sum); \stopuseMPgraphic - \placeexample[here][ex:MulSum]{Simple architecture consisting of a + \placeexample[][ex:MulSum]{Simple architecture consisting of a multiplier and a subtractor.} \startcombination[2*1] {\typebufferlam{MulSum}}{Core description in normal form.} {\boxedgraphic{MulSum}}{The architecture described by the normal form.} \stopcombination + \todo{Intermezzo: functions vs plain values} + + A very simple example of a program in normal form is given in + \in{example}[ex:MulSum]. As you can see, all arguments to the function (which + will become input ports in the generated \VHDL) are at the outer level. + This means that the body of the inner lambda abstraction is never a + function, but always a plain value. + + As the body of the inner lambda abstraction, we see a single (recursive) + let expression, that binds two variables (\lam{mul} and \lam{sum}). These + variables will be signals in the generated \VHDL, bound to the output port + of the \lam{*} and \lam{+} components. + + The final line (the \quote{return value} of the function) selects the + \lam{sum} signal to be the output port of the function. This \quote{return + value} can always only be a variable reference, never a more complex + expression. + + \todo{Add generated VHDL} + \in{Example}[ex:MulSum] showed a function that just applied two other functions (multiplication and addition), resulting in a simple architecture with two components and some connections. There is of @@ -196,7 +196,7 @@ ncline(mux)(res) "posA(out)"; \stopuseMPgraphic - \placeexample[here][ex:AddSubAlu]{Simple \small{ALU} supporting two operations.} + \placeexample[][ex:AddSubAlu]{Simple \small{ALU} supporting two operations.} \startcombination[2*1] {\typebufferlam{AddSubAlu}}{Core description in normal form.} {\boxedgraphic{AddSubAlu}}{The architecture described by the normal form.} @@ -307,7 +307,7 @@ \stopuseMPgraphic \todo{Don't split registers in this image?} - \placeexample[here][ex:NormalComplete]{Simple architecture consisting of an adder and a + \placeexample[][ex:NormalComplete]{Simple architecture consisting of an adder and a subtractor.} \startcombination[2*1] {\typebufferlam{NormalComplete}}{Core description in normal form.} @@ -318,12 +318,13 @@ \subsection[sec:normalization:intendednormalform]{Intended normal form definition} Now we have some intuition for the normal form, we can describe how we want - the normal form to look like in a slightly more formal manner. The following - EBNF-like description captures most of the intended structure (and - generates a subset of \GHC's core format). + the normal form to look like in a slightly more formal manner. The + EBNF-like description in \in{definition}[def:IntendedNormal] captures + most of the intended structure (and generates a subset of \GHC's core + format). - There are two things missing: Cast expressions are sometimes - allowed by the prototype, but not specified here and the below + There are two things missing from this definition: cast expressions are + sometimes allowed by the prototype, but not specified here and the below definition allows uses of state that cannot be translated to \VHDL\ properly. These two problems are discussed in \in{section}[sec:normalization:castproblems] and @@ -376,16 +377,16 @@ {\defref{intended normal form definition} \typebufferlam{IntendedNormal}} - When looking at such a program from a hardware perspective, the - top level lambda abstractions define the input ports. Lambda - abstractions cannot appear anywhere else. The variable reference - in the body of the recursive let expression is the output port. - Most function applications bound by the let expression define a - component instantiation, where the input and output ports are - mapped to local signals or arguments. Some of the others use a - built-in construction (\eg\ the \lam{case} expression) or call a - built-in function (\eg\ \lam{+} or \lam{map}). For these, a - hardcoded \small{VHDL} translation is available. + When looking at such a program from a hardware perspective, the top + level lambda abstractions (\italic{lambda}) define the input ports. + Lambda abstractions cannot appear anywhere else. The variable reference + in the body of the recursive let expression (\italic{toplet}) is the + output port. Most binders bound by the let expression define a + component instantiation (\italic{userapp}), where the input and output + ports are mapped to local signals (\italic{userarg}). Some of the others + use a built-in construction (\eg\ the \lam{case} expression) or call a + built-in function (\italic{builtinapp}) such as \lam{+} or \lam{map}. + For these, a hardcoded \small{VHDL} translation is available. \section[sec:normalization:transformation]{Transformation notation} To be able to concisely present transformations, we use a specific format @@ -472,8 +473,8 @@ \stopdesc To understand this notation better, the step by step application of - the η-abstraction transformation to a simple \small{ALU} will be - shown. Consider η-abstraction, which is a common transformation from + the η-expansion transformation to a simple \small{ALU} will be + shown. Consider η-expansion, which is a common transformation from labmda calculus, described using above notation as follows: \starttrans @@ -482,12 +483,12 @@ λx.E x \lam{E} is not a lambda abstraction. \stoptrans - η-abstraction is a well known transformation from lambda calculus. What + η-expansion is a well known transformation from lambda calculus. What this transformation does, is take any expression that has a function type and turn it into a lambda expression (giving an explicit name to the argument). There are some extra conditions that ensure that this transformation does not apply infinitely (which are not necessarily part - of the conventional definition of η-abstraction). + of the conventional definition of η-expansion). Consider the following function, in Core notation, which is a fairly obvious way to specify a simple \small{ALU} (Note that it is not yet in normal form, but @@ -584,7 +585,7 @@ The type of this expression is \lam{Word}, so it does not match \lam{a -> b} and the transformation does not apply. Next, we have two options for the - next expression to look at: The function position and argument position of + next expression to look at: the function position and argument position of the application. The expression in the argument position is \lam{b}, which has type \lam{Word}, so the transformation does not apply. The expression in the function position is: @@ -597,7 +598,7 @@ function position (which makes the second condition false). In the same way the transformation does not apply to both components of this expression (\lam{case opcode of Low -> (+); High -> (-)} and \lam{a}), so - we will skip to the components of the case expression: The scrutinee and + we will skip to the components of the case expression: the scrutinee and both alternatives. Since the opcode is not a function, it does not apply here. @@ -631,7 +632,7 @@ \stoplambda The other alternative is left as an exercise to the reader. The final - function, after applying η-abstraction until it does no longer apply is: + function, after applying η-expansion until it does no longer apply is: \startlambda alu :: Bit -> Word -> Word -> Word @@ -672,21 +673,29 @@ A \emph{hardware representable} (or just \emph{representable}) type or value is (a value of) a type that we can generate a signal for in hardware. For example, a bit, a vector of bits, a 32 bit unsigned word, etc. Values that are - not runtime representable notably include (but are not limited to): Types, + not runtime representable notably include (but are not limited to): types, dictionaries, functions. \defref{representable} - A \emph{built-in function} is a function supplied by the Cλash framework, whose - implementation is not valid Cλash. The implementation is of course valid - Haskell, for simulation, but it is not expressable in Cλash. - \defref{built-in function} \defref{user-defined function} + A \emph{built-in function} is a function supplied by the Cλash + framework, whose implementation is not used to generate \VHDL. This is + either because it is no valid Cλash (like most list functions that need + recursion) or because a Cλash implementation would be unwanted (for the + addition operator, for example, we would rather use the \VHDL addition + operator to let the synthesis tool decide what kind of adder to use + instead of explicitly describing one in Cλash). \defref{built-in + function} - For these functions, Cλash has a \emph{built-in hardware translation}, so calls - to these functions can still be translated. These are functions like - \lam{map}, \lam{hwor} and \lam{length}. + These are functions like \lam{map}, \lam{hwor}, \lam{+} and \lam{length}. - A \emph{user-defined} function is a function for which we do have a Cλash - implementation available. + For these functions, Cλash has a \emph{built-in hardware translation}, + so calls to these functions can still be translated. Built-in functions + must have a valid Haskell implementation, of course, to allow + simulation. + + A \emph{user-defined} function is a function for which no built-in + translation is available and whose definition will thus need to be + translated to Cλash. \defref{user-defined function} \subsubsection[sec:normalization:predicates]{Predicates} Here, we define a number of predicates that can be used below to concisely @@ -729,12 +738,12 @@ \stoplambda This is obviously not what was supposed to happen! The root of this problem is - the reuse of binders: Identical binders can be bound in different, + the reuse of binders: identical binders can be bound in different, but overlapping scopes. Any variable reference in those overlapping scopes then refers to the variable bound in the inner (smallest) scope. There is not way to refer to the variable in the outer scope. This effect is usually referred to as - \emph{shadowing}: When a binder is bound in a scope where the + \emph{shadowing}: when a binder is bound in a scope where the binder already had a value, the inner binding is said to \emph{shadow} the outer binding. In the example above, the \lam{c} binder was bound outside of the expression and in the inner lambda @@ -943,7 +952,7 @@ \transexample{unusedlet}{Unused let binding removal}{from}{to} \subsubsection{Empty let removal} - This transformation is simple: It removes recursive lets that have no bindings + This transformation is simple: it removes recursive lets that have no bindings (which usually occurs when unused let binding removal removes the last binding from it). @@ -1090,7 +1099,7 @@ of the other value definitions in let bindings and making the final return value a simple variable reference. - \subsubsection[sec:normalization:eta]{η-abstraction} + \subsubsection[sec:normalization:eta]{η-expansion} This transformation makes sure that all arguments of a function-typed expression are named, by introducing lambda expressions. When combined with β-reduction and non-representable binding inlining, all function-typed @@ -1114,7 +1123,7 @@ False -> λy.id y) x \stopbuffer - \transexample{eta}{η-abstraction}{from}{to} + \transexample{eta}{η-expansion}{from}{to} \subsubsection[sec:normalization:appprop]{Application propagation} This transformation is meant to propagate application expressions downwards @@ -1186,7 +1195,7 @@ This transformation makes all non-recursive lets recursive. In the end, we want a single recursive let in our normalized program, so all non-recursive lets can be converted. This also makes other - transformations simpler: They only need to be specified for recursive + transformations simpler: they only need to be specified for recursive let expressions (and simply will not apply to non-recursive let expressions until this transformation has been applied). @@ -1275,7 +1284,7 @@ Note that the return value is not simplified if its not representable. Otherwise, this would cause a direct loop with the inlining of unrepresentable bindings. If the return value is - not representable because it has a function type, η-abstraction + not representable because it has a function type, η-expansion should make sure that this transformation will eventually apply. If the value is not representable for other reasons, the function result itself is not representable, meaning this @@ -1290,8 +1299,8 @@ \stoptrans \starttrans - x = λv0 ... λvn.E - ~ \lam{E} is representable + x = λv0 ... λvn.E \lam{E} is representable + ~ \lam{E} is not a lambda abstraction E \lam{E} is not a let expression --------------------------- \lam{E} is not a local variable reference letrec x = E in x @@ -1493,6 +1502,46 @@ \stopframedtext } + \subsubsection{Scrutinee binder removal} + This transformation removes (or rather, makes wild) the binder to + which the scrutinee is bound after evaluation. This is done by + replacing the bndr with the scrutinee in all alternatives. To prevent + duplication of work, this transformation is only applied when the + scrutinee is already a simple variable reference (but the previous + transformation ensures this will eventually be the case). The + scrutinee binder itself is replaced by a wild binder (which is no + longer displayed). + + Note that one could argue that this transformation can change the + meaning of the Core expression. In the regular Core semantics, a case + expression forces the evaluation of its scrutinee and can be used to + implement strict evaluation. However, in the generated \VHDL, + evaluation is always strict. So the semantics we assign to the Core + expression (which differ only at this particular point), this + transformation is completely valid. + + \starttrans + case x of bndr + alts + ----------------- \lam{x} is a local variable reference + case x of + alts[bndr=>x] + \stoptrans + + \startbuffer[from] + case x of y + True -> y + False -> not y + \stopbuffer + + \startbuffer[to] + case x of + True -> x + False -> not x + \stopbuffer + + \transexample{scrutbndrremove}{Scrutinee binder removal}{from}{to} + \subsubsection{Case normalization} This transformation ensures that all case expressions get a form that is allowed by the intended normal form. This means they @@ -1618,9 +1667,9 @@ values used in our expression representable. There are two main transformations that are applied to \emph{all} unrepresentable let bindings and function arguments. These are meant to address three - different kinds of unrepresentable values: Polymorphic values, + different kinds of unrepresentable values: polymorphic values, higher-order values and literals. The transformation are described - generically: They apply to all non-representable values. However, + generically: they apply to all non-representable values. However, non-representable values that do not fall into one of these three categories will be moved around by these transformations but are unlikely to completely disappear. They usually mean the program was not @@ -1649,7 +1698,7 @@ take care of exactly this. There is one case where polymorphism cannot be completely - removed: Built-in functions are still allowed to be polymorphic + removed: built-in functions are still allowed to be polymorphic (Since we have no function body that we could properly specialize). However, the code that generates \VHDL\ for built-in functions knows how to handle this, so this is not a problem. @@ -1727,11 +1776,11 @@ lambda abstraction. To reduce all higher-order values to one of the above items, a number - of transformations we have already seen are used. The η-abstraction + of transformations we have already seen are used. The η-expansion transformation from \in{section}[sec:normalization:eta] ensures all function arguments are introduced by lambda abstraction on the highest level of a function. These lambda arguments are allowed because of - \in{item}[item:toplambda] above. After η-abstraction, our example + \in{item}[item:toplambda] above. After η-expansion, our example becomes a bit bigger: \startlambda @@ -1742,7 +1791,7 @@ ) q \stoplambda - η-abstraction also introduces extra applications (the application of + η-expansion also introduces extra applications (the application of the let expression to \lam{q} in the above example). These applications can then propagated down by the application propagation transformation (\in{section}[sec:normalization:appprop]). In our @@ -1761,8 +1810,8 @@ representable type). Completely applied top level functions (like the first alternative) are now no longer invalid (they fall under \in{item}[item:completeapp] above). (Completely) applied lambda - abstractions can be removed by β-abstraction. For our example, - applying β-abstraction results in the following: + abstractions can be removed by β-expansion. For our example, + applying β-expansion results in the following: \startlambda λy.λq.let double = λx. x + x in @@ -1873,7 +1922,7 @@ \hs{Bool} Haskell type, which is just an enumerated type. There is, however, a second type of literal that does not have a - representable type: Integer literals. Cλash supports using integer + representable type: integer literals. Cλash supports using integer literals for all three integer types supported (\hs{SizedWord}, \hs{SizedInt} and \hs{RangedWord}). This is implemented using Haskell's \hs{Num} type class, which offers a \hs{fromInteger} method @@ -2117,7 +2166,7 @@ in y + z \stoplambda - Looking at this, we could imagine an alternative approach: Create a + Looking at this, we could imagine an alternative approach: create a transformation that removes let bindings that bind identical values. In the above expression, the \lam{y} and \lam{z} variables could be merged together, resulting in the more efficient expression: @@ -2220,12 +2269,12 @@ expanding some expression. \item[q:soundness] Is our system \emph{sound}? Since our transformations continuously modify the expression, there is an obvious risk that the final - normal form will not be equivalent to the original program: Its meaning could + normal form will not be equivalent to the original program: its meaning could have changed. \item[q:completeness] Is our system \emph{complete}? Since we have a complex system of transformations, there is an obvious risk that some expressions will not end up in our intended normal form, because we forgot some transformation. - In other words: Does our transformation system result in our intended normal + In other words: does our transformation system result in our intended normal form for all possible inputs? \item[q:determinism] Is our system \emph{deterministic}? Since we have defined no particular order in which the transformation should be applied, there is an @@ -2233,18 +2282,20 @@ \emph{different} normal forms. They might still both be intended normal forms (if our system is \emph{complete}) and describe correct hardware (if our system is \emph{sound}), so this property is less important than the previous - three: The translator would still function properly without it. + three: the translator would still function properly without it. \stopitemize Unfortunately, the final transformation system has only been developed in the final part of the research, leaving no more time for verifying these properties. In fact, it is likely that the current transformation system still violates some of these - properties in some cases and should be improved (or extra conditions - on the input hardware descriptions should be formulated). + properties in some cases (see + \in{section}[sec:normalization:non-determinism] and + \in{section}[sec:normalization:stateproblems]) and should be improved (or + extra conditions on the input hardware descriptions should be formulated). This is most likely the case with the completeness and determinism - properties, perhaps als the termination property. The soundness + properties, perhaps also the termination property. The soundness property probably holds, since it is easier to manually verify (each transformation can be reviewed separately). @@ -2321,12 +2372,11 @@ \todo{Define β-reduction and η-reduction?} - Note that the normal form of such a system consists of the set of nodes - (expressions) without outgoing edges, since those are the expressions to which - no transformation applies anymore. We call this set of nodes the \emph{normal - set}. The set of nodes containing expressions in intended normal - form \refdef{intended normal form} is called the \emph{intended - normal set}. + In such a graph a node (expression) is in normal form if it has no + outgoing edges (meaning no transformation applies to it). The set of + nodes without outgoing edges is called the \emph{normal set}. Similarly, + the set of nodes containing expressions in intended normal form + \refdef{intended normal form} is called the \emph{intended normal set}. From such a graph, we can derive some properties easily: \startitemize[KR] @@ -2420,7 +2470,7 @@ Since each of the transformations can be applied to any subexpression as well, there is a constraint on our meaning - definition: The meaning of an expression should depend only on the + definition: the meaning of an expression should depend only on the meaning of subexpressions, not on the expressions themselves. For example, the meaning of the application in \lam{f (let x = 4 in x)} should be the same as the meaning of the application in \lam{f @@ -2441,11 +2491,11 @@ each node in the normal set is also in the intended normal set. Reasoning about our intended normal set is easier, since we know how to generate it from its definition. \refdef{intended normal - form definition}. + form definition} Fortunately, we can also prove the complement (which is equivalent, since $A \subseteq B \Leftrightarrow \overline{B} - \subseteq \overline{A}$): Show that the set of nodes not in + \subseteq \overline{A}$): show that the set of nodes not in intended normal form is a subset of the set of nodes not in normal form. In other words, show that for every expression that is not in intended normal form, that there is at least one transformation