Changeset c58bb11

Timestamp:

Jan 25, 2019, 3:37:07 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:

b4fd981

Parents:

3deb316

Message:

Complete background work on resolution algorithms

Location:

doc

Files:

• bibliography/pl.bib (modified) (1 diff)
• theses/aaron_moss_PhD/phd/resolution-heuristics.tex (modified) (3 diffs)

doc/bibliography/pl.bib

@@ -4150 +4150 @@
 }
 
+@misc{Matsakis17,
+    keywords    = {Rust, Chalk, PROLOG},
+    contributer = {a3moss@uwaterloo.ca},
+    author      = {Nicholas Matsakis},
+    title       = {Lowering {Rust} traits to logic},
+    month       = jan,
+    year        = 2017,
+    howpublished= {\href{http://smallcultfollowing.com/babysteps/blog/2017/01/26/lowering-rust-traits-to-logic/}
+                  {http://smallcultfollowing.com/\-babysteps/\-blog/\-2017/\-01/\-26/\-lowering-rust-traits-to-logic/}},
+    optnote     = {Accessed: 2019-01},
+}
+
 @article{Cormack89,
     keywords    = {parsing, LR, error recovery},

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

@@ -280 +280 @@
 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. 
+Nonetheless, 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. 
 
 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. 
@@ -289 +289 @@
 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{}.
 
+Making the conversion cost of an interpretation independent of the cost of satisfying its assertions has further benefits. 
+Bilson'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. 
+If 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. 
+In 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. 
+The experimental results in Section~\ref{resn-expr-sec} indicate that this is a worthwhile trade-off. 
+
+Optimizing 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:
+
+\begin{cfa}
+sout | "one" | 1 | "two" | 2 | "three" | 3 | "four" | 4 | "five" | 5 | "six" | 6
+        | "seven" | 7 | "eight" | 8 | "nine" | 9 | "ten" | 10 | "end" | nl | nl;
+\end{cfa}
+
+The 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. 
+Secondly, 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:
+
+\begin{cfa}
+forall( dtype ostype | ostream( ostype ) )
+ostype& ?|? ( ostype&, int );
+\end{cfa}
+
+Note 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. 
+On 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!.
+
+To solve this problem, I have developed a \emph{cached} variant of assertion checking. 
+During the course of checking the assertions of a single top-level expression, I cache the results of each assertion checked. 
+The 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. 
+This adjusted assertion declaration is then run through the \CFA{} name mangling algorithm to produce a comparable string-type key. 
+
 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. 
+For instance, Matsakis~\cite{Matsakis17} and the Rust team have been working on checking satisfaction of Rust traits with a PROLOG-based engine.
 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. 
@@ -296 +326 @@
 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}
+\section{Experimental Results} \label{resn-expr-sec}
 
 % use Jenkins daily build logs to rebuild speedup graph with more data