Dr Susmit Sarkar
Director of Research
Biography
I am a Reader in Computer Science at the University of St Andrews, and have been at the school since 2013. Before this, I did postdoctoral work at the University of Cambridge, and obtained my PhD from Carnegie Mellon University. I am a Honorary Fellow at the School of Informatics of the University of Edinburgh, a Fellow of the British Computer Society (BCS), and a Senior Member of the Association of Computing Machinery (ACM).
My research interests are in concurrent and low-level software, and the software-hardware interface (others call this Architecture, or ISA-level). I have done work on memory consistency models, shared memory, dependent types, certified code, parallel cost models, and parallel code refactoring. My work has contributed to the understanding of the ARM, IBM POWER, x86, RISC-V architectures, the C, C++ and Java programming languages. I have served as an invited expert for the RISC-V architecture definition effort, published and reviewed extensively for leading journals and conferences (PLDI, POPL, TOPLAS, ICFP), and reviewed/been on panels for the EPSRC/ERC/ANR(France).
Teaching
This academic year (2022-23) I am teaching:
- CS4204: Concurrency and Multi-Core Architectures
- CS5031: Software Engineering Practice
In the past, I have taught modules at different levels, including:
- CS3050: Logic and Reasoning, a module I designed, developed and delivered for 3 years
- CS3052: Computational Complexity
- IS5102: Database Management Systems
- CS2006: Advanced Programming Projects
I also supervise project students at various levels in the school.
Outside St Andrews: I have delivered short courses and tutorials at a variety of venues, most recently An Introduction to Reasoning with Weak Memory at the Scottish Programming Languages and Verification Summer School 2022 (SPLV'22).
Research areas
My research interests are in specifying, validating, and verifying concurrent software and hardware. I particularly enjoy working at the hardware-software interface (low-level software/architecture-level hardware). Here I have worked extensively on the problem of memory consistency models, for architectures such as ARM, IBM POWER, RISC-V, and for low-level programming languages such as C/C++. I have pushed both down and up the stack, for example working on verification of cache protocols, of high-level parallel algorithmic skeletons, and on refactoring.
Selected publications
-
Open access
Simplifying ARM concurrency: multicopy-atomic axiomatic and operational models for ARMv8
Pulte, C., Flur, S., Deacon, W., French, J., Sarkar, S. & Sewell, P., 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
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-67Research output: Chapter in Book/Report/Conference proceeding › Conference contribution
-
Open access
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
-
Synchronising C/C plus plus and POWER
Sarkar, S., Memarian, K., Owens, S., Batty, M., Sewell, P., Maranget, L., Alglave, J. & Williams, D., Jun 2012, In: ACM SIGPLAN Notices. 47, 6, p. 311-321 11 p.Research output: Contribution to journal › Article › peer-review
-
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
-
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
-
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