Aquinas Hobor: Research Statement

(Also available as a PDF or as a Word document.)

I am interested in improving software reliability through specification and verification techniques.

Recently I have focused on improving the reliability of concurrent programs. Multi-core processors are leading to an increasing number of programs that utilize concurrency. Unfortunately, concurrency bugs tend to be among the most difficult to discover through testing. Therefore to improve the reliability of future software, we need to develop static analysis techniques that prevent concurrency bugs.

Most concurrent programs use threads and locks to control shared-memory concurrency. One formal method for reasoning about such programs is Concurrent Separation Logic (CSL) [O’Hearn 2007]. However, CSL was proposed for a simplified language that did not have first-order locks, threads, or substantial sequential control flow. Still, difficulties in reasoning about concurrent execution meant that the soundness of CSL was uncertain for some time [O’Hearn 2008], until Stephen Brookes developed a semantic model [Brookes 2007].

My work makes CSL more usable and its soundness more reliable. A major goal is end-to-end proofs: if we prove a property of our concurrent source program we should get guarantees about the concurrent program as it actually executes on chip. I developed a machine-checked soundness proof (in Coq) of CSL with respect to the operational semantics of concurrent C minor. C minor was chosen because it is powerful enough to be an intermediate language in an ANSI C compiler and because Xavier Leroy has a machine-verified compiler from (sequential) C minor to PowerPC assembly [Leroy 2006]. A major strength of my approach as compared to others [Gotsman 2007a] is that it directly supports the goal of end-to-end proofs and has the reliability guarantees of machine-checked proof [1].

To handle the soundness proof, I developed a separation technique that allows independent reasoning about the sequential and concurrent features of C minor. The resulting modularity is quite strong and allowed me to reuse an existing machine-checked soundness proof for sequential separation logic with respect to sequential C minor [Appel 2007] with only very minor modification; this modularity was extremely helpful for developing an industrial-sized machine-checked proof. My paper on this result appeared at ESOP 2008 [Hobor 2008]. This modularity should similarly allow the machine-checked soundness proof of the sequential C minor compiler to be largely re-used in a soundness proof of a concurrency-aware C minor compiler (a direction for future work).

In prior work related to concurrency and software verification, during an internship at Microsoft, I developed a system called espC that uses annotations to verify locking protocols; this tool is now being deployed over the Windows code base. Other research interests of mine include weak memory models, certified concurrency-aware compilers, the relationship of properties at the source code level to properties at the machine code level, certified parsers, semantic modeling, machine-checked proofs, modular proof techniques, substructural modal logics, information flow, modules and interfaces, size of trusted code base, editors and tools to aid code development, code analysis techniques, and security.

[1] A major strength of the approach described in [Gotsman 2007a] is that it connects to an implemented shape analysis technique [Gotsman 2007b]; unifying the two approaches is an interesting avenue for future work.

References

[O’Hearn 2007] P. O’Hearn, Resources, Concurrency, and Local Reasoning, TCS 375, May 2007

[O’Hearn 2008] P. O’Hearn, Further Reading on Local Reasoning and Separation Logic,
http://www.dcs.qmul.ac.uk/~ohearn/furtherreading.html#concurrency, fetched Feb 2008

[Brookes 2007] S. Brookes, A Semantics for Concurrent Separation Logic, TCS 375, May 2007

[Leroy 2006] X. Leroy, Formal certification of a compiler back-end, or: programming a compiler with a proof assistant, POPL 2006

[Gotsman 2007a] A. Gotsman, J. Berdine, B. Cook, N. Rinetzky, M. Sagiv, Local reasoning for storable locks and threads, APLAS 2007

[Gotsman 2007b] A. Gotsman, J. Berdine, B. Cook, M. Sagiv, Thread-modular shape analysis, PLDI 2007

[Appel 2007] A. W. Appel, S. Blazy, Separation Logic for Small-step C minor, TPHOLs 2007

[Hobor 2008] A. Hobor, A. W. Appel, and F. Zappa Nardelli, Oracle Semantics for Concurrent Separation Logic, ESOP 2008

web site by Lucy Day Hobor ~ 2008-2015