Changeset f316c68


Ignore:
Timestamp:
Feb 21, 2019, 4:29:44 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:
b3edf7f5
Parents:
a2971cc
Message:

thesis: polish first draft of Ch.4

Location:
doc/theses/aaron_moss_PhD/phd
Files:
2 edited

Legend:

Unmodified
Added
Removed
  • doc/theses/aaron_moss_PhD/phd/experiments.tex

    ra2971cc rf316c68  
    155155Aside from that, the persistent union-find (\textsc{per}) type environment generally performs better than the basic (\textsc{bas}) environment, with similar peak memory usage and an average speedup factor of nearly 2, though the requirements of the \textsc{per} environment for automatic garbage collection and a shared history for combination make retrofitting it into older code difficult.
    156156
    157 \section{Instance Difficulty}
     157\section{Instance Difficulty} \label{instance-expr-sec}
    158158
    159159To characterize the difficulty of expression resolution problem instances, the test suites must be explored at a finer granuarity.
  • doc/theses/aaron_moss_PhD/phd/resolution-heuristics.tex

    ra2971cc rf316c68  
    4949\end{cfa}
    5050
    51 Note that safe and unsafe conversions are handled differently; \CFA{} counts distance of safe conversions (\eg{} !int! to !long! is cheaper than !int! to !unsigned long!), while only counting the number of unsafe conversions (\eg{} !int! to !char! and !int! to !short! both have unsafe cost 1, as in the first fwo declarations above).
    52 These costs are summed over the paramters in a call; in the example above, the cost of the two !int! to !long! conversions for the fourth declaration sum equal to the one !int! to !unsigned long! conversion in the fifth.
     51Note that safe and unsafe conversions are handled differently; \CFA{} counts distance of safe conversions (\eg{} !int! to !long! is cheaper than !int! to !unsigned long!), while only counting the number of unsafe conversions (\eg{} !int! to !char! and !int! to !short! both have unsafe cost 1, as in the first two declarations above).
     52These costs are summed over the parameters in a call; in the example above, the cost of the two !int! to !long! conversions for the fourth declaration sum equal to the one !int! to !unsigned long! conversion in the fifth.
    5353
    5454As part of adding reference types to \CFA{} (see Section~\ref{type-features-sec}), Schluntz added a new $reference$ element to the cost tuple, which counts the number of implicit reference-to-rvalue conversions performed so that candidate interpretations can be distinguished by how closely they match the nesting of reference types; since references are meant to act almost indistinguishably from lvalues, this $reference$ element is the least significant in the lexicographic comparison of cost tuples.
     
    8787Thus, all else equal, if both a binding to !T! and a binding to !T*! are available, the model chooses the more specific !T*! binding with $specialization = -1$.
    8888This process is recursive, such that !T**! has $specialization = -2$.
    89 This calculation works similarly for generic types, \eg{} !box(T)! also has specialization cost -1.
    90 For multi-argument generic types, the least-specialized polymorphic parameter sets the specialization cost, \eg{} the specialization cost of !pair(T, S*)! is -1 (from !T!) rather than -2 (from !S!).
     89This calculation works similarly for generic types, \eg{} !box(T)! also has specialization cost $-1$.
     90For multi-argument generic types, the least-specialized polymorphic parameter sets the specialization cost, \eg{} the specialization cost of !pair(T, S*)! is $-1$ (from !T!) rather than $-2$ (from !S!).
    9191Specialization cost is not counted on the return type list; since $specialization$ is a property of the function declaration, a lower specialization cost prioritizes one declaration over another.
    9292User programmers can choose between functions with varying parameter lists by adjusting the arguments, but the same is not true of varying return types, so the return types are omitted from the $specialization$ element.
     
    9797Bilson's \CFACC{} uses conversion costs based off the left graph in Figure~\ref{safe-conv-graph-fig}.
    9898However, Bilson's design results in inconsistent and somewhat surprising costs, with conversion to the next-larger same-sign type generally (but not always) double the cost of conversion to the !unsigned! type of the same size.
    99 In the redesign, for consistency with the approach of the usual arithmetic conversions, which select a common type primarily based on size, but secondarily on sign, arcs in the new graph are annotated with whether they represent a sign change, and such sign changes are summed in a new $sign$ cost element that lexicographically succeeds than $safe$.
     99In the redesign, for consistency with the approach of the usual arithmetic conversions, which select a common type primarily based on size, but secondarily on sign, arcs in the new graph are annotated with whether they represent a sign change, and such sign changes are summed in a new $sign$ cost element that lexicographically succeeds $safe$.
    100100This means that sign conversions are approximately the same cost as widening conversions, but slightly more expensive (as opposed to less expensive in Bilson's graph).
    101101
     
    122122In terms of the core argument-parameter matching algorithm, the overloaded variables of \CFA{} are not handled differently from zero-argument function calls, aside from a different pool of candidate declarations and setup for different code generation.
    123123Similarly, an aggregate member expression !a.m! can be modelled as a unary function !m! that takes one argument of the aggregate type.
    124 Literals do not require sophisticated resolution, as the syntactic form of each implies their result types (\eg{} !42! is !int!, !"hello"! is !char*!, \etc{}), though struct literals require resolution of the implied constructor call.
     124Literals do not require sophisticated resolution, as the syntactic form of each implies their result types (!42! is !int!, !"hello"! is !char*!, \etc{}), though struct literals require resolution of the implied constructor call.
    125125
    126126Since most expressions can be treated as function calls, nested function calls are the primary component of expression resolution problem instances.
    127127Each function call has an \emph{identifier} which must match the name of the corresponding declaration, and a possibly-empty list of \emph{arguments}.
    128128These arguments may be function call expressions themselves, producing a tree of function-call expressions to resolve, where the leaf expressions are generally nullary functions, variable expressions, or literals.
    129 A single instance of expression resolution consists of matching declarations to all the identifiers in the expression tree of a top-level expression, along with inserting any conversions and assertions necessary for that matching.
     129A single instance of expression resolution consists of matching declarations to all the identifiers in the expression tree of a top-level expression, along with inserting any conversions and satisfying all assertions necessary for that matching.
    130130The cost of a function-call expression is the sum of the conversion costs of each argument type to the corresponding parameter and the total cost of each subexpression, recursively calculated.
    131131\CFA{} expression resolution must produce either the unique lowest-cost interpretation of the top-level expression, or an appropriate error message if none such exists.
    132 The cost model of \CFA{} precludes a simple bottom-up resolution pass, as constraints and costs introduced by calls higher in the expression tree can change the interpretation of those lower in the tree, as in the following example:
     132The cost model of \CFA{} precludes a greedy bottom-up resolution pass, as constraints and costs introduced by calls higher in the expression tree can change the interpretation of those lower in the tree, as in the following example:
    133133
    134134\begin{cfa}
     
    142142!g1! is the cheapest interpretation of !g(42)!, with cost $(0,0,0,0,0,0)$ since the argument type is an exact match, but to downcast the return type of !g1! to an !int! suitable for !f! requires an unsafe conversion for a total cost of $(1,0,0,0,0,0)$.
    143143If !g2! is chosen, on the other hand, there is a safe upcast from the !int! type of !42! to !double!, but no cast on the return of !g!, for a total cost of $(0,0,1,0,0,0)$; as this is cheaper, !g2! is chosen.
    144 Due to this design, in general all feasible interpretations of subexpressions must be propagated to the top of the expression tree before any can be eliminated, a lazy form of expression resolution, as opposed to the eager expression resolution allowed by C, where each expression can be resolved given only the resolution of its immediate subexpressions.
     144Due to this design, all feasible interpretations of subexpressions must in general be propagated to the top of the expression tree before any can be eliminated, a lazy form of expression resolution, as opposed to the eager expression resolution allowed by C, where each expression can be resolved given only the resolution of its immediate subexpressions.
    145145
    146146If there are no feasible interpretations of the top-level expression, expression resolution fails and must produce an appropriate error message.
     
    148148If there are multiple feasible interpretations of a top-level expression, ties are broken based on the conversion cost, calculated as above.
    149149If there are multiple minimal-cost feasible interpretations of a top-level expression, that expression is said to be \emph{ambiguous}, and an error must be produced.
    150 Multiple minimal-cost interpretations of a subexpression do not necessarily imply an ambiguous top-level expression, however, as the subexpression interpretations may be disambiguated based on their return type or by selecting a more-expensive interpretation of that subexpression to reduce the overall expression cost, as above.
    151 
    152 The \CFA{} resolver uses type assertions to filter out otherwise-feasible subexpression interpretations.
     150Multiple minimal-cost interpretations of a subexpression do not necessarily imply an ambiguous top-level expression, however, as the subexpression interpretations may be disambiguated based on their return type or by selecting a more-expensive interpretation of that subexpression to reduce the overall expression cost, as in the example above.
     151
     152The \CFA{} resolver uses type assertions to filter out otherwise-valid subexpression interpretations.
    153153An interpretation can only be selected if all the type assertions in the !forall! clause on the corresponding declaration can be satisfied with a unique minimal-cost set of satisfying declarations.
    154154Type assertion satisfaction is tested by performing type unification on the type of the assertion and the type of the declaration satisfying the assertion.
    155155That is, a declaration which satisfies a type assertion must have the same name and type as the assertion after applying the substitutions in the type environment.
    156156Assertion-satisfying declarations may be polymorphic functions with assertions of their own that must be satisfied recursively.
    157 This recursive assertion satisfaction has the potential to introduce infinite loops into the type resolution algorithm, a situation which \CFACC{} avoids by imposing a hard limit on the depth of recursive assertion satisfaction (currently 4); this approach is also taken by \CC{} to prevent infinite recursion in template expansion, and has proven to be both effective an not unduly restrictive of the language's expressive power.
     157This recursive assertion satisfaction has the potential to introduce infinite loops into the type resolution algorithm, a situation which \CFACC{} avoids by imposing a hard limit on the depth of recursive assertion satisfaction (currently 4); this approach is also taken by \CC{} to prevent infinite recursion in template expansion, and has proven to be effective and not unduly restrictive of the expressive power of \CFA{}.
    158158
    159159Cast expressions must be treated somewhat differently than functions for backwards compatibility purposes with C.
     
    161161C provides a set of built-in conversions and coercions, and user programmers are able to force a coercion over a conversion if desired by casting pointers.
    162162The overloading features in \CFA{} introduce a third cast semantic, \emph{ascription} (\eg{} !int x; double x; (int)x;!), which selects the overload which most-closely matches the cast type.
    163 However, since ascription does not exist in C due to the lack of overloadable identifiers, if a cast argument has an unambiguous interpretation as a conversion argument then it must be interpreted as such, even if the ascription interpretation would have a lower overall cost, as in the following example, adapted from the C standard library:
     163However, since ascription does not exist in C due to the lack of overloadable identifiers, if a cast argument has an unambiguous interpretation as a conversion argument then it must be interpreted as such, even if the ascription interpretation would have a lower overall cost.
     164This is demonstrated in the following example, adapted from the C standard library:
    164165
    165166\begin{cfa}
     
    168169\end{cfa}
    169170
    170 In C semantics, this example is unambiguously upcasting !32! to !unsigned long long!, performing the shift, then downcasting the result to !unsigned!, at total cost $(1,0,4,0,0,0)$.
    171 If ascription were allowed to be a first-class interpretation of a cast expression, it would be cheaper to select the !unsigned! interpretation of !?>>?! by downcasting !x! to !unsigned! and upcasting !32! to !unsigned!, at a total cost of $(1,0,1,0,0,0)$.
     171In C semantics, this example is unambiguously upcasting !32! to !unsigned long long!, performing the shift, then downcasting the result to !unsigned!, at total cost $(1,0,3,1,0,0,0)$.
     172If ascription were allowed to be a first-class interpretation of a cast expression, it would be cheaper to select the !unsigned! interpretation of !?>>?! by downcasting !x! to !unsigned! and upcasting !32! to !unsigned!, at a total cost of $(1,0,1,1,0,0,0)$.
    172173However, this break from C semantics introduces a backwards compatibility break, so to maintain C compatibility the \CFA{} resolver selects the lowest-cost interpretation of the cast argument for which a conversion or coercion to the target type exists (upcasting to !unsigned long long! in the example above, due to the lack of unsafe downcasts), using the cost of the conversion itself only as a tie-breaker.
    173174For example, in !int x; double x; (int)x;!, both declarations have zero-cost interpretations as !x!, but the !int x! interpretation is cheaper to cast to !int!, and is thus selected.
     
    178179\CFA{} expression resolution is not, in general, polynomial in the size of the input expression, as shown in Section~\ref{resn-analysis-sec}.
    179180While this theoretical result is daunting, its implications can be mitigated in practice.
    180 \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.
     181\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, as shown in Section~\ref{instance-expr-sec}.
    181182Secondly, 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.
    182183Programmers 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.
     
    187188Expression 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.
    188189
    189 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.
     190If 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 usually proportional to the complexity of the types being unified.
    190191In 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:
    191192
     
    198199To 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!.
    199200Accordingly, 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.
     201This does not, however, account for the higher costs of unifying two polymorphic type variables, which may in the worst case result in a recursive unification of all type variables in the expression (as discussed in Chapter~\ref{env-chap}).
     202Since this recursive unification reduces the number of type variables, it may happen at most once, for an added $O(p^d)$ cost for a top-level expression with $O(p^d)$ type variables.
    200203
    201204Implicit conversions are also checked in argument-parameter matching, but the cost of checking for the existence of an implicit conversion is again proportional to the complexity of the type, $O(d)$.
    202 Polymorphism again introduces a potential expense here; for a monomorphic function there is only one potential implicit conversion from argument type to parameter type, while if the parameter type is an unbound polymorphic type variable then any implicit conversion from the argument type could potentially be considered a valid binding for that type variable.
     205Polymorphism also introduces a potential expense here; for a monomorphic function there is only one potential implicit conversion from argument type to parameter type, while if the parameter type is an unbound polymorphic type variable then any implicit conversion from the argument type could potentially be considered a valid binding for that type variable.
    203206\CFA{}, however, requires exact matches for the bound type of polymorphic parameters, removing this problem.
    204 An interesting question for future work is whether loosening this requirement incurs significant runtime cost in practice.
     207An interesting question for future work is whether loosening this requirement incurs a significant compiler runtime cost in practice; preliminary results from the prototype system described in Chapter~\ref{expr-chap} suggest it does not.
    205208
    206209Considering the recursive traversal of the expression tree, polymorphism again greatly expands the worst-case runtime.
     
    216219Since the size of the expression is $O(p^d)$, letting $n = p^d$ this simplifies to $O(i^n \cdot n^2)$
    217220
    218 This already high bound does not yet account for the cost of assertion resolution, though.
     221This already high bound does not yet account for the cost of assertion satisfaction, however.
    219222\CFA{} uses type unification on the assertion type and the candidate declaration type to test assertion satisfaction; this unification calculation has cost proportional to the complexity of the declaration type after substitution of bound type variables; as discussed above, this cost is $O(d)$.
    220223If there are $O(a)$ type assertions on each declaration, there are $O(i)$ candidates to satisfy each assertion, for a total of $O(ai)$ candidates to check for each declaration.
    221224However, each assertion candidate may generate another $O(a)$ assertions, recursively until the assertion recursion limit $r$ is reached, for a total cost of $O((ai)^r \cdot d)$.
    222 Now, $a$, $i$, and $r$ are properties of the set of declarations in scope, or the language spec in the case of $r$, so $(ai)^r$ is essentially a constant, albeit a very large one.
     225Now, $a$ and $i$ are properties of the set of declarations in scope, while $r$ is defined by the language spec, so $(ai)^r$ is essentially a constant for purposes of expression resolution, albeit a very large one.
    223226It is not uncommon in \CFA{} to have functions with dozens of assertions, and common function names (\eg{} !?{}!, the constructor) can have hundreds of overloads.
    224227
    225 It is clear that assertion resolution costs can be very large, and in fact a method for heuristically reducing them is one of the key contributions of this thesis, but it should be noted that the worst-case analysis is a particularly poor match for actual code in the case of assertions.
     228It is clear that assertion satisfaction costs can be very large, and in fact a method for heuristically reducing these costs is one of the key contributions of this thesis, but it should be noted that the worst-case analysis is a particularly poor match for actual code in the case of assertions.
    226229It is reasonable to assume that most code compiles without errors, as in an actively-developed project the code will be compiled many times, generally with relatively few new errors introduced between compiles.
    227 However, the worst-case bound for assertion resolution is based on recursive assertion satisfaction exceeding the limit, which is an error case.
     230However, the worst-case bound for assertion satisfaction is based on recursive assertion satisfaction calls exceeding the limit, which is an error case.
    228231In practice, then, the depth of recursive assertion satisfaction should be bounded by a small constant for error-free code, which will account for the vast majority of problem instances.
    229232
    230233Similarly, uses of polymorphism like those that generate the $O(d)$ bound on unification or the $O(i^{p^d})$ bound on number of candidates are particular enough to be rare, but not completely absent.
    231 This analysis points to type unification, argument-parameter matching, and assertion satisfaction as potentially costly elements of expression resolution, and thus potentially profitable targets for tuning on realistic data.
     234This analysis points to type unification, argument-parameter matching, and assertion satisfaction as potentially costly elements of expression resolution, and thus profitable targets for algorithmic investigation.
    232235Type unification is discussed in Chapter~\ref{env-chap}, while the other aspects are covered below.
    233 
    234 % also, unification of two classes is not particularly cheap ... the bounds above may be optimistic
    235236
    236237\subsection{Argument-Parameter Matching} \label{arg-parm-matching-sec}
     
    239240One opportunity for interpretation pruning is by the argument-parameter type matching, but the literature provides no clear answers on whether candidate functions should be chosen according to their available arguments, or whether argument resolution should be driven by the available function candidates.
    240241For programming languages without implicit conversions, argument-parameter matching is essentially the entirety of the expression resolution problem, and is generally referred to as ``overload resolution'' in the literature.
    241 All expression-resolution algorithms form a DAG of interpretations, some explicitly, sone implicitly; in this DAG, arcs point from function-call interpretations to argument interpretations, as in Figure~\ref{res-dag-fig}
     242All expression-resolution algorithms form a DAG of interpretations, some explicitly, some implicitly; in this DAG, arcs point from function-call interpretations to argument interpretations, as in Figure~\ref{res-dag-fig}
    242243
    243244\begin{figure}[h]
     
    279280
    280281Baker~\cite{Baker82} left empirical comparison of different overload resolution algorithms to future work; Bilson~\cite{Bilson03} described an extension of Baker's algorithm to handle implicit conversions and polymorphism, but did not further explore the space of algorithmic approaches to handle both overloaded names and implicit conversions.
    281 This thesis closes that gap in the literature by performing performance comparisons of both top-down and bottom-up expression resolution algorithms.
     282This thesis closes that gap in the literature by performing performance comparisons of both top-down and bottom-up expression resolution algorithms, with results reported in Chapter~\ref{expr-chap}.
    282283
    283284\subsection{Assertion Satisfaction} \label{assn-sat-sec}
     
    286287Before accepting any subexpression candidate, Bilson first checks that that candidate's assertions can all be resolved; this is necessary due to Bilson's addition of assertion satisfaction costs to candidate costs (discussed in Section~\ref{conv-cost-sec}).
    287288If this subexpression interpretation ends up not being used in the final resolution, than the (sometimes substantial) work of checking its assertions ends up wasted.
    288 Bilson's assertion checking function recurses on two lists, !need! and !newNeed!, the current declaration's assertion set and those implied by the assertion-satisfying declarations, respectively, as detailed in the pseudocode below (ancillary aspects of the algorithm are omitted for clarity):
     289Bilson's assertion checking function recurses on two lists, !need! and !newNeed!, the current declaration's assertion set and those implied by the assertion-satisfying declarations, respectively, as detailed in the pseudo-code below (ancillary aspects of the algorithm are omitted for clarity):
    289290
    290291\begin{cfa}
     
    294295        if ( is_empty(need) ) {
    295296                if ( is_empty( newNeed ) ) return { have };
    296                 return checkAssertions( newNeed, {}, have, env );
     297                else return checkAssertions( newNeed, {}, have, env );
    297298        }
    298299
     
    321322Thus, if there is any mutually-compatible set of assertion-satisfying declarations which does not include any polymorphic functions (and associated recursive assertions), then the optimal set of assertions will not require any recursive !newNeed! satisfaction.
    322323More generally, due to the \CFA{} cost model changes I introduced in Section~\ref{conv-cost-sec}, the conversion cost of an assertion-satisfying declaration is no longer dependent on the conversion cost of its own assertions.
    323 As such, all sets of mutually-compatible assertion-satisfying declarations can be sorted by their summed conversion costs, and the recursive !newNeed! satisfaction pass can be limited to only check the feasibility of the minimal-cost sets.
     324As such, all sets of mutually-compatible assertion-satisfying declarations can be sorted by their summed conversion costs, and the recursive !newNeed! satisfaction pass is required only to check the feasibility of the minimal-cost sets.
    324325This 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{}.
    325326
     
    351352During the course of checking the assertions of a single top-level expression, I cache the results of each assertion checked.
    352353The 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.
    353 This adjusted assertion declaration is then run through the \CFA{} name mangling algorithm to produce a comparable string-type key.
     354This adjusted assertion declaration is then run through the \CFA{} name mangling algorithm to produce an equivalent string-type key.
    354355
    355356The 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.
    356 For instance, Matsakis~\cite{Matsakis17} and the Rust team have been working on checking satisfaction of Rust traits with a PROLOG-based engine.
     357For instance, Matsakis~\cite{Matsakis17} and the Rust team have developed a PROLOG-based engine to check satisfaction of Rust traits.
    357358The 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.
    358359Expressing 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.
     
    363364\section{Conclusion \& Future Work} \label{resn-conclusion-sec}
    364365
    365 I have experimented with using expression resolution rather than type unification to choose assertion resolutions; this path should be investigated further in future work.
     366As the results in Chapter~\ref{expr-chap} show, the algorithmic approaches I have developed for \CFA{} expression resolution are sufficient to build a practically-performant \CFA{} compiler.
     367This work may also be of use to other compiler construction projects, notably to members of the \CC{} community as they implement the new Concepts \cite{C++Concepts} standard, which includes type assertions similar to those used in \CFA{}, as well as a C-derived implicit conversion system.
     368
     369I have experimented with using expression resolution rather than type unification to check assertion satisfaction; this variant of the expression resolution problem should be investigated further in future work.
    366370This approach is more flexible than type unification, allowing for conversions to be applied to functions to satisfy assertions.
    367371Anecdotally, this flexibility matches user-programmer expectations better, as small type differences (\eg{} the presence or absence of a reference type, or the usual conversion from !int! to !long!) no longer break assertion satisfaction.
    368 Practically, the resolver prototype uses this model of assertion satisfaction, with no apparent deficit in performance; the generated expressions that are resolved to satisfy the assertions are easier than the general case because they never have nested subexpressions, which eliminates much of the theoretical differences between unification and resolution.
    369 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.
    370 
    371 % Discuss possibility of parallel subexpression resolution
    372 
    373 % Mention relevance of work to C++20 concepts
    374 
    375 % Mention more compact representations of the (growing) cost tuple
     372Practically, the resolver prototype discussed in Chapter~\ref{expr-chap} uses this model of assertion satisfaction, with no apparent deficit in performance; the generated expressions that are resolved to satisfy the assertions are easier than the general case because they never have nested subexpressions, which eliminates much of the theoretical differences between unification and resolution.
     373The 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 to their requesting functions with the proper signatures.
     374
     375Though performance of the existing algorithms is promising, some further optimizations do present themselves.
     376The refined cost model discussed in Section~\ref{conv-cost-sec} is more expressive, but also requires more than twice as many fields; it may be fruitful to investigate more tightly-packed in-memory representations of the cost-tuple, as well as comparison operations that require fewer instructions than a full lexicographic comparison.
     377Integer or vector operations on a more-packed representation may prove effective, though dealing with the negative-valued $specialization$ field may require some effort.
     378
     379Parallelization of various phases of expression resolution may also be useful.
     380The algorithmic variants I have introduced for both argument-parameter matching and assertion satisfaction are essentially divide-and-conquer algorithms, which solve subproblem instances for each argument or assertion, respectively, then check mutual compatibility of the solutions.
     381While the checks for mutual compatibility are naturally more serial, there may be some benefit to parallel resolution of the subproblem instances.
     382
     383The resolver prototype built for this project and described in Chapter~\ref{expr-chap} would be a suitable vehicle for many of these further experiments,and thus a technical contribution of continuing utility.
Note: See TracChangeset for help on using the changeset viewer.