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

美国的计算基础设施在从小型移动设备到大型数据中心的整个系统范围内使用多核处理器和多处理器硬件。与单处理器系统相比，这些系统提供了更高的性能和可伸缩性，但代价很大：编写正确的并发软件是出了名的困难。程序员必须非常小心地协调并发运行的线程之间的同步，以避免意外干扰，同时尽可能消除同步，以避免性能瓶颈。为了应对这一挑战，该项目开发了Synchronicity工具，以根据所需行为的简单规范自动合成高性能并发软件。这项研究有可能通过消除关于并发代码的昂贵的手动编写、测试和推理过程来降低开发计算基础设施的成本，并可能减少满足计算需求所需的硬件资源和能量。同步性从程序员提供的适合在单个线程上执行的软件组件的初始描述开始。然后，它使用反例引导的归纳合成来搜索符合该规范的线程安全并发组件。同步性使用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.