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

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

基本信息

批准号：
1812951
负责人：
Stephen Freund
金额：
$ 20万
依托单位：
Williams College
依托单位国家：
美国
项目类别：
Standard Grant
财政年份：
2018
资助国家：
美国
起止时间：
2018-10-01 至 2022-09-30
项目状态：
已结题

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

项目摘要

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的法定任务，并且使用基金会的知识分子优点和更广泛的影响审查标准，被认为值得通过评估来支持。