EPSRC logo

Details of Grant 

EPSRC Reference: EP/N026314/1
Title: Reliable Many-Core Programming
Principal Investigator: Donaldson, Dr AF
Other Investigators:
Researcher Co-Investigators:
Project Partners:
AMD (Advanced Micro Devices) (Global) ARM Ltd Imagination Technologies Ltd UK
Department: Dept of Computing
Organisation: Imperial College London
Scheme: EPSRC Fellowship
Starts: 03 October 2016 Ends: 02 October 2021 Value (£): 1,005,751
EPSRC Research Topic Classifications:
Fundamentals of Computing
EPSRC Industrial Sector Classifications:
Electronics Information Technologies
Related Grants:
Panel History:
Panel DatePanel NameOutcome
01 Mar 2016 EPSRC ICT Fellowships Interview Panel - Mar 2016 Announced
03 Feb 2016 EPSRC ICT Prioritisation Panel - Feb 2016 Announced
Summary on Grant Application Form
The computational demands of modern computer applications make the

pursuit of high performance more critical than ever, and mobile,

battery-powered devices, as well as concerns related to climate

change, require high performance to co-exist with energy-efficiency.

Due to physical limits, the traditional means for improving hardware

performance by increasing processor frequency now carries an

unacceptably high energy cost. Advances in processor fabrication

technology instead allow the construction of many-core processors,

where hundreds or thousands of processing elements are placed on a

single chip, promising high performance and energy-efficiency through

sheer volume of processing elements.

Many-core devices are present in practically all consumer devices,

including smartphones and tablets. As a result, the general public in

developed countries interact with many-core software daily. Many-core

technology is also used to accelerate safety-critical software in

domains such as medical imaging and autonomous vehicle navigation.

It is thus important that many-core software should be reliable. This

requires reliable software from programmers, but also a reliable

"stack" to support this software, including compilers that allow

software to execute on many-core devices, and the many-core devices

themselves. Recent work on formal verification and testing by myself

and other researchers has identified serious technical problems

spanning the many-core stack. These problems undermine confidence in

applications of many-core technology: defective many-core software

could risk fatal accidents in critical domains, and impact negatively

on users in other important application areas.

My long-term vision is that the reliability of many-core programming

can be transformed through breakthroughs in programming language

specification, formal verification and test case generation, enabling

automated tools to assist programmers and platform vendors in

constructing reliable many-core applications and language

implementations. The aim of this five-year Fellowship is to undertake

foundational research to investigate a number of open problems whose

solution is key to enabling this long-term vision.

First, I seek to investigate whether it is possible to precisely

express the intricacies of many-core programming language using formal

mathematics, providing a rigorous basis on which software and language

implementations can be constructed.

Second, I aim to tackle several open problems that stand in the way of

effective formal verification of many-core software, which would allow

developers to obtain strong guarantees that such software will operate

as required.

Third, I will investigate raising this level of rigour beyond

many-core languages. A growing trend is for applications to be written

in relatively simple, high-level representations, and then

automatically translated into high-performance many-core code. This

translation process must preserve the meaning of programs; I will

investigate methods for formally certifying that it does.

Fourth, I will formulate new methods for testing many-core language

implementations, exploiting the rigorous language definitions brought

by my approach to enable high test coverage of subtle language


Collectively, progress on these problems promises to enable a

*high-assurance* many-core stack. I will demonstrate one instance of

such a stack for the industry-standard OpenCL language and the PENCIL

high-level language, showing that high-level PENCIL programs can be

reliably compiled into rigorously-defined OpenCL, integrated with

verified library components, and deployed on thoroughly tested

implementations from many-core vendors.

Partnership with four leading many-core technology vendors, AMD, ARM,

Imagination Technologies and NVIDIA, provides excellent opportunities

for the advances the Fellowship makes to have broad industrial impact.
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.imperial.ac.uk