Ignore:
Timestamp:
Jan 22, 2019, 4:49:23 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:
104a13e
Parents:
9a38436
Message:

thesis: start asymptotic analysis of resolution problem

File:
1 edited

Legend:

Unmodified
Added
Removed
  • doc/theses/aaron_moss_PhD/phd/resolution-heuristics.tex

    r9a38436 rf2c5726  
    11\chapter{Resolution Heuristics}
    22\label{resolution-chap}
     3
     4% consider using "satisfaction" throughout when talking about assertions
    35
    46The main task of the \CFACC{} type-checker is \emph{expression resolution}, determining which declarations the identifiers in each expression correspond to.
     
    138140\section{Resolution Algorithms}
    139141
     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.
     148
     149\subsection{Analysis} \label{resn-analysis-sec}
     150
     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.
     152
     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:
     155
     156\begin{cfa}
     157        forall(otype T) pair(T) wrap(T x, T y);
     158
     159        wrap(wrap(wrap(1, 2), wrap(3, 4)), wrap(wrap(5, 6), wrap(7, 8)));
     160\end{cfa}
     161
     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.
     164
     165% continue from here
     166
    140167\subsection{Related Work}
    141168
     
    147174I 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.
    148175
     176\section{Experimental Results}
     177
     178% use Jenkins daily build logs to rebuild speedup graph with more data
     179
     180% look back at Resolution Algorithms section for threads to tie up "does the algorithm look like this?"
     181
     182\section{Conclusion \& Future Work}
     183
    149184I have experimented with using expression resolution rather than type unification to choose assertion resolutions; this path should be investigated further in future work.
    150185This approach is more flexible than type unification, allowing for conversions to be applied to functions to satisfy assertions.
     
    153188The 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.
    154189
     190% Discuss possibility of parallel subexpression resolution
     191
    155192% Mention relevance of work to C++20 concepts
Note: See TracChangeset for help on using the changeset viewer.