Changeset 3deb316

Timestamp:

Jan 24, 2019, 6:17:26 PM (5 years ago)

Author:

Aaron Moss <a3moss@…>

Branches:

ADT, aaron-thesis, arm-eh, ast-experimental, cleanup-dtors, enum, forall-pointer-decay, jacob/cs343-translation, jenkins-sandbox, master, new-ast, new-ast-unique-expr, pthread-emulation, qualifiedEnum

Children:

c58bb11

Parents:

e451c0f

Message:

thesis: further description of resolution algorithm variants

Location:

doc/theses/aaron_moss_PhD/phd

Files:

• Makefile (modified) (4 diffs)
• figures/resolution-dag.eps (added)
• figures/resolution-dag.odg (added)
• resolution-heuristics.tex (modified) (8 diffs)
• thesis.tex (modified) (1 diff)

doc/theses/aaron_moss_PhD/phd/Makefile

@@ -2 +2 @@
 BIBDIR = ../../../bibliography
 EVALDIR = evaluation
+FIGDIR = figures
 TEXLIB = .:${BUILD}:${BIBDIR}:
 
@@ -8 +9 @@
 BIBTEX = BIBINPUTS=${TEXLIB} && export BIBINPUTS && bibtex
 
-VPATH = ${EVALDIR}
+VPATH = ${EVALDIR} ${FIGDIR}
 
 BASE = thesis
@@ -25 +26 @@
 resolution-heuristics \
 conclusion \
+}
+
+FIGURES = ${addsuffix .eps, \
+resolution-dag \
 }
 
@@ -47 +52 @@
         dvips ${BUILD}/$< -o ${BUILD}/$@
 
-${BASE}.dvi : Makefile ${SOURCES} ${GRAPHS} ${BIBFILE} ${BUILD}
+${BASE}.dvi : Makefile ${SOURCES} ${GRAPHS} ${FIGURES} ${BIBFILE} ${BUILD}
         ${LATEX} ${BASE}
         ${BIBTEX} ${BUILD}/${BASE}

doc/theses/aaron_moss_PhD/phd/resolution-heuristics.tex

@@ -20 +20 @@
 Ditchfield\cite{Ditchfield92} and Bilson\cite{Bilson03} describe the semantics of \CFA{} unification in more detail.
 
-\subsection{Conversion Cost}
+\subsection{Conversion Cost} \label{conv-cost-sec}
 
 C 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. 
@@ -51 +51 @@
 
 I have also incorporated an unimplemented aspect of Ditchfield's earlier cost model.
-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:
+In 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:
 
 \begin{cfa}
@@ -87 +87 @@
 In 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. 
 Similarly, an aggregate member expression !a.m! can be modelled as a unary function !m! that takes one argument of the aggregate type.
-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.
+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.
 
 Since most expressions can be treated as function calls, nested function calls are the primary component of expression resolution problem instances. 
@@ -99 +99 @@
 \begin{cfa}
 void f(int);
-double g(int); $\C{// g1}$
-int g(double); $\C{// g2}$
+double g(int); $\C[4.5in]{// g1}$
+int g(double); $\C[4.5in]{// g2}$
 
 f( g(42) );
@@ -106 +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)$. 
-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.
+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.
 Due 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.
 
@@ -125 +125 @@
 In 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. 
 C 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. 
-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. 
+The 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. 
 However, 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:
 
@@ -134 +134 @@
 
 In 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)$. 
-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)$. 
-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. 
+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)$. 
+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), using the cost of the conversion itself only as a tie-breaker. 
 For 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. 
 Thus, 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.
@@ -199 +199 @@
 % also, unification of two classes is not particularly cheap ... the bounds above may be optimistic
 
-\subsection{Related Work}
-
-\subsection{Contributions}
-
-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. 
-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. 
-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. 
-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.
+\subsection{Argument-Parameter Matching}
+
+Pruning 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. 
+One 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. 
+For 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.
+All 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}
+
+\begin{figure}[h]
+        \centering
+        \begin{subfigure}[h]{3.5in}
+        \begin{cfa}
+        int *p; $\C[1in]{// pi}$
+        char *p; $\C[1in]{// pc}$
+        
+        double *f(int*, int*); $\C[1in]{// fd}$
+        char *f(char*, int*); $\C[1in]{// fc}$
+        
+        f( f( p, p ), p );
+        \end{cfa}
+        \end{subfigure}~\begin{subfigure}[h]{2in}
+        \includegraphics{figures/resolution-dag}
+        \end{subfigure}
+        \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}
+\end{figure}
+
+Note 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.
+
+Overload 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. 
+Baker's algorithm~\cite{Baker82} takes a single pass from the leaves of the expression tree up, pre-computing argument candidates at each step. 
+For each candidate function, Baker attempts to match argument types to parameter types in sequence, failing if any parameter cannot be matched. 
+
+Bilson~\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. 
+These argument combinations are matched to the parameter types of the candidate function as a unit rather than individual arguments. 
+Bilson'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.
+
+Unlike 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. 
+As presented, this algorithm requires the parameter to have a known type, which is a poor fit for polymorphic type parameters in \CFA{}. 
+Cormack'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.
+
+Ganzinger 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. 
+Persch~\etal{}~\cite{PW:overload} developed a similar two-pass approach where the bottom-up pass is followed by the top-down pass. 
+These 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. 
+This approach of filtering out invalid types is unsuited to \CFA{} expression resolution, however, due to the presence of polymorphic functions and implicit conversions. 
+
+Baker~\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. 
+This thesis closes that gap in the literature by performing performance comparisons of both top-down and bottom-up expression resolution algorithms.
+
+\subsection{Assertion Satisfaction}
+
+The assertion satisfaction algorithm designed by Bilson~\cite{Bilson03} for the original \CFACC{} is the most-relevant prior work to this project. 
+Before 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}). 
+If this subexpression interpretation ends up not being used in the final resolution, than the (sometimes substantial) work of checking its assertions ends up wasted. 
+Bilson'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): 
+
+\begin{cfa}
+List(List(Declaration)) checkAssertions( 
+                List(Assertion) need, List(Assertion) newNeed, List(Declaration) have,
+                Environment env ) {
+        if ( is_empty(need) ) {
+                if ( is_empty( newNeed ) ) return { have };
+                return checkAssertions( newNeed, {}, have, env );
+        }
+
+        Assertion a = head(need);
+        Type adjType = substitute( a.type, env );
+        List(Declaration) candidates = decls_matching( a.name );
+        List(List(Declaration)) alternatives = {}
+        for ( Declaration c; candidates ) {
+                Environment newEnv = env;
+                if ( unify( adjType, c.type, newEnv ) ) {
+                        append( alternatives, 
+                                checkAssertions( 
+                                        tail(need), append(newNeed, c.need), append(have, c), newEnv ) );
+                }
+        }
+        return alternatives;
+}
+\end{cfa}
+
+One 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. 
+Satisfying 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. 
+Nonetheless, 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. 
+
+Another 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. 
+Monomorphic 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. 
+Thus, 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. 
+More 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. 
+As 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.
+This 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{}.
+
+The 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. 
+The 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. 
+Expressing 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. 
+On the other hand, the deeply-recursive nature of the satisfiability problem makes it difficult to adapt to optimizing solver approaches such as linear programming. 
+To 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. 
+As 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. 
+
+% discuss other related work, e.g. Rust
 
 \section{Experimental Results}

doc/theses/aaron_moss_PhD/phd/thesis.tex

@@ -28 +28 @@
 
 \usepackage{footmisc} % for double refs to the same footnote
+
+\usepackage{caption} % for subfigure
+\usepackage{subcaption}
 
 % Hyperlinks make it very easy to navigate an electronic document.