The purpose of the class project is to familiarize you with the state-of-the-art in compiler technology. There are four different types of projects you can choose:
Regardless of the project type you choose, by end of day Friday, April 10, create a private Piazza post to the instructors containing your proposed topic and group members. In addition, if you choose the research or implementation project, please schedule a brief meeting with Sorin on Friday, April 10 between 3-4 PM to propose your topic.
Your goal here is to perform original research. You may already have an idea you’ve been brainstorming, or perhaps you can gain inspiration from something in the reading project list.
Your goal is to re-implement the ideas/algorithms described in an existing body of research. You can look to the reading project list for a ton of possibilities.
We have outlined five broad research areas that could be potential topics for your reading project. Pick one and perform an extensive literature survey of the area. A successful survey is expected to cover ~30 papers 10 papers per student (groups of 2 cover 20 papers, groups of 3 cover 30), so you will need to cover more than just the papers we have listed here. More specifically, each of these lists below is just a starting point. You are expected to follow references and locate other related papers, especially recent work, to fill out your survey.
Automatically Proving the Correctness of Compiler Optimizations
Sorin Lerner, Todd Millstein, and Craig Chambers
PLDI 2003
Automated Soundness Proofs for Dataflow Analyses and Transformations via Local Rules
Sorin Lerner, Todd Millstein, Erika Rice, and Craig Chambers
POPL 2005
Translation Validation
A. Pnueli , M. Siegel , F. Singerman
TACAS 1998
Translation validation for an optimizing compiler
George C. Necula
PLDI 2000
Proving Optimizations Correct using Parameterized Program Equivalence
Sudipta Kundu, Zachary Tatlock, Sorin Lerner
PLDI 2009
Formal Certification Of A Compiler Back-End, Or: Programming A Compiler With A Proof Assistant
Xavier Leroy
POPL 2006
Bringing Extensibility to Verified Compilers
Zachary Tatlock, Sorin Lerner
PLDI 2010
Formal Verification Of Translation Validators: A Case Study On Instruction Scheduling Optimizations
Jean-Baptiste Tristan, Xavier Leroy
POPL 2008
Volatiles are miscompiled, and what to do about it
Eric Eide, John Regehr
EMSOFT 2008
Finding and Understanding Bugs in C Compilers
Xuejun Yang, Yang Chen, Eric Eide, John Regehr
PLDI 2011
Points-To Analysis In Almost Linear Time
Bjarne Steensgaard
POPL 1996
Unification-Based Pointer Analysis With Directional Assignments
Manuvir Das
PLDI 2000
The Ant And The Grasshopper: Fast And Accurate Pointer Analysis For Millions Of Lines Of Code
Ben Hardekopf, Calvin Lin
PLDI 2007
Separation Logic And Abstraction
Matthew Parkinson, Gavin Bierman
POPL 2005
TVLA: A System for Implementing Static Analyses
Tal Lev-Ami, Shmuel Sagiv
SAS 2000
Ownership Types for Safe Region-Based Memory Management in Real-Time Java
Chandrasekhar Boyapati, Alexandru Salcianu, William Beebee, Jr., Martin Rinard
PLDI 2003
Parametric Shape Analysis Via 3-Valued Logic
Mooly Sagiv, Thomas Reps, Reinhard Wilhelm
POPL 1999
Ultra-fast aliasing analysis using CLA: a million lines of C code in a second
Nevin Heintze, Olivier Tardieu
PLDI 2001
Efficient context-sensitive pointer analysis for C programs
Robert P. Wilson, Monica Lam
PLDI 1995
Cloning-Based Context-Sensitive Pointer Alias Analysis Using Binary Decision Diagrams
John Whaley, Monica Lam
PLDI 2004
Checking System Rules Using System Specific, Programmer-Written Compiler Extensions
Dawson Engler, Benjamin Chelf, Andy Chou and Seth Hallem
OSDI 2000
Bugs as Deviant Behavior: A General Approach to Inferring Errors in Systems Code
Dawson Engler, David Yu Chen, Seth Hallem, Andy Chou, and Benjamin Chelf
SOSP 2001
Efficient Detection of All Pointer and Array Access Errors
Todd Austin, Scott Breach, Gurindar Sohi
PLDI 1994
Cyclone: A Safe Dialect of C
Trevor Jim, Greg Morrisett, Dan Grossman, Michael Hicks, James Cheney, Yanling Wang
USENIX 2002
Region-Based Memory Management in Cyclone
Trevor Jim, Greg Morrisett, Dan Grossman, Michael Hicks, James Cheney, Yanling Wang
PLDI 2002
CCured: Type-Safe Retrofitting of Legacy Code
George Necula, Scott McPeak, Westley Weimer
POPL 2002
Language Support for Regions
David Gay, Alex Aiken
PLDI 2001
Secure Execution Via Program Shepherding
Vladimir Kiriansky, Derek Bruening, Saman Amarasinghe
Usenix Security 2002
Static detection of dynamic memory errors
David Evans
PLDI 1996
Volatiles are miscompiled, and what to do about it
Eric Eide, John Regehr
EMSOFT 2008
A few billion lines of code later: using static analysis to find bugs in the real world
Al Bessey, Ken Block, Ben Chelf, Andy Chou, Bryan Fulton, Seth Hallem, Charles Henri-Gros, Asya Kamsky, Scott McPeak, Dawson Engler
CACM 2010
Eraser: A Dynamic Data Race Detector For Multi-Threaded Programs
Stefan Savage, Michael Burrows, Greg Nelson, Patrick Sobalvarro, Thomas Anderson
SOSP 1997
RELAY: Static Race Detection On Millions Of Lines Of Code
Jan Wen Voung, Ranjit Jhala, Sorin Lerner
FSE 2007
Dataflow Analysis For Concurrent Programs Using Datarace Detection
Ravi Chugh, Jan Wen Voung, Ranjit Jhala, Sorin Lerner
PLDI 2008
Effective Static Race Detection For Java
Mayur Naik, Alex Aiken, John Whaley
PLDI 2006
Velodrome: A Sound and Complete Dynamic Atomicity Checker for Multithreaded Programs
Cormac Flanagan, Stephen N. Freund, Jaeheon Yi
PLDI 2008
Adversarial Memory for Detecting Destructive Races
Cormac Flanagan, Stephen N. Freund
PLDI 2010
AtomCaml: First-Class Atomicity Via Rollback
Michael F. Ringenburg, Dan Grossman
ICFP 2005
The Transactional Memory / Garbage Collection Analogy
Dan Grossman
OOPSLA 2007
CoreDet: A Compiler And Runtime System For Deterministic Multithreaded Execution
Tom Bergan, Owen Anderson, Joseph Devietti, Luis Ceze, Dan Grossman
ASPLOS 2010
Language Support for Lightweight Transactions
Tim Harris, Keir Fraser
OOPSLA 2003
Points-To Analysis In Almost Linear Time
Bjarne Steensgaard
POPL 1996
Unification-Based Pointer Analysis With Directional Assignments
Manuvir Das
PLDI 2000
ESP: Path-Sensitive Program Verification In Polynomial Time
Manuvir Das, Sorin Lerner, Mark Seigle
PLDI 2002
Cloning-Based Context-Sensitive Pointer Alias Analysis Using Binary Decision Diagrams
John Whaley, Monica Lam
PLDI 2004
Saturn: A Scalable Framework For Error Detection Using Boolean Satisfiability
Yichen Xie, Alex Aiken
POPL 2005
Using Datalog with Binary Decision Diagrams for Program Analysis
John Whaley, Dzintars Avots, Michael Carbin, Monica S. Lam
APLAS 2005
Fast liveness checking for ssa-form programs
Benoit Boissinot, Sebastian Hack, Daniel Grund, Benoit Dupont, Fabri e Rastello
CGO 2008
RELAY: Static Race Detection On Millions Of Lines Of Code
Jan Wen Voung, Ranjit Jhala, Sorin Lerner
FSE 2007
Dataflow Analysis For Concurrent Programs Using Datarace Detection
Ravi Chugh, Jan Wen Voung, Ranjit Jhala, Sorin Lerner
PLDI 2008
Making Context-Sensitive Points-to Analysis with Heap Cloning Practical For The Real World
Chris Lattner, Andrew Lenharth, and Vikram Adve
PLDI 2007
If none of the other options suit you, we also have a default project for you to work on.