SHF: Small: Collaborative Research: Synchronicity: A Framework for Synthesizing Concurrent Software from Sequential and Cooperative Specifications

美国的计算基础设施在从小型移动的设备到大型数据中心的整个系统范围内使用多核处理器和多处理器硬件。 这些系统提供了比单处理器系统更高的性能和扩展能力，但代价很大：编写正确的并发软件是众所周知的挑战。 程序员必须非常小心地协调并发运行的线程之间的同步，以避免意外的干扰，同时尽可能消除同步以避免性能瓶颈。 为了解决这一挑战，该项目开发的同步工具，自动合成高性能并发软件从所需的行为的简单规范。 这项研究有可能降低开发计算基础设施的成本，通过消除手动编写，测试和推理并发代码的昂贵过程，它可以减少硬件资源和能源，以满足计算需求。 同步性开始于程序员提供的适合在单个线程上执行的软件组件的初始描述。 然后使用反例引导的归纳合成来搜索符合该规范的线程安全并发组件。同步性使用Lipton归约理论的扩展形式验证线程安全性。 可以找到多个线程安全的并发解决方案，并且Synchronicity会根据它们在程序员提供的工作负载上的性能自动进行排名。该项目致力于增加所有学生接受科学教育的机会，包括妇女、代表性不足的群体和第一代大学生。研究人员包括来自这些团体的本科生和研究生。该奖项反映了NSF的法定使命，并被认为值得通过使用基金会的智力价值和更广泛的影响审查标准进行评估来支持。

The nation's computing infrastructure utilizes multicore processors and multiprocessor hardware across the entire spectrum of systems from small mobile devices to huge data centers. These systems offer increased performance and scaling over single-processor systems, but at a significant cost: writing correct concurrent software is notoriously challenging. Programmers must take extreme care to orchestrate synchronization between concurrently running threads to avoid unintended interference while simultaneously eliminating synchronization whenever possible to avoid performance bottlenecks. To address this challenge, this project develops the Synchronicity tool to automatically synthesize high-performance concurrent software from simple specifications of the desired behavior. This research has the potential to reduce the costs of developing computing infrastructure, by eliminating the costly process of manually writing, testing, and reasoning about concurrent code, and it may reduce the hardware resources and energy required to meet computing needs. Synchronicity starts with an initial programmer-provided description of a software component suitable execution on a single thread. It then uses counterexample-guided inductive synthesis to search for thread-safe concurrent components conforming to that specification. Synchronicity verifies thread safety using an extended form of Lipton's theory of reduction. Multiple thread-safe concurrent solutions may be found, and Synchronicity automatically ranks according to their performance on a programmer-supplied workload. The project is committed to increasing access to science education for all students, including women, under-represented groups, and first-generation college students. The investigators include students from these groups in this research, at both the undergraduate and graduate level.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.