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.

Specifically, here are some projects I have been involved in:

• Recently, I have been trying to formalize the memory consistency behaviour of machine code on real multiprocessor architectures, including (so far) the x86, Power and ARM architectures. This should serve as a solid foundation for verifying low-level concurrent code. See the weak memory project website for more details.

• Before this, my thesis work was in “foundational certified code”, the idea that we formalize low-level semantics of machine code, and directly prove programs safe on this semantics. This is usually done by a very low-level type system, aka typed assembly language. I was involved in proving the soundness of one such type system, called TALT. Along the way, I defined a new dependently-typed program language where very expressive specifications were written out explicitly as types.

• Among the other projects I have been involved in, I have used, and in a minor way, developed, the proof assistant Twelf, and formalized and used the general proof assistant front-end Ott.

top

Publications

Note that in many cases copyright to the articles below have been assigned to others, such as journals or conference organizing bodies. The copies here are personal author copies.

Bibliography

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

Journals:

• Ott: Effective Tool Support for the Working Semanticist (pdf, doi, bib, abstract), Peter Sewell, Francesco Zappa Nardelli, Scott Owens, Gilles Peskine, Thomas Ridge, Susmit Sarkar, and Rok Strniša, JFP, Volume 20, Number 1, January 2010 Journal version of the original ICFP '07 Ott paper. In comparison to that one, this version has much expanded discussion and many more examples, and a detailed explanation of the binding specifications (“bindspecs”) of Ott. See also the Ott web page.
• Foundational certified code in the Twelf metalogical framework (ps, pdf, doi, bib, abstract), Karl Crary and Susmit Sarkar ACM TOCL, Volume 9, Number 3, June 2008 Journal version of the CADE '03 paper. In comparison to that one, this version describes a more modern variant of the system and proof.

Conference, workshop, and position papers:

• A Better x86 Memory Model: x86-TSO (ps, pdf, doi, bib, abstract), Scott Owens, Susmit Sarkar, and Peter Sewell, TPHOLS '09 Describes a TSO-like model, extended to the x86 with x86-specific features such as locked instructions, and which is (we think) the intended architecture behaviour. See the technical report version for more testing results and details of formalisation. See also the Weak Memory project's homepage.
• Relaxed memory models must be rigorous (ps, pdf, bib), Francesco Zappa Nardelli, Peter Sewell, Jaroslav Ševčík, Susmit Sarkar, Scott Owens, Luc Maranget, Mark Batty, and Jade Alglave, (EC)² '09 A short position paper arguing why we really need to be rigorous. See also the Weak Memory project's homepage.
• The Semantics of x86-CC Multiprocessor Machine Code (ps, pdf, doi, bib, abstract), Susmit Sarkar, Peter Sewell, Francesco Zappa Nardelli, Scott Owens, Tom Ridge, Thomas Braibant, Magnus O. Myreen, and Jade Alglave, POPL '09 The Causal Consistency model, based on the Intel and AMD manuals circa Jun 2008. The mathematical and empirical results hold, however, the manuals we based it on turned out to be simultaneously unsound and too weak for the processors of the time, as noted in the addendum added in the published version. We now believe a TSO model is a better model. See also the Weak Memory project's homepage.
• The Semantics of Power and ARM Multiprocessor Machine Code (ps, pdf, bib), Jade Alglave, Anthony Fox, Samin Ishtiaq, Magnus O. Myreen, Susmit Sarkar, Peter Sewell, and Francesco Zappa Nardelli, DAMP '09 Our first cut at formally specifying the relaxed memory model exhibited by the Power and ARM processors. A preliminary work, not completely correct. See also the Weak Memory project's homepage.
• Ott: Effective Tool Support for the Working Semanticist (ps, pdf, doi, bib, abstract), Peter Sewell, Francesco Zappa Nardelli, Scott Owens, Gilles Peskine, Thomas Ridge, Susmit Sarkar, and Rok Strniša, ICFP '07 The Ott tool, a tool for producing LaTeX and various proof assistant definitions from readable definitions. An expanded version was published in JFP. See also the Ott web page.
• Specifying real-world binding structures (ps, pdf, bib), Susmit Sarkar, Peter Sewell, and Francesco Zappa Nardelli, WMM '07 Sketching the motivation and semantics for the Ott bindspec language. See also the Ott web page.
• Small Proof Witnesses for LF (ps, pdf, doi, bib, abstract), Susmit Sarkar, Brigitte Pientka and Karl Crary, ICLP '05 Using “oracles” (as described by Necula and Rahul in their POPL '01 paper) within Twelf in a completely generic way.
• Foundational Certified Code in a Metalogical Framework (ps, pdf, bib, abstract), Karl Crary and Susmit Sarkar, CADE '03 The original safety proof of TALT on x86 paper. The technical report version extended this by including a short discussion of metaproofs in Twelf. The later journal version describes a more modern variant of the system and proof.

Technical reports and dissertations:

• A Better x86 Memory Model: x86-TSO (Extended Version) (pdf), Scott Owens, Susmit Sarkar, and Peter Sewell, UCAM-CL-TR-745 The technical report version of the TPHOLS '09 paper. This version extends that with much more results of testing, and details of formalisation and proof. See also the Weak Memory project's homepage.
• A Dependently Typed Programming Language, with applications to Foundational Certified Code Systems (pdf), Susmit Sarkar, CMU-CS-09-128 My Ph.D. dissertation, including the definition and uses of the LF/ML language, and the safety proof of TALT on x86, fully formalised in Twelf.
• Foundational Certified Code in a Metalogical Framework (ps, pdf, abstract), Karl Crary and Susmit Sarkar, CMU-CS-03-108 The technical report version of the CADE '03 paper. This extends that version by including a short discussion of metaproofs in Twelf. Both are superseded by the later journal version, which describes a more modern variant of the system and proof.
• Robust Non-parametric Relevance Feedback for Image Retrieval (ps, pdf), Ashwin T.V., Sugata Ghosal, Abhinanda Sarkar, Navendu Jain, and Susmit Sarkar, IBM India Research Laboratory Technical Report, Dec 2001 An old work, in part based on work I did in a summer internship.

top

Talks:

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

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.

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:

Jade Alglave, Thomas Braibant, Karl Crary, Anthony Fox, Samin Ishtiaq, Magnus O. Myreen, Francesco Zappa Nardelli, Scott Owens, Gilles Peskine, Brigitte Pientka, Tom Ridge, Peter Sewell, Rok Strniša

top