Jan 25, 2019, 3:37:07 PM (5 years ago)
Aaron Moss <a3moss@…>
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

Complete background work on resolution algorithms

1 edited


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

    r3deb316 rc58bb11  
    280280One 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.
    281281Satisfying 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.
    282 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.
     282Nonetheless, with the environment data structures discussed in Chapter~\ref{env-chap}, 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.
    284284Another 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.
    289289This 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{}.
     291Making the conversion cost of an interpretation independent of the cost of satisfying its assertions has further benefits.
     292Bilson's algorithm checks assertions for all subexpression interpretations immediately, including those which are not ultimately used; I have developed a \emph{deferred} variant of assertion checking which waits until a top-level interpretation has been generated to check any assertions.
     293If the assertions of the minimal-cost top-level interpretation cannot be satisfied then the next-most-minimal-cost interpretation's assertions are checked, and so forth until a minimal-cost satisfiable interpretation (or ambiguous set thereof) is found, or no top-level interpretations are found to have satisfiable assertions.
     294In the common case where the code actually does compile this saves the work of checking assertions for ultimately-rejected interpretations, though it does rule out some pruning opportunities for subinterpretations with unsatisfiable assertions or which are more expensive than a minimal-cost polymorphic function with the same return type.
     295The experimental results in Section~\ref{resn-expr-sec} indicate that this is a worthwhile trade-off.
     297Optimizing assertion satisfaction for common idioms has also proved effective in \CFA{}; the code below is an unexceptional print statement derived from the \CFA{} test suite that nonetheless is a very difficult instance of expression resolution:
     300sout | "one" | 1 | "two" | 2 | "three" | 3 | "four" | 4 | "five" | 5 | "six" | 6
     301        | "seven" | 7 | "eight" | 8 | "nine" | 9 | "ten" | 10 | "end" | nl | nl;
     304The first thing that makes this expression so difficult is that it is 23 levels deep; Section~\ref{resn-analysis-sec} indicates that the worst-case bounds on expression resolution are exponential in expression depth.
     305Secondly, the !?|?! operator is significantly overloaded in \CFA{} --- there are 74 such operators in the \CFA{} standard library, and while 9 are arithmetic operators inherited from C, the rest are polymorphic I/O operators that look something like this:
     308forall( dtype ostype | ostream( ostype ) )
     309ostype& ?|? ( ostype&, int );
     312Note that !ostream! is a trait with 25 type assertions, and that the output operators for the other arithmetic types are also feasible for the !int!-type parameters due to implicit conversions.
     313On this instance, deferred assertion satisfaction saves wasted work checking assertions on the wrong output operators, but does nothing about the 23 repeated checks of the 25 assertions to determine that !ofstream! (the type of !sout!) satisfies !ostream!.
     315To solve this problem, I have developed a \emph{cached} variant of assertion checking.
     316During the course of checking the assertions of a single top-level expression, I cache the results of each assertion checked.
     317The search key for this cache is the assertion declaration with its type variables substituted according to the type environment to distinguish satisfaction of the same assertion for different types.
     318This adjusted assertion declaration is then run through the \CFA{} name mangling algorithm to produce a comparable string-type key.
    291320The 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.
     321For instance, Matsakis~\cite{Matsakis17} and the Rust team have been working on checking satisfaction of Rust traits with a PROLOG-based engine.
    292322The 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.
    293323Expressing 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.
    296326As 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.
    298 % discuss other related work, e.g. Rust
    300 \section{Experimental Results}
     328\section{Experimental Results} \label{resn-expr-sec}
    302330% use Jenkins daily build logs to rebuild speedup graph with more data
Note: See TracChangeset for help on using the changeset viewer.