Advanced Formal Verification Techniques for Heterogeneous Multi-core Programming

Lead Research Organisation: Imperial College London
Department Name: Dept of Computing

Abstract

Heterogeneous multi-core processors are key to complex computational problems such as real-time medical imaging, financial analysis and high-definition video, because of the increased processing power they make available. The reliability and probity of such applications is of critical importance, yet heterogeneous multi-core processors are notoriously difficult to program correctly. There is a need for analysis and verification techniques to help detect and fix errors early in the design of multi-core software. The development of such techniques is the aim of the proposed Fellowship research.The research will involve extending the capabilities of existing theoretical computer science techniques based on typechecking and model checking. Typechecking is a commonly used lightweight method for eliminating errors in computer programs: a basic typechecker will reject an invalid expression such as Hello + 1. More complex typechecking, based on session types , can allow a protocol between two parties in a system to be automatically checked. One part of the Fellowship research will involve extending the notion of session types to be applicable to heterogeneous multi-core processors. New typechecking methods will also be developed to help programmers deal with complex issues arising from the management of separate memory spaces in multi-core systems.Model checking is a technique for verifying hardware and software systems which attempts to find system bugs by checking an abstract model of the system. Model checking is less widely used than typechecking, but model checking techniques have recently been incorporated in software products from major vendors such as Microsoft. A major part of the fellowship research will involve developing advanced model checking techniques to help find errors associated with the dynamic behaviour of software for heterogeneous multi-core processors.Part of the research will involve developing a set of open-source tools based on the novel formal analysis techniques. Experience has shown that developers interested in multi-core programming are reluctant to adopt new languages and formalisms, and will only consider new techniques if they are easy and intuitive to use, and can be integrated into an existing development tool-chain. To increase the potential for eventual adoption by industry, the new techniques developed during the Fellowship research will involve regular input and advice from Codeplay Software Ltd., a UK based company specialising in development tools for multi-core processors.

Publications

10 25 50
publication icon
Amani S (2012) Automatic Verification of Message-Based Device Drivers in Electronic Proceedings in Theoretical Computer Science

publication icon
Betts A (2015) The Design and Implementation of a Verification Technique for GPU Kernels in ACM Transactions on Programming Languages and Systems

publication icon
Donaldson A (2012) Counterexample-guided abstraction refinement for symmetric concurrent programs in Formal Methods in System Design

Related Projects

Project Reference Relationship Related To Start End Award Value
EP/G051100/1 26/05/2009 01/09/2011 £235,502
EP/G051100/2 Transfer EP/G051100/1 01/11/2011 31/07/2012 £64,242
 
Description Please see details under EP/G051100/1: the current award EP/G051100/2 was a continuation of EP/G051100/1 after that award was transferred to Imperial College London, and the details under EP/G051100/1 summarise the findings and impact of both awards.
Exploitation Route Please see details under EP/G051100/1: the current award EP/G051100/2 was a continuation of EP/G051100/1 after that award was transferred to Imperial College London, and the details under EP/G051100/1 summarise the findings and impact of both awards.
Sectors Digital/Communication/Information Technologies (including Software),Education

 
Description FP7
Amount € 600,000 (EUR)
Funding ID 287767 
Organisation European Commission 
Sector Public
Country European Union (EU)
Start 11/2011 
End 02/2015
 
Description Intel Research Office
Amount $271,400 (USD)
Organisation Intel Corporation 
Sector Private
Country United States
Start 05/2013 
End 04/2016
 
Description Intel 
Organisation Intel Corporation
Country United States 
Sector Private 
PI Contribution We have been investigating formal verification techniques for high assurance device drivers.
Collaborator Contribution As well as funding, Intel have provided expertise and access to software.
Impact The partnership has led to submitted papers, but not yet to any published outputs.
Start Year 2013