SHF: Small: Ordering-Based Semantics for Emerging Models of Parallel Computing

SHF：小型：并行计算新兴模型的基于排序的语义

• 批准号: 1116055
• 负责人: Michael Scott
• 金额: $ 49.75万
• 依托单位: University of Rochester
• 依托单位国家: 美国
• 项目类别: Standard Grant
• 财政年份: 2011
• 资助国家: 美国
• 起止时间: 2011-08-01 至 2015-07-31
• 项目状态: 已结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=1116055&HistoricalAwards=false
• 关键词: SHF; Small; Ordering; Based; Semantics

With the proliferation of multicore processors has come resurgenceof interest in parallel programming languages and models,particularly those intended to make it easier for non-expertprogrammers to correctly implement important classes of parallelapplications. Unfortunately, most such languages and models are informally -- and thus imprecisely -- defined. The aim of the sponsored research is to develop more formal definitions, which willbe needed in order to truly understand and reason about programs,guide language implementations, and verify implementationcorrectness. Within computer science and allied fields, formaldefinitions will facilitate the transition to ubiquitous parallelcomputing. For society at large, this transition will be essentialto maintain the momentum of the IT revolution, across government,industry, science, the arts, and entertainment.The technical core of the sponsored research is the use ofhistory-based executions to capture both the behavior of individualthreads of control and the interactions among those threads. In adeparture from previous work, the interactions are always expressedin terms of atomic blocks, which can capture arbitrarylanguage-level synchronization mechanisms. Specific topics beingaddressed include transactional memory (including the concepts ofpublication and privatization), explicit speculation, and determinism. The notion of determinism, in particular, is centralto several emerging languages and models specifically intended for non-expert programmers. A formal framework for the definition ofdeterminism will allow alternative definitions to be compared,contrasted, and correctly implemented.

随着多核处理器的普及，人们对并行编程语言和模型重新产生了兴趣，特别是那些旨在使非专家程序员更容易正确实现重要类并行应用程序的语言和模型。 不幸的是，大多数这样的语言和模型都是非正式的，因此定义得不精确。 赞助研究的目的是开发更正式的定义，这将是为了真正理解和推理程序所需要的，指导语言实现，并验证实现的正确性。 在计算机科学和相关领域，形式化的定义将促进向无处不在的并行计算的过渡。 对于整个社会来说，这种转变对于保持IT革命的势头至关重要，包括政府、工业、科学、艺术和娱乐。赞助研究的技术核心是使用基于历史的执行来捕获单个控制线程的行为以及这些线程之间的交互。 与以前的工作不同，该方法的交互总是用原子块来表示，它可以捕获任意语言级别的同步机制。 具体的主题包括事务性记忆（包括公开和私有化的概念）、明确的推测和决定论。 特别是决定论的概念，是几种专门为非专业程序员设计的新兴语言和模型的核心。 一个正式的框架定义ofdeterminism将允许替代定义进行比较，对比，并正确地实施。

项目成果

Leveraging hardware TM in Haskell

在 Haskell 中利用硬件 TM

• DOI: 10.1145/3293883.3295711
• 发表时间: 2019
• 期刊: Proceedings of the 24th Symposium on Principles and Practice of Parallel Programming
• 作者: Yates, Ryan;Scott, Michael L.
• 通讯作者: Scott, Michael L.