LFCS Seminar: 11 February 2020 - Ben Simner

Title: Relaxed Systems Architecture: Instruction Fetching

Abstract:

Computing relies on architecture specifications to decouple hardware and software development. Historically these have been prose documents, with all the problems that entails, but research over the last ten years has developed rigorous and executable-as-test-oracle specifications of mainstream architecture instruction sets and "user-mode" concurrency; clarifying architectures and bringing them into the scope of programming-language semantics and verification. However, the system semantics (those parts of the architecture required for operating systems, kernels and hypervisors), remains obscure In this talk we will go beyond our "user-mode" concurrency and present the first steps towards the systems architecture: instruction fetching and cache maintenance.

Affiliation:

Department of Computer Science and Technology, University of Cambridge.