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

随着多核处理器的激增，人们对并行编程语言和模型重新产生了兴趣，特别是那些旨在使非专业程序员更容易正确实现重要的并行应用程序类的编程语言和模型。不幸的是，大多数这样的语言和模型都是非正式定义的，因此也不是很精确。赞助研究的目的是开发更正式的定义，以便真正理解和推理程序，指导语言实现，并验证实现的正确性。在计算机科学和相关领域，形式定义将促进向无处不在的并行计算的过渡。对于整个社会来说，这种转变对于保持IT革命的势头至关重要，涉及政府、工业、科学、艺术和娱乐业。受赞助研究的技术核心是使用基于历史的执行来捕捉各个控制线程的行为和这些线程之间的交互。在前人工作的基础上，交互总是用原子块来表示，这可以捕获任意语言级的同步机制。讨论的具体主题包括事务性内存(包括发布和私有化的概念)、显式推测和决定论。决定论的概念尤其集中在几种专门为非专业程序员设计的新兴语言和模型中。决定论定义的正式框架将允许对备选定义进行比较、对比和正确实施。

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.