权益分类	功能权益	普通用户	{{item.name}}会员
{{category.name}}	{{benefitItem.name}}

Lina4WM Linearizability Proofs for Weak Memory Models

Lina4WM 弱内存模型的线性化证明

基本信息

批准号：
163003744
负责人：
Professorin Dr. Heike Wehrheim
金额：
--
依托单位：
Department für Informatik
依托单位国家：
德国
项目类别：
Research Grants
财政年份：
2010
资助国家：
德国
起止时间：
2009-12-31 至 2017-12-31
项目状态：
已结题

来源：
https://gepris.dfg.de/gepris/projekt/163003744?language=en
关键词：
Lina4WM Linearizability Proofs Weak Memory

项目摘要

Today, parallel programs are often actually run on multi-core machines and therefore executed truly concurrent. This can considerably improve the performance of parallel programs. The increased performance does however come at some price: the memory models of multi-core machines are much weaker than the commonly assumed sequentially consistent memory models. This leads to unexpected executions of parallel programs and ultimately to errors. The project Lina4WM investigates the correctness of a specific class of parallel programs on weak memory models. The class of programs consists of so-called concurrent data structures, i.e., algorithms which allow for a concurrent access to data structures like stacks, queues or hash tables. Such algorithms are highly optimized for concurrency and also contain data races. They are therefore particularly vulnerable to weak memory model effects. The project aims at the development of a proof methodology for the correctness of concurrent data structures on weak memory models. The key correctness criterion for parallel data structures is linearizability. The basis of the proof methodology are machine assisted simulation proofs. The project will thus work on simulation based proofs of linearizability of concurrent data structures on multi-core machines.

如今，并行程序通常在多核机器上运行，因此可以真正地并行执行。这可以大大提高并行程序的性能。然而，性能的提高是有代价的：多核机器的内存模型比通常假设的顺序一致的内存模型弱得多。这将导致并行程序的意外执行，并最终导致错误。Lina4WM项目研究了一类特定的并行程序在弱内存模型上的正确性。这类程序由所谓的并发数据结构组成，即允许并发访问堆栈、队列或哈希表等数据结构的算法。这些算法针对并发性进行了高度优化，同时也包含数据竞争。因此，它们特别容易受到弱记忆模型效应的影响。该项目旨在开发一种证明方法，用于在弱内存模型上并发数据结构的正确性。并行数据结构的关键正确性准则是线性化。证明方法的基础是机器辅助仿真证明。因此，该项目将在多核机器上对并发数据结构的线性性进行基于仿真的证明。