SHF: Small: Symbolic Commutativity Analysis for Multicore Concurrency

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

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.