SHF: Small: Concurrency with Specified Orders

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

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.