Susmit Sarkar

I am an EPSRC Research Fellow in the Programming, Logic and Semantics Group of the Computer Laboratory, University of Cambridge.

Contact details:

Email:

Susmit . Sarkar @ cl . cam . ac . uk

Address:

Computer Laboratory,
University of Cambridge,
15, J J Thomson Avenue,
Cambridge, CB3 0FD
United Kingdom

Office:

FS 17, William Gates Building

Elsewhere:

DBLP
Google Scholar
ACM

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.

Publications:

• NEW!Fast RMWs for TSO: Semantics and Implementation (forthcoming, accepted to PLDI '13)
• NEW!An Axiomatic Memory Model for POWER Multiprocessors (CAV '12)
• NEW!Synchronising C/C++ and POWER (PLDI '12)
• Fences in Weak Memory Models (Extended Version) (FMSD '12)
• 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)

For more, here is a complete list of papers I have written, and here is a bibliography (bibtex).

Talks:

• NEW! Shared Memory Concurrency in the Real World: Working with Relaxed Memory Consistency (slides, pdf) : Invited Tutorial at POPL, Jan'13 (TutorialFest).
• Inventing Abstractions: An academic view on industrial memory models (slides, pdf) : Invited Talk at REORDER, Jul'12.
• Synchronising C/C++ and POWER (slides, pdf) : Talk at PLDI, Jun'12.
• 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: