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.