Verification of Shared-Memory Concurrent Software

软件产品正变得越来越复杂。其中一个主要原因是对有效利用多个执行核心的并发软件的需求。在过去的两三年里，这样的系统，如英特尔的Core Duo，已经变得无处不在。不幸的是，开发可靠的并发程序是一项困难而专业的任务，需要高技能的工程师，他们的大部分精力都花在测试和验证阶段。因此，软件公司有强烈的经济和战略动机来自动化部分验证过程。随机模拟和测试虽然是自动化的，但有几个限制，特别是在并发软件的情况下，在这种情况下，过多的可能的线程交叉通常会合谋掩盖设计缺陷。另一方面，形式验证也可以是自动化的，实现它的工具检查并发程序的所有可能行为。许多工具可以在商业上找到硬件设计中的功能缺陷。这类工具的使用很广泛，供应商也很多。相比之下，解决高质量软件需求的正式工具市场--甚至更多的并发软件需求--仍处于初级阶段。拟议的研究项目专注于共享变量并发，即消除与多线程程序相关的编程错误，在多线程程序中，线程通过共享内存部分进行通信。这种编程范例经常被使用，并且是商品计算系统上的主要并发形式。此外，与并发性相关的错误通常依赖于进程调度，这很难控制。因此，这样的错误很难测试和复制，但可能会产生广泛的和潜在的破坏性后果。我们建议研究(I)通过自动总结线程的方法进行验证，(Ii)识别事务，使偏序减少，以及(Iii)CraigInterpolation导出线程不变量。我们的主要目标是用C/C++编写的低级应用程序，我们将同时支持POSIX线程API和Win32线程API，以最大限度地提高我们研究的适用性。我们将与工业用户合作，评估我们的方法和工具的好处。

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.