algorithm.tex 12.2 KB
 Michael Banken committed Oct 16, 2017 1 \chapter{Algorithm}  Michael Banken committed Jun 11, 2018 2   Michael Banken committed Oct 16, 2017 3 \section{Idea}  Michael Banken committed Jun 11, 2018 4 5 6 7 8 9 10 11 12 13 14 15 Since our approach to identifying candidates is large based on set theory, the algorithms for finding are also making heavy use of set operations, using essentially the same construction method for creating the set of optimization candidates as the definitions presented in \autoref{chap:candidates}. \subsection{Graph Optimization} Optimization of the theory graph happens one theory at a time, beginning at the outer most edges of the theory graphs, i.e. those theories that are not included by any other theory. It may seem counter intuitive, since we are changing the theories before modifying the theories they depend upon, however our use of future lite code (see \autoref{sec:futurelite}) means that any change that might affect the outer theories should be discarded anyway, as it may be a desired part of the theory, even if it is not referenced in the theory itself, resulting in no effective gain for resolving inner theories first. This is not true for the other direction, as removing unnecessary inclusions may significantly reduce the amount of dependencies that might limit our pruning of the inner theories. As a result of these observations, it is a strictly better option to always prioritize outer theories and since the runtime will already will already be dominating the time needed for a sort, we can do so with little additional cost (see \autoref{sec:runtime}). \subsection{Theory Optimization}  Michael Banken committed Jun 12, 2018 16 Optimization of a theory itself happens in two separate passes. The first pass detects and eliminates superfluous inclusions. The second pass cleans up any remaining simply redundant inclusions.  Michael Banken committed Jun 11, 2018 17 18 19  The reason for separating these passes is to avoid the removal of simply redundant inclusions, that will later have to be reinserted when eliminating a partially superfluous inclusion. An example for such a hazard is the example of an overlap between the two types of candidates in \autoref{fig:redundantoverlap}  Michael Banken committed Jun 12, 2018 20 21 \subsubsection{First pass - Eliminating superfluous inclusions}  Michael Banken committed Jun 14, 2018 22 23 24 In the first pass we first take a selection of optimization candidates, namely those theories that are directly included, but not used in the current theory. These are the theories that need to be replaced. The algorithm then computes all the necessary replacements by looking at all indirect inclusions that result from the inclusion to be replaced. The necessary replacements are those that are used by the theory or its future and are not already included by the theory or by one of its necessary dependencies.  Michael Banken committed Jun 12, 2018 25 26 27  For this algorithm it is not necessary to make a distinction between purely and partially superfluous inclusions, as the pure case is entirely subsumed by the partial case with an empty set of necessary inclusions.  Michael Banken committed Jun 14, 2018 28 29 30 31 32 33 34 35 36 As we discussed in \autoref{sec:puresivia} this pass cannot be expected to remove all the inclusions that are unneeded for retaining a valid graph, but what we do expect it to leave a valid graph valid. Proof sketch: \begin{itemize} \item Any theory used by the current theory or its future is either directly included by the current theory or indirectly. \item Any directly included theory that is necessary isn't a candidate and will therefore remain. \item Any indirectly included theory is either included by a theory that is retained or by one that is being replaced. Since the replacement of a theory inclusion is the necessary subset of its included theories, all necessary dependencies will remain included. \end{itemize}  Michael Banken committed Jun 12, 2018 37 38 \subsubsection{Second pass - Eliminating simply redundant inclusions}  Michael Banken committed Jun 14, 2018 39 The idea behind the second pass is to collect all those theories that are included indirectly by the current theory and throwing away all of those direct inclusions that are part of this set. This will leave us exactly with those inclusions that are not simply redundant, without changing the flattened theory graph.  Michael Banken committed Jun 12, 2018 40   Michael Banken committed Jun 14, 2018 41 42 43 Proof sketch: \begin{itemize} \item Simply redundant inclusions are those, that are both directly and indirectly included.  Michael Banken committed Jun 12, 2018 44 We get rid of those direct inclusions that are also indirect, so clearly all simply redundant inclusions must be gone.  Michael Banken committed Jun 14, 2018 45 46 47 48 \item For the invariance of the flattened theory graph, we must first assume that theories are partially ordered by inclusion and inclusion paths are of finite depth, ie. that cyclic inclusions are not present.\\ If we do so, all indirect inclusions must ultimately be the result of a direct inclusion, so all relevant direct inclusions are still in the set.\\ If these assumptions are wrong however, not only could we run into problems, but we will inevitably do so if the current theory is part of the cycle. It is therefore best to only perform this operation on a graph that satisfies our assumption. \end{itemize}  Michael Banken committed Jun 12, 2018 49   Michael Banken committed Jun 11, 2018 50 51 52 53 \subsection{Future Lite Code} \label{sec:futurelite} In \autoref{sec:viability} we already mentioned the problem of future lite code. The obvious method for aquiring the future lite code is traversing the entire theory graph and whenever we find a theory inclusion, we make a note for the included theory that the theory we are currently traversing is part of its future code. Unfortunately this requires traversing the graph in its entirety.  Michael Banken committed Jun 14, 2018 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 105 106 107 108 109 110 For the actual algorithm we skip this part and instead put create a map of used theories in the future code, since this is the part we actually require. Since this means potentially going over every theory for every theory (or at least reasonably close to it), our worst case runtime for this part of the algorithm is quadratic in the number of theories in the graph. This runtime is especially problematic, since we need to update the the information after every step of the optimization to make proper use of any improvements of the graph. We can demonstrate this by considering the following example. \begin{figure}[h] \begin{tikzpicture}[node distance=2cm]\footnotesize \node[thy] (bottom) {\begin{tabular}{l} \textsf{bottom}\\\hline X\\\hline ... \end{tabular}}; \node[thy, above of = bottom] (middle) {\begin{tabular}{l} \textsf{middle}\\\hline Y\\\hline not X \end{tabular}}; \node[thy, above of = middle] (top) {\begin{tabular}{l} \textsf{top}\\\hline ...\\\hline X, but not Y \end{tabular}}; \draw[include] (bottom) -- (middle); \draw[include] (middle) -- (top); \end{tikzpicture} \caption{Example of a graph where optimizing changes the future.} \label{fig:changeablefuture} \end{figure} As we can immediately see in \autoref{fig:changeablefuture}, it is possible to replace the partially superfluous inclusion of middle in top with bottom. The result is the changed graph in \autoref{fig:changedfuture}. \begin{figure}[h] \begin{tikzpicture}[node distance=2cm]\footnotesize \node[thy] (bottom) {\begin{tabular}{l} \textsf{bottom}\\\hline X\\\hline ... \end{tabular}}; \node[thy, above of = bottom] (middle) {\begin{tabular}{l} \textsf{middle}\\\hline Y\\\hline not X \end{tabular}}; \node[thy, above of = middle] (top) {\begin{tabular}{l} \textsf{top}\\\hline ...\\\hline X, but not Y \end{tabular}}; \draw[include] (bottom) -- (middle); \draw[include, bend left] (bottom) edge (top); \end{tikzpicture} \caption{Example of a graph where optimizing changes the future.} \label{fig:changedfuture} \end{figure} In the changed graph we can now optimize the purely superfluous inclusion of bottom in the theory middle. We could not have done this in the earlier graph, since X and therefore bottom was used in middle's future. Thus we need an updated version of the future to make full use of earlier optimizations. To somewhat mitigate the effect this has on the performance, the future is created step by step, as we work our way from the outer edges of the graph towards the core.  Michael Banken committed Jun 11, 2018 111   Michael Banken committed Oct 16, 2017 112 \section{Pseudo Code}  Michael Banken committed Jun 12, 2018 113 114 115  \subsection{Optimizing graph}  Michael Banken committed Jun 14, 2018 116 The following code applies the optimizations to the entire theory graph.  Michael Banken committed Jun 11, 2018 117 118  \begin{algorithm}[H]  Michael Banken committed Jun 12, 2018 119 120 121 \label{alg:graph} \KwData{theoryGraph = theory graph to be optimized} \KwResult{replacements = map from theories to maps of theory inclusions to their replacement}  Michael Banken committed Jun 11, 2018 122  \Begin{  Michael Banken committed Jun 12, 2018 123 124 125 126 127 128 129 130 131 132 133 134  futureUses := empty map\; replacements := empty map\; theoryGraph := sort(theoryGraph)\; theoryGraphRev := reverse(theoryGraph)\; \For{theory $\leftarrow$ theoryGraph}{ add include $\rightarrow$ usedTheories(theory) $\cup$ futureUses(theory) to futureUses\; add theory $\rightarrow$ optimize(theory, futureUses(theory)) to replacements\; \For{include $\leftarrow$ includes(theory)}{ replace include $\rightarrow$ futureUses(include)$\cup$usedTheories(include)$\cup$futureUses(theory) in futureUses\; } \KwRet replacements \; }  Michael Banken committed Jun 11, 2018 135  }  Michael Banken committed Jun 12, 2018 136  \caption{optimizeGraph(theorygraph)}  Michael Banken committed Jun 11, 2018 137 138 \end{algorithm}  Michael Banken committed Jun 12, 2018 139 \subsection{Optimizing theory}  Michael Banken committed Jun 11, 2018 140   Michael Banken committed Jun 14, 2018 141 The following pseudo code applies optimizations to a given theory.  Michael Banken committed Jun 11, 2018 142   Michael Banken committed Jun 12, 2018 143 144 145 146 147 148 149 150 151 152 153 154 155 156 \begin{algorithm}[H] \KwData{theory = theory from our theory graph\\ futureUse = set of theories used by theories including $theory$ in future lite code\\ pass changes that were already applied to the graph} \KwResult{replacements = map from theory inclusions to their replacement} \Begin{ replacements = superfluousIncludes(theory, futureUse)\; \For{removal $\leftarrow$ redundantIncludes(theory, futureUse)}{ add removal $\rightarrow$ $\emptyset$ to replacements\; } \KwRet replacements\; } \caption{optimize(theory, futureUse)} \end{algorithm}  Michael Banken committed Jun 11, 2018 157 158 159 160 161 162 163 164 165 166 167 168 169 170 171 172 173 174 175 176 177 178 179 180 181 182 183  \subsection{Finding superfluous inclusions} \label{sec:alg_si} The following pseudo code is for finding superfluous inclusions (see: \autoref{sec:superinc}). \begin{algorithm}[H] \KwData{theory = theory from our theory graph\\ futureUse = set of theories used by theories including $theory$ in future lite code\\ pass changes that were already applied to the graph} \KwResult{replacements = map from theory inclusions to their replacement} \Begin{ replacements := empty map\; futureUsedTheories := usedTheories(theory) $\cup$ futureUse\; candidates := DirectInludes(theory) $\setminus$ futureUsedTheories\; \For{candidate $\leftarrow$ candidates}{ neededCandidateIncludes := Includes(candidate) $\cap$ futureUsedTheories \; remainingIncludes := Includes((directIncludes(theory) $\cap$ futureUsedTheories))$\cup$ (directIncludes(theory) $\cap$ futureUsedTheories) \; neededCandidateIncludes := neededCandidateIncludes $\setminus$ remainingIncludes\; add candidate $\rightarrow$ neededCandidateIncludes to replacements\; } \KwRet superfluousIncludes\; \caption{superfluousIncludes(theory, futureUse)} } \end{algorithm} Note that in \autoref{sec:superinc} we made a destinction between purely and partially superfluous inclusions. However we do not need to make this distinction while searching for them, as we can search for them by using the criteria for generally superfluous inclusion. Since they only differ in the set of inclusions that needs to be retained and we write that set in our result anyway, both can be accomplished by the same routine.  Michael Banken committed Jun 12, 2018 184 185 186 \subsection{Finding simply redundant inclusions} \label{sec:alg_sri} The following pseudo code is for finding simply redundant inclusions (see: \autoref{sec:redinc}).  Michael Banken committed Jun 11, 2018 187 188  \begin{algorithm}[H]  Michael Banken committed Jun 12, 2018 189  \KwData{$theory$ = theory from our theory graph\\  Michael Banken committed Jun 11, 2018 190  pass changes that were already applied to the graph}  Michael Banken committed Jun 12, 2018 191  \KwResult{$redundantIncludes$ = set of simply redundant inclusions}  Michael Banken committed Jun 11, 2018 192  \Begin{  Michael Banken committed Jun 12, 2018 193 194 195 196  $subIncludes := \emptyset$\ $redundantIncludes := \emptyset$\; \For{$i \leftarrow directIncludes(theory)$}{ $subIncludes := subIncludes \cup includes(i)$\;  Michael Banken committed Jun 11, 2018 197  }  Michael Banken committed Jun 12, 2018 198 199 200 201 202 203 204 205  \For{$i \leftarrow directIncludes(theory)$}{ \If{$i \in subIncludes$} { $redundantIncludes := redundantIncludes \cup \{i\}$\; } } \KwRet $redundantIncludes$\; } \caption{simplyRedundantIncludes(theory, futureUse)}  Michael Banken committed Jun 11, 2018 206 207 \end{algorithm}  Michael Banken committed Oct 16, 2017 208 209 \section{Complexity analysis} \subsection{Runtime}  Michael Banken committed Jun 11, 2018 210 \label{sec:runtime}  Michael Banken committed Jun 14, 2018 211 212   Michael Banken committed Jun 11, 2018 213 \subsection{Memory}