SHF: Small: Concurrency with Specified Orders

并发编程的需求正在增长，特别是在多核革命之后。该项目旨在帮助并发程序员提高工作效率，并生产出更高质量的软件。这将对社会的软件基础设施至关重要。该项目将开发可轻松应用于许多主流编程语言(如C、Java和Scala)的通用技术。该项目的新颖性是指定顺序的概念，以及程序逻辑和众所周知的并发算法的机器检查证明。该项目的影响是并行编程的方法，允许程序员编写一次，证明一次，并在任何地方高效运行。研究人员将与一名博士生一起研究该项目，并将结果教授给本科和研究生课程的学生。对于并发程序，程序员经常面临他们对执行的假设与特定体系结构的内存模型之间的不匹配。例如，程序员可能需要执行两条指令才能使程序正确，但大多数体系结构的执行顺序都不正确。这个项目将使程序员能够指定这样的假设，证明正确性，并在各种各样的体系结构上高效运行。特定的顺序比现有的机制更容易理解、推理和优化，例如障碍(汇编语言)、原子排序(C)和挥发物(Java、Scala)。该奖项反映了NSF的法定使命，并通过使用基金会的智力优势和更广泛的影响审查标准进行评估，被认为值得支持。

The need for concurrent programming is growing, especially after the multi-core revolution. This project aims to help concurrent programmers be more productive and produce software of higher quality. This will be of paramount importance for society's software infrastructure. The project will develop general techniques that are easily applicable to many mainstream programming languages such as C++, Java, and Scala. The project's novelties are a notion of specified orders along with a program logic and machine-checked proofs of well-known concurrent algorithms. The project's impacts are approaches to concurrent programming that allow programmers to write once, prove once, and run efficiently anywhere. The investigator will work with a PhD student on the project and will teach the results to students in an undergraduate course and a graduate course.For concurrent programs, programmers often face a mismatch between their assumptions about execution and the memory model of a specific architecture. For example, a programmer may need two instructions to execute in order for the program to be correct, yet most architectures execute out of order. This project will enable programmers to specify such assumptions, prove correctness, and run efficiently on a wide variety of architectures. Specified orders are easier to understand, reason with, and optimize than existing mechanisms such as barriers (assembly language), atomic orderings (C++), and volatiles (Java, Scala).This award reflects NSF's statutory mission and has been deemed worthy of support through evaluation using the Foundation's intellectual merit and broader impacts review criteria.