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.