Verification of Shared-Memory Concurrent Software

Lead Research Organisation: University of Oxford
Department Name: Computer Science

Abstract

Software products are becoming increasingly complex. One of the chiefreasons for this is the demand for concurrent software thatefficiently exploits multiple execution cores. Such systems, such asIntel's Core Duo, have become ubiquitous over the last two or threeyears. Unfortunately, developing reliable concurrent programs is adifficult and specialised task, requiring highly skilled engineers,most of whose efforts are spent on the testing and validationphases. As a result, there is a strong economic andstrategic incentive for software houses to automate parts of theverification process.Random simulation and testing, while automated, has severelimitations, particularly in the case of concurrent software, in whichthe plethora of possible thread interleavings often conspires toconceal design flaws. Formal verification, on the other hand, can alsobe automated, and tools that implement it check a concurrent programfor all its possible behaviours.Numerous tools to hunt down functional flaws in hardware designs have beenavailable commercially for a number of years. The use of such tools iswidespread, and there is a broad range of vendors. In contrast, the marketfor formal tools that address the need for quality software---and even moreso for concurrent software---is still in its infancy.The proposed research project focuses on shared-variableconcurrency, i.e., eliminating programming errors related tomulti-threaded programs in which the threads communicate via a sharedportion of the memory. This programming paradigm is frequently used,and is the predominant form of concurrency on commodity computingsystems. Furthermore, errors relating to concurrency often depend onthe process schedule, which is difficult to control. As a consequence,such errors are difficult to test for and to reproduce, yet can havewide-ranging and potentially devastating consequences.We propose to investigate (i) verification by means of automatedsummarisation of threads, (ii) identification of transactions,enabling partial-order reductions, and (iii) Craiginterpolation to derive thread invariants. Our primary target arelow-level applications written in C/C++, and we will supportboth the POSIX thread API and the WIN32 thread API to maximizethe applicability of our research. We will evaluate the benefit of ourmethods and tools in collaboration with industrial users.

Publications

10 25 50
publication icon
Alglave J (2014) Computer Aided Verification

publication icon
Alglave J (2013) Computer Aided Verification

publication icon
Brain M (2013) Deciding floating-point logic with abstract conflict driven clause learning in Formal Methods in System Design

publication icon
Chen H (2017) Bit-Precise Procedure-Modular Termination Analysis in ACM Transactions on Programming Languages and Systems

publication icon
D'Silva V (2013) Abstract conflict driven learning in ACM SIGPLAN Notices

publication icon
D'Silva V (2012) Static Analysis

publication icon
David C (2018) Program Synthesis for Program Analysis in ACM Transactions on Programming Languages and Systems

 
Description Software products are becoming increasingly complex, and one of the chief reasons for this is the demand for concurrent software that efficiently exploits multi-core hardware. Such systems are now commonplace in everything from mobile phones to medical devices. Unfortunately developing reliable concurrent programs is a difficult and specialised task, requiring highly skilled engineers, most of whose efforts are spent on the testing and validation phases. This project worked towards automating parts of the verification process, focusing on eliminating programming errors related to multi-threaded programs in which the threads communicate via a shared portion of the memory. We have further developed CBMC, a Bounded Model Checker for ANSI-C and C++ programs. This tool is in use at IBM and won the gold medal in the Competition on Software Verification in 2014. Our research findings have been used to validate parts of the linux kernel, now used on mobile phones worldwide.
Exploitation Route The main beneficiaries of our work will be (i) other researchers in both academia and industry, who will be able to leverage our ideas and algorithms in the context of their own research, and (ii) industries for which software quality is of critical importance, such as those required to provide evidence of third-party safety certification (SIL3 or above) for their software. We have released binaries, source code and the papers proofs on our website.
Sectors Digital/Communication/Information Technologies (including Software),Electronics,Energy,Financial Services, and Management Consultancy,Healthcare,Manufacturing, including Industrial Biotechology,Security and Diplomacy,Transport

URL http://www.cprover.org/wmm/
 
Description There exists an extensive range of applications for CBMC, the software tool further developed by this grant, for full details see http://www.cprover.org/cbmc/applications.shtml. CBMC has been used in the automotive industry for checking functionality of software, for verification of C code in pacemakers, for analysing driver interactions with semi-autonomous vehicles, and for run-time verification in ultra-critical systems used in aircraft. Tools using our technology are being sold by BTC embedded systems, Tata Consulting Services and used in-house by Toyota Motor Corporation.
First Year Of Impact 2011
Sector Digital/Communication/Information Technologies (including Software),Electronics,Energy,Financial Services, and Management Consultancy,Healthcare,Manufacturing, including Industrial Biotechology,Transport
Impact Types Economic