| EPSRC Reference: |
EP/N026314/1 |
| Title: |
Reliable Many-Core Programming |
| Principal Investigator: |
Donaldson, Professor AF |
| Other Investigators: |
|
| Researcher Co-Investigators: |
|
| Project Partners: |
|
| Department: |
Computing |
| Organisation: |
Imperial College London |
| Scheme: |
EPSRC Fellowship |
| Starts: |
03 October 2016 |
Ends: |
31 January 2019 |
Value (£): |
1,005,751
|
| EPSRC Research Topic Classifications: |
| Fundamentals of Computing |
|
|
| EPSRC Industrial Sector Classifications: |
| Electronics |
Information Technologies |
|
| Related Grants: |
|
| Panel History: |
|
|
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
features.
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
|
|
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.imperial.ac.uk |