Greg Bronevetsky, Cornell University
February 15, 2006


    Recent trends in microprocessor design are shifting us from large 
powerful processors to multiple simpler processors on the same chip. 
While dual-core designs are already on the market, 100 cores per chip 
are expected over the next several years. While offering application 
designers the potential for significant performance improvements, 
multi-core processors have a programmability drawback in that only 
explicitly multi-threaded applications can come close to fully 
exploiting their performance potential. As the last few decades of 
research on parallel programming models shows, writing and verifying 
such programs is a significant challenge, one that is still far from 
being solved.

    In this talk I will focus on my ongoing work in the verification of 
shared memory applications. In particular, my work has focused on 
techniques to formally prove such applications correct. In this talk I 
will discuss a correctness proof of an application-level checkpointing 
protocol for multi-threaded applications running on top of shared 
memory. This protocol transforms the source code of the application so 
that the resulting application 1. does the same thing as the old and 2. 
records checkpoints from which it can restart. I will discuss the proof 
at a high level and give an idea of what it takes to make such a proof 
fully formal and checkable by an automated theorem prover.