Changeset f2c5726 for doc/theses/aaron_moss_PhD

Timestamp:

Jan 22, 2019, 4:49:23 PM (6 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:

104a13e

Parents:

9a38436c

Message:

thesis: start asymptotic analysis of resolution problem

File:

• doc/theses/aaron_moss_PhD/phd/resolution-heuristics.tex (modified) (4 diffs)

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

@@ -1 +1 @@
 \chapter{Resolution Heuristics}
 \label{resolution-chap}
+
+% consider using "satisfaction" throughout when talking about assertions
 
 The main task of the \CFACC{} type-checker is \emph{expression resolution}, determining which declarations the identifiers in each expression correspond to. 
@@ -138 +140 @@
 \section{Resolution Algorithms}
 
+\CFA{} expression resolution is not, in general, polynomial in the size of the input expression, as shown in Section~\ref{resn-analysis-sec}. 
+While this theoretical result is daunting, its implications can be mitigated in practice.
+\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. 
+Secondly, 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. 
+Programmers 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. 
+If 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. 
+
+\subsection{Analysis} \label{resn-analysis-sec}
+
+Expression 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. 
+
+If 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. 
+In 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: 
+
+\begin{cfa}
+        forall(otype T) pair(T) wrap(T x, T y);
+
+        wrap(wrap(wrap(1, 2), wrap(3, 4)), wrap(wrap(5, 6), wrap(7, 8)));
+\end{cfa}
+
+To 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!. 
+According 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. 
+
+% continue from here
+
 \subsection{Related Work}
 
@@ -147 +174 @@
 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.
 
+\section{Experimental Results}
+
+% use Jenkins daily build logs to rebuild speedup graph with more data
+
+% look back at Resolution Algorithms section for threads to tie up "does the algorithm look like this?"
+
+\section{Conclusion \& Future Work}
+
 I have experimented with using expression resolution rather than type unification to choose assertion resolutions; this path should be investigated further in future work. 
 This approach is more flexible than type unification, allowing for conversions to be applied to functions to satisfy assertions. 
@@ -153 +188 @@
 The 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.
 
+% Discuss possibility of parallel subexpression resolution
+
 % Mention relevance of work to C++20 concepts