SHF: Small: Symbolic Commutativity Analysis for Multicore Concurrency

SHF：小型：多核并发的符号交换性分析

• 批准号: 2008633
• 负责人: Eric Koskinen
• 金额: $ 49.59万
• 依托单位: Stevens Institute of Technology
• 依托单位国家: 美国
• 项目类别: Standard Grant
• 财政年份: 2020
• 资助国家: 美国
• 起止时间: 2020-06-01 至 2023-05-31
• 项目状态: 已结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=2008633&HistoricalAwards=false
• 关键词: SHF; Small; Symbolic; Commutativity; Analysis

Modern software applications need results to be computed quickly as a matter of practicality, system safety or even security. Unfortunately, CPU speeds themselves are no longer increasing as they used to and hardware companies, instead, offer multicore CPUs. This poses a classical, but notoriously difficult problem: how to divide software programs into multiple interoperating tasks, that can execute concurrently, without stepping on each others' feet. It is well-known that data structure "commutativity" is one route to concurrency. Intuitively, two data-structure operations commute, provided that they can be executed in either order. In this way, commutativity characterizes the independence of program fragments. In recent years, researchers have shown that this can enable concurrency in contexts such as transactional memory, optimistic concurrency, runtime systems and parallelizing compilers. However, it remains an open question as to how to safely extract commutativity information from source code.This project is developing techniques to automatically verify and even synthesize commutativity from source code. Further, this commutativity is employed (integrated with so-called linearizability) in a new parallelizing compiler and transactional object system. These new tools enable programmers to focus on writing correct sequential programs, and yet automatically exploit multicore architectures. The impacts of this work include advances in mathematical foundations, algorithms, symbolic program analysis, compilers and runtime systems. The project also involves engagement with students through multiple tiers of education - ranging from pre-college math students to summer school modules - and outreach aimed at broadening participation of underrepresented groups.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.

现代软件应用程序需要快速计算结果，这是出于实用性、系统安全性甚至安全性的考虑。不幸的是，CPU速度本身不再像过去那样增加，硬件公司转而提供多核CPU。这提出了一个经典的，但众所周知的困难的问题：如何将软件程序划分为多个互操作的任务，可以并发执行，而不会踩在对方的脚。众所周知，数据结构的“可交换性”是实现并发性的一条途径。直观地说，两个数据结构操作可以互换，只要它们可以以任何顺序执行。这样，可交换性表征了程序片段的独立性。近年来，研究人员已经表明，这可以在事务内存，乐观并发，运行时系统和并行编译器等环境中实现并发。然而，如何安全地从源代码中提取交换性信息仍然是一个悬而未决的问题。本项目正在开发自动验证甚至从源代码合成交换性的技术。此外，这种交换性（与所谓的线性化集成）在一个新的并行编译器和事务对象系统。这些新工具使程序员能够专注于编写正确的顺序程序，同时自动利用多核架构。这项工作的影响包括数学基础，算法，符号程序分析，编译器和运行时系统的进步。 该项目还包括通过多层次教育（从大学预科数学学生到暑期学校模块）与学生互动，以及旨在扩大代表性不足群体参与的外联活动。该奖项反映了NSF的法定使命，并通过使用基金会的智力价值和更广泛的影响审查标准进行评估，被认为值得支持。

项目成果

Decomposing Data Structure Commutativity Proofs with $m\!n$-Differencing

用 $m!n$ 差分分解数据结构交换性证明

• DOI: 10.1007/978-3-030-67067-2_5
• 发表时间: 2021
• 期刊: ACM Transactions on Computer Systems (TOCS)
• 作者: Eric Koskinen;Kshitij Bansal
• 通讯作者: Kshitij Bansal

Veracity: declarative multicore programming with commutativity

• DOI: 10.1145/3563349
• 发表时间: 2022-03
• 期刊: Proceedings of the ACM on Programming Languages
• 作者: A. Chen;Parisa Fathololumi;Eric Koskinen;Jared Pincus

Better Predicate Pruning and Heuristics for Commutativity Synthesis

更好的谓词修剪和启发式交换性综合

• 发表时间: 2023
• 期刊: International Symposium on Automated Technology for Verification and Analysis
• 作者: Chen, Adam;Brennan, Tegan;Fathololumi, Parisa;Koskinen, Eric;Nicola, Mihai;Pincus, Jared
• 通讯作者: Pincus, Jared