Senior Submission
There are two compiler universes. In universe Σ\SigmaΣ, they statically analyze code. Its optimizers are theorem provers, that apply equivalence preserving transformations to speed up computation. Many small hints about the structure of data and computation are provided by the programmer to that end. On the other hand, in universe Ω\OmegaΩ programs are hard to analyze statically. Here, optimizers are anthropologists; they observe the program behavior and optimize for its predicted future. One universe bases its optimizations on facts, the other one on predictions, or even fictions. What, if they are not that different after all? Non-refutable facts are hard to come by, even in universe Σ\SigmaΣ. And from Ω\OmegaΩ we learn, that it can be very efficient to rely on fictions – as long as they are not refuted.
We propose to search for ways of integrating those two worlds. We argue that, with the proper accounting, predictions and assumptions can be used for optimizations; just like facts. Such a compiler uses optimizations which are correct ``up to some context of assumptions''. By controlling the scope of assumptions, and tracking their dependencies, target code comes with a description of a particular execution context, under which it is correct.
Wed 18 JulDisplayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change
13:30 - 15:24 | |||
14:00 25mDoctoral symposium paper | Optimization based on Facts and Fiction Doc Symposium Olivier Flückiger Northeastern University, USA File Attached | ||
14:25 16mDoctoral symposium paper | Two-phase Analysis for Precision and Scalability Doc Symposium Anastasios Antoniadis University of Athens, Greece File Attached | ||
14:41 16mDoctoral symposium paper | Transparent Static Analysis for the Detection of Security Vulnerabilities Doc Symposium Goran Piskachev Fraunhofer IEM File Attached | ||
14:57 16mDoctoral symposium paper | Improving Symbolic Flat Memory Models with Pointer Alias Analysis Doc Symposium Timotej Kapus Imperial College London File Attached | ||
15:13 16mDoctoral symposium paper | Auto-tuning Framework for Multi-core Interference Analysis Doc Symposium Dan Iorga Imperial College London, UK |