Christopher Pulte

missing photo

Christopher Pulte

christopher.pulte@cl.cam.ac.uk
University of Cambridge
Computer Laboratory
15 JJ Thomson Avenue
Cambridge, CB30FD




Research Associate at the Computer Laboratory, University of Cambridge with Peter Sewell. My research interests are in programming language semantics and type systems, concurrency, and verification.


I am working in the area of relaxed memory concurrency, in particular on the semantics of concurrent ARMv8 and RISC-V (and POWER) machine code programs: establishing the architectural semantics and developing precise formalisations, as a basis for testing and verification, and to inform programming language implementation above these architectures.

From 2014 to 2018 I did my PhD at the University of Cambridge, supervised by Peter Sewell. My thesis (below) tries to provide a better understanding of the relaxed memory concurrency models of ARMv8 and RISC-V (and to a lesser degree Power). The main results are an operational concurrency model for the multicopy atomic ARMv8 architecture and its equivalence proof with the reference axiomatic model, and an equivalent simpler operational model for ARMv8 and RISC-V based on Kang et al.’s Promising semantics for C11.

Before the PhD, from 2013 to 2014, I did the MPhil in Computer Science at the University of Cambridge, with thesis “Synthesis of impure ML from monadic HOL functions”, extending a tool for the proof-producing translation of imperative ML from HOL4 as part of the CakeML project, supervised by Magnus Myreen.

Before then, from 2010-2013, I did the BSc in Computer Science at TU Dortmund. My undergraduate thesis topic was Visibly Pushdown Automata, supervised by Thomas Schwentick.

Software

With my colleagues I am working on executable formalisations of the semantics of ARMv8 and RISC-V programs. This includes the ISA semantics in Sail and concurrency models in rmem, both on github. The concurrency models can be tried in the online interface.

Publications

Repairing and Mechanising the JavaScript Relaxed Memory Model.

Conrad Watt, Christopher Pulte, Anton Podkopaev, Guillaume Barbier, Stephen Dolan, Shaked Flur, Jean Pichon-Pharabod, Shu-yu Guo, to appear in PLDI 2020.

ARMv8-A system semantics: instruction fetch in relaxed architectures.

Ben Simner, Shaked Flur, Christopher Pulte, Alasdair Armstrong, Jean Pichon-Pharabod, Luc Maranget, Peter Sewell, in ESOP 2020. [www] [pdf] [pdf (extended version)]

Promising-ARM/RISC-V: a simpler and faster operational concurrency model.

Christopher Pulte, Jean Pichon-Pharabod, Jeehoon Kang, Sung-Hwan Lee, Chung-Kil Hur, in PLDI 2019. [www] [pdf]

The Semantics of Multicopy Atomic ARMv8 and RISC-V.

Christopher Pulte, PhD Thesis. 2018. [www]

ISA Semantics for ARMv8-A, RISC-V, and CHERI-MIPS.

Alasdair Armstrong, Thomas Bauereiss, Brian Campbell, Alastair Reid, Kathryn E. Gray, Robert M. Norton, Prashanth Mundkur, Mark Wassell, Jon French, Christopher Pulte, Shaked Flur, Ian Stark, Neel Krishnaswami, Peter Sewell, in POPL 2019. [www] [pdf]

The RISC-V Instruction Set Manual Volume I: Unprivileged ISA.

A. Waterman and K. Asanović, editors. December 2018. Document Version 20181221-Public-Review-draft. Contributors: Arvind, K. Asanović, R. Avižienis, J. Bachmeyer, C. F. Batten, A. J. Baum, A. Bradbury, S. Beamer, P. Briggs, C. Celio, C. Chang, D. Chisnall, P. Clayton, P. Dabbelt, R. Espasa, S. Flur, S. Freudenberger, J. Gray, M. Hamburg, J. Hauser, D. Horner, B. Hoult, A. Joannou, O. Johansson, B. Keller, Y. Lee, P. Loewenstein, D. Lustig, Y. Manerkar, L. Maranget, M. Martonosi, J. Myers, V. Nagarajan, R. Nikhil, J. Oberhauser, S. O’Rear, A. Ou, J. Ousterhout, D. Patterson, C. Pulte, J. Renau, C. Schmidt, P. Sewell, S. Sarkar, M. Taylor, W. Terpstra, M. Thomas, T. Thorn, C. Trippel, R. VanDeWalker, M. Vijayaraghavan, M. Wachs, A. Waterman, R. Watson, D. Williams, A. Wright, R. Zandijk, and S. Zhang. [www]

Simplifying ARM Concurrency: Multicopy-atomic Axiomatic and Operational Models for ARMv8.

Christopher Pulte, Shaked Flur, Will Deacon, Jon French, Susmit Sarkar, Peter Sewell, in POPL 2018. [www] [pdf]

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

Shaked Flur, Susmit Sarkar, Christopher Pulte, Kyndylan Nienhuis, Luc Maranget, Kathryn E. Gray, Ali Sezgin, Mark Batty, Peter Sewell, in POPL 2017. [www] [pdf]

Modelling the ARMv8 Architecture, Operationally: Concurrency and ISA.

Shaked Flur, Kathryn E. Gray, Christopher Pulte, Susmit Sarkar, Ali Sezgin, Luc Maranget, Will Deacon, Peter Sewell, in POPL 2016. [www] [pdf]

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

Kathryn E. Gray, Gabriel Kerneis, Dominic P. Mulligan, Christopher Pulte, Susmit Sarkar, Peter Sewell, in MICRO 2015. [pdf]