Campus Event Calendar
Event Entry
What and Who
Tales from the Jungle
Peter Sewell
University of Cambridge
SWS Distinguished Lecture Series
AG 1, AG 2, AG 3, AG 4, AG 5, SWS, RG1, MMCI
Expert Audience
English
Note: We use this to send email in the morning.
Date, Time and Location
Monday, 18 February 2013
10:30
90 Minutes
E1 5
002
Saarbrücken
Abstract
We rely on a computational infrastructure that is a densely intertwined
mass of software and hardware: programming languages, network
protocols, operating systems, and processors. It has accumulated
great complexity, from a combination of engineering design decisions,
contingent historical choices, and sheer scale, yet it is defined at
best by prose specifications, or, all too often, just by the common
implementations. Can we do better? More specifically, can we apply
rigorous methods to this mainstream infrastructure, taking the
accumulated complexity seriously, and if we do, does it help? My
colleagues and I have looked at these questions in several contexts:
the TCP/IP network protocols with their Sockets API; programming
language design, including the Java module system, the C11/C++11
concurrency model, and the C programming language; the hardware
concurrency behaviour of x86, IBM POWER, and ARM multiprocessors; and
compilation of concurrent code.
In this talk I will draw some lessons from what did and did not
succeed, looking especially at the empirical nature of some of the
work, at the social process of engagement with the various different
communities, and at the mathematical and software tools we used.
Domain-specific modelling languages (based on functional programming
ideas) and proof assistants were invaluable for working with the large
and loose specifications involved: idioms within HOL4 for TCP, our Ott
tool for programming language specification, and Owens's Lem tool for
portable semantic definitions, with HOL4, Isabelle, and Coq, for the
relaxed-memory concurrency semantics work. Our experience with these
suggests something of what is needed to make mathematically rigorous
engineering of mainstream computer systems (and in systems research)
mass of software and hardware: programming languages, network
protocols, operating systems, and processors. It has accumulated
great complexity, from a combination of engineering design decisions,
contingent historical choices, and sheer scale, yet it is defined at
best by prose specifications, or, all too often, just by the common
implementations. Can we do better? More specifically, can we apply
rigorous methods to this mainstream infrastructure, taking the
accumulated complexity seriously, and if we do, does it help? My
colleagues and I have looked at these questions in several contexts:
the TCP/IP network protocols with their Sockets API; programming
language design, including the Java module system, the C11/C++11
concurrency model, and the C programming language; the hardware
concurrency behaviour of x86, IBM POWER, and ARM multiprocessors; and
compilation of concurrent code.
In this talk I will draw some lessons from what did and did not
succeed, looking especially at the empirical nature of some of the
work, at the social process of engagement with the various different
communities, and at the mathematical and software tools we used.
Domain-specific modelling languages (based on functional programming
ideas) and proof assistants were invaluable for working with the large
and loose specifications involved: idioms within HOL4 for TCP, our Ott
tool for programming language specification, and Owens's Lem tool for
portable semantic definitions, with HOL4, Isabelle, and Coq, for the
relaxed-memory concurrency semantics work. Our experience with these
suggests something of what is needed to make mathematically rigorous
engineering of mainstream computer systems (and in systems research)
a commonplace reality.
Contact
Claudia Richter
9303 9103
--email hidden
Video Broadcast
Yes
Kaiserslautern
G26
206
passcode not visible
logged in users only
Claudia Richter, 02/12/2013 15:12 -- Created document.