Lazy sequentialization for TSO and PSO via shared memory abstractions
Lazy sequentialization for TSO and PSO via shared memory abstractions
复制标题
DOI：
10.5555/3077629.3077662
复制
发表时间：
2016-10
期刊：
影响因子：
--
通讯作者：
Ermenegildo Tomasco;Truc L. Nguyen;Omar Inverso;B. Fischer;S. L. Torre;G. Parlato
中科院分区：
文献类型：
--
作者：
Ermenegildo Tomasco;Truc L. Nguyen;Omar Inverso;B. Fischer;S. L. Torre;G. Parlato
延迟顺序化是并发程序进行有界验证的最有效方法之一。现有工具假定顺序一致性（SC），因此对弱内存模型（wmm）进行延迟顺序化的可行性仍然未经测试。在这里，我们描述了总存储顺序（TSO）和部分存储顺序（PSO）内存模型的第一种延迟序列化方法。我们用共享内存抽象（SMA）上的操作替换所有共享内存访问，SMA是一种抽象数据类型，封装了底层WMM的语义，并在更简单的SC模型下实现它。我们给出了基于时间循环双链表的TSO和PSO的有效SMA实现，这是一种新的数据结构，可以有效地模拟存储缓冲区。我们通过实验，在SV-COMP并发性基准测试和现实世界的实例上都表明，这种方法与基于有界模型检查的延迟序列化相结合可以很好地工作。
Lazy sequentialization is one of the most effective approaches for the bounded verification of concurrent programs. Existing tools assume sequential consistency (SC), thus the feasibility of lazy sequentializations for weak memory models (WMMs) remains untested. Here, we describe the first lazy sequentialization approach for the total store order (TSO) and partial store order (PSO) memory models. We replace all shared memory accesses with operations on a shared memory abstraction (SMA), an abstract data type that encapsulates the semantics of the underlying WMM and implements it under the simpler SC model. We give efficient SMA implementations for TSO and PSO that are based on temporal circular doubly-linked lists, a new data structure that allows an efficient simulation of the store buffers. We show experimentally, both on the SV-COMP concurrency benchmarks and a real world instance, that this approach works well in combination with lazy sequentialization on top of bounded model checking.