CAREER: Verifying Threaded Software Using Resource Bounds -- An Approach Towards Dependable Concurrency

软件开发正面临着向无处不在的并发编程的范式转变，产生了人类曾经创建的最复杂的技术构件之一的软件。并发编程给程序员带来了几种风险和危险，他们被令人费解和不可重现的并发程序行为以及逃避传统质量保证技术的新型错误所淹没。如果不解决这种情况，我们将进入一个软件普遍不可靠的时代，后果从程序员生产力崩溃到关键任务系统的灾难性故障。这个项目将采取措施应对并发软件危机，通过产生验证技术来帮助非专业程序员检测并发错误，或证明它们的缺失。该技术将面临验证方法经常遇到的并发爆炸问题。该项目的目标是一个框架，在该框架下，可以将对具有无限并发资源(如执行线程)的程序的分析合理地简化为在较小的常量资源约束下的分析，从而使状态空间的使用更加实用。因此，该项目将在很大程度上消除作为并发程序分析复杂性的主要原因的特定计算资源的影响。通过开发工具来检测并发程序中原本无法检测到的错误行为和漏洞，该项目将为避免迫在眉睫的软件质量危机做出贡献。

Software development is facing a paradigm shift towards ubiquitousconcurrent programming, giving rise to software that is among the mostcomplex technical artifacts ever created by humans. Concurrent programmingpresents several risks and dangers for programmers who are overwhelmed by puzzling and irreproducible concurrent program behavior, and by new types of bugs that elude traditional quality assurance techniques. If this situation is not addressed, we are drifting into an era of widespread unreliable software, with consequences ranging from collapsed programmer productivity, to catastrophic failures in mission-critical systems.This project will take steps against a concurrent software crisis, byproducing verification technology that assists non-specialist programmersin detecting concurrency errors, or demonstrating their absence. Theproposed technology will confront the concurrency explosion problem thatverification methods often suffer from. The project's goal is a frameworkunder which the analysis of programs with unbounded concurrency resources(such as threads of execution) can be soundly reduced to an analysis undera small constant resource bound, making the use of state space explorerspractical. As a result, the project will largely eliminate the impact ofunspecified computational resources as the major cause of complexity inanalyzing concurrent programs. By developing tools for detecting otherwise undetectable misbehavior and vulnerabilities in concurrent programs, the project will contribute its part to averting a looming software quality crisis.