source: doc/theses/aaron_moss_PhD/phd/resolution-heuristics.tex @ f2c5726

Last change on this file since f2c5726 was f2c5726, checked in by Aaron Moss <a3moss@…>, 5 years ago

thesis: start asymptotic analysis of resolution problem

  • Property mode set to 100644
File size: 21.0 KB
1\chapter{Resolution Heuristics}
4% consider using "satisfaction" throughout when talking about assertions
6The main task of the \CFACC{} type-checker is \emph{expression resolution}, determining which declarations the identifiers in each expression correspond to.
7Resolution is a straightforward task in C, as no declarations share identifiers, but in \CFA{} the name overloading features discussed in Section~\ref{overloading-sec} generate multiple candidate declarations for each identifier.
8I refer to a given matching between identifiers and declarations in an expression as an \emph{interpretation}; an interpretation also includes information about polymorphic type bindings and implicit casts to support the \CFA{} features discussed in Sections~\ref{poly-func-sec} and~\ref{implicit-conv-sec}, each of which increase the proportion of feasible candidate interpretations.
9To choose between feasible interpretations, \CFA{} defines a \emph{conversion cost} to rank interpretations; the expression resolution problem is thus to find the unique minimal-cost interpretation for an expression, reporting an error if no such interpretation exists.
11\section{Expression Resolution}
13\subsection{Type Unification}
15The polymorphism features of \CFA{} require binding of concrete types to polymorphic type variables.
16Briefly, \CFACC{} keeps a mapping from type variables to the concrete types they are bound to as an auxiliary data structure during expression resolution; Chapter~\ref{env-chap} describes this \emph{environment} data structure in more detail.
17A \emph{unification} algorithm is used to simultaneously check two types for equivalence with respect to the substitutions in an environment and update that environment.
18Essentially, unification recursively traverses the structure of both types, checking them for equivalence, and when it encounters a type variable it replaces it with the concrete type it is bound to; if the type variable has not yet been bound, the unification algorithm assigns the equivalent type as the bound type of the variable, after performing various consistency checks.
19Ditchfield\cite{Ditchfield92} and Bilson\cite{Bilson03} describe the semantics of \CFA{} unification in more detail.
21\subsection{Conversion Cost}
23C does not have an explicit cost model for implicit conversions, but the ``usual arithmetic conversions''\cit{} used to decide which arithmetic operators to use define one implicitly.
24Beginning with the work of Bilson\cite{Bilson03}, \CFA{} has defined a \emph{conversion cost} for each function call in a way that generalizes C's conversion rules.
25Loosely defined, the conversion cost counts the implicit conversions utilized by an interpretation.
26With more specificity, the cost is a lexicographically-ordered tuple, where each element corresponds to a particular kind of conversion.
27In Bilson's \CFA{} design, conversion cost is a 3-tuple, $(unsafe, poly, safe)$, where $unsafe$ is the count of unsafe (narrowing) conversions, $poly$ is the count of polymorphic type bindings, and $safe$ is the sum of the degree of safe (widening) conversions.
28The following example lists the cost in the Bilson model of calling each of the following functions with two !int! parameters:
31void f(char, long); $\C{// (1,0,1)}$
32forall(otype T) void f(T, long); $\C{// (0,1,1)}$
33void f(long, long); $\C{// (0,0,2)}$
34void f(int, unsigned long); $\C{// (0,0,2)}$
35void f(int, long); $\C{// (0,0,1)}$
38Note that safe and unsafe conversions are handled differently; \CFA{} counts ``distance'' of safe conversions (\eg{} !int! to !long! is cheaper than !int! to !unsigned long!), while only counting the number of unsafe conversions (\eg{} !int! to !char! and !int! to !short! both have unsafe cost 1).
40As part of adding reference types to \CFA{} (see Section~\ref{type-features-sec}), Schluntz added a new $reference$ element to the cost tuple, which counts the number of implicit reference-to-rvalue conversions performed so that candidate interpretations can be distinguished by how closely they match the nesting of reference types; since references are meant to act almost indistinguishably from lvalues, this $reference$ element is the least significant in the lexicographic comparison of cost tuples.
42I have also refined the \CFA{} cost model as part of this thesis work.
43Bilson's \CFA{} cost model includes the cost of polymorphic type bindings from a function's type assertions in the $poly$ element of the cost tuple; this has the effect of making more-constrained functions more expensive than less-constrained functions.
44However, type assertions actually make a function \emph{less} polymorphic, and as such functions with more type assertions should be preferred in type resolution.
45As an example, some iterator-based algorithms can work on a forward iterator that only provides an increment operator, but are more efficient on a random-access iterator that can be incremented by an arbitrary number of steps in a single operation.
46The random-access iterator has more type constraints, but should be chosen whenever those constraints can be satisfied.
47As such, I have added a $specialization$ element to the \CFA{} cost tuple, the values of which are always negative.
48Each type assertion subtracts 1 from $specialization$, so that more-constrained functions will cost less and thus be chosen over less-constrained functions, all else being equal.
49A more sophisticated design would define a partial order over sets of type assertions by set inclusion (\ie{} one function would only cost less than another if it had a strict superset of assertions,  rather than just more total assertions), but I did not judge the added complexity of computing and testing this order to be worth the gain in specificity.
51I have also incorporated an unimplemented aspect of Ditchfield's earlier cost model.
52In the example below, adapted from \cite[89]{Ditchfield92}, Bilson's cost model only distinguished between the first two cases by accounting extra cost for the extra set of !otype! parameters, which, as discussed above, is not a desirable solution:
55forall(otype T, otype U) void f(T, U);  $\C[3.25in]{// polymorphic}$
56forall(otype T) void f(T, T);  $\C[3.25in]{// less polymorphic}$
57forall(otype T) void f(T, int);  $\C[3.25in]{// even less polymorphic}$
58forall(otype T) void f(T*, int); $\C[3.25in]{// least polymorphic}$
61I account for the fact that functions with more polymorphic variables are less constrained by introducing a $var$ cost element that counts the number of type variables on a candidate function.
62In the example above, the first !f! has $var = 2$, while the remainder have $var = 1$.
63My new \CFA{} cost model also accounts for a nuance un-handled by Ditchfield or Bilson, in that it makes the more specific fourth function above cheaper than the more generic third function.
64The fourth function is presumably somewhat optimized for handling pointers, but the prior \CFA{} cost model could not account for the more specific binding, as it simply counted the number of polymorphic unifications.
66In my modified model, each level of constraint on a polymorphic type in the parameter list results in a decrement of the $specialization$ cost element.
67Thus, all else equal, if both a binding to !T! and a binding to !T*! are available, \CFA{} will pick the more specific !T*! binding.
68This process is recursive, such that !T**! produces a -2 specialization cost, as opposed to the -1 cost for !T*!.
69This works similarly for generic types, \eg{} !box(T)! also has specialization cost -1.
70For multi-argument generic types, the least-specialized polymorphic parameter sets the specialization cost, \eg{} the specialization cost of !pair(T, S*)! is -1 (from !T!) rather than -2 (from !S!).
71Since the user programmer provides parameters, but cannot provide guidance on return type, specialization cost is not counted for the return type list.
72Since both $vars$ and $specialization$ are properties of the declaration rather than any particular interpretation, they are prioritized less than the interpretation-specific conversion costs from Bilson's original 3-tuple.
73The current \CFA{} cost tuple is thus as follows:
76        (unsafe, poly, safe, vars, specialization, reference)
79\subsection{Expression Cost}
81The mapping from \CFA{} expressions to cost tuples is described by Bilson in \cite{Bilson03}, and remains effectively unchanged modulo the refinements to the cost tuple described above.
82Nonetheless, some salient details are repeated here for the sake of completeness.
84On a theoretical level, the resolver algorithm treats most expressions as if they were function calls.
85Operators in \CFA{} (both those existing in C and added features like constructors) are all modelled as function calls.
86In terms of the core argument-parameter matching algorithm, the overloaded variables of \CFA{} are not handled differently from zero-argument function calls, aside from a different pool of candidate declarations and setup for different code generation.
87Similarly, an aggregate member expression !a.m! can be modelled as a unary function !m! that takes one argument of the aggregate type.
88Literals do not require sophisticated resolution, as the syntactic form of each implies their result types (\eg{} !42! is int, !"hello"! is !char*!, \etc{}), though struct literals require resolution of the implied constructor call.
90Since most expressions can be treated as function calls, nested function calls are the primary component of expression resolution problem instances.
91Each function call has an \emph{identifier} which must match the name of the corresponding declaration, and a possibly-empty list of \emph{arguments}.
92These arguments may be function call expressions themselves, producing a tree of function-call expressions to resolve, where the leaf expressions are generally nullary functions, variable expressions, or literals.
93A single instance of expression resolution consists of matching declarations to all the identifiers in the expression tree of a top-level expression, along with inserting any conversions and assertions necessary for that matching.
94The cost of a function-call expression is the sum of the conversion costs of each argument type to the corresponding parameter and the total cost of each subexpression, recursively calculated.
95\CFA{} expression resolution must produce either the unique lowest-cost interpretation of the top-level expression, or an appropriate error message if none such exists.
96The cost model of \CFA{} precludes a simple bottom-up resolution pass, as constraints and costs introduced by calls higher in the expression tree can change the interpretation of those lower in the tree, as in the following example:
99void f(int);
100double g(int); $\C{// g1}$
101int g(double); $\C{// g2}$
103f( g(42) );
106!g1! is the cheapest interpretation of !g(42)!, with cost $(0,0,0,0,0,0)$ since the argument type is an exact match, but to downcast the return type of !g1! to an !int! suitable for !f! requires an unsafe conversion for a total cost of $(1,0,0,0,0,0)$.
107If !g2! is chosen, on the other hand, there is a safe upcast from the !int! type of !42! to !double!, but no cast on the return of !g!, for a total cost of $(0,0,1,0,0,0)$; as this is cheaper, $g2$ is chosen.
108Due to this design, in general all feasible interpretations of subexpressions must be propagated to the top of the expression tree before any can be eliminated, a lazy form of expression resolution, as opposed to the eager expression resolution allowed by C, where each expression can be resolved given only the resolution of its immediate subexpressions.
110If there are no feasible interpretations of the top-level expression, expression resolution fails and must produce an appropriate error message.
111If any subexpression has no feasible interpretations, the process can be short-circuited and the error produced at that time.
112If there are multiple feasible interpretations of a top-level expression, ties are broken based on the conversion cost, calculated as above.
113If there are multiple minimal-cost feasible interpretations of a top-level expression, that expression is said to be \emph{ambiguous}, and an error must be produced.
114Multiple minimal-cost interpretations of a subexpression do not necessarily imply an ambiguous top-level expression, however, as the subexpression interpretations may be disambiguated based on their return type or by selecting a more-expensive interpretation of that subexpression to reduce the overall expression cost, as above.
116The \CFA{} resolver uses type assertions to filter out otherwise-feasible subexpression interpretations.
117An interpretation can only be selected if all the type assertions in the !forall! clause on the corresponding declaration can be satisfied with a unique minimal-cost set of satisfying declarations.
118Type assertion satisfaction is tested by performing type unification on the type of the assertion and the type of the declaration satisfying the assertion.
119That is, a declaration which satisfies a type assertion must have the same name and type as the assertion after applying the substitutions in the type environment.
120Assertion-satisfying declarations may be polymorphic functions with assertions of their own that must be satisfied recursively.
121This recursive assertion satisfaction has the potential to introduce infinite loops into the type resolution algorithm, a situation which \CFACC{} avoids by imposing a hard limit on the depth of recursive assertion satisfaction (currently 4); this approach is also taken by \CC{} to prevent infinite recursion in template expansion, and has proven to be both effective an not unduly restrictive of the language's expressive power.
123Cast expressions must be treated somewhat differently than functions for backwards compatibility purposes with C.
124In C, cast expressions can serve two purposes, \emph{conversion} (\eg{} !(int)3.14!), which semantically converts a value to another value in a different type with a different bit representation, or \emph{coercion} (\eg{} !void* p; (int*)p;!), which assigns a different type to the same bit value.
125C provides a set of built-in conversions and coercions, and user programmers are able to force a coercion over a conversion if desired by casting pointers.
126The overloading features in \CFA{} introduce a third cast semantics, \emph{ascription} (\eg{} !int x; double x; (int)x;!), which selects the overload which most-closely matches the cast type.
127However, since ascription does not exist in C due to the lack of overloadable identifiers, if a cast argument has an unambiguous interpretation as a conversion argument then it must be interpreted as such, even if the ascription interpretation would have a lower overall cost, as in the following example, adapted from the C standard library:
130unsigned long long x;
131(unsigned)(x >> 32);
134In C semantics, this example is unambiguously upcasting !32! to !unsigned long long!, performing the shift, then downcasting the result to !unsigned!, at total cost $(1,0,4,0,0,0)$.
135If ascription were allowed to be a first-class interpretation of a cast expression, it would be cheaper to select the !unsigned! interpretation of $?>>?$ by downcasting !x! to !unsigned! and upcasting !32! to !unsigned!, at a total cost of $(1,0,1,0,0,0)$.
136However, this break from C semantics introduces a backwards compatibility break, so to maintain C compatibility the \CFA{} resolver selects the lowest-cost interpretation of the cast argument for which a conversion or coercion to the target type exists (upcasting to !unsigned long long! in the example above, due to the lack of unsafe downcasts), only using the cost of the conversion itself as a tie-breaker.
137For example, in !int x; double x; (int)x;!, both declarations have zero-cost interpretations as !x!, but the !int x! interpretation is cheaper to cast to !int!, and is thus selected.
138Thus, in contrast to the lazy resolution of nested function-call expressions discussed above, where final interpretations for each subexpression are not chosen until the top-level expression is reached, cast expressions introduce eager resolution of their argument subexpressions, as if that argument was itself a top-level expression.
140\section{Resolution Algorithms}
142\CFA{} expression resolution is not, in general, polynomial in the size of the input expression, as shown in Section~\ref{resn-analysis-sec}.
143While this theoretical result is daunting, its implications can be mitigated in practice.
144\CFACC{} does not solve one instance of expression resolution in the course of compiling a program, but rather thousands; therefore, if the worst case of expression resolution is sufficiently rare, worst-case instances can be amortized by more-common easy instances for an acceptable overall runtime.
145Secondly, while a programmer \emph{can} deliberately generate a program designed for inefficient compilation\footnote{see for instance \cite{Haberman16}, which generates arbitrarily large \CC{} template expansions from a fixed-size source file.}, source code tends to follow common patterns.
146Programmers generally do not want to run the full compiler algorithm in their heads, and as such keep mental shortcuts in the form of language idioms.
147If the compiler can be tuned to handle idiomatic code more efficiently, then the reduction in runtime for idiomatic (but otherwise difficult) resolution instances can make a significant difference in total compiler runtime.
149\subsection{Analysis} \label{resn-analysis-sec}
151Expression resolution has a number of components which contribute to its runtime, including argument-parameter type unification, recursive traversal of the expression tree, and satisfaction of type assertions.
153If the bound type for a type variable can be looked up or mutated in constant time (as asserted in Table~\ref{env-bounds-table}), then the runtime of the unification algorithm to match an argument to a parameter is proportional to the complexity of the types being unified.
154In C, complexity of type representation is bounded by the most-complex type explicitly written in a declaration; in \CFA{}, however, polymorphism can generate more-complex types:
157        forall(otype T) pair(T) wrap(T x, T y);
159        wrap(wrap(wrap(1, 2), wrap(3, 4)), wrap(wrap(5, 6), wrap(7, 8)));
162To resolve the outermost !wrap!, the resolver must check that !pair(pair(int))! unifies with itself, but at three levels of nesting, !pair(pair(int))! is more complex than either !pair(T)! or !T!, the types in the declaration of !wrap!.
163According to this argument, then, the cost of a single argument-parameter unification is !O(d)!, where !d! is the depth of the expression tree, and the cost of argument-parameter unification for a single candidate for a given function call expression is !O(pd)!, where !p! is the number of parameters.
165% continue from here
167\subsection{Related Work}
171One improvement I have implemented to the assertion resolution scheme in \CFACC{} is to change the search for satisfying declarations from depth-first to breadth-first.
172If there are $n$ candidates to satisfy a single assertion, the candidate with the lowest conversion cost among those that have all their assertions satisfied should be chosen.
173Bilson's \CFACC{} would immediately attempt to recursively satisfy the assertions of each candidate that passed type unification; this work is wasted if that candidate is not selected to satisfy the assertion, and the wasted work may be quite substantial if the candidate function produces deeply-recursive assertions.
174I have modified \CFACC{} to first sort assertion satisfaction candidates by conversion cost, and only resolve recursive assertions until a unique minimal-cost candidate or an ambiguity is detected.
176\section{Experimental Results}
178% use Jenkins daily build logs to rebuild speedup graph with more data
180% look back at Resolution Algorithms section for threads to tie up "does the algorithm look like this?"
182\section{Conclusion \& Future Work}
184I have experimented with using expression resolution rather than type unification to choose assertion resolutions; this path should be investigated further in future work.
185This approach is more flexible than type unification, allowing for conversions to be applied to functions to satisfy assertions.
186Anecdotally, this flexibility matches user-programmer expectations better, as small type differences (\eg{} the presence or absence of a reference type, or the usual conversion from !int! to !long!) no longer break assertion satisfaction.
187Practically, the resolver prototype uses this model of assertion satisfaction, with no apparent deficit in performance; the generated expressions that are resolved to satisfy the assertions are easier than the general case because they never have nested subexpressions, which eliminates much of the theoretical differences between unification and resolution.
188The main challenge to implement this approach in \CFACC{} would be applying the implicit conversions generated by the resolution process in the code-generation for the thunk functions that \CFACC{} uses to pass type assertions with the proper signatures.
190% Discuss possibility of parallel subexpression resolution
192% Mention relevance of work to C++20 concepts
Note: See TracBrowser for help on using the repository browser.