Details of Grant 

EPSRC Reference:	EP/H027351/1
Title:	Multiprocessors: From Microarchitecture to Semantic Theory
Principal Investigator:	Sarkar, Dr S
Other Investigators:
Researcher Co-Investigators:
Project Partners:	ARM Ltd IBM University of Texas at Austin
Department:	Computer Science and Technology
Organisation:	University of Cambridge
Scheme:	Postdoc Research Fellowship
Starts:	10 June 2010	Ends:	15 July 2013	Value (£):	269,820
EPSRC Research Topic Classifications:	Fundamentals of Computing
EPSRC Industrial Sector Classifications:	Information Technologies
Related Grants:
Panel History:	Panel Date Panel Name Outcome 16 Dec 2009 PDF Computer Science Sift Panel Excluded 26 Jan 2010 PDRF Computer Science Interview Panel Announced
Summary on Grant Application Form
Modern computers have become predominantly multicore, providing programmers with many simultaneously-executing threads of execution sharing the system memory. Concurrent programming is challenging, and this trend in hardware should have been an ideal application target for previous academic work on software verification. Concurrent programming has been extensively studied, with the development of areas such as model checking, process calculi, separation logic, and rely-guarantee reasoning. Unfortunately, realistic architectures violate a key assumption of most such work, that all threads have a consistent view of memory, an assumption often referred to as Sequential Consistency. Instead, programmers are actually faced with a Relaxed Memory Model , with only approximate consistency, making programming and verification significantly more challenging.Relaxed memory models arise, ultimately, from hardware (and compiler) implementation features designed for performance. Unfortunately, there is no clear understanding of how the microarchitectural choices made in hardware implementations lead to programmer-observable consequences. This is an instance of a more general problem, that modern hardware is too complex to understand without formal proofs, as witnessed by a succession of errata in deployed processors. Hardware verification is itself a field that has received a great deal of study. However, the field has still not reached the point of verifying global semantic properties, such as relaxed memory models, that emerge from the interaction of multiple disparate subsystems, each of which suffers from imprecise specifications.I propose to create a general theory of the programmer-observable behaviour which emerges from the microarchitectural choices and optimizations made in multiprocessor implementations. I will develop abstract mathematical models of the implementations, and explain with proof the observable consequences of those implementations. With specifications derived from that theory, I will go on to study the hardware verification problem, establishing techniques and methods for verifying global programmer-visible properties. Throughout, I will address not just safety properties, but also progress and liveness properties that sophisticated programmers rely on.Such a general theory is critical for a better understanding of multiprocessor semantics, by both programmers and hardware implementers, and for enabling these different communities to communicate their knowledge to each other. It is also an essential prerequisite for sound theories of concurrent programming. An improved understanding and communication of these issues is imperative for reliable multiprocessor usage.
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
Impacts
Description This information can now be found on Gateway to Research (GtR) http://gtr.rcuk.ac.uk Summary 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