SHF: Small: Concurrency with Specified Orders

SHF：小：指定订单并发

• 批准号: 1815496
• 负责人: Jens Palsberg
• 金额: $ 39.6万
• 依托单位: University of California-Los Angeles
• 依托单位国家: 美国
• 项目类别: Standard Grant
• 财政年份: 2018
• 资助国家: 美国
• 起止时间: 2018-10-01 至 2024-09-30
• 项目状态: 已结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=1815496&HistoricalAwards=false
• 关键词: SHF; Small; Concurrency; Specified; Orders

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.

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

项目成果

Sound and efficient concurrency bug prediction

• DOI: 10.1145/3468264.3468549
• 发表时间: 2021-08
• 期刊: Proceedings of the 29th ACM Joint Meeting on European Software Engineering Conference and Symposium on the Foundations of Software Engineering
• 作者: Yan Cai;Hao Yun;Jinqiu Wang;L. Qiao;J. Palsberg

A formalization of Java’s concurrent access modes

Java 并发访问模式的形式化

• DOI: 10.1145/3360568
• 发表时间: 2019
• 期刊: Proceedings of the ACM on Programming Languages
• 作者: Bender, John;Palsberg, Jens
• 通讯作者: Palsberg, Jens

Low-Overhead Deadlock Prediction

• DOI: 10.1145/3377811.3380367
• 发表时间: 2020-06
• 期刊: 2020 IEEE/ACM 42nd International Conference on Software Engineering (ICSE)
• 作者: Yan Cai;Ruijie Meng;J. Palsberg

Compiling Volatile Correctly in Java

在 Java 中正确编译 Volatile

• 发表时间: 2022
• 期刊: 36th European Conference on Object-Oriented Programming (ECOOP 2022
• 作者: Liu, Shuyang;Bender, John;Palsberg, Jens
• 通讯作者: Palsberg, Jens