SHF: Medium: A Code-Centric Approach to Specifying, Checking, and Discovering Shared-Memory Communication

SHF：Medium：以代码为中心的方法来指定、检查和发现共享内存通信

• 批准号: 1064497
• 负责人: Daniel Grossman
• 金额: $ 90.12万
• 依托单位: University of Washington
• 依托单位国家: 美国
• 项目类别: Continuing Grant
• 财政年份: 2011
• 资助国家: 美国
• 起止时间: 2011-08-01 至 2016-07-31
• 项目状态: 已结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=1064497&HistoricalAwards=false
• 关键词: SHF; Medium; Code; Centric; Approach

This project aims to improve the practice of shared-memory concurrent programming by exploring a fundamentally new way to specify, verify, test, and monitor how threads communicate via memory. Shared-memory concurrency has become an increasingly important style of programming because it is a common way to utilize multicore processors, i.e., machines where there is more than one processing core, and desktops, laptops, servers, and even mobile devices are increasingly multicore. Shared-memory concurrency is widely recognized as difficult and error-prone, and much prior work has aimed to detect bugs related to this style automatically. This project complements prior work by focusing on application-specific specifications in terms of how different parts of the code-base use concurrency to communicate, rather than focusing on how individual pieces of data are used. This approach aims to improve the quality of software used throughout society, to improve the productivity of software developers and testers, and to influence how students are taught concurrent programming.At the heart of the approach is a communication graph in which the nodes are program points and the edges indicate communication via shared memory. That is, for each edge, the code that the source node represents performs a write in one thread that is subsequently read in another thread by the code that the target node represents. Such graphs can form the foundation for conceptual and intellectual tools useful throughout the development and maintenance of software, including specifications (declarations of what communication is allowed), static checking (program analysis to infer possible communication), dynamic checking (efficient run-time communication monitoring), testing (design/evaluation of a test-suite in terms of communication coverage), and automatic anomaly detection and bug isolation (in terms of unexpected communication) for deployed software. This project is developing and evaluating tools inspired by this foundation, leveraging synergies across the execution stack, including work on computer architecture, run-time systems, compilers, programming languages, automatic testing, and static analysis.

该项目旨在通过探索一种全新的方法来指定、验证、测试和监视线程如何通过内存进行通信，从而改进共享内存并发编程的实践。共享内存并发已经成为一种越来越重要的编程风格，因为它是利用多核处理器的常见方式，即具有多个处理核心的机器，台式机、笔记本电脑、服务器，甚至移动设备都越来越多核。共享内存并发被广泛认为是困难和容易出错的，以前的许多工作都旨在自动检测与这种风格相关的错误。本项目是对以前工作的补充，它侧重于特定于应用程序的规范，即代码库的不同部分如何使用并发进行通信，而不是侧重于如何使用单个数据段。该方法旨在提高全社会使用的软件的质量，提高软件开发人员和测试人员的生产率，并影响学生学习并发编程的方式。该方法的核心是一个通信图，其中节点是程序点，边表示通过共享内存进行通信。也就是说，对于每条边，源节点表示的代码在一个线程中执行写入，该线程随后由目标节点表示的代码在另一个线程中读取。这些图表可以形成整个软件开发和维护过程中有用的概念性和智能化工具的基础，包括规范(允许什么通信的声明)、静态检查(推断可能的通信的程序分析)、动态检查(有效的运行时通信监控)、测试(根据通信覆盖设计/评估测试套件)，以及部署软件的自动异常检测和错误隔离(根据意外通信)。该项目正在开发和评估受此基础启发的工具，利用整个执行堆栈的协同效应，包括计算机体系结构、运行时系统、编译器、编程语言、自动测试和静态分析方面的工作。