Max-Planck-Institut für Informatik
max planck institut
mpii logo Minerva of the Max Planck Society

MPI-INF or MPI-SWS or Local Campus Event Calendar

<< Previous Entry Next Entry >> New Event Entry Edit this Entry Login to DB (to update, delete)
What and Who
Title:Rigorous Acrchitectural Modelling for Production Multiprocessors
Speaker:Kathy Gray
coming from:University of Cambridge
Speakers Bio:
Event Type:SWS Colloquium
Visibility:D1, D2, D3, D4, D5, SWS, RG1, MMCI
We use this to send out email in the morning.
Level:Expert Audience
Date, Time and Location
Date:Wednesday, 16 December 2015
Duration:90 Minutes
Building:E1 5
Processor architectures are critical interfaces in computing, but they are typically defined only by prose and pseudocode documentation.

This is especially problematic for the subtle concurrency behaviour of weakly consistent multiprocessors such as ARM and IBM POWER:
the traditional documentation does not define precisely what programmer-observable behaviour is (and is not) allowed for concurrent
code; it is not executable as a test oracle for pre-Silicon or post-Silicon hardware testing; it is not executable as an emulator for
software testing; and it is not mathematically rigorous enough to serve as a foundation for software verification.

In this talk, I will present a rigorous architectural envelope model for IBM POWER and ARM multiprocessors, that aims to support all of
these for small-but-intricate test cases, integrating an operational concurrency model with an ISA model for the sequential behaviour of a
substantial fragment of the user-mode instruction set (expressed in a new ISA description language). I will present the interface between
the two, whose requirements drove the development of our new language Sail. I will also present the interesting aspects of Sail's dependent
type system, which is a light-weight system balancing the benefits of static bounds and effects checking with the usability of the language
for engineers. Futher, our models can be automatically translated into executable code, which, combined with front-ends for concurrency
litmus tests and ELF executables, can interactively or exhaustively explore all the allowed behaviours of small test cases.

Joint work with: S. Flur, G. Kerneis*, L. Maranget**, D. Mulligan, C. Pulte, S. Sarkar***, and P. Sewell, University of Cambridge
(* Google, ** Inria, *** St Andrews)

Name(s):Claudia Richter
Phone:0681 93039103
EMail:--email address not disclosed on the web
Video Broadcast
Video Broadcast:NoTo Location:
Tags, Category, Keywords and additional notes
Attachments, File(s):
  • Claudia Richter, 12/08/2015 02:51 PM -- Created document.