Changeset eeb0767


Ignore:
Timestamp:
Oct 16, 2018, 7:22:39 PM (3 years ago)
Author:
Aaron Moss <a3moss@…>
Branches:
aaron-thesis, arm-eh, cleanup-dtors, deferred_resn, jacob/cs343-translation, jenkins-sandbox, master, new-ast, new-ast-unique-expr, no_list, persistent-indexer
Children:
57b0b1f
Parents:
7b61ce8
Message:

Add discussion of variants of environment data structures to thesis

Location:
doc
Files:
3 edited

Legend:

Unmodified
Added
Removed
  • doc/bibliography/pl.bib

    r7b61ce8 reeb0767  
    19411941}
    19421942
     1943@article{Galil91,
     1944  keywords = {union-find},
     1945  contributer = {a3moss@uwaterloo.ca},
     1946  title={Data structures and algorithms for disjoint set union problems},
     1947  author={Galil, Zvi and Italiano, Giuseppe F},
     1948  journal={ACM Computing Surveys (CSUR)},
     1949  volume={23},
     1950  number={3},
     1951  pages={319--344},
     1952  year={1991},
     1953  publisher={ACM}
     1954}
     1955
    19431956@article{Liskov75,
    19441957    keywords    = {abstract data types, encapsulation, verification},
     
    20782091    year        = {1998},
    20792092    pages       = {393-407},
     2093}
     2094
     2095@book{Aho74,
     2096  keywords = {algorithms, textbook, union-find},
     2097  contributer = {a3moss@uwaterloo.ca},
     2098  title = {The Design and Analysis of Computer Algorithms},
     2099  author = {Aho, Alfred V and Hopcroft, John E and Ullman, Jeffrey D},
     2100  year = {1974},
     2101  publisher = {Addison-Wesley},
     2102  address = {Reading, MA, USA}
    20802103}
    20812104
     
    28772900    month       = oct,
    28782901    year        = 1988,
    2879     pages       = {143-149}
     2902    pages       = {143--149}
     2903}
     2904
     2905@InProceedings{Patwary10,
     2906keywords = {union-find},
     2907contributer = {a3moss@uwaterloo.ca},
     2908author={Patwary, Md. Mostofa Ali and Blair, Jean and Manne, Fredrik},
     2909editor={Festa, Paola},
     2910title={Experiments on Union-Find Algorithms for the Disjoint-Set Data Structure},
     2911booktitle={Experimental Algorithms},
     2912year=2010,
     2913publisher={Springer Berlin Heidelberg},
     2914address={Berlin, Heidelberg},
     2915pages={411--423},
     2916isbn={978-3-642-13193-6}
    28802917}
    28812918
     
    35543591    publisher   = {ACM Press},
    35553592    address     = {New York, NY, USA},
     3593}
     3594
     3595@article{Galler64,
     3596  keywords={union-find, original},
     3597  contributer={a3moss@uwaterloo.ca},
     3598  title={An improved equivalence algorithm},
     3599  author={Galler, Bernard A and Fisher, Michael J},
     3600  journal={Communications of the ACM},
     3601  volume={7},
     3602  number={5},
     3603  pages={301--303},
     3604  year={1964},
     3605  publisher={ACM}
    35563606}
    35573607
     
    74767526}
    74777527
     7528@article{Tarjan84,
     7529 keywords = {union-find},
     7530 contributer = {a3moss@uwaterloo.ca},
     7531 author = {Tarjan, Robert E. and van Leeuwen, Jan},
     7532 title = {Worst-case Analysis of Set Union Algorithms},
     7533 journal = {J. ACM},
     7534 issue_date = {April 1984},
     7535 volume = {31},
     7536 number = {2},
     7537 month = mar,
     7538 year = {1984},
     7539 issn = {0004-5411},
     7540 pages = {245--281},
     7541 numpages = {37},
     7542 url = {http://doi.acm.org/10.1145/62.2160},
     7543 doi = {10.1145/62.2160},
     7544 acmid = {2160},
     7545 publisher = {ACM},
     7546 address = {New York, NY, USA},
     7547}
     7548
    74787549% X
    74797550
  • doc/theses/aaron_moss_PhD/phd/thesis.tex

    r7b61ce8 reeb0767  
    2323% \usepackage[pdftex]{graphicx} % For including graphics N.B. pdftex graphics driver
    2424\usepackage{graphicx}
     25
     26\usepackage{amsthm} % for theorem environment
     27\newtheorem{theorem}{Theorem}
    2528
    2629\usepackage{footmisc} % for double refs to the same footnote
  • doc/theses/aaron_moss_PhD/phd/type-environment.tex

    r7b61ce8 reeb0767  
    55As discussed in Chapter~\ref{resolution-chap}, 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.
    66Furthermore, expression resolution involves a search through many related possible solutions, so being able to re-use shared subsets of type environment data and to switch between environments quickly is desirable for performance.
    7 In this chapter I discuss and empirically compare a number of type environment data structure variants, including some novel variations on the union-find\cit{} data structure introduced in this thesis.
     7In this chapter I discuss and empirically compare a number of type environment data structure variants, including some novel variations on the union-find\cite{Galler64} data structure introduced in this thesis.
    88
    9 \section{Definitions}
     9\section{Definitions} \label{env-defn-sec}
    1010
    1111For purposes of this chapter, a \emph{type environment} $T$ is a set of \emph{type classes} $\myset{T_1, T_2, \cdots, T_{|T|}}$.
     
    4545$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.
    4646It 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 $unify_bound$ operation which may fail.
    48 In \CFACC{}, $unify_bound(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.
    49 If the bound types cannot be unified (\eg{} !struct A! with !int*!), then $unify_bound$ 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 result in a call to $unify_bound$ on !int! and the bound type of the class containing !R!.
     47$unify$ depends on an internal $unifyBound$ operation which may fail.
     48In \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.
     49If 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.
     50For 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 result in a call to $unifyBound$ on !int! and the bound type of the class containing !R!.
    5151As 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.
    5252
     
    5757The invalid state of $T$ on failure is not important, given that a combination failure will result in the resolution algorithm backtracking to a different environment.
    5858$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'$.
    59 Like for $unify$, $combine$ can always find a mutually-consistent division 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.
     59Like for $unify$, $combine$ can always find a mutually-consistent 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.
    6060
    6161Finally, the backtracking access patterns of the compiler can be exploited to reduce memory usage or runtime through use of an appropriately designed data structure.
    6262The 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 closely-related nodes as arguments to $combine$.
    6363As 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.
    64 These operations can be naively implemented by a deep copy of $T$ into $H$ and vice versa, but have more efficient implementations in persistency-aware data structures.
     64These operations can be naively implemented by a deep copy of $T$ into $H$ and vice versa, but have more efficient implementations in persistency-aware data structures.
     65
     66\section{Approaches}
     67
     68\subsection{Na\"{\i}ve}
     69
     70The type environment data structure used in Bilson's\cite{Bilson03} original implementation of \CFACC{} is a straightforward translation of the definitions in Section~\ref{env-defn-sec} to \CC{} code; a !TypeEnvironment! contains a list of !EqvClass! type equivalence classes, each of which contains the type bound information and a tree-based sorted set of type variables.
     71This 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{env-bounds-table}, does not support many of the desired operations with any particular efficiency.
     72Some variations on this structure may improve performance somewhat; for instance, replacing the !EqvClass! variable storage with a hash-based 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 remove the need to check each type class individually to maintain the disjointness property.
     73These improvements do not change the fundamental issues with this data structure, however.
     74
     75\subsection{Incremental Inheritance}
     76
     77One more invasive modification to this data structure which I investigated is to support swifter combinations of closely-related 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 which have been modified with respect to the parent.
     78This approach provides constant-time 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.
     79Since 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 re-using storage and reducing computation in many cases.
     80
     81For this environment I also employed a lazily-generated index of type variables to their containing class, which could be in either the current environment or an ancestor.
     82Any 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 that all local changes to the type environment are listed in its index.
     83However, not adding type variables to the index until lookup or mutation preserves the constant-time environment copy operation in the common case in which the copy is not mutated from its parent during its lifecycle.
     84
     85This 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'' base case is properly handled.
     86The 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.
     87These issues can be solved by ``flattening'' parent nodes into their children before the parents leave scope, but given the tree structure of the inheritance graph it is more straightforward to store the parent nodes in reference-counted or otherwise automatically garbage-collected heap storage.
     88
     89\subsection{Union-Find}
     90
     91Given the nature of the classes of type variables as disjoint sets, another natural approach to implementing a type environment is the union-find disjoint set data structure\cite{Galler64}.
     92Union-find 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.
     93The union-find 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.
     94$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.
     95$union$ involves making the representative of one set a child of the representative of the other, generally employing a rank- or size-based heuristic to ensure that the tree remains somewhat balanced.
     96If both path compression and a balancing heuristic are employed, both $union$ and $find$ run in amortized $O(\alpha(n))$ worst-case time; this bound by the inverse Ackermann function is a small constant for all practical values of $n$.
     97
     98The union-find $find$ and $union$ operations have obvious applicability to the $find$ and $unify$ type environment operations in Table~\ref{env-op-table}, but the union-find data structure must be augmented to fully implement the type environment operations.
     99In particular, the type class bound cannot be easily included in the union-find data structure, as the requirement to make it the class representative breaks the balancing properties of $union$, and requires too-close integration of the type environment $unifyBound$ internal operation.
     100This issue can be solved by including a side map from class representatives to the type class bound.
     101If 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 union-find data structure without a linear search for class representatives through all elements.
     102
     103\subsection{Union-Find with Classes}
     104
     105Another type environment operation not supported directly by the union-find data structure is $report$, which lists the type variables in a given class, and similarly $remove$, which removes a class and all its type variables from the environment.
     106Since the union-find data structure stores only links from children to parents and not vice-versa, 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.
     107The situation is even worse for the $remove$ operation, where a na\"{\i}ve removal of every element belonging to a specific class would likely remove some parents before their children, requiring either extra bookkeeping or passes through the data structure to remove the leaf elements of the class first.
     108Unfortunately, the literature\cite{Tarjan84,Galil91,Patwary10} on union-find 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.
     109
     110The core idea of this ``union-find with classes'' data structure and algorithm is to keep the members of each class stored in a circularly-linked list.
     111Rem's algorithm\cite{Dijkstra76}, dating from the 1970s, also includes a circularly-linked list data structure.
     112\TODO{Check this from source} However, Rem's algorithm has an entirely flat class hierarchy, where all elements were direct children of the representative, giving constant-time $find$ at the cost of linear-time $union$ operations.
     113In my version, the list data structure does not affect the layout of the union-find tree, maintaining the same asymptotic bounds as union-find.
     114In more detail, each element is given a !next! pointer to another element in the same class; this !next! pointer initially points to the element itself.
     115When two classes are unified, the !next! pointers of the representatives of those classes are swapped, splicing the two circularly-linked lists together.
     116Importantly, though this approach requires an extra pointer per element, it does maintain the linear space bound of union-find, and because it only requires updating the two root nodes in $union$ it does not asymptotically increase runtime either.
     117The basic approach is compatible with all path-compression techniques, and allows the members of any class to be retrieved in time linear in the size of the class simply by following the !next! pointers from any element.
     118
     119If the path-compression optimization is abandoned, union-find with classes also encodes a reversible history of all the $union$ operations applied to a given class.
     120Theorem~\ref{env-reverse-thm} demonstrates that the !next! pointer of the representative of a class always points to a leaf from the last-added subtree.
     121This property is sufficient to reverse the most-recent $union$ operation by finding the ancestor of that leaf that is an immediate child of the representative, breaking its parent link, and swapping the !next! pointers back\footnote{Union-by-size may be a more appropriate approach than union-by-rank in this instance, as adding two known sizes is a reversible operation, but the rank increment operation cannot be reliably reversed.}.
     122Once the $union$ operation has been reversed, Theorem~\ref{env-reverse-thm} still holds for the reduced class, and the process can be repeated recursively until the entire set is split into its component elements.
     123
     124\begin{theorem} \label{env-reverse-thm}
     125The !next! pointer of a class representative in the union-find with classes algorithm without path compression points to a leaf from the most-recently-added subtree.
     126\end{theorem}
     127
     128\begin{proof}
     129        By induction on the height of the tree. \\
     130        \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 most-recently-added (and only) leaf in the tree. \\
     131        \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 most-recently-added subtree $T'$ has a smaller height than $T$, thus by the inductive hypothesis before the most-recent $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.
     132\end{proof}
    65133
    66134% Future work: design multi-threaded version of C&F persistent map --- core idea is some sort of thread-boundary edit node
Note: See TracChangeset for help on using the changeset viewer.