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.)