Susmit Sarkar

Research Interests

I am interested, broadly speaking, in finding out what programs are supposed to be doing, and proving that they actually do what they are supposed to do. In this interplay of specification and verification, I bring to bear ideas and techniques from the fields of logic, programming language theory, type theory, automated deduction and mechanized theorem proving.

My research has focused on low-level code, where specifications have historically been very murky and vague. My recent work has been on shared memory concurrency, which on modern systems leads to subtle memory consistency issues, a phenomenon called relaxed-memory consistency. I helped clarify and formalize such widely used systems as the architectures x86, Power, and ARM, and the new C11/C++11 concurrency model.

top

Publications

Significant papers

• Clarifying and Compiling C/C++ Concurrency: From C++11 to POWER (POPL '12)
• Understanding POWER multiprocessors (PLDI '11)
• x86-TSO: A Rigorous and Usable Programmer's Model for x86 Multiprocessors (CACM '10)
• Mathematizing C++ Concurrency (POPL '11)
• Foundational certified code in the Twelf metalogical framework (TOCL '08)

All the papers I have written.

Bibliography

A bibliography (bibtex) of the papers I have written.

top

Talks:

• Understanding POWER Multiprocesors (slides, pdf) : Talk at PLDI, Jun'11.
• Multiprocessor Architectures Don't Really Exist (But They Should) (slides, pdf) : Invited Talk at MTV, Dec'09.
• The Semantics of X86-CC Multiprocessor Machine Code (slides, pdf) : Talk at POPL, Jan'09.
• Real-World Binding Structures (slides, pdf) : Talk at WMM, Sep'07.
• Small Proof Witnesses for LF (slides, ppt) : Talk at ICLP, Oct'05.
• Certified Typechecking in Foundational Certified Code Systems (slides, ppt) : Talk at Dagstuhl, Sep'04.
• Foundational Certified Code in a Metalogical Framework (slides, ppt) : Talk at CADE, Aug'03.

Funding

• EPSRC EP/H027351: Multiprocessors: From Microarchitecture to Semantic Theory (2010 - 2013): EPSRC Postdoctoral Fellowship in Theoretical Computer Science
• EPSRC EP/F036425: Reasoning with Relaxed Memory Models (2008 - 2012): Sewell, Parkinson, Fraser, Zappa Nardelli, Sarkar

Teaching:

• In Feb 2007, I gave a Theory Mini Course on Twelf, a system aimed at specifying, implementing, and proving properties of deductive systems, in particular, programming languages and logics. Materials for the course may be found here.
• At Cambridge, I have supervised Types (a part II course) for the Computer Laboratory, and Semantics of Programming Languages (a part IB course).
• At Carnegie Mellon University, I served as a teaching assistant for 15-399 (Constructive Logic, a junior/senior year course), and 15-251 (Great Ideas in Theoretical Computer Science, a sophomore year course).

Collaborators and co-authors:

top