SHF: Medium: Formal Analysis of Concurrent Software on Relaxed Memory Models

程序员越来越多地设计并行软件，以有效地利用多处理器和多核体系结构的计算能力。编写正确的并发软件具有挑战性，特定于系统的并发库特别容易受到攻击，因为它们受到多处理器系统中管理共享内存读写关系的微妙而复杂的规则的影响。这个项目的目标是开发一种技术，它将帮助程序员构建高性能和正确的系统级并发软件，并对底层体系结构的基本细节进行精确建模。研究人员将探索基于约束和操作风格的实验和商业存储模型的精确机器可读描述规范。为了让开发人员理解特定内存模型的微妙之处，这个项目将研究算法和工具，用于检查两个规范之间的等价性，并自动生成显示差异的测试程序。将在常用数据结构的无锁实现上开发和评估用于验证与内存模型规范相关的并发库和用于自动插入内存排序围栏的工具。建议的研究将被整合到一个新的多处理器程序设计的高级课程中。

Programmers are increasingly designing concurrent software to effectively harness the computational power of multi-processor and multi-core architectures. Writing correct concurrent software is challenging, and system-specific concurrency libraries are particularly vulnerable in that they are affected by the subtle and complex rules governing the relationship among reads and writes to shared memory in multi-processor systems. The goal of this project is to develop technology that will assist programmers in building high-performance and correct system-level concurrent software with respect to precise modeling of the essential details of the underlying architecture. The investigators will explore specifications for accurate machine-readable descriptions of experimental and commercial memory models in both constraint-based and operational styles. To allow developers to understand subtleties of specific memory models, this project will investigate algorithms and tools for checking equivalence between two specifications and for automatically generating test programs that exhibit the differences. Tools for verifying concurrency libraries with respect to memory model specifications and for automatic insertion of memory ordering fences, will be developed and evaluated on lock-free implementations of commonly used data structures. The proposed research will be integrated in a new upper-level course on multiprocessor programming.