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

SHF：小型：协作研究：同步性：根据顺序和协作规范合成并发软件的框架

基本信息

批准号：
1813133
负责人：
Cormac Flanagan
金额：
$ 30万
依托单位：
University of California-Santa Cruz
依托单位国家：
美国
项目类别：
Standard Grant
财政年份：
2018
资助国家：
美国
起止时间：
2018-10-01 至 2021-09-30
项目状态：
已结题

来源：
https://www.nsf.gov/awardsearch/showAward?AWD_ID=1813133&HistoricalAwards=false
关键词：
SHF Small Collaborative Research Synchronicity

项目摘要

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.

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