Changeset 1836081 for doc/theses/aaron_moss_PhD/phd/typeenvironment.tex
 Timestamp:
 Mar 7, 2019, 3:17:13 PM (4 years ago)
 Branches:
 aaronthesis, armeh, cleanupdtors, enum, forallpointerdecay, jacob/cs343translation, jenkinssandbox, master, newast, newastuniqueexpr, pthreademulation, qualifiedEnum
 Children:
 d438111
 Parents:
 247c8f3
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

doc/theses/aaron_moss_PhD/phd/typeenvironment.tex
r247c8f3 r1836081 4 4 One key data structure for expression resolution is the \emph{type environment}. 5 5 As discussed in Chapter~\ref{resolutionchap}, being able to efficiently determine which type variables are bound to which concrete types or whether two type environments are compatible is a core requirement of the resolution algorithm. 6 Furthermore, expression resolution involves a search through many related possible solutions, so being able to reuse shared subsets of typeenvironment data and to switch between environments quickly is desirable for performance.7 In this chapter I discuss a number of type environment datastructure variants, including some novel variations on the unionfind \cite{Galler64} data structure introduced in this thesis.6 Furthermore, expression resolution involves a search through many related possible solutions, so the ability to reuse shared subsets of typeenvironment data and to switch between environments quickly is desirable for performance. 7 In this chapter, I discuss a number of type environment datastructure variants, including some novel variations on the unionfind \cite{Galler64} data structure introduced in this thesis. 8 8 Chapter~\ref{exprchap} contains empirical comparisons of the performance of these data structures when integrated into the resolution algorithm. 9 9 … … 11 11 12 12 For purposes of this chapter, a \emph{type environment} $T$ is a set of \emph{type classes} $\myset{T_1, T_2, \cdots, T_{T}}$. 13 Each type class $T_i$ contains a set of \emph{type variables} $\myset{v_{i,1}, v_{i,2}, \cdots, v_{i,T_i}}$; note that the sets of variables contained in two distinct classes in the same environment must be disjoint. 14 Each individual type class $T_i$ may also be associated with a \emph{bound}, $b_i$; this bound contains the \emph{bound type} which the variables in the type class are replaced with, but also includes other information in \CFACC{}, including whether type conversions are permissible on the bound type and what sort of type variables are contained in the class (data types, function types, or variadic tuples). 13 Each type class $T_i$ contains a set of \emph{type variables} $\myset{v_{i,1}, v_{i,2}, \cdots, v_{i,T_i}}$. 14 Since the type classes represent an equivalence relation over the type variables the sets of variables contained in two distinct classes in the same environment must be disjoint. 15 Each individual type class $T_i$ may also be associated with a \emph{bound}, $b_i$; this bound contains the \emph{bound type} that the variables in the type class are replaced with, but also includes other information in \CFACC{}, including whether type conversions are permissible on the bound type and what sort of type variables are contained in the class (data types, function types, or variadic tuples). 15 16 16 17 \begin{table} … … 19 20 \centering 20 21 \begin{tabular}{r@{\hskip 0.25em}ll} 21 $find(T, v_{i,j})$ & $\rightarrow T_i  \bot$ & Locate class for variable \\ 22 \hline 23 $find(T, v_{i,j})$ & $\rightarrow T_i~~\mathsf{fail}$ & Locate class for variable \\ 22 24 $report(T_i)$ & $\rightarrow \{ v_{i,j} \cdots \}$ & List variables for class \\ 23 $bound(T_i)$ & $\rightarrow b_i  \bot$ & Get bound for class \\24 $insert( v_{i,1})$ && New singlevariable class \\25 $bound(T_i)$ & $\rightarrow b_i~~\mathsf{fail}$ & Get bound for class \\ 26 $insert(T, v_{i,1})$ & & New singlevariable class \\ 25 27 $add(T_i, v_{i,j})$ & & Add variable to class \\ 26 28 $bind(T_i, b_i)$ & & Set or update class bound \\ 27 $unify(T, T_i, T_j)$ & $\rightarrow \top  \bot$ & Combine two type classes \\ 29 \hline 30 $unify(T, T_i, T_j)$ & $\rightarrow \mathsf{pass}~~\mathsf{fail}$ & Combine two type classes \\ 28 31 $split(T, T_i)$ & $\rightarrow T'$ & Revert the last $unify$ operation on $T_i$ \\ 29 $combine(T, T')$ & $\rightarrow \ top  \bot$ & Merge two environments \\32 $combine(T, T')$ & $\rightarrow \mathsf{pass}~~\mathsf{fail}$ & Merge two environments \\ 30 33 $save(T)$ & $\rightarrow H$ & Get handle for current state \\ 31 $backtrack(T, H)$ & & Return to handle state 34 $backtrack(T, H)$ & & Return to handle state \\ 35 \hline 32 36 \end{tabular} 33 37 \end{table} 34 38 35 39 Given this basic structure, type environments in \CFACC{} need to support eleven basic operations, summarized in Table~\ref{envoptable}. 36 The first s evenoperations are straightforward queries and updates on these data structures:37 The lookup operation $find(T, v_{i,j})$ produces $T_i$, the type class in $T$ whichcontains variable $v_{i,j}$, or an invalid sentinel value for no such class.40 The first six operations are straightforward queries and updates on these data structures: 41 The lookup operation $find(T, v_{i,j})$ produces $T_i$, the type class in $T$ that contains variable $v_{i,j}$, or an invalid sentinel value for no such class. 38 42 The other two query operations act on type classes, where $report(T_i)$ produces the set $\myset{v_{i,1}, v_{i,2}, \cdots, v_{i,T_i}}$ of all type variables in a class $T_i$ and $bound(T_i)$ produces the bound $b_i$ of that class, or a sentinel indicating no bound is set. 39 43 40 The update operation $insert(T, v_{i,1})$ creates a new type class $T_i$ in $T$ that contains only the variable $v_{i,1}$ and no bound; due to the disjointness property $v_{i,1}$ cannot belong to any other type class in $T$.44 The update operation $insert(T, v_{i,1})$ creates a new type class $T_i$ in $T$ that contains only the variable $v_{i,1}$ and no bound; due to the disjointness property, $v_{i,1}$ cannot belong to any other type class in $T$. 41 45 The $add(T_i, v_{i,j})$ operation adds a new type variable $v_{i,j}$ to class $T_i$; again, $v_{i,j}$ cannot exist elsewhere in $T$. 42 46 $bind(T_i, b_i)$ mutates the bound for a type class, setting or updating the current bound. 43 47 44 The $unify$ operation is the fundamental nontrivial operation a type environment datastructure must support.48 The $unify$ operation is the fundamental nontrivial operation a typeenvironment datastructure must support. 45 49 $unify(T, T_i, T_j)$ merges a type class $T_j$ into another $T_i$, producing a failure result and leaving $T$ in an invalid state if this merge fails. 46 50 It is always possible to unify the type variables of both classes by simply taking the union of both sets; given the disjointness property, no checks for set containment are required, and the variable sets can simply be concatenated if supported by the underlying data structure. 47 $unify$ depends on an internal $unifyBound$ operation which may fail.48 In \CFACC{}, $unifyBound(b_i, b_j) \rightarrow b'_i \bot$ checks that the type classes contain the same sort of variable, takes the tighter of the two conversion permissions, and checks if the bound types can be unified.51 $unify$ depends on an internal $unifyBound$ operation, which may fail. 52 In \CFACC{}, $unifyBound(b_i, b_j) \rightarrow b'_i~~\mathsf{fail}$ checks that the type classes contain the same sort of variable, takes the tighter of the two conversion permissions, and checks if the bound types can be unified. 49 53 If the bound types cannot be unified (\eg{} !struct A! with !int*!), then $unifyBound$ fails, while other combinations of bound types may result in recursive calls. 50 For instance, unifying !R*! with !S*! for type variables !R! and !S! will result in a call to $unify(T, find($!R!$), find($!S!$))$, while unifying !R*! with !int*! will resultin a call to $unifyBound$ on !int! and the bound type of the class containing !R!.54 For instance, unifying !R*! with !S*! for type variables !R! and !S! results in a call to $unify(T, find($!R!$), find($!S!$))$, while unifying !R*! with !int*! results in a call to $unifyBound$ on !int! and the bound type of the class containing !R!. 51 55 As such, a call to $unify(T, T_i, T_j)$ may touch every type class in $T$, not just $T_i$ and $T_j$, collapsing the entirety of $T$ into a single type class in extreme cases. 52 56 For more information on \CFA{} unification, see \cite{Bilson03}. 53 The inverse of $unify$ is $split(T, T_i)$, which produces a new environment $T'$ whichis the same as $T$ except that $T_i$ has been replaced by two classes corresponding to the arguments to the previous call to $unify$ on $T_i$.54 If there has been nocall to $unify$ on $T_i$ (\ie{} $T_i$ is a singleelement class) $T_i$ is absent in $T'$.55 56 Given the nature of the expression resolution problem as backtracking search, caching and concurrency are both useful tools to decrease runtime.57 The inverse of $unify$ is $split(T, T_i)$, which produces a new environment $T'$ that is the same as $T$ except that $T_i$ has been replaced by two classes corresponding to the arguments to the previous call to $unify$ on $T_i$. 58 If there is no prior call to $unify$ on $T_i$ (\ie{} $T_i$ is a singleelement class) $T_i$ is absent in $T'$. 59 60 Given the nature of the expression resolution problem as a backtracking search, caching and concurrency are both useful tools to decrease runtime. 57 61 However, both of these approaches may produce multiple distinct descendants of the same initial type environment, which have possibly been mutated in incompatible ways. 58 As such, to effectively employ either c oncurrency or caching, the type environment data structure must support an efficient method to check if two type environments are compatible and merge them if so.59 $combine(T,T')$ attempts to merge an environment $T'$ into another environment $T$, producing $\ top$ if successful or leaving $T$ in an invalid state and producing $\bot$ otherwise.60 The invalid state of $T$ on failure is not important, given that a combination failure will resultin the resolution algorithm backtracking to a different environment.62 As such, to effectively employ either caching or concurrency, the type environment data structure must support an efficient method to check if two type environments are compatible and merge them if so. 63 $combine(T,T')$ attempts to merge an environment $T'$ into another environment $T$, producing $\mathsf{pass}$ if successful or leaving $T$ in an invalid state and producing $\mathsf{fail}$ otherwise. 64 The invalid state of $T$ on failure is not important, given that a combination failure results in the resolution algorithm backtracking to a different environment. 61 65 $combine$ proceeds by calls to $insert$, $add$, and $unify$ as needed, and can be roughly thought of as calling $unify$ on every pair of classes in $T$ that have variables $v'_{i,j}$ and $v'_{i,k}$ in the same class $T'_i$ in $T'$. 62 66 Like $unify$, $combine$ can always find a mutuallyconsistent partition of type variables into classes (in the extreme case, all type variables from $T$ and $T'$ in a single type class), but may fail due to inconsistent bounds on merged type classes. … … 65 69 The set of mutations to a type environment across the execution of the resolution algorithm produce an implicit tree of related environments, and the backtracking search typically focuses only on one leaf of the tree at once, or at most a small number of closelyrelated nodes as arguments to $combine$. 66 70 As such, the ability to save and restore particular type environment states is useful, and supported by the $save(T) \rightarrow H$ and $backtrack(T, H)$ operations, which produce a handle for the current environment state and mutate an environment back to a previous state, respectively. 67 These operations can be naively implemented by a deep copy of $T$ into $H$ and vice versa, but have more efficient implementations in persistencyaware data structures .68 69 \section{Approaches} 71 These operations can be naively implemented by a deep copy of $T$ into $H$ and vice versa, but have more efficient implementations in persistencyaware data structures such as the persistent unionfind introduced in Section~\ref{envpersistentunionfind}. 72 73 \section{Approaches} \label{envapproachessec} 70 74 71 75 \subsection{Na\"{\i}ve} \label{naiveenvsec} … … 73 77 The type environment data structure used in Bilson's~\cite{Bilson03} original implementation of \CFACC{} is a straightforward translation of the definitions in Section~\ref{envdefnsec} to \CC{} code; a !TypeEnvironment! contains a list of !EqvClass! type equivalence classes, each of which contains the type bound information and a treebased sorted set of type variables. 74 78 This approach has the benefit of being easy to understand and not imposing lifecycle or inheritance constraints on its use, but, as can be seen in Table~\ref{envboundstable}, does not support many of the desired operations with any particular efficiency. 75 Some variations on this structure may improve performance somewhat; for instance, replacing the !EqvClass! variable storage with a hashbased set would reduce search and update times from $O(\log n)$ to amortized $O(1)$, while adding an index for the type variables in the entire environment would removethe need to check each type class individually to maintain the disjointness property.79 Some variations on this structure may improve performance somewhat; for instance, replacing the !EqvClass! variable storage with a hashbased set reduces search and update times from $O(\log n)$ to amortized $O(1)$, while adding an index for the type variables in the entire environment removes the need to check each type class individually to maintain the disjointness property. 76 80 These improvements do not change the fundamental issues with this data structure, however. 77 81 78 82 \subsection{Incremental Inheritance} \label{incenvsec} 79 83 80 One more invasive modification to this data structure which I investigated is to support swifter combinations of closelyrelated environments in the backtracking tree by storing a reference to a \emph{parent} environment within each environment, and having that environment only store type classes whichhave been modified with respect to the parent.84 One more invasive modification to this data structure that I investigated is to support swifter combinations of closelyrelated environments in the backtracking tree by storing a reference to a \emph{parent} environment within each environment, and having that environment only store type classes that have been modified with respect to the parent. 81 85 This approach provides constanttime copying of environments, as a new environment simply consists of an empty list of type classes and a reference to its (logically identical) parent; since many type environments are no different than their parent, this speeds backtracking in this common case. 82 Since all mutations made to a child environment are by definition compatible with the parent environment, two descendants of a common ancestor environment can be combined by iteratively combining the changes made in one environment then that environment's parentuntil the common ancestor is reached, again reusing storage and reducing computation in many cases.83 84 For this environment I also employed a lazilygenerated index of type variables to their containing class, which could be in either the current environment or an ancestor.85 Any mutation of a type class in an ancestor environment would cause that class to be copied into the current environment before mutation, as well as added to the index, ensuring thatall local changes to the type environment are listed in its index.86 Since all mutations made to a child environment are by definition compatible with the parent environment, two descendants of a common ancestor environment can be combined by iteratively combining the changes made in one environment, then that environment's parent, until the common ancestor is reached, again reusing storage and reducing computation in many cases. 87 88 For this environment, I also employed a lazilygenerated index of type variables to their containing class, which could be in either the current environment or an ancestor. 89 Any mutation of a type class in an ancestor environment causes that class to be copied into the current environment before mutation, as well as added to the index, ensuring all local changes to the type environment are listed in its index. 86 90 However, not adding type variables to the index until lookup or mutation preserves the constanttime environment copy operation in the common case in which the copy is not mutated from its parent during its lifecycle. 87 91 88 This approach imposes some performance penalty on $combine$ if related environments are not properly linked together, as the entire environment needs to be combined rather than just the diff , but is correct as long as the ``null parent'' basecase is properly handled.92 This approach imposes some performance penalty on $combine$ if related environments are not properly linked together, as the entire environment needs to be combined rather than just the difference, but is correct as long as the ``null parent'' basecase is properly handled. 89 93 The lifecycle issues are somewhat more complex, as many environments may descend from a common parent, and all of these need their parent to stay alive for purposes of lookup. 90 These issues can be solved by ``flattening'' parent nodes into their children before the parent s leave scope, but given the tree structure of the inheritance graph it is more straightforward to store the parent nodes in referencecounted or otherwise automatically garbagecollected heap storage.94 These issues can be solved by ``flattening'' parent nodes into their children before the parent's scope ends, but given the tree structure of the inheritance graph it is more straightforward to store the parent nodes in referencecounted or otherwise automatically garbagecollected heap storage. 91 95 92 96 \subsection{UnionFind} \label{envunionfindapproach} 93 97 94 Given the nature of the classes of type variables as disjoint sets, another natural approach to implementing a type environment is the unionfind disjoint set datastructure~\cite{Galler64}.98 Given the nature of the classes of type variables as disjoint sets, another natural approach to implementing a type environment is the unionfind disjointset datastructure~\cite{Galler64}. 95 99 Unionfind efficiently implements two operations over a partition of a collection of elements into disjoint sets; $find(x)$ locates the \emph{representative} of $x$, the element which canonically names its set, while $union(r, s)$ merges two sets represented by $r$ and $s$, respectively. 96 100 The unionfind data structure is based on providing each element with a reference to its parent element, such that the root of a tree of elements is the representative of the set of elements contained in the tree. 97 101 $find$ is then implemented by a search up to the parent, generally combined with a \emph{path compression} step that links nodes more directly to their ancestors to speed up subsequent searches. 98 102 $union$ involves making the representative of one set a child of the representative of the other, generally employing a rank or sizebased heuristic to ensure that the tree remains somewhat balanced. 99 If both path compression and a balancing heuristic are employed, both $union$ and $find$ run in amortized $O(\alpha(n))$ worstcase time; this bound by the inverse Ackermann function is a small constant for all practical values of $n$.103 If both path compression and a balancing heuristic are employed, both $union$ and $find$ run in amortized $O(\alpha(n))$ worstcase time; this inverse Ackermann bound is a small constant for all practical values of $n$ \cite{Tarjan75}. 100 104 101 105 The unionfind $find$ and $union$ operations have obvious applicability to the $find$ and $unify$ type environment operations in Table~\ref{envoptable}, but the unionfind data structure must be augmented to fully implement the type environment operations. 102 In particular, the type 103 This issue can be solved by including a side map from class representatives to the type 106 In particular, the typeclass bound cannot be easily included in the unionfind data structure, as the requirement to make it the class representative breaks the balancing properties of $union$, and requires tooclose integration of the type environment $unifyBound$ internal operation. 107 This issue can be solved by including a side map from class representatives to the typeclass bound. 104 108 If placeholder values are inserted in this map for type classes without bounds than this also has the useful property that the key set of the map provides an easily obtainable list of all the class representatives, a list which cannot be derived from the unionfind data structure without a linear search for class representatives through all elements. 105 109 … … 108 112 Another type environment operation not supported directly by the unionfind data structure is $report$, which lists the type variables in a given class, and similarly $split$, which reverts a $unify$ operation. 109 113 Since the unionfind data structure stores only links from children to parents and not viceversa, there is no way to reconstruct a class from one of its elements without a linear search over the entire data structure, with $find$ called on each element to check its membership in the class. 110 The situation is even worse for the $split$ operation, which would require extra information to maintain the order that each child was added to its parent node.111 Unfortunately, the literature \cite{Tarjan84,Galil91,Patwary10} on unionfind does not present a way to keep references to children without breaking the asymptotic time bounds of the algorithm; I have discovered a method to do so which, despite its simplicity, seems to be novel.114 The situation is even worse for the $split$ operation, which requires extra information to maintain the order that each child is added to its parent node. 115 Unfortunately, the literature \cite{Tarjan84,Galil91,Patwary10} on unionfind does not present a way to keep references to children without breaking the asymptotic time bounds of the algorithm; I have discovered a method to do so, which, despite its simplicity, seems to be novel. 112 116 113 117 The core idea of this ``unionfind with classes'' data structure and algorithm is to keep the members of each class stored in a circularlylinked list. … … 133 137 134 138 \begin{theorem} \label{envreversethm} 135 The !next! pointer of a class representative in the unionfind with classes algorithm without path compressionpoints to a leaf from the mostrecentlyadded subtree.139 The !next! pointer of a class representative in the unionfind with classes algorithm, without path compression, points to a leaf from the mostrecentlyadded subtree. 136 140 \end{theorem} 137 141 … … 139 143 By induction on the height of the tree. \\ 140 144 \emph{Base case:} A height 1 tree by definition includes only a single item. In such a case, the representative's !next! pointer points to itself by construction, and the representative is the mostrecentlyadded (and only) leaf in the tree. \\ 141 \emph{Inductive case:} By construction, a tree $T$ of height greater than 1 has children of the root (representative) node that were representative nodes of classes merged by $union$. By definition, the mostrecentlyadded subtree $T'$ has a smaller height than $T$, thus by the inductive hypothesis before the mostrecent $union$ operation the !next! pointer of the root of $T'$ pointed to one of the leaf nodes of $T'$; by construction the !next! pointer of the root of $T$ points to this leaf after the $union$ operation.145 \emph{Inductive case:} By construction, a tree $T$ of height greater than 1 has children of the root (representative) node that were representative nodes of classes merged by $union$. By definition, the mostrecentlyadded subtree $T'$ has a smaller height than $T$, thus by the inductive hypothesis before the mostrecent $union$ operation, the !next! pointer of the root of $T'$ pointed to one of the leaf nodes of $T'$; by construction the !next! pointer of the root of $T$ points to this leaf after the $union$ operation. 142 146 \end{proof} 143 147 … … 147 151 \label{envpersistentunionfind} 148 152 149 Given the backtracking nature of the resolution algorithm discussed in Section~\ref{envdefnsec}, the abilities to quickly switch between related versions of a type environment and to deduplicate shared data betweenenvironments are both assets to performance.153 Given the backtracking nature of the resolution algorithm discussed in Section~\ref{envdefnsec}, the abilities to quickly switch between related versions of a type environment and to deduplicate shared data among environments are both assets to performance. 150 154 Conchon and Filli\^{a}tre~\cite{Conchon07} present a persistent unionfind data structure based on the persistent array of Baker~\cite{Baker78,Baker91}. 151 155 152 In Baker's persistent array, an array referencecontains either a pointer to the array or a pointer to an \emph{edit node}; these edit nodes contain an array index, the value in that index, and another array reference pointing either to the array or a different edit node.153 In this manner, a tree of edits is formed, rooted at the actual array. 156 In Baker's persistent array, an \emph{array reference} contains either a pointer to the array or a pointer to an \emph{edit node}; these edit nodes contain an array index, the value in that index, and another array reference pointing either to the array or a different edit node. 157 By construction, these array references always point to a node more like the actual array, forming a tree of edits rooted at the actual array. 154 158 Reads from the actual array at the root can be performed in constant time, as with a nonpersistent array. 155 159 The persistent array can be mutated in constant time by directly modifying the underlying array, then replacing its array reference with an edit node containing the mutated index, the previous value at that index, and a reference to the mutated array. If the current array reference is not the root, mutation consists simply of constructing a new edit node encoding the change and referring to the current array reference. 156 The mutation algorithm at the root is in some sense a special case of the key operation on persistent arrays, $reroot$. 157 160 161 The mutation algorithm at the root is a special case of the key operation on persistent arrays, $reroot$. 158 162 A rerooting operation takes any array reference and makes it the root node of the array. 159 This is accomplished by tracing the path from some edit node to the root node of the array (always the underlying array), recursively applying the edits to the underlying array and replacing each edit node's successor with the inverse edit.163 This operation is accomplished by tracing the path from some edit node to actual array at the root node, recursively applying the edits to the underlying array and replacing each edit node's successor with the inverse edit. 160 164 In this way, any previous state of the persistent array can be restored in time proportional to the number of edits to the current state of the array. 161 165 While $reroot$ does maintain the same value mapping in every version of the persistent array, the internal mutations it performs break threadsafety, and thus it must be used behind a lock in a concurrent context. … … 164 168 165 169 While Conchon and Filli\^{a}tre~\cite{Conchon07} implement their persistent unionfind data structure over a universe of integer elements in the fixed range $[1,N]$, the type environment problem needs more flexibility. 166 In particular, an arbitrary number of type variables must be added to the environment. 167 As such, a persistent hash table is a more suitable structure than a persistent array, providing the same expected asymptotic time bounds while allowing a dynamic number of elements. 168 Besides replacing the underlying array with a hash table, the other major change in this approach is to replace the two types of array references, !Array! and !Edit!, with four node types, !Table!, !Edit!, !Add!, and !Remove!, where !Add! adds a new keyvalue pair, !Remove! removes a key, and !Edit! mutates an existing keyvalue pair. 169 In this variant of \CFACC{}, this persistent hash table is used as the side map discussed in Section~\ref{envunionfindapproach} for class bounds. 170 The actual unionfind data structure is slightly modified from this approach, with a !Base! node containing the root unionfind data structure, !Add! nodes adding new elements, !AddTo! nodes defining the union of two type classes, and !Remove! and !RemoveFrom! nodes as inverses of the previous two elements, for purposes of maintaining the edit list; Figure~\ref{persistentunionfindfig} demonstrates the structure of a simple example. 170 In particular, an arbitrary number of type variables may be added to the environment. 171 As such, a persistent hash table is a more suitable structure than a persistent array, providing the same expected asymptotic time bounds, while allowing a dynamic number of elements. 172 Besides replacing the underlying array with a hash table, the other major change in this approach is to replace the two types of array references, !Array! and !Edit!, with four node types, !Table!, !Edit!, !Add!, and !Remove!, where !Add! adds a new keyvalue pair, !Remove! removes a keyvalue pair, and !Edit! mutates an existing keyvalue pair. 173 In this variant of \CFACC{}, this persistent hashtable is used as the side map discussed in Section~\ref{envunionfindapproach} for class bounds. 174 The actual unionfind data structure is slightly modified from this approach, with a !Base! node containing the root unionfind data structure, !Add! nodes adding new elements, !AddTo! nodes defining the union of two type classes, and !Remove! and !RemoveFrom! nodes as inverses of the previous two elements, for purposes of maintaining the edit list. 175 Figure~\ref{persistentunionfindfig} demonstrates the structure of a simple example. 171 176 Making !AddTo! and !RemoveFrom! single nodes provides semantic information missing from the raw array updates in Conchon and Filli\^{a}tre's data structure. 172 177 !RemoveFrom! is implemented using the ``leaf of last union'' approach discussed in Section~\ref{envunionfindclassesapproach}; this does, however, preclude the use of pathcompression algorithms in this persistent unionfind data structure. … … 181 186 This added semantic information on $union$ operations in the persistent unionfind edit tree exposes a new option for combining type environments. 182 187 If the type environments are part of the same edit tree, one environment $T'$ can be combined with another $T$ by only testing the edits on the path from $T'$ to $T$ in both the persistent unionfind data structure describing the classes and the persistent hash table containing the class bounds. 183 This is generally more efficient than testing the compatibility of all type classes in $T'$, as only those that are actually different than those in $T$ must be considered.184 This improved performance comes at the cost of some flexibility, however, as the edittree link must be maintained between any two environments to be combined under this algorithm.188 This approach is generally more efficient than testing the compatibility of all type classes in $T'$, as only those that are actually different than those in $T$ must be considered. 189 However, the improved performance comes at the cost of some flexibility, as the edittree link must be maintained between any two environments to be combined under this algorithm. 185 190 186 191 The procedure for $combine(T, T')$ based on edit paths is as follows: 187 192 The shared edit trees for classes and bindings are rerooted at $T$, and the path from $T'$ to $T$ is followed to create a list of actual edits. 188 193 By tracking the state of each element, redundant changes such as an !Edit! followed by an !Edit! can be reduced to their form in $T'$ by dropping the later (more like $T$) !Edit! for the same key; !Add! and !Remove! cancel similarly. 189 This procedure is repeated for both the class edit tree and the binding edittree.190 When the list of net changes to the environment has beenproduced, the additive changes are applied to $T$.191 For example, if a type class exists in $T'$ but not $T$, the corresponding !Add! edit will be applied to $T$, but in the reverse situation the !Remove! edit will not beapplied to $T$, as the intention is to produce a new environment representing the union of the two sets of type classes; similarly, !AddTo! edits are applied to unify typeclasses in $T$ that are united in $T'$, but !RemoveFrom! edits that split type classes are not.192 The new environment, $T''$ can always be constructed with a consistent partitioning of type variables; in the extreme case, all variables from both $T$ and $T'$ will be united in a single type class in $T''$.193 Where $combine$ can fail is in unifying the bound types; if any class in $T'$ has a class bound which does not unify with the merged class in $T''$ than $combine$ fails.194 195 \section{Analysis} 196 197 In this section I present asymptotic analyses of the various approaches to atype environment data structure discussed in the previous section.194 This procedure is repeated for both the class edittree and the binding edittree. 195 When the list of net changes to the environment is produced, the additive changes are applied to $T$. 196 For example, if a type class exists in $T'$ but not $T$, the corresponding !Add! edit is applied to $T$, but in the reverse situation the !Remove! edit is not applied to $T$, as the intention is to produce a new environment representing the union of the two sets of type classes; similarly, !AddTo! edits are applied to unify typeclasses in $T$ that are united in $T'$, but !RemoveFrom! edits that split type classes are not. 197 A new environment, $T''$, can always be constructed with a consistent partitioning of type variables; in the extreme case, all variables from both $T$ and $T'$ are united in a single type class in $T''$. 198 $combine$ can fail to unify the bound types; if any class in $T'$ has a class bound that does not unify with the merged class in $T''$, then $combine$ fails. 199 200 \section{Analysis} \label{envanalysissec} 201 202 In this section, I present asymptotic analyses of the various approaches to the type environment data structure discussed in the previous section. 198 203 My results are summarized in Table~\ref{envboundstable}; in all cases, $n$ is the number of type classes, $m$ is the maximum size of a type class, and $p$ the number of edits between two environments or one environment and the empty environment. 199 $u(n)$ captures the recursive cost of class unification ; I have kept this separate so that the $O(n)$ number of recursive class unifications can be separated from the direct cost of each recursive step.204 $u(n)$ captures the recursive cost of class unification, which is kept separate so that the $O(n)$ number of recursive class unifications can be distinguished from the direct cost of each recursive step. 200 205 201 206 \begin{table} … … 205 210 \begin{tabular}{rllll} 206 211 \hline 207 & \textbf{Na\"{\i}ve} & \textbf{Incremental} & \textbf{UnionFind} & \textbf{Persistent UF} \\ 208 \hline 209 $find$ & $O(n)$ & $O(p)$ & $O(\alpha(m))$ & $O(\log m)$ \\ 210 $report$ & $O(m)$ & $O(m)$ & $O(n\alpha(m))$ & $O(m)$ \\ 211 $bound$ & $O(1)$ & $O(1)$ & $O(1)$ & $O(1)$ \\ 212 $insert$ & $O(1)$ & $O(1)$ & $O(1)$ & $O(1)$ \\ 213 $add$ & $O(1)$ & $O(m)$ & $O(1)$ & $O(1)$ \\ 214 $bind$ & $O(1)$ & $O(1)$ & $O(1)$ & $O(1)$ \\ 215 $unify$ & $O(m + u(n))$ & $O(m + u(n))$ & $O(1 + u(n))$ & $O(1 + u(n))$ \\ 216 $split$ &  &  &  & $O(\log m)$ \\ 217 $combine$ & $O(n^2m + nu(n))$ & $O(p^2m + pu(n))$ & $O(n\alpha(m) + nu(n))$ & $O(p \log m + pu(n))$ \\ 218 $save$ & $O(nm)$ & $O(1)$ & $O(nm)$ & $O(1)$ \\ 219 $backtrack$ & $O(nm)$ & $O(pm)$ & $O(nm)$ & $O(p)$ \\ 212 & \textbf{Na\"{\i}ve} & \textbf{Incremental} & \textbf{UnionFind} & \textbf{Persistent UF} \\ 213 \hline 214 $find$ & $O(n)$ & $O(p)$ & $O(\alpha(m))$ & $O(\log m)$ \\ 215 $report$ & $O(m)$ & $O(m)$ & $O(nm\alpha(m))$ & $O(m)$ \\ 216 $bound$ & $O(1)$ & $O(1)$ & $O(1)$ & $O(1)$ \\ 217 $insert$ & $O(1)$ & $O(1)$ & $O(1)$ & $O(1)$ \\ 218 $add$ & $O(1)$ & $O(m)$ & $O(1)$ & $O(1)$ \\ 219 $bind$ & $O(1)$ & $O(1)$ & $O(1)$ & $O(1)$ \\ 220 $unify$ & $O(m + u(n))$ & $O(m + u(n))$ & $O(1 + u(n))$ & $O(1 + u(n))$ \\ 221 $split$ &  &  &  & $O(\log m)$ \\ 222 $combine$ & $O(n^2m $ & $O(p^2m $ & $O(nm\alpha(m) $ & $O(p \log m $ \\ 223 & $~~~+ nu(n))$ & $~~~+ pu(n))$ & $~~~+ nu(n))$ & $~~~+ pu(n))$ \\ 224 $save$ & $O(nm)$ & $O(1)$ & $O(nm)$ & $O(1)$ \\ 225 $backtrack$ & $O(nm)$ & $O(pm)$ & $O(nm)$ & $O(p)$ \\ 220 226 \hline 221 227 \end{tabular} … … 225 231 \label{naiveincrementalanalysis} 226 232 227 The na\"{\i}ve type environment data structure does not have an overallindex for type variables, but does have an index for each type class, assumed to be hashbased here.233 The na\"{\i}ve type environment data structure does not have an environmentwide index for type variables, but does have an index for each type class, assumed to be hashbased here. 228 234 As a result, every class's index must be consulted for a $find$ operation, at an overall cost of $O(n)$. 229 235 The incremental variant builds an overall hashbased index as it is queried, but may need to recursively check its parent environments if its local index does not contain a type variable, and may have as many parents as times it has been modified, for cost $O(p)$. … … 238 244 The na\"{\i}ve $combine$ operation must traverse each of the classes of one environment, merging in any class of the other environment that shares a type variable. 239 245 Since there are at most $n$ classes to unify, the unification cost is $O(nm + nu(n))$, while traversal and $find$ costs to locate classes to merge total $O(n^2m)$, for an overall cost of $O(n^2m + nu(n))$. 240 The incremental $combine$ operation works similarly, but only needs to consider classes modified in either environment sincethe common ancestor of both environments, allowing the $n$ cost terms to be substituted for $p$, for an overall cost of $O(p^m + pu(n))$.246 The incremental $combine$ operation works similarly, but only needs to consider classes modified in either environment with respect to the common ancestor of both environments, allowing the $n$ cost terms to be substituted for $p$, for an overall cost of $O(p^m + pu(n))$. 241 247 Neither variant supports the $split$ operation to undo a $unify$. 242 248 … … 248 254 249 255 The unionfind data structure is designed to support $find$ efficiently, and thus for any variant, the cost is simply the distance up the tree to the representative element. 250 For basic unionfind, this is amortized to the inverse Ackermann function, $O(\alpha(m))$, essentially a small constant, though the loss of path compression in persistent unionfind raises this cost to the still cheap$O(\log m)$.251 Basic unionfind is not designed to support the $report$ operation, however, so it must be simulated by checking the representative of every type variable, at cost $O(n \alpha(m))$.256 For basic unionfind, this is amortized to the inverse Ackermann function, $O(\alpha(m))$, essentially a small constant, though the loss of path compression in persistent unionfind raises this cost to $O(\log m)$. 257 Basic unionfind is not designed to support the $report$ operation, however, so it must be simulated by checking the representative of every type variable, at cost $O(nm\alpha(m))$. 252 258 Persistent unionfind, on the other hand, uses the ``with classes'' extension to unionfind described in Section~\ref{envunionfindclassesapproach} to run $report$ in $O(m)$ time. 253 259 … … 256 262 Since $add$ simply involves attaching a new child to the class root, it is also a $O(1)$ operation for all unionfind environment variants. 257 263 258 Unionfind is also designed to support $unify$ in constant time, and as such, given class representatives, the variablemerging most of $unify$ for both variants is $O(1)$ to make one representative the child of the other, plus the $O(u(n))$ term for $unifyBound$.264 Unionfind is also designed to support $unify$ in constant time, and as such, given class representatives, the variablemerging cost of $unify$ for both variants is $O(1)$ to make one representative the child of the other, plus the $O(u(n))$ term for $unifyBound$. 259 265 Basic unionfind does not support $split$, but persistent unionfind can accomplish it using the mechanism described in Section~\ref{envunionfindclassesapproach} in $O(\log m)$, the cost of traversing up to the root of a class from a leaf without path compression. 260 266 $combine$ on the basic unionfind data structure works similarly to the data structures discussed above in Section~\ref{naiveincrementalanalysis}, with a $O(nu(n))$ term for the $O(n)$ underlying $unify$ operations, and a $O(n\alpha(m))$ term to find the classes which need unification by checking the class representatives of each corresponding type variable in both environments for equality. … … 268 274 \section{Conclusion \& Future Work} 269 275 270 This chapter has discussed the type environment data structure, as well as some more sophisticated approaches to optimize its performance for workloads encountered in the expression resolution problem, and asymptotic analysis of each approach.276 This chapter presents the type environment data structure in Section~\ref{envdefnsec}, as well as some more sophisticated approaches to optimize performance for workloads encountered in the expression resolution problem in Section~\ref{envapproachessec}, and asymptotic analysis of each approach in Section~\ref{envanalysissec}. 271 277 Chapter~\ref{exprchap} provides experimental performance results for a representative set of these approaches. 272 278 One contribution of this thesis is the unionfind with classes data structure for efficient retrieval of unionfind class members, along with a related algorithm for reversing the history of $union$ operations in this data structure. … … 275 281 276 282 This persistent unionfind data structure is efficient, but not threadsafe; as suggested in Section~\ref{resnconclusionsec}, it may be valuable to parallelize the \CFA{} expression resolver. 277 However, allowing multiple threads concurrent access to the persistent data structure is likely to result in a sort of``reroot thrashing'', as different threads reroot the data structure to their own versions of interest.278 It is possible this could be mitigated by partitioning the data structure into separate subtrees for each thread, with each subtree having its own root node, and the boundaries betweenthem implemented with a lockequipped !ThreadBoundary! edit node.283 However, allowing multiple threads concurrent access to the persistent data structure is likely to result in ``reroot thrashing'', as different threads reroot the data structure to their own versions of interest. 284 This contention could be mitigated by partitioning the data structure into separate subtrees for each thread, with each subtree having its own root node, and the boundaries among them implemented with a lockequipped !ThreadBoundary! edit node.
Note: See TracChangeset
for help on using the changeset viewer.