<p>An optimising compiler typically applies some set of <a href="https://en.wikipedia.org/wiki/Rewriting" rel="noreferrer">rewrites</a> to some intermediate representation of the program, replacing terms with other terms which are supposed to be equivalent but more efficient. For example, <code>x * 8</code> may be rewritten as <code>x &lt;&lt; 3</code>, or <code>push x; push x</code> may be rewritten as <code>push x; dup</code>.</p>
<p>In the most general case, systems of rewrite rules may not terminate: for example, if somebody had the great idea to also rewrite <code>x &lt;&lt; 3</code> as <code>x * 8</code>, then the compiler itself would loop infinitely (or perhaps overflow the stack), applying the two rules back and forth forever. Intuitively, &quot;nobody would do that&quot;, because each rewrite rule should make the program &quot;more efficient&quot;, and a program can't be made infinitely &quot;more efficient&quot;, so there must reach a point at which no more rules can apply. That intuitive idea can in principle <a href="https://en.wikipedia.org/wiki/Loop_variant" rel="noreferrer">be made formal</a>, but actually formalising it seems difficult; you'd need some mathematical measure of &quot;how efficient&quot; a given term is, and then show that each rewrite rule always improves that measure. But there are many real optimisations which don't necessarily respect simple measures (e.g. number of instructions).</p>
<p>So my question is: how do implementors of optimising compilers ensure that the compiler itself will always terminate? Are formal proofs practical (if so, how is &quot;more efficient&quot; formalised in practice?), or are other techniques used?</p>
<p>I'm especially interested in answers about how large, complex compilers like GCC and LLVM handle this; but answers based on experience from developing any optimising compiler, or on research, are also welcome.</p>

<compilers><implementation><optimization>
How to ensure that an optimising compiler will terminate?
CC BY-SA 4.0
2023-08-26T03:02:23.403Z
A trivial fix would be to just keep a list of terms that have previously been considered, and check all proposed rewrites against this list.  The same way that graph search algorithms still manage to terminate even when the graph contains cycles.
Nate Eldredge
CC BY-SA 4.0
2023-08-26T10:38:26.237Z
@NateEldredge Some rewrite systems might allow for infinite chains ─ either by making the term larger, or if the individual terms themselves can have unbounded variations (e.g. literal values). Probably not very likely to happen by accident with an optimiser; there are some rewrites like $x \maptso x * 1` which might occasionally be needed to allow a different optimisation to be performed, but such rewrites normally wouldn't be included if the algorithm isn't designed to know what to do with them.
kaya3
CC BY-SA 4.0
2023-08-26T18:15:13.713Z
GCC and LLVM both internally have heuristic stopping points - give up if the function has >N variables, or you've done more than M rewrites, etc, etc. It's nowhere near perfect and can lead to rough edges where a minor tweak to a function suddenly causes it to be terribly optimized, but it tends to work reasonably well in practice.
TLW
CC BY-SA 4.0
2023-08-26T19:13:17.737Z
As a minor shift in the question, I'd point out that there are finite but still unacceptably expensive optimizations.  For instance, operations which take exponential time with respect to the length of the code are unacceptable (unless bounded with additional logic).
Cort Ammon
CC BY-SA 4.0
2023-08-26T19:23:23.363Z
@CortAmmon Sure, but it's generally easier to prove that an algorithm terminates than to prove it terminates within a certain number of steps as a function of the input size; and the latter is desirable for performance but the former is mandatory for correctness. To keep the question focused I'm interested in termination only.
kaya3
CC BY-SA 4.0
2023-08-29T20:26:26.713Z
Here's a fun bit of information: LLVM peephole optimizations like you describe _often do not terminate_! The ALIVE checker work identified some of these situations: https://ieeexplore.ieee.org/document/7886903
cody
CC BY-SA 4.0
2023-08-29T20:48:48.520Z
@cody Good find! Care to write up an answer about it? It looks like the paper directly addresses this question.
kaya3
CC BY-SA 4.0
2023-08-29T21:14:02.943Z
I actually don't have the reputation to answer this question, as it is "active", maybe @alexis-king can add something to their answer?
cody
CC BY-SA 4.0
2023-08-29T22:10:32.927Z
@cody Oh, whoops, I didn't realise you were prevented from answering. I've unprotected the question ─ it would be great to see your comment expanded into an answer, if you would like to write one.
kaya3
CC BY-SA 4.0
2024-03-12T08:39:01.053Z
'a program can't be made infinitely "more efficient"' - Some programs can! Blum's speedup theorem proves it, by constructing a sequence of programs which all compute the same function, but each one has arbitrarily-lower complexity than the previous; e.g. we can make the 2nd exponentially faster than the 1st, the 3rd exponentially faster than the 2nd, and so on *forever* :) https://en.wikipedia.org/wiki/Blum%27s_speedup_theorem
Warbo
CC BY-SA 4.0
2024-03-12T11:32:45.220Z
@Warbo That's the intuition at least. The intuition is more straightforwardly violated when a rewrite rule makes the program less efficient, which happens frequently in practice due to the difficulty of knowing what will really be faster on complex hardware. But anyway, if this intuition can be formalised (using cost models) then its proof relies on the costs being [well-ordered](https://en.wikipedia.org/wiki/Well-order). Blum's theorem works because the set of asymptotic complexity classes is not well-ordered.
kaya3
<p>A very simple method is to look at the size of the code that you are trying to optimise, calculating some constant N based on the size, and stopping the optimization after N transformations have been made. The disadvantage if you do this carelessly is that you might have transformations that produce incorrect code unless another transformation is also made. For example if a compiler detects that x and y are never used simultaneously then it might change all uses of y to uses of x. It deletes the variable y (resulting in invalid code) and now it must immediately change all uses of y to uses of x to be back with valid code. So the check for &gt;= N transformation can only be done when some primitive transformation is completed.</p>
<p>And I think you would make that value N large enough so that stopping optimisation because of it would be very rare, so rare that it is likely a bug in your compiler that produces a loop. The compiler <em>might</em> then want to produce a warning, asking you to send your code to the compiler developers so they can look for problems.</p>

CC BY-SA 4.0
2023-08-28T22:55:32.343Z
2023-09-02T16:48:26.977Z
2023-09-02T16:48:26.977Z
gnasher729
<h1>The roots of the problem: cost models, and monotonicity</h1>
<p>You're really getting at the heart of the problem when you say:</p>
<blockquote>
<p>each rewrite rule should make the program &quot;more efficient&quot;</p>
</blockquote>
<p>After all, why would you change the program in a way that makes it slower?  But there are two problems:</p>
<ol>
<li><p>Cost models: how can we tell if something is faster or slower?</p>
</li>
<li><p>Monotonicity: what if we need to make some changes that temporarily make the program slower, in order to eventually reach a global optimum?</p>
</li>
</ol>
<p>That's the conceptual framework.  Follows are some approaches for dealing with the problems in practice.  These are <em>complementary</em>, not conflicting.</p>
<h1>Timeouts</h1>
<p>This might seem like a cop-out—and if you would get stuck in a loop without it, it actually is.  But more broadly, optimisation is limited by a lack of computational resources, so, if appropriately designed, an optimiser should be able to make your code faster and faster the more time you give it (obviously with seriously diminishing returns); then, a timeout makes sense.  You can also imagine an iterative optimiser, which gives a passable result immediately, so the user gets immediate feedback, but then continues optimising further in the background.</p>
<p>Edit: <a href="https://langdev.stackexchange.com/a/2813/">another answer</a> draws a distinction between limiting wallclock time and limiting e.g. the number of rewrites performed.  These are both reasonable directions to go in, depending on broader goals.  In particular, going with the latter rather than the former provides a path to supporting reproducible builds; but the former can provide a more consistent user experience in contexts where that's not important.</p>
<h1>Canonicalisation</h1>
<p>One place these sorts of problems can start to creep in is due to redundancies in the ir—you mention x &lt;&lt; 3 vs x * 8.  But here's a question: is there really a need for the ir to support bitshifts?  Arguably, taking advantage of bitshifts is solely an <em>instruction selection</em> problem, but not relevant to program analysis.  So leave &lt;&lt; out of the ir entirely—make it so that you couldn't say x &lt;&lt; 3 even if you wanted to.</p>
<p>Similarly, simple algebraic properties like associativity and commutativity—is it a+b or b+a? a+(b+c) or (a+b)+c?—remove all question and represent + in your ir as a node with a variable number of dependencies that does not know which order they go in.  Similarly, don't represent subtraction; only addition and negation.</p>
<p>One more example: scheduling.  A traditional ir based on a basic-block control-flow-graph presumes a particular schedule—a particular instruction ordering—even though this information is not relevant for most optimisations prior to code generation.  The <em>sea of nodes</em> representation (some exposition <a href="https://darksi.de/d.sea-of-nodes/" rel="nofollow noreferrer">here</a> iirc) destroys some unnecessary information about scheduling and ordering.</p>
<h1>Abstract interpretation</h1>
<p>Abstract interpretation is an approach to optimisation which treats it as an analysis problem moreso than a transformation problem.  (Or, rather, abstract interpretation is an approach to analysis which works well for optimisation.)  For instance, rather than <em>replacing</em> 2+3 with the constant 5, you would simply annotate it with the fact that its value is 5.  Instead of removing dead code, you'd just mark it as dead.  A full treatment is out of scope, but casting optimisations as abstract interpretations rather than transformations has a number of advantages, including that termination proofs are generally not hard.  Recommended reading: <a href="https://scholarship.rice.edu/bitstream/handle/1911/96451/TR95-252.pdf" rel="nofollow noreferrer">combining analyses, combining optimisations</a>, particularly chapters 2 and 3.</p>
<h1>E-graphs</h1>
<p>E-graphs have come into vogue recently.  The basic idea of e-graphs is that the base nodes of the program ir, rather than simply being terms, will instead be <em>sets</em> of terms, which are all known to be equal.  So for instance, rather than <em>replacing</em> x*8 with x&lt;&lt;3, you'd <em>add</em> x&lt;&lt;3 to a set of equivalent terms: {x*8, x&lt;&lt;3}.  Then, at the end, once you've done all your optimisation, you <em>extract</em> some representative program, choosing one element from each set using some cost model.  (Edit: <a href="https://langdev.stackexchange.com/a/2817/">Alexis's answer</a> discusses these in more detail.)  This helps get around the problem of monotonicity by admitting rewrites that make the program slower—since the ir is <em>augmented</em> with the slow term, instead of having to <em>get rid</em> of the fast term to make a place for the slow term, it doesn't cause problems, and if it ultimately helps you get to a faster term, great.  May still have to be combined with a timeout.  Recommended reading: <a href="https://egraphs-good.github.io/" rel="nofollow noreferrer">https://egraphs-good.github.io/</a>, and papers and videos linked therefrom.</p>
<p>To give an example of some of the synergies here: we <em>could</em> handle commutativity and associativity purely at the level of e-graphs: have a set containing {a+b, b+a}.  But e-graphs have a tendency to grow very large, requiring a lot of computational resources (both space and time); so even if using e-graphs, it's a good idea to use the other approach I described for canonicalising associativity and commutativity, as that will increase the performance of the structure.</p>

CC BY-SA 4.0
2023-08-25T19:21:04.057Z
2024-07-27T06:07:08.233Z
2024-07-27T06:07:08.233Z
Moonchild
CC BY-SA 4.0
2023-08-26T18:10:58.163Z
Re `shl` versus `mul`: this kind of works, but the flipside of `lsr` versus `div` _doesn't_ for several reasons. First, `x lsr 2` != `x div 4` for negative values. Second, and admittedly this depends somewhat on your IR design, `x lsr y` typically produces _some_ value (may be `undef`) for all values of `y`, whereas `x div y` is often trapping for `y=0`. This impedes later optimizations, as you can speculate `x lsr y` in places where you can't speculate `x div y`. You can define that your IR treats `x div 0 == undef` - but that just pushes the problem to instruction selection time.
TLW
CC BY-SA 4.0
2023-08-26T18:12:38.747Z
It's a whole lot slower to have bunches and bunches of optimization passes calculate themselves if an input to a div is guaranteed to be a power of 2 (this is not so easy as it sounds, as said input may not be a _constant_ power of 2...), then it is to do it once and store it in the operation itself.
TLW
CC BY-SA 4.0
2023-08-26T18:38:46.303Z
(x >> 0) = (x div (2^0)) = (x div 1).  If 'lsr' means 'logical shift' (as opposed to arithmetic shift), I know of no language that admits the application of such an operation to negative values.  (If the issue is rounding, rightshift is a flooring division, which it makes sense to support generally.)  I don't know why it would be necessary to 'have bunches and bunches of optimization passes calculate themselves if an input to a div is guaranteed to be a power of 2'.
Moonchild
CC BY-SA 4.0
2023-08-26T20:42:44.503Z
The issue is not rounding. The issue is: if I see `x lsr y`, I know in isolation I can speculate it safely, where as if I see `x div y` I do _not_ know I can speculate it safely without having to infer more about y.
TLW
CC BY-SA 4.0
2023-08-26T20:45:32.567Z
"I don't know why it would be necessary to 'have bunches and bunches of optimization passes calculate themselves if an input to a div is guaranteed to be a power of 2'. " -> there are many optimizations that can be applied to bitshifts that cannot be applied to general divisions/multiplications (for instance, `popcnt(a lsr b) <= popcnt(a)`). Which means that if you are saying "don't have lsr in your IR at all; just use div" said optimizations have to figure out 'is this div actually a bitshift'.
TLW
CC BY-SA 4.0
2023-08-26T20:47:02.880Z
And if you're not very careful what happens is you end up doing _redundant_ calculations of "is this div actually a bitshift" all over the place... so you end up looking at it and going "this is doing redundant work, let's cache this"... and the most convenient way to cache the knowledge of "this div is actually a shift" is by, well, having a shift opcode.
TLW
CC BY-SA 4.0
2023-08-26T21:56:45.827Z
Wouldn't you like to be able to speculate _all_ divisions where the denominator is known to be nonzero?

In general, it is useful to have analysis frameworks which can produce facts about terms—including, perhaps, that one is a power of two.  And such a fact is useful generally, not just for this application.  And I did mention that there are advantages to casting these problems as analyses rather than transformations.

I do think that canonically transforming into right-shifts where possible would be harmless in most contexts, but I also don't think it would be particularly advantageous.
Moonchild
CC BY-SA 4.0
2023-08-27T20:41:45.300Z
@Moonchild: In Java, `-1>>>16` is 0xFFFF, as is `-1L >>> 48`.
supercat
CC BY-SA 4.0
2023-08-27T20:50:04.050Z
The "sea of nodes" notion doesn't seem to fit with the fact that it's possible for two values to be matching in numerical terms, but not be semantically interchangeable.  For example, given `extern int arr[]; int *p;` within a statement controlled by `if (arr+4 == p)` could process machine code that accesses `*p` so that it uses the static address `arr+4`, but only if it refrains from making assumptions about whether such accesses might affect objects that might immeiately follow `arr`, but niethr clang nor gcc properly preserves that distinction.
supercat
CC BY-SA 4.0
2023-08-27T22:05:05.063Z
Good point about java.  I would implement that internally as conversion to unsigned followed by plain shift.  I'm not sure what point you're trying to make about sea of nodes; we work all the time with equivalence relations which are weaker than operational equality (for example, floating-point =—if you assume there are no nans—does not distinguish +0 from -0); this has nothing to do with the compiler ir.
Moonchild
CC BY-SA 4.0
2023-08-28T21:41:16.363Z
@Moonchild: Both clang and gcc seem to have difficulty recognizing situations where two values compare equal, or would be known to have identical machine-level representations, are not not semantically equivalent, e.g. because they have different sequencing implications.  If the Effective Type Rule is interpreted as allowing the ET of storage to be usefully changed by writing the storage using the new type, for example, a function that reads a storage location using type T1, and then uses type T2 to write a value with the same bit pattern, any preceding reads using T1 should be...
supercat
CC BY-SA 4.0
2023-08-28T21:43:26.847Z
...sequenced before any following reads using type T2, but neither clang nor gcc is able to honor that sequencing relationship.  Even if one writes a value with a different bit pattern between the aforementioned read using T1 and write using T2, clang and gcc will decide that since the value written will be overwritten, they can optimize out that extra assignment.
supercat
CC BY-SA 4.0
2023-08-28T21:51:42.407Z
I understand your complaints about gcc and clang.  I just don't see what that has to do with sea of nodes.
Moonchild
CC BY-SA 4.0
2023-08-31T16:18:25.530Z
@Moonchild: Most situations where consolidating accesses made via certain lvalues might affect program behavior could be easily identified by examining the code between those accesses.  I don't think a sea of nodes can very  well record the fact that certain chains of accesses must remain in ordered with respect to the operations therein, but may be freely reordered with respect to other operations.
supercat
CC BY-SA 4.0
2023-08-31T19:40:38.217Z
@supercat Sea of nodes expresses ordering dependencies with explicit edges.  This allows it to eliminate _unnecessary_ ordering dependencies, but if some ordering relationships are necessary to preserve the program semantics, there is no reason they cannot be expressed.
Moonchild
CC BY-SA 4.0
2023-08-31T20:07:40.677Z
@Moonchild: If a sea of nodes would contain sufficient information to allow compilers like clang and gcc to interleave two sequences of operations while retaining sequencing within each sequence, what would those compilers be gaining by unsound consolidation of operations?
supercat
<p>The <a href="https://langdev.stackexchange.com/a/2813">existing answer</a> is good and representative of the techniques currently used in most optimizing compilers. I’d like to add to that by mentioning <a href="https://rosstate.org/publications/eqsat/" rel="noreferrer">equality saturation</a>, a newer technique that seems quite promising.</p>
<p>The key idea behind equality saturation is to generalize the representation of expressions to represent the <a href="https://en.wikipedia.org/wiki/Fixed_point_(mathematics)" rel="noreferrer">fixed point</a> of applying a collection of rewritings. Given the example of <code>x &lt;&lt; 3</code> versus <code>x * 8</code> from your question, an approach based on equality saturation would transform both expressions to a form that represents <em>both versions at the same time</em>. That is, the result of rewriting the term would be a sort of “superposition” of both <code>x &lt;&lt; 3</code> and <code>x * 8</code>.</p>
<p>By repeatedly applying rewritings to these “expression superpositions”, an optimizer can theoretically eventually produce a result that simultaneously represents all possible rewritings, and this is known as “saturation”. Since this represents the union of all possible rewritings, it is <em>canonical</em>, and there is no need to “bounce between” two different representations. After saturation been performed, a final code generation pass can transform the “expression superposition” into a concrete expression by using heuristics that attempt to select the best representation out of the set of known possibilities.</p>
<p>One immediate question is how to represent these “expression superpositions”. Though it would theoretically be possible to represent them directly as a set containing every version of the term, this would be prohibitively expensive due to the combinatorial explosion of potential rewritings. For that reason, equality saturation represents these superposition terms as <em>graphs</em> that permit sharing between possibilities with common structure. Since these graphs represent a set of equivalent terms, they are known as <em>e-graphs</em>.</p>
<p>Unfortunately, use of e-graphs alone does not fully mitigate the practical challenges of equality saturation. Some rewritings are difficult to efficiently encode into the e-graph structure, and some analyses are difficult to perform. The 2020 paper <a href="https://arxiv.org/pdf/2004.03082.pdf" rel="noreferrer"><code>egg</code>: Fast and Extensible Equality Saturation</a> presents a more comprehensive design for practical application of equality saturation, <a href="https://docs.rs/egg/latest/egg/" rel="noreferrer">realized in Rust as the <code>egg</code> library</a>.</p>
<p>Equality saturation is a young technique under active research, so it remains to be seen to what extent it will supplant traditional, more ad-hoc rewriting techniques. Nevertheless, <code>egg</code> is the most immediately practical realization of the idea to date, and is already being applied in serious compiler projects like <a href="https://github.com/bytecodealliance/wasmtime/tree/main/cranelift" rel="noreferrer">cranelift</a>. Its principled approach provides many conceptual and practical simplifications, so I’d certainly call it an approach worth considering for any new optimizer.</p>

CC BY-SA 4.0
2023-08-25T19:41:01.167Z
2023-08-25T19:41:01.167Z
Alexis King
CC BY-SA 4.0
2023-08-25T22:28:47.240Z
"My code is being optimized by a quantum optimizer utilizing superpositions of nodes" :P
Seggan
CC BY-SA 4.0
2023-08-26T18:16:37.713Z
How does this handle rewrites that can be applied infinitely? E.g. `x -> x+0 -> x+0+0 -> ...`
TLW
CC BY-SA 4.0
2023-08-26T18:27:10.120Z
@TLW There's a nice talk on `egg` that goes into that [here](https://www.youtube.com/watch?v=6cJMI9z2TeU). Specifically, the speaker talks about how something like that is handled at [this timestamp](https://youtu.be/6cJMI9z2TeU?t=510) (though you might need to watch the beginning to fully understand that part). The brief answer is that such things are represented by cycles between e-classes of the e-graph.
David Young
CC BY-SA 4.0
2023-08-26T20:41:19.727Z
I guess my confusion lies in the following: Post tag machines are Turing-complete, and so finding the step at which an arbitrary Post tag machine has the shortest queue depth would imply solving the Halting problem - and yet it seems as though you could reduce a Post tag machine to an instance of compiler optimization via rewrite rules.
TLW
CC BY-SA 4.0
2023-08-26T21:03:31.943Z
@TLW IIRC, the loop in the equality saturation algorithm is not guaranteed to halt and they use a timeout. I think it can always detect simple cycles like that one, though (assuming the term size doesn't cause it to time out).
David Young
<p>All that I've seen work with rule application limits, i.e. you give up after a certain number of steps. If you know how these limits work, you sometimes can create examples for programs that have an effective infinite execution time, but they work in practice.
The same holds by the way for template applications.</p>
<p>In theory, one could imagine timeouts, but I haven't seen it in practice and would advise against it for a lot of reasons.</p>
<p>The idea with the measure will not work in practice because lots of algorithms have provably no measure that could be used. I'd expect that this statement is also true for templates.
Besides, you'd have the practical problem that it would be outright complex to define a measure that works for a combination of transformations that are done together.</p>

CC BY-SA 4.0
2023-08-25T18:40:38.900Z
2023-08-25T18:40:38.900Z
feldentm
CC BY-SA 4.0
2023-08-27T15:14:24.377Z
An interesting take on timeouts: the Rust compiler, as of 1.72, no longer limits the duration of compile-time expression evaluations, thereby allowing arbitrarily long computations at compile-time. _Instead_, after a certain time as elapsed, it will emit a warning that the computation is taking a long time, and then continue emitting those warnings with an exponential back-off, leaving it up to the user to interrupt when they are out of patience.
Matthieu M.
CC BY-SA 4.0
2023-08-28T18:32:00.950Z
How do you integrate such an approach into fully automated builds? The good thing about application limits in contrast to timeouts is that they are independent of a system's hardware or current load. Also, from my experience, they are good at detecting infinite application loops in cases, where small numbers should be reasonable.
feldentm
CC BY-SA 4.0
2023-08-28T19:27:22.143Z
The problem about limits (aka "fuel") is that they can be so arbitrary. As you mentioned a minute change -- including upgrading the compiler -- and suddenly what was enough isn't... and trying to figure out the limit is always a pain. The warnings, instead, are just that - warnings. They do not trigger the termination of the build. Now, do mind that Rust 1.72 is fresh off the press (released a few days ago). Still, my expectation is that the intent is that a _human_ will, during the course of development, judge the compile-time worth it; and CI will just run the computation until completion.
Matthieu M.
<p>Modern compilers don't have a clear separation between register allocation, code generation and peephole optimization anymore, because these things feed into each other.</p>
<p>For example, when you have complex addressing modes available that calculate a table access by bit-shifting an index register and adding the result to a base address register, and the data is accessed twice, there is a trade-off between calculating the address once and assigning it to a register, and calculating it twice.</p>
<p>If you want to find the optimal representation, you need to generate two different register allocations and see which one generates the fastest/shortest/... code. This depends on what else is inside the same function -- if many values are live, then repeating the calculation will win, as it saves the space and memory accesses for spilling a register, but if there are only few registers used, then using one to get a shorter representation and faster execution time for the accesses will be the better choice.</p>
<p>It doesn't stop there -- with modern CPUs disliking branches as much as they do, it is often beneficial to merge basic blocks, speculatively execute a branch and discard its result if it turns out the branch was not taken. This, of course, feeds back into the number of registers that are live at that point.</p>
<p>The solution here is to either have good heuristics on which representation will likely produce a good outcome and accept that it will not be optimal, or to present later stages with multiple alternatives, but in general decisions that have been taken are not revisited later except for a few that are obvious (for example, the assembler choosing a shorter encoding for a branch based on distance).</p>

CC BY-SA 4.0
2023-08-28T04:31:42.900Z
2023-08-28T04:31:42.900Z
Simon Richter
<p>As requested, I'm going to do my best to summarize the <a href="https://ieeexplore.ieee.org/document/7886903" rel="noreferrer">Termination-Checking for LLVM Peephole Optimizations</a> paper, by Menendez and Nagarakatte.</p>
<p>The reality of compiler optimization staging is that it is a bit messy. Each pass or individual &quot;peephole&quot; optimization (so-called because they perform a local transformation on low-level code without much regard for context) usually improves performance, but the order in which they are run may affect effectiveness or termination. This order is usually determined by hand, based on messy heuristics.</p>
<p>Clang/LLVM peephole passes are typically run until saturation, that is a set of rules of the form <span class="math-container">$\text{source fragment pattern} \rightarrow \text{target fragment pattern}$</span> are repeatedly run until no rule applies. This requires preventing the exact situation from the original question, where a rewrite <span class="math-container">$a\rightarrow b$</span> occurs, and then another rule performs <span class="math-container">$b\rightarrow a$</span>, which enables the first one to fire again, etc.</p>
<p>Things can be more subtle, where many rules have to interact to produce such non-termination. Typically this is avoided by the human having a notional concept of why a transformation is not &quot;undone&quot; by other transformations, or having <strong>side conditions</strong> on the applications of rules, e.g. <span class="math-container">$\%x \ll 3 \rightarrow \%x*8$</span> only if <span class="math-container">$\%x$</span> contains a <em>signed</em> integer and the converse only in the unsigned case (this is just notional, I don't actually know what the conditions are here).</p>
<p>Predictably, humans get this wrong, and the paper gives some examples of this occurring in the wild, with an example not much more complex than the shift one.</p>
<p>Ideally, one would &quot;just&quot; check mechanically termination of the combination of rules. There are many termination checking algorithms out there for such tasks (there's even a <a href="https://termination-portal.org/wiki/Termination_Competition" rel="noreferrer">competition</a>!), but this is a difficult task, and algorithms do not tend to scale well or handle bit-vectors easily, so the authors propose detecting <strong>non-termination</strong> at the cost of missing a few potential termination bugs.</p>
<p>They do this by trying to detect <strong>looping</strong>:</p>
<ol>
<li>Try to &quot;guess&quot; a sequence of abstract rules <span class="math-container">$a\rightarrow b \rightarrow \ldots\rightarrow a$</span></li>
<li>Check whether this sequence is <em>feasible</em>, that is if the patterns can concretely be realized into an input program <span class="math-container">$a'$</span> which triggers these rewrites.</li>
</ol>
<p>It's obvious that given rule <span class="math-container">$a\rightarrow b$</span> and <span class="math-container">$c\rightarrow d$</span>, <span class="math-container">$b$</span> looks <em>nothing alike</em> <span class="math-container">$c$</span>, (e.g. <span class="math-container">$b$</span> is <span class="math-container">$\mathtt{nand}\ X\ Y$</span>  and <span class="math-container">$c$</span> is <span class="math-container">$X\ +\ Y$</span>) then the rules cannot fire in succession, so these &quot;mismatches&quot; are pruned eagerly.</p>
<p>Then the more &quot;semantic&quot; conditions are checked, e.g. <span class="math-container">$C_2 = C_1\ \&amp;\ C_2$</span> as in the paper example, which is easily seen to be satisfiable (take <span class="math-container">$C_2$</span> to be all zeroes, say).</p>
<p>I'll skip some additional details about how such loops are checked to be feasible, but the conclusion is that this approach <em>did</em> find a bunch of looping optimization sequences (184 of them!) within their tool, called <a href="https://github.com/AliveToolkit/alive2" rel="noreferrer">alive2</a>.</p>
<p>So what next? I imagine that these loops, if correctly identified (bugs in the alive2 tool are possible, and there is a manual step of translating the actual C++ optimization code to the alive2 optimization DSL) are being fixed by hand. I'd guess (complete speculation) that this is usually done by adding more conditions to avoid firing a rule in such a way that the loop is feasible, rather than removing or dramatically modifying rules. Generally mature systems are (correctly!) reluctant to make large changes. The paper doesn't say.</p>
<p>It would be an exciting challenge to see if termination tools can be actually put to task here. I think the main obstruction is expressing the side conditions, and the general user-friendliness of termination analysis, which is quite a bit behind that of SMT solvers, for instance.</p>

CC BY-SA 4.0
2023-08-30T16:12:09.893Z
2023-08-30T16:38:21.230Z
2023-08-30T16:38:21.230Z
cody
# How to ensure that an optimising compiler will terminate?
Posted by: username_0 on 2023-08-25
An optimising compiler typically applies some set of [rewrites](https://en.wikipedia.org/wiki/Rewriting) to some intermediate representation of the program, replacing terms with other terms which are supposed to be equivalent but more efficient. For example, `x * 8` may be rewritten as `x << 3`, or `push x; push x` may be rewritten as `push x; dup`.

In the most general case, systems of rewrite rules may not terminate: for example, if somebody had the great idea to also rewrite `x << 3` as `x * 8`, then the compiler itself would loop infinitely (or perhaps overflow the stack), applying the two rules back and forth forever. Intuitively, "nobody would do that", because each rewrite rule should make the program "more efficient", and a program can't be made infinitely "more efficient", so there must reach a point at which no more rules can apply. That intuitive idea can in principle [be made formal](https://en.wikipedia.org/wiki/Loop_variant), but actually formalising it seems difficult; you'd need some mathematical measure of "how efficient" a given term is, and then show that each rewrite rule always improves that measure. But there are many real optimisations which don't necessarily respect simple measures (e.g. number of instructions).

So my question is: how do implementors of optimising compilers ensure that the compiler itself will always terminate? Are formal proofs practical (if so, how is "more efficient" formalised in practice?), or are other techniques used?

I'm especially interested in answers about how large, complex compilers like GCC and LLVM handle this; but answers based on experience from developing any optimising compiler, or on research, are also welcome.
**Tags:** compilers implementation optimization
> **Comments:**
> **username_1**: A trivial fix would be to just keep a list of terms that have previously been considered, and check all proposed rewrites against this list.  The same way that graph search algorithms still manage to terminate even when the graph contains cycles.  
> **username_0**: @NateEldredge Some rewrite systems might allow for infinite chains ─ either by making the term larger, or if the individual terms themselves can have unbounded variations (e.g. literal values). Probably not very likely to happen by accident with an optimiser; there are some rewrites like $x \maptso x * 1` which might occasionally be needed to allow a different optimisation to be performed, but such rewrites normally wouldn't be included if the algorithm isn't designed to know what to do with them.  
> **username_2**: GCC and LLVM both internally have heuristic stopping points - give up if the function has >N variables, or you've done more than M rewrites, etc, etc. It's nowhere near perfect and can lead to rough edges where a minor tweak to a function suddenly causes it to be terribly optimized, but it tends to work reasonably well in practice.  
> **username_3**: As a minor shift in the question, I'd point out that there are finite but still unacceptably expensive optimizations.  For instance, operations which take exponential time with respect to the length of the code are unacceptable (unless bounded with additional logic).  
> **username_0**: @CortAmmon Sure, but it's generally easier to prove that an algorithm terminates than to prove it terminates within a certain number of steps as a function of the input size; and the latter is desirable for performance but the former is mandatory for correctness. To keep the question focused I'm interested in termination only.  
> **username_4**: Here's a fun bit of information: LLVM peephole optimizations like you describe _often do not terminate_! The ALIVE checker work identified some of these situations: https://ieeexplore.ieee.org/document/7886903  
> **username_0**: @cody Good find! Care to write up an answer about it? It looks like the paper directly addresses this question.  
> **username_4**: I actually don't have the reputation to answer this question, as it is "active", maybe @alexis-king can add something to their answer?  
> **username_0**: @cody Oh, whoops, I didn't realise you were prevented from answering. I've unprotected the question ─ it would be great to see your comment expanded into an answer, if you would like to write one.  
> **username_5**: 'a program can't be made infinitely "more efficient"' - Some programs can! Blum's speedup theorem proves it, by constructing a sequence of programs which all compute the same function, but each one has arbitrarily-lower complexity than the previous; e.g. we can make the 2nd exponentially faster than the 1st, the 3rd exponentially faster than the 2nd, and so on *forever* :) https://en.wikipedia.org/wiki/Blum%27s_speedup_theorem  
> **username_0**: @Warbo That's the intuition at least. The intuition is more straightforwardly violated when a rewrite rule makes the program less efficient, which happens frequently in practice due to the difficulty of knowing what will really be faster on complex hardware. But anyway, if this intuition can be formalised (using cost models) then its proof relies on the costs being [well-ordered](https://en.wikipedia.org/wiki/Well-order). Blum's theorem works because the set of asymptotic complexity classes is not well-ordered.  
---
## 6 answers
### Answer by username_7 on 2023-08-25. Score: 35 | Accepted answer
# The roots of the problem: cost models, and monotonicity

You're really getting at the heart of the problem when you say:

> each rewrite rule should make the program "more efficient"

After all, why would you change the program in a way that makes it slower? But there are two problems:

1. Cost models: how can we tell if something is faster or slower?
2. Monotonicity: what if we need to make some changes that temporarily make the program slower, in order to eventually reach a global optimum?

That's the conceptual framework. Follows are some approaches for dealing with the problems in practice. These are *complementary*, not conflicting.

# Timeouts

This might seem like a cop-out—and if you would get stuck in a loop without it, it actually is. But more broadly, optimisation is limited by a lack of computational resources, so, if appropriately designed, an optimiser should be able to make your code faster and faster the more time you give it (obviously with seriously diminishing returns); then, a timeout makes sense. You can also imagine an iterative optimiser, which gives a passable result immediately, so the user gets immediate feedback, but then continues optimising further in the background.

Edit: [another answer](https://langdev.stackexchange.com/a/2813/) draws a distinction between limiting wallclock time and limiting e.g. the number of rewrites performed. These are both reasonable directions to go in, depending on broader goals. In particular, going with the latter rather than the former provides a path to supporting reproducible builds; but the former can provide a more consistent user experience in contexts where that's not important.

# Canonicalisation

One place these sorts of problems can start to creep in is due to redundancies in the ir—you mention x << 3 vs x \* 8. But here's a question: is there really a need for the ir to support bitshifts? Arguably, taking advantage of bitshifts is solely an *instruction selection* problem, but not relevant to program analysis. So leave << out of the ir entirely—make it so that you couldn't say x << 3 even if you wanted to.

Similarly, simple algebraic properties like associativity and commutativity—is it a+b or b+a? a+(b+c) or (a+b)+c?—remove all question and represent + in your ir as a node with a variable number of dependencies that does not know which order they go in. Similarly, don't represent subtraction; only addition and negation.

One more example: scheduling. A traditional ir based on a basic-block control-flow-graph presumes a particular schedule—a particular instruction ordering—even though this information is not relevant for most optimisations prior to code generation. The *sea of nodes* representation (some exposition [here](https://darksi.de/d.sea-of-nodes/) iirc) destroys some unnecessary information about scheduling and ordering.

# Abstract interpretation

Abstract interpretation is an approach to optimisation which treats it as an analysis problem moreso than a transformation problem. (Or, rather, abstract interpretation is an approach to analysis which works well for optimisation.) For instance, rather than *replacing* 2+3 with the constant 5, you would simply annotate it with the fact that its value is 5. Instead of removing dead code, you'd just mark it as dead. A full treatment is out of scope, but casting optimisations as abstract interpretations rather than transformations has a number of advantages, including that termination proofs are generally not hard. Recommended reading: [combining analyses, combining optimisations](https://scholarship.rice.edu/bitstream/handle/1911/96451/TR95-252.pdf), particularly chapters 2 and 3.

# E-graphs

E-graphs have come into vogue recently. The basic idea of e-graphs is that the base nodes of the program ir, rather than simply being terms, will instead be *sets* of terms, which are all known to be equal. So for instance, rather than *replacing* x\*8 with x<<3, you'd *add* x<<3 to a set of equivalent terms: {x\*8, x<<3}. Then, at the end, once you've done all your optimisation, you *extract* some representative program, choosing one element from each set using some cost model. (Edit: [Alexis's answer](https://langdev.stackexchange.com/a/2817/) discusses these in more detail.) This helps get around the problem of monotonicity by admitting rewrites that make the program slower—since the ir is *augmented* with the slow term, instead of having to *get rid* of the fast term to make a place for the slow term, it doesn't cause problems, and if it ultimately helps you get to a faster term, great. May still have to be combined with a timeout. Recommended reading: <https://egraphs-good.github.io/>, and papers and videos linked therefrom.

To give an example of some of the synergies here: we *could* handle commutativity and associativity purely at the level of e-graphs: have a set containing {a+b, b+a}. But e-graphs have a tendency to grow very large, requiring a lot of computational resources (both space and time); so even if using e-graphs, it's a good idea to use the other approach I described for canonicalising associativity and commutativity, as that will increase the performance of the structure.
> **Comments:**
> **username_2** (2023-08-26): Re `shl` versus `mul`: this kind of works, but the flipside of `lsr` versus `div` _doesn't_ for several reasons. First, `x lsr 2` != `x div 4` for negative values. Second, and admittedly this depends somewhat on your IR design, `x lsr y` typically produces _some_ value (may be `undef`) for all values of `y`, whereas `x div y` is often trapping for `y=0`. This impedes later optimizations, as you can speculate `x lsr y` in places where you can't speculate `x div y`. You can define that your IR treats `x div 0 == undef` - but that just pushes the problem to instruction selection time.  
> **username_2** (2023-08-26): It's a whole lot slower to have bunches and bunches of optimization passes calculate themselves if an input to a div is guaranteed to be a power of 2 (this is not so easy as it sounds, as said input may not be a _constant_ power of 2...), then it is to do it once and store it in the operation itself.  
> **username_7** (2023-08-26): (x >> 0) = (x div (2^0)) = (x div 1).  If 'lsr' means 'logical shift' (as opposed to arithmetic shift), I know of no language that admits the application of such an operation to negative values.  (If the issue is rounding, rightshift is a flooring division, which it makes sense to support generally.)  I don't know why it would be necessary to 'have bunches and bunches of optimization passes calculate themselves if an input to a div is guaranteed to be a power of 2'.  
> **username_2** (2023-08-26): The issue is not rounding. The issue is: if I see `x lsr y`, I know in isolation I can speculate it safely, where as if I see `x div y` I do _not_ know I can speculate it safely without having to infer more about y.  
> **username_2** (2023-08-26): "I don't know why it would be necessary to 'have bunches and bunches of optimization passes calculate themselves if an input to a div is guaranteed to be a power of 2'. " -> there are many optimizations that can be applied to bitshifts that cannot be applied to general divisions/multiplications (for instance, `popcnt(a lsr b) <= popcnt(a)`). Which means that if you are saying "don't have lsr in your IR at all; just use div" said optimizations have to figure out 'is this div actually a bitshift'.  
> **username_2** (2023-08-26): And if you're not very careful what happens is you end up doing _redundant_ calculations of "is this div actually a bitshift" all over the place... so you end up looking at it and going "this is doing redundant work, let's cache this"... and the most convenient way to cache the knowledge of "this div is actually a shift" is by, well, having a shift opcode.  
> **username_7** (2023-08-26): Wouldn't you like to be able to speculate _all_ divisions where the denominator is known to be nonzero?

In general, it is useful to have analysis frameworks which can produce facts about terms—including, perhaps, that one is a power of two.  And such a fact is useful generally, not just for this application.  And I did mention that there are advantages to casting these problems as analyses rather than transformations.

I do think that canonically transforming into right-shifts where possible would be harmless in most contexts, but I also don't think it would be particularly advantageous.  
> **username_8** (2023-08-27): @Moonchild: In Java, `-1>>>16` is 0xFFFF, as is `-1L >>> 48`.  
> **username_8** (2023-08-27): The "sea of nodes" notion doesn't seem to fit with the fact that it's possible for two values to be matching in numerical terms, but not be semantically interchangeable.  For example, given `extern int arr[]; int *p;` within a statement controlled by `if (arr+4 == p)` could process machine code that accesses `*p` so that it uses the static address `arr+4`, but only if it refrains from making assumptions about whether such accesses might affect objects that might immeiately follow `arr`, but niethr clang nor gcc properly preserves that distinction.  
> **username_7** (2023-08-27): Good point about java.  I would implement that internally as conversion to unsigned followed by plain shift.  I'm not sure what point you're trying to make about sea of nodes; we work all the time with equivalence relations which are weaker than operational equality (for example, floating-point =—if you assume there are no nans—does not distinguish +0 from -0); this has nothing to do with the compiler ir.  
> **username_8** (2023-08-28): @Moonchild: Both clang and gcc seem to have difficulty recognizing situations where two values compare equal, or would be known to have identical machine-level representations, are not not semantically equivalent, e.g. because they have different sequencing implications.  If the Effective Type Rule is interpreted as allowing the ET of storage to be usefully changed by writing the storage using the new type, for example, a function that reads a storage location using type T1, and then uses type T2 to write a value with the same bit pattern, any preceding reads using T1 should be...  
> **username_8** (2023-08-28): ...sequenced before any following reads using type T2, but neither clang nor gcc is able to honor that sequencing relationship.  Even if one writes a value with a different bit pattern between the aforementioned read using T1 and write using T2, clang and gcc will decide that since the value written will be overwritten, they can optimize out that extra assignment.  
> **username_7** (2023-08-28): I understand your complaints about gcc and clang.  I just don't see what that has to do with sea of nodes.  
> **username_8** (2023-08-31): @Moonchild: Most situations where consolidating accesses made via certain lvalues might affect program behavior could be easily identified by examining the code between those accesses.  I don't think a sea of nodes can very  well record the fact that certain chains of accesses must remain in ordered with respect to the operations therein, but may be freely reordered with respect to other operations.  
> **username_7** (2023-08-31): @supercat Sea of nodes expresses ordering dependencies with explicit edges.  This allows it to eliminate _unnecessary_ ordering dependencies, but if some ordering relationships are necessary to preserve the program semantics, there is no reason they cannot be expressed.  
> **username_8** (2023-08-31): @Moonchild: If a sea of nodes would contain sufficient information to allow compilers like clang and gcc to interleave two sequences of operations while retaining sequencing within each sequence, what would those compilers be gaining by unsound consolidation of operations?  
---
### Answer by username_9 on 2023-08-25. Score: 22
The [existing answer](https://langdev.stackexchange.com/a/2813) is good and representative of the techniques currently used in most optimizing compilers. I’d like to add to that by mentioning [equality saturation](https://rosstate.org/publications/eqsat/), a newer technique that seems quite promising.

The key idea behind equality saturation is to generalize the representation of expressions to represent the [fixed point](https://en.wikipedia.org/wiki/Fixed_point_(mathematics)) of applying a collection of rewritings. Given the example of `x << 3` versus `x * 8` from your question, an approach based on equality saturation would transform both expressions to a form that represents *both versions at the same time*. That is, the result of rewriting the term would be a sort of “superposition” of both `x << 3` and `x * 8`.

By repeatedly applying rewritings to these “expression superpositions”, an optimizer can theoretically eventually produce a result that simultaneously represents all possible rewritings, and this is known as “saturation”. Since this represents the union of all possible rewritings, it is *canonical*, and there is no need to “bounce between” two different representations. After saturation been performed, a final code generation pass can transform the “expression superposition” into a concrete expression by using heuristics that attempt to select the best representation out of the set of known possibilities.

One immediate question is how to represent these “expression superpositions”. Though it would theoretically be possible to represent them directly as a set containing every version of the term, this would be prohibitively expensive due to the combinatorial explosion of potential rewritings. For that reason, equality saturation represents these superposition terms as *graphs* that permit sharing between possibilities with common structure. Since these graphs represent a set of equivalent terms, they are known as *e-graphs*.

Unfortunately, use of e-graphs alone does not fully mitigate the practical challenges of equality saturation. Some rewritings are difficult to efficiently encode into the e-graph structure, and some analyses are difficult to perform. The 2020 paper [`egg`: Fast and Extensible Equality Saturation](https://arxiv.org/pdf/2004.03082.pdf) presents a more comprehensive design for practical application of equality saturation, [realized in Rust as the `egg` library](https://docs.rs/egg/latest/egg/).

Equality saturation is a young technique under active research, so it remains to be seen to what extent it will supplant traditional, more ad-hoc rewriting techniques. Nevertheless, `egg` is the most immediately practical realization of the idea to date, and is already being applied in serious compiler projects like [cranelift](https://github.com/bytecodealliance/wasmtime/tree/main/cranelift). Its principled approach provides many conceptual and practical simplifications, so I’d certainly call it an approach worth considering for any new optimizer.
> **Comments:**
> **username_10** (2023-08-25): "My code is being optimized by a quantum optimizer utilizing superpositions of nodes" :P  
> **username_2** (2023-08-26): How does this handle rewrites that can be applied infinitely? E.g. `x -> x+0 -> x+0+0 -> ...`  
> **username_11** (2023-08-26): @TLW There's a nice talk on `egg` that goes into that [here](https://www.youtube.com/watch?v=6cJMI9z2TeU). Specifically, the speaker talks about how something like that is handled at [this timestamp](https://youtu.be/6cJMI9z2TeU?t=510) (though you might need to watch the beginning to fully understand that part). The brief answer is that such things are represented by cycles between e-classes of the e-graph.  
> **username_2** (2023-08-26): I guess my confusion lies in the following: Post tag machines are Turing-complete, and so finding the step at which an arbitrary Post tag machine has the shortest queue depth would imply solving the Halting problem - and yet it seems as though you could reduce a Post tag machine to an instance of compiler optimization via rewrite rules.  
> **username_11** (2023-08-26): @TLW IIRC, the loop in the equality saturation algorithm is not guaranteed to halt and they use a timeout. I think it can always detect simple cycles like that one, though (assuming the term size doesn't cause it to time out).  
---
### Answer by username_4 on 2023-08-30. Score: 8
As requested, I'm going to do my best to summarize the [Termination-Checking for LLVM Peephole Optimizations](https://ieeexplore.ieee.org/document/7886903) paper, by Menendez and Nagarakatte.

The reality of compiler optimization staging is that it is a bit messy. Each pass or individual "peephole" optimization (so-called because they perform a local transformation on low-level code without much regard for context) usually improves performance, but the order in which they are run may affect effectiveness or termination. This order is usually determined by hand, based on messy heuristics.

Clang/LLVM peephole passes are typically run until saturation, that is a set of rules of the form $\text{source fragment pattern} \rightarrow \text{target fragment pattern}$ are repeatedly run until no rule applies. This requires preventing the exact situation from the original question, where a rewrite $a\rightarrow b$ occurs, and then another rule performs $b\rightarrow a$, which enables the first one to fire again, etc.

Things can be more subtle, where many rules have to interact to produce such non-termination. Typically this is avoided by the human having a notional concept of why a transformation is not "undone" by other transformations, or having **side conditions** on the applications of rules, e.g. $\%x \ll 3 \rightarrow \%x\*8$ only if $\%x$ contains a *signed* integer and the converse only in the unsigned case (this is just notional, I don't actually know what the conditions are here).

Predictably, humans get this wrong, and the paper gives some examples of this occurring in the wild, with an example not much more complex than the shift one.

Ideally, one would "just" check mechanically termination of the combination of rules. There are many termination checking algorithms out there for such tasks (there's even a [competition](https://termination-portal.org/wiki/Termination_Competition)!), but this is a difficult task, and algorithms do not tend to scale well or handle bit-vectors easily, so the authors propose detecting **non-termination** at the cost of missing a few potential termination bugs.

They do this by trying to detect **looping**:

1. Try to "guess" a sequence of abstract rules $a\rightarrow b \rightarrow \ldots\rightarrow a$
2. Check whether this sequence is *feasible*, that is if the patterns can concretely be realized into an input program $a'$ which triggers these rewrites.

It's obvious that given rule $a\rightarrow b$ and $c\rightarrow d$, $b$ looks *nothing alike* $c$, (e.g. $b$ is $\mathtt{nand}\ X\ Y$ and $c$ is $X\ +\ Y$) then the rules cannot fire in succession, so these "mismatches" are pruned eagerly.

Then the more "semantic" conditions are checked, e.g. $C\_2 = C\_1\ \&\ C\_2$ as in the paper example, which is easily seen to be satisfiable (take $C\_2$ to be all zeroes, say).

I'll skip some additional details about how such loops are checked to be feasible, but the conclusion is that this approach *did* find a bunch of looping optimization sequences (184 of them!) within their tool, called [alive2](https://github.com/AliveToolkit/alive2).

So what next? I imagine that these loops, if correctly identified (bugs in the alive2 tool are possible, and there is a manual step of translating the actual C++ optimization code to the alive2 optimization DSL) are being fixed by hand. I'd guess (complete speculation) that this is usually done by adding more conditions to avoid firing a rule in such a way that the loop is feasible, rather than removing or dramatically modifying rules. Generally mature systems are (correctly!) reluctant to make large changes. The paper doesn't say.

It would be an exciting challenge to see if termination tools can be actually put to task here. I think the main obstruction is expressing the side conditions, and the general user-friendliness of termination analysis, which is quite a bit behind that of SMT solvers, for instance.
---
### Answer by username_12 on 2023-08-25. Score: 7
All that I've seen work with rule application limits, i.e. you give up after a certain number of steps. If you know how these limits work, you sometimes can create examples for programs that have an effective infinite execution time, but they work in practice.
The same holds by the way for template applications.

In theory, one could imagine timeouts, but I haven't seen it in practice and would advise against it for a lot of reasons.

The idea with the measure will not work in practice because lots of algorithms have provably no measure that could be used. I'd expect that this statement is also true for templates.
Besides, you'd have the practical problem that it would be outright complex to define a measure that works for a combination of transformations that are done together.
> **Comments:**
> **username_13** (2023-08-27): An interesting take on timeouts: the Rust compiler, as of 1.72, no longer limits the duration of compile-time expression evaluations, thereby allowing arbitrarily long computations at compile-time. _Instead_, after a certain time as elapsed, it will emit a warning that the computation is taking a long time, and then continue emitting those warnings with an exponential back-off, leaving it up to the user to interrupt when they are out of patience.  
> **username_12** (2023-08-28): How do you integrate such an approach into fully automated builds? The good thing about application limits in contrast to timeouts is that they are independent of a system's hardware or current load. Also, from my experience, they are good at detecting infinite application loops in cases, where small numbers should be reasonable.  
> **username_13** (2023-08-28): The problem about limits (aka "fuel") is that they can be so arbitrary. As you mentioned a minute change -- including upgrading the compiler -- and suddenly what was enough isn't... and trying to figure out the limit is always a pain. The warnings, instead, are just that - warnings. They do not trigger the termination of the build. Now, do mind that Rust 1.72 is fresh off the press (released a few days ago). Still, my expectation is that the intent is that a _human_ will, during the course of development, judge the compile-time worth it; and CI will just run the computation until completion.  
---
### Answer by username_14 on 2023-08-28. Score: 4
Modern compilers don't have a clear separation between register allocation, code generation and peephole optimization anymore, because these things feed into each other.

For example, when you have complex addressing modes available that calculate a table access by bit-shifting an index register and adding the result to a base address register, and the data is accessed twice, there is a trade-off between calculating the address once and assigning it to a register, and calculating it twice.

If you want to find the optimal representation, you need to generate two different register allocations and see which one generates the fastest/shortest/... code. This depends on what else is inside the same function -- if many values are live, then repeating the calculation will win, as it saves the space and memory accesses for spilling a register, but if there are only few registers used, then using one to get a shorter representation and faster execution time for the accesses will be the better choice.

It doesn't stop there -- with modern CPUs disliking branches as much as they do, it is often beneficial to merge basic blocks, speculatively execute a branch and discard its result if it turns out the branch was not taken. This, of course, feeds back into the number of registers that are live at that point.

The solution here is to either have good heuristics on which representation will likely produce a good outcome and accept that it will not be optimal, or to present later stages with multiple alternatives, but in general decisions that have been taken are not revisited later except for a few that are obvious (for example, the assembler choosing a shorter encoding for a branch based on distance).
---
### Answer by username_6 on 2023-08-28. Score: 1
A very simple method is to look at the size of the code that you are trying to optimise, calculating some constant N based on the size, and stopping the optimization after N transformations have been made. The disadvantage if you do this carelessly is that you might have transformations that produce incorrect code unless another transformation is also made. For example if a compiler detects that x and y are never used simultaneously then it might change all uses of y to uses of x. It deletes the variable y (resulting in invalid code) and now it must immediately change all uses of y to uses of x to be back with valid code. So the check for >= N transformation can only be done when some primitive transformation is completed.

And I think you would make that value N large enough so that stopping optimisation because of it would be very rare, so rare that it is likely a bug in your compiler that produces a loop. The compiler *might* then want to produce a warning, asking you to send your code to the compiler developers so they can look for problems.
---
