Susmit Sarkar

View Scopus Profile

Susmit Sarkar

Prof

 https://orcid.org/0000-0002-4259-9213

  • KY16 9SS

    United Kingdom

Accepting Postgraduate Research Students

PhD projects

Shared memory concurrency; verification; parallelism; programming languages; compilers; static analysis; hardware architecture design; memory consistency models

Search results

  • 2024

    Towards specification-guarded refactoring

    Barwell, A. D., Brown, C. M. & Sarkar, S., 7 Sept 2024, Logic-based program synthesis and transformation: 34th International symposium, LOPSTR 2024, Milan, Italy, September 9–10, 2024, Proceedings. Bowles, J. & Søndergaard, H. (eds.). Cham: Springer, p. 149–165 (Lecture notes in computer science; vol. 14919).

    Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

    Open Access
    File
  • 2023

    Compound memory models

    Goens, A., Chakraborty, S., Sarkar, S., Agarwal, S., Oswald, N. & Nagarajan, V., 6 Jun 2023, In: Proceedings of the ACM on Programming Languages. 7, PLDI, 24 p., 153.

    Research output: Contribution to journal › Article › peer-review

    Open Access
    File
  • 2022

    Towards a refactoring tool for dependently-typed programs (Extended abstract)

    Brown, C. M., Barwell, A., Thompson, S., Sarkar, S. & Brady, E. C., 31 Jul 2022. 8 p.

    Research output: Contribution to conference › Paper › peer-review

    File
  • 2021

    Proving renaming for Haskell via dependent types: a case-study in refactoring soundness

    Barwell, A. D., Brown, C. M. & Sarkar, S., 18 Jul 2021, 8th International workshop on rewriting techniques for program transformations and evaluation (WPTE 2021). 10 p.

    Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

    Open Access
    File
  • 2020

    Fast and correct load-link/store-conditional instruction handling in DBT systems

    Kristien, M., Spink, T., Campbell, B., Sarkar, S., Stark, I., Franke, B., Böhm, I. & Topham, N., 2 Oct 2020, CASES '20: Proceedings of the International Conference on Compilers, Architectures and Synthesis for Embedded Systems. IEEE Computer Society, Vol. Early Access. 11 p. (IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems; vol. 39, no. 11).

    Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

    Open Access
    File
  • 2018

    Automatically deriving cost models for structured parallel processes using hylomorphisms

    Castro, D., Hammond, K., Sarkar, S. & Alguwaifli, Y., 1 Feb 2018, In: Future Generation Computer Systems. 79, Part 2, p. 653-668

    Research output: Contribution to journal › Article › peer-review

    Open Access
    File

  • Memory consistency models using constraints

    Akgün, Ö., Hoffmann, R. & Sarkar, S., 27 Aug 2018, The Seventeenth Workshop on Constraint Modelling and Reformulation (ModRef 2018), Proceedings. 16 p.

    Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

    Open Access
    File

  • Simplifying ARM concurrency: multicopy-atomic axiomatic and operational models for ARMv8

    Pulte, C., Flur, S., Deacon, W., French, J., Sarkar, S. & Sewell, P., 1 Jan 2018, Proceedings of the ACM on Programming Languages (POPL '18). New York: ACM, p. 1-29 29 p. 19. (Proceedings of the ACM on Programming Languages; vol. 2, no. POPL).

    Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

    Open Access
    File
  • 2017

    Mixed-size concurrency: ARM, POWER, C/C++11, and SC

    Flur, S., Sarkar, S., Pulte, C., Nienhuis, K., Maranget, L., Gray, K., Sezgin, A., Batty, M. & Sewell, P., 1 Jan 2017, Proceedings of the 44th annual ACM-SIGPLAN Symposium on Principles of programming languages (POPL 2017). Fluet, M. (ed.). New York: ACM, p. 429-442 14 p. (ACM SIGPLAN Notices; vol. 52, no. 1).

    Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

    Open Access
    File

  • Verification of a lazy cache coherence protocol against a weak memory model

    Banks, C., Elver, M., Hoffmann, R., Sarkar, S., Jackson, P. & Nagarajan, V., 2 Oct 2017, Proceedings of the 17th Conference on Formal Methods in Computer-Aided Design (FMCAD 2017). Stewart, D. & Weissenbacher, G. (eds.). FMCAD Inc, p. 60-67

    Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

    Open Access
    File
  • 2016

    Farms, pipes, streams and reforestation: reasoning about structured parallel processes using types and hylomorphisms

    Castro, D., Hammond, K. & Sarkar, S., 4 Sept 2016, Proceedings of the 21st ACM SIGPLAN International Conference on Functional Programming (ICFP 2016). New York, NY: ACM, p. 4-17 14 p. (ACM SIGPLAN Notices; vol. 51, no. 9).

    Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

    Open Access
    File

  • Fence placement for legacy Data-Race-Free programs via synchronization read detection

    McPherson, A. J., Nagarajan, V., Sarkar, S. & Cintra, M., 7 Jan 2016, In: ACM Transactions on Architecture and Code Optimization (TACO). 12, 4, 23 p., 46.

    Research output: Contribution to journal › Article › peer-review

    Open Access
    File

  • Modelling the ARMv8 architecture, operationally: concurrency and ISA

    Flur, S., Gray, K., Pulte, C., Sarkar, S., Sezgin, A., Maranget, L., Deacon, W. & Sewell, P., 11 Jan 2016, Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL '16). Gill, A. (ed.). New York: ACM, p. 608-621 14 p. (ACM SIGPLAN Notices; vol. 51, no. 1).

    Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

    Open Access
    File

  • Timing properties and correctness for structured parallel programs on x86-64 multicores

    Hammond, K., Brown, C. M. & Sarkar, S., 2016, Foundational and Practical Aspects of Resource Analysis: 4th International Workshop, FOPARA 2015, London, UK, April 11, 2015. Revised Selected Papers. van Eekelen, M. & Dal Lago, U. (eds.). Springer, p. 101-125 26 p. (Lecture Notes in Computer Science; vol. 9964).

    Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

    Open Access
    File
  • 2015

    An integrated concurrency and core-ISA architectural envelope definition, and test oracle, for IBM POWER multiprocessors

    Gray, K., Kerneis, G., Mulligan, D., Pulte, C., Sarkar, S. & Sewell, P., 5 Dec 2015, MICRO-48 Proceedings of the 48th International Symposium on Microarchitecture . New York, NY: ACM, p. 635-646 12 p.

    Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

    Open Access
    File

  • Fence placement for legacy data-race-free programs via synchronization read detection

    McPherson, A., Nagarajan, V., Sarkar, S. & Cintra, M., 24 Jan 2015, PPoPP 2015 Proceedings of the 20th ACM SIGPLAN Symposium on Principles and Practice of Parallel Programming. New York, NY: ACM, p. 249-250 2 p.

    Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

    Open Access
    File
  • 2012

    An Axiomatic Memory Model for POWER Multiprocessors

    Mador-Haim, S., Maranget, L., Sarkar, S., Memarian, K., Alglave, J., Owens, S., Alur, R., Martin, M., Sewell, P. & Williams, D., Jul 2012, Proceedings of the 24th International Conference on Computer Aided Verification. Madhusudan, P. & Seshia, S. (eds.). Springer-Verlag, p. 495 512 p. (Lecture Notes in Computer Science; vol. 7358).

    Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

  • Clarifying and Compiling C/C++ Concurrency: from C++11 to POWER

    Batty, M., Memarian, K., Owens, S., Sarkar, S. & Sewell, P., Jan 2012, In: ACM SIGPLAN Notices. 47, 1, p. 509-520 12 p.

    Research output: Contribution to journal › Article › peer-review

  • Clarifying and Compiling C/C plus plus Concurrency: from C++11 to POWER

    Batty, M., Memarian, K., Owens, S., Sarkar, S. & Sewell, P., 2012, POPL 12: PROCEEDINGS OF THE 39TH ANNUAL ACM SIGPLAN-SIGACT SYMPOSIUM ON PRINCIPLES OF PROGRAMMING LANGUAGES. NEW YORK: ACM, p. 509-520 12 p.

    Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

  • Fences in weak memory models (extended version)

    Alglave, J., Maranget, L., Sarkar, S. & Sewell, P., Apr 2012, In: Formal methods in system design. 40, 2, p. 170-205 36 p.

    Research output: Contribution to journal › Article › peer-review

  • Synchronising C/C++ and power

    Sarkar, S., Memarian, K., Owens, S., Batty, M., Sewell, P., Maranget, L., Alglave, J. & Williams, D., 2012, PLDI'12 - Proceedings of the 2012 ACM SIGPLAN Conference on Programming Language Design and Implementation. p. 311-321 11 p. (Proceedings of the ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI)).

    Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

  • Synchronising C/C plus plus and POWER

    Sarkar, S., Memarian, K., Owens, S., Batty, M., Sewell, P., Maranget, L., Alglave, J. & Williams, D., 1 Jun 2012, In: ACM SIGPLAN Notices. 47, 6, p. 311-321 11 p.

    Research output: Contribution to journal › Article › peer-review

  • 2011

    Litmus: Running Tests against Hardware

    Alglave, J., Maranget, L., Sarkar, S. & Sewell, P., 2011, TOOLS AND ALGORITHMS FOR THE CONSTRUCTION AND ANALYSIS OF SYSTEMS. Abdulla, P. & Leino, K. (eds.). BERLIN: Springer-Verlag, p. 41-44 4 p. (Lecture Notes in Computer Science; vol. 6605).

    Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

  • Mathematizing C++ Concurrency

    Batty, M., Owens, S., Sarkar, S., Sewell, P. & Weber, T., Jan 2011, In: ACM SIGPLAN Notices. 46, 1, p. 55-66 12 p.

    Research output: Contribution to journal › Article › peer-review

  • Mathematizing C plus plus Concurrency

    Batty, M., Owens, S., Sarkar, S., Sewell, P. & Weber, T., 2011, POPL 11: PROCEEDINGS OF THE 38TH ANNUAL ACM SIGPLAN-SIGACT SYMPOSIUM ON PRINCIPLES OF PROGRAMMING LANGUAGES. NEW YORK: ACM, p. 55-66 12 p.

    Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

  • Nitpicking C++ concurrency

    Blanchette, J. C., Weber, T., Batty, M., Owens, S. & Sarkar, S., 2011, PPDP'11 - Proceedings of the 2011 Symposium on Principles and Practices of Declarative Programming. p. 113-123 11 p. (PPDP'11 - Proceedings of the 2011 Symposium on Principles and Practices of Declarative Programming).

    Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

  • Nitpicking C plus plus Concurrency

    Blanchette, J. C., Weber, T., Batty, M., Owens, S. & Sarkar, S., 2011, PPDP 11 - PROCEEDINGS OF THE 2011 SYMPOSIUM ON PRINCIPLES AND PRACTICES OF DECLARATIVE PROGRAMMING. NEW YORK: ACM, p. 113-123 11 p.

    Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

  • Understanding POWER Multiprocessors

    Sarkar, S., Sewell, P., Alglave, J., Maranget, L. & Williams, D., 2011, PLDI 11: PROCEEDINGS OF THE 2011 ACM CONFERENCE ON PROGRAMMING LANGUAGE DESIGN AND IMPLEMENTATION. NEW YORK: ACM, p. 175-186 12 p.

    Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

  • Understanding POWER Multiprocessors

    Sarkar, S., Sewell, P., Alglave, J., Maranget, L. & Williams, D., Jun 2011, In: ACM SIGPLAN Notices. 46, 6, p. 175-186 12 p.

    Research output: Contribution to journal › Article › peer-review

  • 2010

    Fences in Weak Memory Models

    Alglave, J., Maranget, L., Sarkar, S. & Sewell, P., 2010, COMPUTER AIDED VERIFICATION, PROCEEDINGS. Touili, T., Cook, B. & Jackson, P. (eds.). BERLIN: Springer-Verlag, p. 258-272 15 p. (Lecture Notes in Computer Science; vol. 6174).

    Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

  • Ott: Effective tool support for the working semanticist

    Sewell, P., Nardelli, F. Z., Owens, S., Peskine, G., Ridge, T., Sarkar, S. & Strnisa, R., Jan 2010, In: Journal of Functional Programming. 20, 01, p. 71-122 52 p.

    Research output: Contribution to journal › Article › peer-review

  • x86-TSO: A Rigorous and Usable Programmer's Model for x86 Multiprocessors

    Sewell, P., Sarkar, S., Owens, S., Nardelli, F. Z. & Myreen, M. O., Jul 2010, In: Communications of the ACM. 53, 7, p. 89-97 9 p.

    Research output: Contribution to journal › Article › peer-review

  • 2009

    A Better x86 Memory Model: x86-TSO

    Owens, S., Sarkar, S. & Sewell, P., 2009, THEOREM PROVING IN HIGHER ORDER LOGICS, PROCEEDINGS. Berghofer, S., Nipkow, T., Urban, C. & Wenzel, M. (eds.). BERLIN: Springer-Verlag, p. 391-407 17 p. (Lecture Notes in Computer Science; vol. 5674).

    Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

  • The semantics of power and aRM multiprocessor machine code

    Alglave, J., Fox, A., Samin Ishtiaq, I., Myreen, M. O., Sarkar, S., Sewell, P. & Nardelli, F. Z., 2009, Proceedings of the 4th ACM SIGPLAN Workshop on Declarative Aspects of Multicore Programming, DAMP'09. p. 13-24 12 p. (Proceedings of the 4th ACM SIGPLAN Workshop on Declarative Aspects of Multicore Programming, DAMP'09).

    Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

  • The Semantics of x86-CC Multiprocessor Machine Code

    Sarkar, S., Sewell, P., Nardelli, F. Z., Owens, S., Ridge, T., Braibant, T., Myreen, M. O. & Alglave, J., Jan 2009, In: ACM SIGPLAN Notices. 44, 1, p. 379-391 13 p.

    Research output: Contribution to journal › Article › peer-review

  • 2008

    Foundational certified code in the Twelf metalogical framework

    Crary, K. & Sarkar, S., 2008, In: ACM Transactions on Computational Logic. 9, 3, 26 p., ARTN 16.

    Research output: Contribution to journal › Article › peer-review

  • 2007

    Ott: Effective tool support for the working semanticist

    Sewell, P., Nardelli, F. Z., Owens, S., Peskine, G., Ridge, T., Sarkar, S. & Strnisa, R., Sept 2007, In: ACM SIGPLAN Notices. 42, 9, p. 1-12 12 p.

    Research output: Contribution to journal › Article › peer-review

  • Ott: Effective Tool Support for the Working Semanticist

    Sewell, P., Nardelli, F. Z., Owens, S., Peskine, G., Ridge, T., Sarkar, S. & Strnisa, R., 2007, ICFP'07 PROCEEDINGS OF THE 2007 ACM SIGPLAN INTERNATIONAL CONFERENCE ON FUNCTIONAL PROGRAMMING. NEW YORK: ACM, p. 1-12 12 p.

    Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

  • 2005

    Small proof witnesses for LF

    Sarkar, S., Pientka, B. & Crary, K., 2005, Proceedings of 21st International Conference on Logic Programming (ICLP 2005). Springer, Vol. 3668. p. 387-401 15 p. (Lecture Notes in Computer Science).

    Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

  • 2003

    Foundational certified code in a metalogical framework

    Crary, K. & Sarkar, S., 2003, Automated Deduction - CADE-19 - 19th International Conference on Automated Deduction, Proceedings. Baader, F. (ed.). Springer-Verlag, p. 106-120 15 p. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); vol. 2741).

    Research output: Chapter in Book/Report/Conference proceeding › Conference contribution