EPSRC logo

Details of Grant 

EPSRC Reference: EP/H005633/1
Title: Semantic Foundations for Real-World Systems
Principal Investigator: Sewell, Professor PM
Other Investigators:
Researcher Co-Investigators:
Project Partners:
ARM Ltd IBM UK Ltd Microsoft
Oracle Corporation Oswego State University of New York
Department: Computer Science and Technology
Organisation: University of Cambridge
Scheme: Leadership Fellowships
Starts: 01 January 2010 Ends: 31 December 2014 Value (£): 1,523,815
EPSRC Research Topic Classifications:
Fundamentals of Computing
EPSRC Industrial Sector Classifications:
Electronics Information Technologies
Related Grants:
Panel History:
Panel DatePanel NameOutcome
01 Jul 2009 Fellowships 2009 Final Allocation Panel Announced
10 Jun 2009 Fellowships 2009 Interview - Panel D Deferred
Summary on Grant Application Form
Computer systems have been pervasive for many years, but despite this, and despite the huge resources devoted to their construction, they are still typically insecure, prone to failure, and hard to use. Major failures are commonplace, in sharp contrast with the products of other engineering industries, and dealing with them, and with the day-to-day lesser flaws, has huge economic and social costs. The core technical difficulty is system complexity: the range of behavior, the large scale, and the legacy of old design choices combine to make it hard to understand these systems well enough to engineer them well. My main research goal is to develop intellectual tools that suffice for solid system-building, analogous to the applied mathematics of more traditional engineering disciplines. This must be grounded on real systems - it cannot be done in theoretical isolation. My approach, as documented in the Track Record, is to focus on the key articulation points in the hierarchy of abstractions used to build systems: programming languages, processor instruction sets, network protocols, and so forth. These are relatively stable points in a rapidly changing environment, are critical to all system development, and are small enough that a modest team can address them. Each demands different research: new language constructs, new specification, reasoning, and testing techniques, and so forth. In this Fellowship I will pursue this approach, focussing on the problems in building computer systems above the intricate relaxed memory models of modern multiprocessors. Multiprocessor systems are now the norm (as further speed-up of sequential processors has recently become impractical), but programming them is very challenging. A key difficulty is that these systems do not provide a sequentially consistent memory, in which events appear to occur in a single global time order, but instead permit subtle reorderings, rendering intuitive global-time reasoning unsound. Much previous work across a range of Computer Science, in programming languages, program logics, concurrency theory, model checking, and so on, makes the now-unrealistic assumption of sequential consistency, and it must now be revisited in this more complex setting.I will develop precise mathematical models of the behavior of real-world multiprocessors that take such reorderings into account, and develop semantics and reasoning techniques above them. Using those, I will consider the verification of high-performance concurrent algorithms (as used in operating system and hypervisor kernels), the design of higher-level languages, and verified compilation of those languages to real machines. This will enable future applications to be developed above a high-confidence and high-performance substrate. It should also have a broader beneficial effect on research in Computer Science, drawing together mathematically well-founded theory and systems-building practice.
Key Findings
This information can now be found on Gateway to Research (GtR) http://gtr.rcuk.ac.uk
Potential use in non-academic contexts
This information can now be found on Gateway to Research (GtR) http://gtr.rcuk.ac.uk
Description This information can now be found on Gateway to Research (GtR) http://gtr.rcuk.ac.uk
Date Materialised
Sectors submitted by the Researcher
This information can now be found on Gateway to Research (GtR) http://gtr.rcuk.ac.uk
Project URL:  
Further Information:  
Organisation Website: http://www.cam.ac.uk