Verification of Shared-Memory Concurrent Software

点击翻译按钮获取中文摘要

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.