AfterMath

11 April 2016

Producing Wrong Data Without Doing Anything Obviously Wrong!

Authors: Mytkowicz, Diwan, Hauswirth, Sweeney
Conference: ASPLOS’09

Imagine you are working on a compiler optimization and benchmarking shows that it is effective: you obtain a nice speedup on a standard benchmark suite. However, your colleague, using another user account on the same machine with a seemingly identical setup, measures the opposite effect: a slowdown of the same magnitude as your purported speedup. Could this happen? If yes, why? This paper looks at the notion of measurement bias by which seemingly innocuous features of the environment can greatly effect the results of the experimental evaluation of a system.

26 March 2016

Liquid Types

Authors: Rondon, Kawaguchi, Jhala
Conference: PLDI 2008

Functional programming languages provide type systems that ensure invariants on programs at compile-time. To obtain even finer properties captured by types, several authors have proposed to adopt dependent types as a way to improve expressivity of type systems. Unfortunately, type inference needs considerable programmers’ guidance by means of type annotations. Liquid types provide an exciting compromise.

20 March 2016

Equality Saturation: a New Approach to Optimization

Authors: Tate, Stepp, Tatlock, Lerner
Conference: POPL 2009

A common challenge in optimizing compilers is the phase ordering problem: in which order should different optimizations be applied? The problematic issue is that applying one optimization may change the program such that some other, potentially more profitable, optimization can no longer be performed. Equality saturation is a clever idea for getting around the phase ordering problem. As an interesting side effect, an optimizer based on equality saturation can also be used for translation validation of other optimizers.

17 March 2016

Example-Directed Synthesis: a Type-Theoretic Interpretation

Authors: Frankle, Osera, Walker, Zdancewic
Conference: POPL 2016

This is a very interesting paper about a cool and rather hot topic: program synthesis. Since the paper has been accepted at POPL 2016, one expects a theoretical investigation of the subject. As the title of the paper suggests, it is indeed the case. A surprise comes from a quite detailed explanation on the implementation challenges the authors have faced in developing a prototype.

16 March 2016

The Brioche Manifesto

This is a kind of a revolution. This is something I dreamed about since the beginning of my graduate studies.