Susmit Sarkar — Publication List

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:

• Fences in Weak Memory Models (Extended Version) (pdf, bib) Jade Alglave, Luc Maranget, Susmit Sarkar, and Peter Sewell, FMSD, Volume 40, Number 2, 2012, pages 170 – 205 Extended version of the CAV'10 paper.
• x86-TSO: A Rigorous and Usable Programmer's Model for x86 Multiprocessors (pdf, doi, abstract, bib) Peter Sewell, Susmit Sarkar, Scott Owens, Francesco Zappa Nardelli and Magnus O. Myreen, Commun. ACM, Volume 53, Number 7, Jul 2010, pages 89 – 97 An accessible presentation of the x86-TSO machine, together with an up-to-date account of the confusion in the technical documentation. This is based on the TPHOLS '09 and the POPL '09 papers, where the technical details can be found.
• 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:

• An Axiomatic Memory Model for POWER Multiprocessors (pdf) Sela Mador-Haim, Luc Maranget, Susmit Sarkar, Kayvan Memarian, Jade Alglave, Scott Owens, Rajeev Alur, Milo M. K. Martin, Peter Sewell, and Derek Williams. CAV '12 An axiomatic characterization of POWER multiprocessors, proved equivalent to the operational PLDI'11 model, and suitable for fast exploration via SAT solving.
• Synchronising C/C++ and POWER (pdf, bib) Susmit Sarkar, Mark Batty, Scott Owens, Kayvan Memarian, Luc Maranget, Jade Alglave, Peter Sewell, and Derek Williams. PLDI '12 Synchronising instructions on POWER (load conditional/store reserve), and on C++11 (read-modify-writes), and compilation mappings between them.
• Clarifying and Compiling C/C++ Concurrency: From C++11 to POWER (pdf, ps, bib) Mark Batty, Kayvan Memarian, Scott Owens, Susmit Sarkar and Peter Sewell. POPL '12 Correctly compiling C++ concurrency to POWER.
• Nitpicking C++ Concurrency (pdf, bib) Jasmin Christian Blanchette, Tjark Weber, Mark Batty, Scott Owens and Susmit Sarkar. PPDP '11 An efficient exploration of the C++0x model, using Nitpick and Isabelle.
• Understanding POWER multiprocessors (pdf, ps, abstract, bib) Susmit Sarkar, Peter Sewell, Jade Alglave, Luc Maranget and Derek Williams. PLDI '11 An operational characterization of the POWER relaxed memory model. Look also at the accompanying website.
• Litmus: Running Tests Against Hardware (pdf, ps, doi, abstract, bib) Jade Alglave, Luc Maranget, Susmit Sarkar and Peter Sewell. TACAS '11 Tool description of our litmus tool, which runs small concurrent programs (litmus tests) a large number of times.
• Mathematizing C++ Concurrency (pdf, ps, abstract, bib) Mark Batty, Scott Owens, Susmit Sarkar, Peter Sewell and Tjark Weber, POPL '11 A mathematical description of the concurrency proposal in C++0x. This is based on the Final Committee Draft version of 2010.
• Fences in Weak Memory Models (pdf, ps, doi, abstract, bib) Jade Alglave, Luc Maranget, Susmit Sarkar and Peter Sewell, CAV '10 A generic global-time based class of weak-memory models, which can be instantiated to (among others) a fragment of a Power model. Also contains ways of automatically testing such models against hardware.
• 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, doi, 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.