Principles of Programming Seminar

Wednesday, October 19, 2016 - 3:30pm to 4:30pm


8102 Gates & Hillman Centers


PETER SEWELL, Professor of Computer Science

It's tempting to think that machine instructions are atomic updates to a global mutable state, of register and memory values.  In the sequential world that's a good model, but concurrent contexts expose a slew of more interesting behaviour.  We set out to understand real multiprocessor semantics in 2007, to give a basis for software verification.  We're still not done, but we now have credible operational models for much of what goes on.  I'll talk about some key points of this, including our experimental investigation and validation, the Lem and Sail metalanguages for expressing the semantics, our interactions with processor vendors, especially IBM and ARM, and work with the CHERI team on secure hardware and software.  It's impacted hardware testing, architecture design, and high-level language design along the way. This is part of the REMS project, aiming to apply semantics to improve the quality of mainstream computer systems; REMS also includes work on the C language and C/C++ concurrency model, on ELF linking, on POSIX filesystems,  on the TCP and TLS network and security protocols, on the CakeML verified compiler, and on program logics.   I'll start with a quick overview of REMS. This is joint work with Shaked Flur, Susmit Sarkar, Kathryn E. Gray, Christopher Pulte, Kyndylan Nienhuis, Luc Maranget, Ali Sezgin, Gabriel Kerneis, Dominic Mulligan, Anthony Fox, Robert Norton-Wright. — Peter Sewell is a Professor of Computer Science at the University of Cambridge Computer Laboratory.  He held an EPSRC Leadership Fellowship from 2010-2014 and a Royal Society University Research Fellowship from 1999-2007; he took his PhD in Edinburgh in 1995, supervised by Robin Milner, after studying in Cambridge and Oxford. His research aims to build rigorous foundations for the engineering of real-world computer systems, to make them better-understood, more robust, and more secure. Faculty Host: Robert Harper

Event Website:

For More Information, Contact:


Seminar Series