Changeset 3deb316


Ignore:
Timestamp:
Jan 24, 2019, 6:17:26 PM (3 years ago)
Author:
Aaron Moss <a3moss@…>
Branches:
aaron-thesis, arm-eh, cleanup-dtors, jacob/cs343-translation, jenkins-sandbox, master, new-ast, new-ast-unique-expr
Children:
c58bb11
Parents:
e451c0f
Message:

thesis: further description of resolution algorithm variants

Location:
doc/theses/aaron_moss_PhD/phd
Files:
2 added
3 edited

Legend:

Unmodified
Added
Removed
  • doc/theses/aaron_moss_PhD/phd/Makefile

    re451c0f r3deb316  
    22BIBDIR = ../../../bibliography
    33EVALDIR = evaluation
     4FIGDIR = figures
    45TEXLIB = .:${BUILD}:${BIBDIR}:
    56
     
    89BIBTEX = BIBINPUTS=${TEXLIB} && export BIBINPUTS && bibtex
    910
    10 VPATH = ${EVALDIR}
     11VPATH = ${EVALDIR} ${FIGDIR}
    1112
    1213BASE = thesis
     
    2526resolution-heuristics \
    2627conclusion \
     28}
     29
     30FIGURES = ${addsuffix .eps, \
     31resolution-dag \
    2732}
    2833
     
    4752        dvips ${BUILD}/$< -o ${BUILD}/$@
    4853
    49 ${BASE}.dvi : Makefile ${SOURCES} ${GRAPHS} ${BIBFILE} ${BUILD}
     54${BASE}.dvi : Makefile ${SOURCES} ${GRAPHS} ${FIGURES} ${BIBFILE} ${BUILD}
    5055        ${LATEX} ${BASE}
    5156        ${BIBTEX} ${BUILD}/${BASE}
  • doc/theses/aaron_moss_PhD/phd/resolution-heuristics.tex

    re451c0f r3deb316  
    2020Ditchfield\cite{Ditchfield92} and Bilson\cite{Bilson03} describe the semantics of \CFA{} unification in more detail.
    2121
    22 \subsection{Conversion Cost}
     22\subsection{Conversion Cost} \label{conv-cost-sec}
    2323
    2424C 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.
     
    5151
    5252I have also incorporated an unimplemented aspect of Ditchfield's earlier cost model.
    53 In 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:
     53In the example below, adapted from \cite[p.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:
    5454
    5555\begin{cfa}
     
    8787In 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.
    8888Similarly, an aggregate member expression !a.m! can be modelled as a unary function !m! that takes one argument of the aggregate type.
    89 Literals 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.
     89Literals 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.
    9090
    9191Since most expressions can be treated as function calls, nested function calls are the primary component of expression resolution problem instances.
     
    9999\begin{cfa}
    100100void f(int);
    101 double g(int); $\C{// g1}$
    102 int g(double); $\C{// g2}$
     101double g(int); $\C[4.5in]{// g1}$
     102int g(double); $\C[4.5in]{// g2}$
    103103
    104104f( g(42) );
     
    106106
    107107!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)$.
    108 If !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.
     108If !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.
    109109Due 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.
    110110
     
    125125In 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.
    126126C 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.
    127 The 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.
     127The overloading features in \CFA{} introduce a third cast semantic, \emph{ascription} (\eg{} !int x; double x; (int)x;!), which selects the overload which most-closely matches the cast type.
    128128However, 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:
    129129
     
    134134
    135135In 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)$.
    136 If 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)$.
    137 However, 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.
     136If 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)$.
     137However, 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), using the cost of the conversion itself only as a tie-breaker.
    138138For 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.
    139139Thus, 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.
     
    199199% also, unification of two classes is not particularly cheap ... the bounds above may be optimistic
    200200
    201 \subsection{Related Work}
    202 
    203 \subsection{Contributions}
    204 
    205 One 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.
    206 If 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.
    207 Bilson'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.
    208 I 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.
     201\subsection{Argument-Parameter Matching}
     202
     203Pruning possible interpretations as early as possible is one way to reduce the real-world cost of expression resolution, provided that a sufficient proportion of interpretations are pruned to pay for the cost of the pruning algorithm.
     204One opportunity for interpretation pruning is by the argument-parameter type matching, but the literature provides no clear answers on whether candidate functions should be chosen according to their available arguments, or whether argument resolution should be driven by the available function candidates.
     205For programming languages without implicit conversions, argument-parameter matching is essentially the entirety of the expression resolution problem, and is generally referred to as ``overload resolution'' in the literature.
     206All expression-resolution algorithms form a DAG of interpretations, some explicitly, sone implicitly; in this DAG, arcs point from function-call interpretations to argument interpretations, as in Figure~\ref{res-dag-fig}
     207
     208\begin{figure}[h]
     209        \centering
     210        \begin{subfigure}[h]{3.5in}
     211        \begin{cfa}
     212        int *p; $\C[1in]{// pi}$
     213        char *p; $\C[1in]{// pc}$
     214       
     215        double *f(int*, int*); $\C[1in]{// fd}$
     216        char *f(char*, int*); $\C[1in]{// fc}$
     217       
     218        f( f( p, p ), p );
     219        \end{cfa}
     220        \end{subfigure}~\begin{subfigure}[h]{2in}
     221        \includegraphics{figures/resolution-dag}
     222        \end{subfigure}
     223        \caption[Resolution DAG for a simple expression.]{Resolution DAG for a simple expression. Functions that do not have a valid argument matching are covered with an \textsf{X}.} \label{res-dag-fig}
     224\end{figure}
     225
     226Note that some interpretations may be part of more than one super-interpretation, as with the second $pi$ in the bottom row, while some valid subexpression interpretations, like $fd$ in the middle row, are not used in any interpretation of their superexpression.
     227
     228Overload resolution was first seriously considered in the development of compilers for the Ada programming language, with different algorithms making various numbers of passes over the expression DAG, these passes being either top-down or bottom-up.
     229Baker's algorithm~\cite{Baker82} takes a single pass from the leaves of the expression tree up, pre-computing argument candidates at each step.
     230For each candidate function, Baker attempts to match argument types to parameter types in sequence, failing if any parameter cannot be matched.
     231
     232Bilson~\cite{Bilson03} similarly pre-computes argument-candidates in a single bottom-up pass in the original \CFACC{}, but then explicitly enumerates all possible argument combinations for a multi-parameter function.
     233These argument combinations are matched to the parameter types of the candidate function as a unit rather than individual arguments.
     234Bilson's approach is less efficient than Baker's, as the same argument may be compared to the same parameter many times, but does allow a more straightforward handling of polymorphic type-binding and tuple-typed expressions.
     235
     236Unlike Baker and Bilson, Cormack's algorithm~\cite{Cormack81} requests argument candidates that match the type of each parameter of each candidate function, in a single pass from the top-level expression down; memoization of these requests is presented as an optimization.
     237As presented, this algorithm requires the parameter to have a known type, which is a poor fit for polymorphic type parameters in \CFA{}.
     238Cormack's algorithm can be modified to request argument interpretations of \emph{any} type when provided an unbound parameter type, but this eliminates any pruning gains that could be provided by the algorithm.
     239
     240Ganzinger and Ripken~\cite{Ganzinger80} propose an approach (later refined by Pennello~\etal{}~\cite{Pennello80}) that uses a top-down filtering pass followed by a bottom-up filtering pass to reduce the number of candidate interpretations; they prove that for the Ada programming language a small number of such iterations is sufficient to converge to a solution for the overload resolution problem.
     241Persch~\etal{}~\cite{PW:overload} developed a similar two-pass approach where the bottom-up pass is followed by the top-down pass.
     242These approaches differ from Baker, Bilson, or Cormack in that they take multiple passes over the expression tree to yield a solution by applying filtering heuristics to all expression nodes.
     243This approach of filtering out invalid types is unsuited to \CFA{} expression resolution, however, due to the presence of polymorphic functions and implicit conversions.
     244
     245Baker~\cite{Baker82} left empirical comparison of different overload resolution algorithms to future work; Bilson~\cite{Bilson03} described an extension of Baker's algorithm to handle implicit conversions and polymorphism, but did not further explore the space of algorithmic approaches to handle both overloaded names and implicit conversions.
     246This thesis closes that gap in the literature by performing performance comparisons of both top-down and bottom-up expression resolution algorithms.
     247
     248\subsection{Assertion Satisfaction}
     249
     250The assertion satisfaction algorithm designed by Bilson~\cite{Bilson03} for the original \CFACC{} is the most-relevant prior work to this project.
     251Before accepting any subexpression candidate, Bilson first checks that that candidate's assertions can all be resolved; this is necessary due to Bilson's addition of assertion satisfaction costs to candidate costs (discussed in Section~\ref{conv-cost-sec}).
     252If this subexpression interpretation ends up not being used in the final resolution, than the (sometimes substantial) work of checking its assertions ends up wasted.
     253Bilson's assertion checking function recurses on two lists, !need! and !newNeed!, the current declaration's assertion set and those implied by the assertion-satisfying declarations, respectively, as detailed in the pseudocode below (ancillary aspects of the algorithm are omitted for clarity):
     254
     255\begin{cfa}
     256List(List(Declaration)) checkAssertions(
     257                List(Assertion) need, List(Assertion) newNeed, List(Declaration) have,
     258                Environment env ) {
     259        if ( is_empty(need) ) {
     260                if ( is_empty( newNeed ) ) return { have };
     261                return checkAssertions( newNeed, {}, have, env );
     262        }
     263
     264        Assertion a = head(need);
     265        Type adjType = substitute( a.type, env );
     266        List(Declaration) candidates = decls_matching( a.name );
     267        List(List(Declaration)) alternatives = {}
     268        for ( Declaration c; candidates ) {
     269                Environment newEnv = env;
     270                if ( unify( adjType, c.type, newEnv ) ) {
     271                        append( alternatives,
     272                                checkAssertions(
     273                                        tail(need), append(newNeed, c.need), append(have, c), newEnv ) );
     274                }
     275        }
     276        return alternatives;
     277}
     278\end{cfa}
     279
     280One shortcoming of this approach is that if an earlier assertion has multiple valid candidates, later assertions may be checked many times due to the structure of the recursion.
     281Satisfying declarations for assertions are not completely independent of each other, since the unification process may produce new type bindings in the environment, and these bindings may not be compatible between independently-checked assertions.
     282Nonetheless, with the environment data structures discussed in Chapter~\ref{env-chapter}, I have found it more efficient to produce a list of possibly-satisfying declarations for each assertion once, then check their respective environments for mutual compatibility when combining lists of assertions together.
     283
     284Another improvement I have made to the assertion resolution scheme in \CFACC{} is to consider all assertion-satisfying combinations at one level of recursion before attempting to recursively satisfy any !newNeed! assertions.
     285Monomorphic functions are cheaper than polymorphic functions for assertion satisfaction because they are an exact match for the environment-adjusted assertion type, whereas polymorphic functions require an extra type binding.
     286Thus, if there is any mutually-compatible set of assertion-satisfying declarations which does not include any polymorphic functions (and associated recursive assertions), then the optimal set of assertions will not require any recursive !newNeed! satisfaction.
     287More generally, due to the \CFA{} cost model changes I introduced in Section~\ref{conv-cost-sec}, the conversion cost of an assertion-satisfying declaration is no longer dependent on the conversion cost of its own assertions.
     288As such, all sets of mutually-compatible assertion-satisfying declarations can be sorted by their summed conversion costs, and the recursive !newNeed! satisfaction pass can be limited to only check the feasibility of the minimal-cost sets.
     289This significantly reduces wasted work relative to Bilson's approach, as well as avoiding generation of deeply-recursive assertion sets for a significant performance improvement relative to Bilson's \CFACC{}.
     290
     291The assertion satisfaction aspect of \CFA{} expression resolution bears some similarity to satisfiability problems from logic, and as such other languages with similar trait and assertion mechanisms make use of logic-program solvers in their compilers.
     292The combination of the assertion satisfaction elements of the problem with the conversion cost model of \CFA{} makes this logic-solver approach difficult to apply in \CFACC{}, however.
     293Expressing assertion resolution as a satisfiability problem ignores the cost optimization aspect, which is necessary to decide between what are often many possible satisfying assignments of declarations to assertions.
     294On the other hand, the deeply-recursive nature of the satisfiability problem makes it difficult to adapt to optimizing solver approaches such as linear programming.
     295To maintain a well-defined programming language, any optimization algorithm used must provide an exact (rather than approximate) solution; this constraint also rules out a whole class of approximately-optimal generalized solvers.
     296As such, I opted to continue Bilson's approach of designing a bespoke solver for \CFA{} assertion satisfaction, rather than attempting to re-express the problem in some more general formalism.
     297
     298% discuss other related work, e.g. Rust
    209299
    210300\section{Experimental Results}
  • doc/theses/aaron_moss_PhD/phd/thesis.tex

    re451c0f r3deb316  
    2828
    2929\usepackage{footmisc} % for double refs to the same footnote
     30
     31\usepackage{caption} % for subfigure
     32\usepackage{subcaption}
    3033
    3134% Hyperlinks make it very easy to navigate an electronic document.
Note: See TracChangeset for help on using the changeset viewer.