Ignore:
Timestamp:
Jan 22, 2019, 11:23:43 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:
e451c0f
Parents:
f2c5726
Message:

thesis: continue asymptotic analysis of resolution

File:
1 edited

Legend:

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

    rf2c5726 r104a13e  
    33
    44% consider using "satisfaction" throughout when talking about assertions
     5% "valid" instead of "feasible" interpretations
    56
    67The main task of the \CFACC{} type-checker is \emph{expression resolution}, determining which declarations the identifiers in each expression correspond to.
     
    147148If 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.
    148149
    149 \subsection{Analysis} \label{resn-analysis-sec}
     150\subsection{Worst-case Analysis} \label{resn-analysis-sec}
    150151
    151152Expression 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.
    152153
    153154If 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.
    154 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:
     155In C, complexity of type representation is bounded by the most-complex type explicitly written in a declaration, effectively a small constant; in \CFA{}, however, polymorphism can generate more-complex types:
    155156
    156157\begin{cfa}
     
    161162
    162163To 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!.
    163 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.
    164 
     164Accordingly, 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
     166Considering the recursive traversal of the expression tree, polymorphism again greatly expands the worst-case runtime.
     167Letting $i$ be the number of candidate declarations for each function call, if all of these candidates are monomorphic then there are no more than $i$ unambiguous interpretations of the subexpression rooted at that function call.
     168Ambiguous minimal-cost subexpression interpretations may also be collapsed into a single \emph{ambiguous interpretation}, as the presence of such a subexpression interpretation in the final solution is an error condition.
     169One safe pruning operation during expression resolution is to discard all subexpression interpretations with greater-than-minimal cost for their return type, as such interpretations will never beat the minimal-cost interpretation with their return type for the overall optimal solution.
     170As such, with no polymorphism each declaration will generate no more than one minimal-cost interpretation with its return type, so the number of possible subexpression interpretations is $O(i)$ (note that in C, which lacks overloading, $i \leq 1$).
     171With polymorphism, however, a single declaration (like !wrap! above) can have many concrete return types after type variable substitution, and could in principle have a different concrete return type for each combination of argument interpretations.
     172Calculated recursively, the bound on the total number of candidate interpretations is $O(i^{p^d})$, each with a distinct type.
     173
     174Given these calculations of number of subexpression interpretations and matching costs, the upper bound on runtime for generating candidates for a single subexpression $d$ levels up from the leaves is $O( i^{p^d} \cdot pd )$.
     175Since there are $O(p^d)$ subexpressions in a single top-level expression, the total worst-case cost of argument-parameter matching with the overloading and polymorphism features of \CFA{} is $O( i^{p^d} \cdot pd \cdot p^d )$.
     176
     177This already high bound does not yet account for the cost of assertion resolution, though.
    165178% continue from here
     179
     180% need to discuss that n == p^d, that that i^p^d bound is **super** rare, and will usually be closer to $i$
     181
     182% missing a +1 somewhere in these bounds; also, pd is O(n) ()
    166183
    167184\subsection{Related Work}
Note: See TracChangeset for help on using the changeset viewer.