<p>I'm not sure how novel it is, or if it's too much on the applied side for your interest, but <a href="http://lambda-the-ultimate.org/node/3557">Hoopl</a> shows how a control/data flow optimization can be modularised, with propagation of facts about control-graph vertices being independent of the language and specific optimization.</p>

<p>They reference a 2002 algorithm of Lerner, Grove and Chambers which composes simple optimizations into a "superoptimization".</p>

CC BY-SA 3.0
2011-04-22T17:49:56.293Z
2011-04-22T17:49:56.293Z
Max
<p>I suppose the <a href="http://cseweb.ucsd.edu/~ztatlock/eqsat/">Equality Saturation</a> technique, as a different approach to the problem of optimization passes ordering, would be relevant. To my knowledge, it has however not yet been proved practical by a concrete implementation in a full-fledged compiler. The following <a href="http://cseweb.ucsd.edu/~lerner/papers/popl10.html">Generating Compiler Optimizations from Proofs</a> may also be of interest.</p>

CC BY-SA 4.0
2021-10-26T18:02:25.047Z
A decade later: The [egg](https://egraphs-good.github.io/) library is a concrete implementation which is quite fast, and my [Cammy](https://esolangs.org/wiki/Cammy) language has a reference compiler which uses it for optimizations.
Corbin
CC BY-SA 3.0
2011-05-06T21:45:59.617Z
2011-05-06T21:45:59.617Z
gasche
<p>There has been a bit of a revival in verified optimizing compilers. In addition to Lerner's paper (mentioned in a previous comment), you might look at the <a href="http://compcert.inria.fr/index.html" rel="nofollow">CompCert</a> project led by Xavier Leroy. They've done some cool stuff with specifying optimizations as machine-checkable proofs (using <strong>Coq</strong>). I haven't yet read the papers, but The <a href="http://www.cs.princeton.edu/~appel/VST/" rel="nofollow">Verified Software Toolchain</a> project at Princeton also seems to be producing interesting results in this area. </p>

CC BY-SA 3.0
2011-12-01T17:21:45.070Z
We are also working on a project similar to CompCert: CerCo (http://cerco.cs.unibo.it/).  Unlike CompCert, we aim to produce a verified concrete cost preserving compiler for a large subset of C (CompCert only shows that extensional properties of the source program are preserved by compilation).  We are also implementing in the compiler a few moderately complex loop optimizations, as well as "mild" optimizations like CompCert employs, which will of course need verifying as being cost-preserving.
Dominic Mulligan
CC BY-SA 3.0
2011-12-01T16:35:58.470Z
2011-12-05T09:19:35.073Z
2011-12-05T09:19:35.073Z
John Lasseter
<p>Recognizing that baz[i] += force(foo[i],foo[j]) in a double FOR loop has independent results for (i,j) and reordering the calls into a space filling curve on (i,j) to cut down on cache misses.  </p>

<p>Not quite "peephole" but getting cache oblivious behavior for "free" is nice. </p>

CC BY-SA 3.0
2011-05-06T21:55:44.187Z
2011-11-30T19:45:41.537Z
2011-11-30T19:45:41.537Z
Chad Brewbaker
<p>I'm interested in optimization of data flow and control flow graphs and in particular more computationally complex.
But it will also be interesting to know about the latest inventions in the field of peephole optimizations.</p>

CC BY-SA 3.0
2011-12-01T21:16:53.850Z
In my [thesis](http://cafxx.strayorange.com/app/cv/addendum/thesis/ferraris_compiler_optimizations_call_graph_flattening.pdf) ([slides](http://cafxx.strayorange.com/app/cv/addendum/thesis/ferraris_compiler_optimizations_call_graph_flattening.pptx)) I have discussed and implemented call-graph flattening in LLVM; basically it's an interprocedural transformation that gets rid of the notion of "function" because it merges all code together, allowing a bunch of interesting possibilities such as interprocedural code motion, callsite-optimized calling conventions, stackless execution and so on.
CAFxX
CC BY-SA 3.0
2012-01-05T16:07:34.370Z
@CAFxX: slides crashed Open Office .. do you happen to have online pictures instead?
Yttrill
CC BY-SA 3.0
2012-01-05T17:48:30.867Z
@Yttrill: http://www.slideshare.net/CAFxX/compiler-optimizations-based-on-callgraph-flattening
CAFxX
CC BY-SA 3.0
2012-01-09T14:10:27.397Z
Thanks, able to view with that, although the graphs were to fine to be visible the text was good.
Yttrill
<optimization><compilers>
What's new in compiler optimization techniques over last few years?
Evgeny Gavrin
# What's new in compiler optimization techniques over last few years?

(Asked by: username_0 on 2011-04-22)

I'm interested in optimization of data flow and control flow graphs and in particular more computationally complex.
But it will also be interesting to know about the latest inventions in the field of peephole optimizations.

**Tags:** optimization, compilers
> **Comments:**
> **username_1**: In my [thesis](http://cafxx.strayorange.com/app/cv/addendum/thesis/ferraris_compiler_optimizations_call_graph_flattening.pdf) ([slides](http://cafxx.strayorange.com/app/cv/addendum/thesis/ferraris_compiler_optimizations_call_graph_flattening.pptx)) I have discussed and implemented call-graph flattening in LLVM; basically it's an interprocedural transformation that gets rid of the notion of "function" because it merges all code together, allowing a bunch of interesting possibilities such as interprocedural code motion, callsite-optimized calling conventions, stackless execution and so on.  
> **username_2**: @CAFxX: slides crashed Open Office .. do you happen to have online pictures instead?  
> **username_1**: @Yttrill: http://www.slideshare.net/CAFxX/compiler-optimizations-based-on-callgraph-flattening  
> **username_2**: Thanks, able to view with that, although the graphs were to fine to be visible the text was good.  

---

## 4 answers

### Answer by username_3 on 2011-04-22. Score: 8 | Accepted answer

I'm not sure how novel it is, or if it's too much on the applied side for your interest, but [Hoopl](http://lambda-the-ultimate.org/node/3557) shows how a control/data flow optimization can be modularised, with propagation of facts about control-graph vertices being independent of the language and specific optimization.

They reference a 2002 algorithm of Lerner, Grove and Chambers which composes simple optimizations into a "superoptimization".


---

### Answer by username_4 on 2011-05-06. Score: 8

I suppose the [Equality Saturation](http://cseweb.ucsd.edu/~ztatlock/eqsat/) technique, as a different approach to the problem of optimization passes ordering, would be relevant. To my knowledge, it has however not yet been proved practical by a concrete implementation in a full-fledged compiler. The following [Generating Compiler Optimizations from Proofs](http://cseweb.ucsd.edu/~lerner/papers/popl10.html) may also be of interest.

> **Comments:**
> **username_5**: A decade later: The [egg](https://egraphs-good.github.io/) library is a concrete implementation which is quite fast, and my [Cammy](https://esolangs.org/wiki/Cammy) language has a reference compiler which uses it for optimizations.  

---

### Answer by username_6 on 2011-12-01. Score: 6

There has been a bit of a revival in verified optimizing compilers. In addition to Lerner's paper (mentioned in a previous comment), you might look at the [CompCert](http://compcert.inria.fr/index.html) project led by Xavier Leroy. They've done some cool stuff with specifying optimizations as machine-checkable proofs (using **Coq**). I haven't yet read the papers, but The [Verified Software Toolchain](http://www.cs.princeton.edu/~appel/VST/) project at Princeton also seems to be producing interesting results in this area.

> **Comments:**
> **username_7**: We are also working on a project similar to CompCert: CerCo (http://cerco.cs.unibo.it/).  Unlike CompCert, we aim to produce a verified concrete cost preserving compiler for a large subset of C (CompCert only shows that extensional properties of the source program are preserved by compilation).  We are also implementing in the compiler a few moderately complex loop optimizations, as well as "mild" optimizations like CompCert employs, which will of course need verifying as being cost-preserving.  

---

### Answer by username_8 on 2011-05-06. Score: 5

Recognizing that baz[i] += force(foo[i],foo[j]) in a double FOR loop has independent results for (i,j) and reordering the calls into a space filling curve on (i,j) to cut down on cache misses.

Not quite "peephole" but getting cache oblivious behavior for "free" is nice.


---

