SHF: Small: Semantics, Static Analysis, and Refencing of Concurrent Programs with Weak Memory Models

SHF：小型：具有弱内存模型的并发程序的语义、静态分析和引用

• 批准号: 1617717
• 负责人: Patrick Cousot
• 金额: $ 48.14万
• 依托单位: New York University
• 依托单位国家: 美国
• 项目类别: Standard Grant
• 财政年份: 2016
• 资助国家: 美国
• 起止时间: 2016-09-01 至 2020-08-31
• 项目状态: 已结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=1617717&HistoricalAwards=false
• 关键词: SHF; Small; Semantics; Static; Analysis

Modern computers have parallel multicore architectures sharing ahierarchy of caches and memories from fast and expensive ones to largeand cheaper ones. The consequence is that not all cores runningconcurrently see the shared memory in the same way: some see newlystored values while others see older ones. This is called weakconsistency models for shared memory on a single chip or memorydistributed on several chips or on networks. This modern design makes the task of designing and programming parallel computers very complex. In particular the same program may have very different behaviors when running on different architectures whereas the same program had the same effect on allmachines of the previous generation. This project define a generic formal semantics of parallel programs with weak consistency models parameterized by a formal definition of the computer architecture. Based on this parameterized semantics, the project investigates invariance proof methods to be used by programmers and verification tools to prove properties of parallel programs with weak consistency models. The project contributes to formal methods and tools for concurrent programming which, by the foreseeable evolution of hardware design, will be inevitable in the future.The publications and prototypes from this project are widely disseminated.

现代计算机拥有并行的多核体系结构，共享从快速而昂贵的高速缓存和存储器到大型而廉价的高速缓存和存储器的层次结构。结果是，并不是所有同时运行的内核都以相同的方式看到共享内存：一些内核看到的是新存储的值，而另一些内核看到的是较旧的值。对于单个芯片上的共享内存或分布在多个芯片或网络上的内存，这称为弱一致性模型。这种现代的设计使得设计和编程并行计算机的任务变得非常复杂。特别是，当相同的程序在不同的体系结构上运行时，可能具有非常不同的行为，而相同的程序在上一代的所有机器上具有相同的效果。该项目定义了一种通用的并行程序的形式化语义，该程序具有由计算机体系结构的形式化定义参数化的弱一致性模型。基于这种参数化语义，该项目研究了程序员和验证工具所使用的不变性证明方法，以证明具有弱一致性模型的并行程序的性质。该项目为并发编程提供了形式化的方法和工具，通过硬件设计的可预见的发展，这将是未来不可避免的。该项目的出版物和原型被广泛传播。