CPA-CPL: Scalable Analysis for Concurrent Programs

并发是几乎所有关键计算基础设施（包括操作系统、数据库、internet路由表和银行系统）的普遍特性。此外，最近的一些技术趋势，如广泛采用多核处理器、面向web的体系结构和点对点系统，使得并发性在主流系统中比以往任何时候都更加重要。不幸的是，并发系统很难构建，因为程序员很难在心里考虑这些并发系统可以交互的许多可能方式。这项研究的广泛目标是为程序员提供开发可靠、高效和健壮的并发系统所需的工具。研究人员将把他们的努力集中在一种特定的工具上，即静态分析工具。事实上，静态算法在程序优化和错误检测方面的进步表明，静态分析可以显著提高计算机系统的可靠性和性能。然而，大多数这些算法的进步仅限于顺序程序，而忽略了并发带来的挑战，其中需要静态检查和优化的潜力是最大的。本研究将为并发程序开发可扩展和精确的分析技术。然而，同时实现可伸缩性和精确性是很困难的，因为这两个目标之间存在公认的紧张关系。为了应对这一挑战，一般的方法将是首先设计可靠且可伸缩的分析（可能以牺牲精度为代价），然后通过经验识别常见的并发编程习惯，在这些习惯中我们的分析失去了精度，并开发针对这些习惯的分析技术，从而迭代地改进这些分析。

Concurrency is a prevalent feature of almost all critical computing infrastructure, including operating systems, databases, internet-routing tables, and banking systems. Furthermore, several recent trends in technology, such as the widespread adoption of multi-core processors, web-service-oriented architectures, and peer-to-peer systems, are making concurrency more important than ever in mainstream systems. Unfortunately, concurrent systems are hard to build, because programmers have a hard time mentally accounting for the many possible ways in which these concurrent systems can interact. The broad goal of this research is to provide programmers with the tools they need to develop concurrent systems that are reliable, efficient and robust.The investigators will focus their efforts on one particular kind of tool, namely static analysis tools. Indeed, advances in static algorithms for program optimization and error detection have shown that static analysis can dramatically improve the reliability and performance of computer systems. However, most of these algorithmic advances are limited to sequential programs and ignore the challenges introduced by concurrency, where the need for static checking and potential for optimization are the greatest.This research will develop scalable and precise analysis techniques for concurrent programs. Achieving scalability and precision at the same time, however, is difficult because there is a widely acknowledged tension between these two goals. To address this challenge, the general methodology will be to design analyses that are sound and scalable first (likely at the expense of precision), and then to iteratively refine these analyses by empirically identifying the common concurrent programming idioms where our analyses lose precision, and developing analysis techniques targeted at these idioms.