Details of Grant 

EPSRC Reference:	EP/M017044/1
Title:	Verifying concurrent algorithms on Weak Memory Models
Principal Investigator:	Derrick, Professor J
Other Investigators:	Struth, Professor G
Researcher Co-Investigators:
Project Partners:	University of Augsburg University of Paderborn University of Queensland
Department:	Computer Science
Organisation:	University of Sheffield
Scheme:	Standard Research
Starts:	29 May 2015	Ends:	28 November 2018	Value (£):	389,207
EPSRC Research Topic Classifications:	Fundamentals of Computing
EPSRC Industrial Sector Classifications:	No relevance to Underpinning Sectors
Related Grants:	EP/M017176/1
Panel History:	Panel Date Panel Name Outcome 02 Dec 2014 EPSRC ICT Prioritisation Panel - Dec 2014 Announced
Summary on Grant Application Form
Multi-core computing architectures have become ubiquitous over the last decade. This has been driven by the demand for continual performance improvements to cope with the every increasing sophistication of applications (for example, in the areas of graphics and audio processing). It has been necessary due to the constraints on chip manufacture which have prevented the continuation of performance improvements of earlier decades achieved primarily by speeding up sequential computation. The inherent parallelism these multi-core architectures entail offer great technical opportunities. Exploiting these opportunities presents a number of technical challenges. The high-level aim of this project is to address two key technical challenges in the area. Firstly, in order to fully exploit the potential concurrency, programmers are developing very subtle concurrent algorithms which dispense with the need to lock shared memory and data structures. Linearizability is the standard correctness criterion for concurrent programs. However, the complexity of these algorithms means that checking their correctness with a high degree of confidence is extremely difficult. Verification is needed, and we seek to develop appropriate proof methods to support it. Secondly, most prior work on correctness assumes a memory model (sequential consistency) which is not implemented in practice. In reality to increase efficiency, typical multicore systems communicate via shared memory and use relaxed memory models which give greater scope for optimization. These are the memory models implemented in processors such as x86, PowerPC, and ARM, and on these linearizability isn't the only relevant correctness criteria, and we shall also develop proof methods to quiescent consistency, which is emerging as an alternative correctness criteria on these processors.
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.shef.ac.uk