[talks] CJ Bell general exam

Melissa Lawson mml at CS.Princeton.EDU
Thu May 14 10:26:15 EDT 2009


CJ Bell will present his research seminar/general exam on Tuesday May 19 at 
10AM in Room 402.  The members of his committee are:  David Walker, advisor, 
Andrew Appel, and Brian Kernighan. Everyone is invited to attend his talk and 
those faculty wishing to remain for the oral exam following are welcome to do so.
His abstract and reading list follow below.
----------------------------------------------------------------------
ABSTRACT:

We have developed a concurrent separation logic to reason about the
correctness of programs that use produce and consume instructions for
synchronized communication between threads. Our motivation behind such
a logic is the decoupled software pipelining (DSWP) optimization in
the context of proof-carrying code (PCC).

PCC is a technique that allows untrusted code to be proven safe with
respect to a desired security model. Such code, when accompanied by a
formal proof of safety, can be validated and shown safe to execute.
One advantage of PCC over its alternatives is that it ensures safe
native code execution with minimal runtime checks. With an optimizing
compiler, native code is typically faster. To generate proofs of
safety, however, it is necessary that the optimizations preserve proof
annotations.

DSWP is an optimization that attempts to break while-loops into
dependent tasks that run in parallel and communicate their
dependencies through channels. The tasks are chosen to mitigate
stalling of the entire operation when accessing resources that other
tasks do not depend on. For example, a goal of DSWP is to use
low-latency communication channels to reduce pipeline stalls caused by
memory loads that, due to the variable latency of memory access, are
difficult to prevent using optimizations such as instruction
scheduling.

Communication channels are a synchronization method that has not yet
been explored in the context of concurrent separation logic, although
other mechanisms such as locks and conditional critical regions have
been investigated. Separation logic tracks resource ownership, which
is particularly useful for DSWP in order to break loops into
concurrent tasks. Our logic facilitates sound reasoning about the use
of communication channels to pass values between threads. Furthermore,
our logic reasons about the history of values produced and consumed.
It may be used in any situation where the programmer desires to pass
data between threads, but there is also potential for its use as a
target language for a certifying implementation of the DSWP
optimization in a PCC framework.


----------------------------------------------------------------------
TEXTBOOKS:

Types and Programming Languages (Pierce, B.)

Compiling with Proofs, ch. 1-6 (Necula, G.)

----------------------------------------------------------------------
PAPERS:

[1] BI as an Assertion Language for Mutable Data Strunctures (Ishtiaq
S., O'Hearn P.)

[2] Resources, Concurrency, and Local Reasoning (O'Hearn P.)

[3] Permission Accounting in Separation Logic (Bornat R.)

[4] Types for Atomicity (Flanagan, Qadeer S.)

[5] Analysis and Optimization of Explicitly Parallel Programs using
the Parallel Program Graph Representation (Sarkar V.)

[6] Automatic Thread Extraction with Decouples Software Pipelining
(Ottoni G., August D.)

[7] A Concurrent Execution Semantics for Parallel Program Graphs and
Program Dependence Graphs  (Sarkar V.)

[8] Local Reasoning for Storable Locks and Threads (Gotsman A.)

[9] A Verifiable SSA Program representation for Aggressive Compiler
Optimization (Menon V. S.)

[10] Revisiting the Sequential Programming Model for Multi-Core
(Bridges M., August D.)



More information about the talks mailing list