CAREER: Engineering High-Quality Concurrent Software

一个综合的研究计划将开发用于构建并发软件的技术以及用于指定并发软件的属性和验证并发软件的技术。 并行软件的构造由工程协调抽象支持，这些抽象捕获通信、同步和进程互连的公共模式。 这项工作的重点是发展的抽象，满足一类现实世界的问题，特别是科学计算问题的需求。 这些抽象的有效性进行评估，将其应用到现实世界的问题的解决方案。 使用抽象和替代并发编程技术开发的解决方案的开发成本的测量将形成实证评估的基础，以表征协调抽象的相对优点。 使用FLAVERS程序流分析方法研究并发软件正确性规范的验证问题。 这项工作的重点是纳入FLAVERS的抽象，以提高分析的速度和分析结果的准确性。 评估FLAVERS的有效性进行评估，通过将其应用到验证常见的类的正确性属性和现实世界的并发应用程序，如那些建立与协调抽象。

An integrated program of research will develop techniques for building concurrent software and techniques for specifying properties of and validating concurrent software. The construction of concurrent software is supported by engineering coordination abstractions that capture common patterns of communication, synchronization and process inter- connectivity. This work focuses on development of abstractions that satisfy the needs of a class of real-world problems, specifically scientific computing problems. The effectiveness of these abstractions is evaluated by applying them to the solution of real-world problems. Measurement of development costs for solutions developed using abstractions and alternative concurrent programming technologies will form the basis of empirical evaluation to characterize the relative merits of coordination abstractions. The validation of specifications of correctness properties of concurrent software is investigated using a program flow analysis called FLAVERS. This work focuses on incorporation of abstractions in FLAVERS to increase both the speed of analysis and the accuracy of analysis results. Evaluation of the effectiveness of FLAVERS is assessed by applying it to the verification of common classes of correctness properties and to real-world concurrent applications, such as those built with coordination abstractions.