Reading Papers - Atomicity Violation
# Early Days
# VVEIS'03 - High-level Data Race *
本文定义了 high-level data race 的概念(事实上就是 atomicity violation 的概念),同时提出了 view consistency 。
Taxonomy : atomicity violation detection
Tag : high-level data race
本文在假定 low-level data race 不存在的基础上讨论。
# High-level Data Race
high-level data race 的基本定义如下:
A high-level data race can occur when two concurrent threads access a set V of shared variables, which should be accessed atomically, but at least one of the threads does not access the variables in V atomically.
检测 high-level data race 的主要挑战是如何判断哪些变量可以被认为是一个 atomic set 。这在实践中是一个不可判定问题,除非开发者人工给出 specification 。这种分析任务的另外一个挑战是,有时仍然希望允许对 atomic set 的 partial access ,例如 setXY
和 getX
的并发。
high-level data race 的 refined 版本的定义如下,相比前者有机会得到更低的误报率:
A high-level data race can occur when two concurrent threads access a set V of shared variables, which should be accessed atomically, but at least one of the threads accesses V partially several times such that those partial accesses diverge.
理解 refined definition 的关键在于理解 partial access 的 diverge ,这是指什么呢?
# View Consistency
view, maximal view :
对于某个由线程 执行、由锁 保护的 synchronized block ,则 执行时 访问的所有 field 所组成的集合是一个由 相对于 生成的 view 。用 表示由 生成的所有 view 的总集合。
若 满足 ,则称 是一个由 生成的 maximal view 。显然 maximal view 可能有多个,用 表示由 生成的所有 maximal view 的总集合。
maximal view 对错误检测没有实质贡献,其作用是在发现错误时提高计算效率以及减少冗余的错误报告。为便于理解可在思考时仅考虑 view 。
overlap :
对于线程 以及由另一线程 生成的 view ,定义线程 与 的 overlapping views 为 中每个 与 的非空交集,即:
overlap 的作用是过滤无关变量:显然,对于分属不同线程的两个 view ,只有其公共访问的 field 可能出现并发错误。
chain & compatible :
对于线程 以及由另一线程 生成的 maximal view ,当且仅当 与 的所有 overlapping views 能构成一个 chain 结构时,称 和 是 compatible 的:
chain & compatible 是 view consistency 的核心概念。
chain 的含义是,对于分属两个线程 的任意两个 view 的公共部分 ,所有这样的 恰能构成一个线性的偏序关系 。
view consistency :
最终,view consistency 由所有线程之间的 compatible 关系构成:
具体地讲,view consistency 要求程序中的任意两个线程之间都是 compatible 的,也就是 view 之间任何的公共访问都能构成 chain 。
为什么认为能构成 chain 就是 race free 的呢?
# View Consistency 误报和漏报
view consistency 存在误报:
- 程序可能使用了过于粗粒度的锁,也就是说,程序中的某些 synchronized block 可以被划分为多个更小的 block 。
view consistency 存在漏报:
Assume a set of fields that must be accessed atomically, but is only accessed one element at a time by every thread. Then no view of any thread includes all variables as one set, and the view consistency approach cannot find the problem.
Another source of false negatives is the fact that a particular (random) run through the program may not reveal the inconsistent views, if the corresponding code sections are not executed even once.
# View Consistency 动态检测
本文基于 view consistency 实现了一个动态检测工具,对程序进行插桩,生成 event log 并将程序的执行建模为 event trace ,然后在运行时刻对其进行观测和分析。这可以分为两个步骤:
event analysis :读取事件序列并重建运行时环境。
event interpretation :可以有多个 event interpreter ;每个 event interpreter 构建关于 event trace 的模型,记录 event trace 并根据自己的模型进行分析和错误检测。
# SRC-TN-2002-004 - Stale-Value Error
本文定义了 state-value error 的概念,并提出了一种基于 invariant 的策略,可用于进一步实现静态或动态的检查器。
SRC-TN-2002-004 - Finding Stale-Value Errors in Concurrent Programs
Taxonomy : atomicity violation detection
Tag : state-value error / invariant-based
state-value error 指的是这样一类并发错误:在锁保护下从共享变量读取值到局部变量,但在稍后使用该值时未被锁保护。
本文提出了一种基于 invariant 的策略,在被测程序中插桩对两个 invariant 的维护和检查,可用于进一步实现静态或动态的检查器。
定义 表示局部变量 的值是否过时。
定义 表示局部变量 的最近一次被写入更新是否在临界区内发生。
对于 :
初始时对所有局部变量 令 。
每当局部变量 被读取时,检查 。
每当局部变量 被写入时,在每个写指令 之前,简单的策略是对于 均插入 ,复杂的策略需要考虑 的情况,此时需要传播 的状态。
每当进入任何临界区时,对每个局部变量 ,在进入临界区之前插入 。
对于 :
- 每当局部变量 被写入时,若写入发生在临界区内,则在写指令之前插入 ,否则插入 。
# Miscellaneous
# AVIO
AVIO
Taxonomy : xxx
Tag : xxx
AVIO
# ISCA'08 - Atom-Aid
Atom-Aid 基于已有的支持 implicit atomicity 的硬件,使用更聪明的 chunk 划分策略在运行时刻以更高的概率 survive and detect atomicity violation 。
ISCA'08 - Atom-Aid - Detecting and Surviving Atomicity Violations
Taxonomy : atomicity violation detection / atomicity violation survive / implicit atomicity
Tag : hardware support / speculative execution
Preceding Work : ISCA'07 - BulkSC *
# Implicit Atomicity
一些硬件架构(例如 BulkSC)设计不同策略(在不需要程序注解的情况下)将一系列连续的内存读写操作划分为若干个 atomic block(或称为 chunk),允许 chunk 内部的处理器指令重排,但仅允许以 chunk 的粒度发生线程调度。这将减少可能的线程交错的种类数。同时,硬件的 chunk 划分策略对上层的软件代码是不可见的。
此类提案的主要目的是弥合 strict 和 relaxed 的 memory model 之间的性能差距,同时保持较低的硬件复杂性。本文定义上述硬件架构所提供的性质为 implicit atomicity ,因为此类提案的一个副作用是隐藏程序中的 atomicity violation 。
Atom-Aid 使用更聪明的策略而不是随意地划分 chunk ,进一步提高隐藏 atomicity violation 的概率。
Atom-Aid 在支持 implicit atomicity 的 BulkSC 的基础上实现,但它并不受限于特定的硬件架构。
# Smart Chunking
Atom-Aid 在运行时尝试推断出 critical section 应当被设置的位置,并据此划分 chunk 边界。具体地讲:
Atom-Aid 在运行时维护过去已提交的 chunk 的读写集合。用 和 表示当前处理器的读写集,用 和 表示远端(另一)处理器的读写集。
对于当前 chunk 内的内存读写指令,可以通过这些记录来识别潜在的 atomicity violation ,此时被该指令访问的变量会被记入 。
此后,若当前处理器再次访问 中的变量,Atom-Aid 会在前一次的访问指令之前插入 chunk boundary ,使两次对同一变量的访问处于相同 chunk 内。
最后,Atom-Aid 利用 BulkSC 的机制拒绝当前 chunk 的 speculative execution ,则新的执行将保证两次访问的原子性。
然而,不能在每个这样的指令处都插入 chunk boundary ,这样在许多情况下反而会破坏由原本的 chunk 所保证的原子性。例如在一段执行区间内对某一变量的访问指令有三条,而前两条才需要保持原子性。
对于上述情况,Atom-Aid 设计了更聪明的机制,大致上是在 未发生变化时保证同一个 chunk 不被分割两次,具体的判定规则详见论文原文。
# OOPSLA'11 - Commutativity-Guided Checking
本文利用并发数据结构的基础方法的可靠性,以高效检测由后续开发的自定义操作所引入的 atomicity violation 。
Taxonomy : atomicity violation detection
Tag : linearizability / concurrenct data structure
Preceding Work : xxx
# Mover Reduction
# Introduction
为便于描述,我们假定此处所述的一条 指令 或者说一个 动作 (action) 是如下程序行为之一:
锁的获取或释放,用 和 表示;
对单个共享内存的一次读写,直接用表达式表示(例如 );
其它无关动作,例如 thread-local memory access 等,用 表示。
我们将一次执行建模为一组由不同线程执行的动作交错组成的事件序列,则有如下关于 mover 的定义:
在一次执行 中,对于由线程 执行的一个动作 ,若 的直接后继 是由另一个线程 执行的,且在 上交换 和 的位置不会改变程序的执行结果,则称 是一个 right mover 。
类似地,若 的直接前继 是由另一个线程 执行的,且在 上交换 和 的位置不会改变程序的执行结果,则称 是一个 left mover 。
所有的锁获取指令 都是 right mover 。
- TODO. explanation
类似地,所有的锁释放指令 都是 left mover 。
# PLDI'03 - Type System for Atomicity
本文(在我已知范围内)首次定义了 atomicity 的概念,并基于 mover reduction 提出了一种 Java 类型系统,用于指定及检查方法的原子性。
Taxonomy : atomicity violation detection / mover reduction
Tag : type system / java
本文提出的类型系统支持开发者的如下行为:
为程序语句标注 atomicity property ,包括基本属性 const, mover, atomic, cmpd, error ,条件属性,以及 guarded_by (?) 。
将方法标记为 atomic 。
随后,类型系统利用 mover reduction 静态地检查每个 atomic 方法是否满足原子性。
# POPL'04 - Atomizer
Atomizer 实现了基于 mover reduction 和 Lockset 算法的动态分析技术,在运行时刻验证每个人工标注的代码块的原子性。
POPL'04 - Atomizer - A Dynamic Atomicity Checker For Multithreaded Programs
Taxonomy : atomicity violation detection / mover reduction
Tag : lockset / dynamic analysis / manual annotation
本文首先建模了多线程程序的基本语义,包括 standard semantics 和 serialized semantics ,并指出满足原子性要求的程序应当是满足 serialized semantics 的。
随后,本文基于 mover reduction 建模了等价的 instrumented semantics ,事实上以形式化的方法描述了 mover 属性的动态传播和变化,以及基于 mover reduction 的运行时检查。
最后,本文引入 Lockset 算法的思想得到 extended instrumented semantics ,在运行时维护每个变量的 candidate lock set ,并据此更新程序的 mover 属性,避免要求开发者人工指定每个变量需要受到哪些锁的保护。
有关三个层次的程序语义的具体形式化规则,详见论文原文。
Atomizer 插桩被测程序,并实现了基于 mover reduction 和 Lockset 算法的动态分析技术,以在运行时刻检测原子性违反。
Atomizer 为每个变量维护一个状态机,就像原始的 Lockset 算法那样,并且同样不处理数组访问。
Atomizer 实际上实现的是 relaxed semantics ,以减少对 benign race 的误报:在原先的语义中,任何变量的 candidate lock set 演化为空集时都将直接报告错误,而 relaxed semantics 则仅将后续对该变量的所有访问归类为 non-movers 。
Atomizer 允许开发者人工标注函数或代码块为 atomic ,也可以使用简单的启发式策略,即认为:
所有类向外界暴露的公开接口应当是 atomic 的;
所有 synchronized 的函数和代码块应当是 atomic 的。
此外,Atomizer 还实现了一些改进策略以期能进一步减少误报,大体来说仍然是一些对 mover reduction 的放宽。
# Conflict Serializability
# PPoPP'06 - Conflict/View Serializability *
本文提出了 conflict serializability 和 view serializability ,并据此提出基于 access tree 和 happens-before relationship 的动态检测算法。
PPoPP'06 - Accurate and Efficient Runtime Detection of Atomicity Errors in Concurrent Programs
Taxonomy : atomicity violation detection / conflict serializability
Tag : correctness criteria / happens-before analysis / dynamic analysis / java
# PLDI'08 - Velodrome
Velodrome 在 POPL'04 - Atomizer 的基础上扩展了 conflict serializability 的语义,在 transaction 的模型上提出了 sound and complete 的动态分析算法来检测 atomicity violation 。
PLDI'08 - Velodrome - A Sound and Complete Dynamic Atomicity Checker for Multithreaded Programs
Taxonomy : atomicity violation detection / conflict serializability
Tag : happens-before / transaction / dynamic analysis / manual annotation / java
Preceding Work : POPL'04 - Atomizer
Velodrome 首先以类似 POPL'04 - Atomizer 的方法建模了程序的语义,并在其基础上追加了 transaction 的概念,以解决 Atomizer 误报率过高的问题:用 和 标注线程 执行中的一段程序为 transaction ,由人工标注或启发式策略给出,仅是用于测试的标注,无实际作用。
Velodrome 在 transaction model 上扩展了 happens-before 关系:
- 对于两个 transaction 和 ,若存在两个操作 满足 happens before ,则称 happens before 。
Velodrome 的动态分析算法类似于 Atomizer ,基于语义在运行时维护状态转换,同时构建和维护 transaction happens-before graph 。根据数据库相关理论,如果图上出现环路,则认为程序是 not conflict-serializable 的。
Velodrome 的一个重要挑战是责任分配 (blame assignment) ,即在发现 transaction-level 的环路后如何进一步定位错误到具体代码行。为此 Velodrome 额外引入了 Step 的语义,但在一些特殊情况下该问题仍是不可解的,详见论文原文。
Velodrome 还实现了一些优化来改善性能,包括 graph node gc 和 unnecessary node elimination ,详见论文原文。
# PLDI'14 - DoubleChecker *
DoubleChecker
Taxonomy : atomicity violation detection / conflict serializability
Tag : dynamic analysis / java
Preceding Work : PLDI'08 - Velodrome
# Atomic-Set Serializability
# POPL'06 - Atomic Set
本文提出了一种 data-centric 的模型用以避免 high-level data race(即 atomicity violation),在此模型上归纳了 11 种有问题的线程交错场景,并证明了不符合所有交错场景的并发执行是 serializable 的。本文也是 atomic-set serializability 的起源。
POPL'06 - Associating Synchronization Constraints with Data in an Object-Oriented Language
Taxonomy : atomicity violation detection / atomic-set serializability
Tag : correctness criteria / manual annotation / java
本文在假定 low-level data race 不存在的基础上讨论。
# A Data-Centric Approach
传统的避免 low/high-level data race 的方法是 code-centric 的,例如声明某些方法或代码块是 atomic 的,这种方法有两个主要缺点:
atomic section 的数量正相关于 shared field access 的指令数;
缺乏模块化特性,例如程序员还需要记住对超类中 field 的访问是否需要保护。
本文提出了一种 data-centric 的方法,允许程序员直接将 field 标注为属于某个 atomic set ,而后编译器会推断对属于同一个 atomic set 的不同 field 的引用是否满足原子性。
可以将方法的参数标记为 unitfor ,(没太看懂)。
atomic set
unitfor
owned field
# New Definition of Data Race
atomic set and units of work :
定义 为程序中所有 memory location 构成的集合,其中一些子集 可能被标注为 atomic set 。
- 定义每个指令都是对某个 memory location 的访问,记为 或 ,假定这样的指令是最小的执行单位,不可再被其他线程打断。
每个 atomic set 都会有一组与之相关(即存在对 中 field 的访问)的代码块,称这些代码块为 的 units of work ,记为 。定义一个 unit of work 为一组指令序列。
对于给定的 atomic set 和 unit of work ,从 中任取两个访问 中 field 的指令,其执行都应是 atomic 的。
根据如上定义,进一步有:
每个 unit of work 都可能与多个 atomic set 有关,定义 为与 相关的所有 atomic set 构成的集合。
定义 的 dynamic atomic set 为 ,即与 相关的所有 atomic set 之并。
unit of work 可以嵌套,定义 表示 嵌在 的内部,这种嵌套关系最终在整个程序上构成一个森林。
定义 和 为属于 unit of work 的读写操作。
每个线程都由一系列的 unit of work 构成。对于给定的 unit of work ,定义 为 所属的线程。
problematic interleaving scenarios :
本文总结了 11 种非法的 interleaving scenarios ,如果分属不同线程的两个 unit of work 和 中出现了其中任意一种(即作为子序列存在),则认为此程序执行中存在 data race 。
interleaving scenario | description | |
---|---|---|
1. | 更新时先前读取的值已过时 | |
2. | 两次读取的值不一致 | |
3. | 观测到了“中间状态” | |
4. | 读取的值与先前写入的值不一致 | |
5. | ... | ... |
关于该定义的完备性的证明,详见论文原文。
# ICSE'08 - Atomic-Set Serializability
本文在 POPL'06 的基础上正式提出了 atomic-set serializability ,并提出了检测对应 violation 的动态分析方法。
ICSE'08 - Dynamic Detection of Atomic-Set-Serializability Violations
Taxonomy : atomicity violation detection / atomic-set serializability
Tag : dynamic analysis / manual annotation / java
Preceding Work : POPL'06 - Atomic Set
# Atomic-Set Serializability vs Conflict/View Serializability
相比于 PPoPP'06 - Conflict/View Atomicity 中提出的 criterion ,本文及先前工作中提出的 atomic-set serializability 更加全面地涵盖了多种类型的并发错误,并且 atomic set 基于人工标注,具有分辨出 programmer-specified non-problematic atomicity violation 以减少误报的能力。
# Race Automaton
本文为每个 problematic interleaving scenario 构建一个 race automaton ,尝试对程序执行的内存访问序列进行自动机匹配。
在 POPL'06 - Atomic Set 的基础上扩充了几个对称的情形后,共有 14 个这样的 pattern ,因此完备的检测需要为每个 tuple 这 14 个 race automaton ,其中 是 units of work 的全集, 是 memory location 的全集。
本文使用 bitset 进行状态压缩,用一个 64 位整数来表示每个 tuple 的全部 14 个状态机。程序在运行时刻维护每个 tuple 的状态,在每个内存访问指令处更新所有与之相关的状态机。
疑问: 的 scalability?
# Scheduling Control
# FSE'08 - AtomFuzzer
AtomFuzzer 针对某一特定常见类型的 atomicity violation 设计了动态检测方法,在随机调度的同时检测可疑的程序行为,并尝试将程序执行引向可能触发错误的方向。
FSE'08 - Randomized Active Atomicity Violation Detection in Concurrent Programs
Taxonomy : atomicity violation detection / scheduling control
Tag : random scheduling / manual annotation / no false positives
Preceding Work : POPL'04 - Atomizer
AtomFuzzer 针对一种特定类型的 atomicity violation ,其 pattern 如下:
线程 在 atomic block 内先获取后释放互斥锁 ;
另一线程 随后在 (any?) atomic block 内先获取后释放互斥锁 ;
之后,线程 在该 atomic block 内再次获取互斥锁 。
符合该 pattern 的一个示例如下:
see the paper.
实践表明,这是一种非常常见的 bug pattern ,因而作者认为针对其进行测试是合理的。
与 POPL'04 - Atomizer 相同,AtomFuzzer 假定用户已经人工标注了 atomic 的代码块,或使用简单的启发式策略来判断。
AtomFuzzer 的策略非常简单:在随机调度线程的同时维护程序状态,检测 bug pattern 是否出现。
如果存在某一线程 ,在当前 atomic block 内先后获取释放某一互斥锁 ,并即将再获取该锁,则在获取前暂停 的执行并尝试调度其它线程,以期能发现另一线程 以满足 bug pattern 。
# ICSE'10 - ASSETFuzzer *
ASSETFuzzer
Taxonomy : atomicity violation detection / scheduling control / atomic-set serializability
Tag : random scheduling / manual annotation / java
Preceding Work : RaceFuzzer, ICSE'08 - Atomic-Set Serializability
ICSE'08 - Atomic-Set Serializability 所用的动态分析技术仅限于其能监控的当次执行,然而错误的执行通常难以触发,需要合理的调度机制才能实现高效的并发错误检测。ASSETFuzzer 则利用当次执行中获得的动态信息来指导下次 test run 的调度。
KEY Idea :即便是一次没有出错的执行,其中也蕴涵能帮助找到错误的 hints :即便 trace 中不存在 problematic access pattern ,但可能存在某个 pattern 的某种排列组合,ASSETFuzzer 利用这一信息来尝试探索错误的执行。
ASSETFuzzer 从 RaceFuzzer 中获得灵感,同样是分为两个阶段;不同的是,RaceFuzzer 的第一阶段是静态检测,而 ASSETFuzzer 的第一阶段是从实际执行中提取偏序关系以缩小其需要探索的线程交错空间。
在第一阶段,ASSETFuzzer
# ASSETFuzzer 第一阶段推理
# Atomic Region Inference
# OOPSLA'10 - TransFinder
TransFinder 在编译时刻基于 conflict serializability 为 unsynchronized SPMD programs 自动识别可能的 atomic region 。
OOPSLA'10 - Automatic Atomic Region Identification in Shared Memory SPMD Programs
Taxonomy : atomicity region inference / conflict serializability
Tag : static analysis / SPMD programs
在运行时生成的 precedence graph 以 atomic region 为节点、以 region 内的共享内存读写操作之间的冲突关系为边,类似于 PLDI'08 - Velodrome 中的 transaction happens-before graph 。根据数据库理论,对于一个给定的 schedule ,可以通过检测 precedence graph 上是否存在环路来判定此次执行的 conflict serializability 。
TransFinder 利用上述思想设计了静态概念的 conflict graph ,在编译时刻生成该图并检测图上是否存在环路,进而推测可能需要新设 atomic region 的程序段。
定义 concurrent shared basic block (CSBB) 为仅含单个单变量访问操作的基本块,定义 CSBB 的冲突为该操作的冲突。
conflict graph 以 CSBB 为节点、程序控制流走向和 CSBB 之间的冲突关系为边。
conflict cycle 是 conflict graph 中同时包含了两类边的环路,任何 inter-thread conflict cycle 都表明可能存在 conflict interleavings 。
SPMD (single program, multiple data) 程序 中只存在单个相同程序的复数实例,即程序中的每个线程都共享相同的代码。
考虑到 ,在大型程序中可能有过多的边,进而可能导致 DFS 判环算法的复杂度 变得不可接受。而对于 SPMD 程序,可以构造 projected conflict graph 来大幅减少边的数量。
简单来说,projecting 的过程就是将两个线程中对应的节点进行合并,消除自环后,直接利用 conflict edge 构造强连通分量 (SCC) ,每个 SCC 对应一个 atomic region 。
还利用语义信息来处理程序中的环路和条件分支:TBD.
# MICRO'10 - AtomTracker ^
AtomTracker 提出了一种类贪心的算法,利用程序执行的 memory trace 全自动(无标注)地推理 atomic region ;同时还给出了对应的运行时检测算法,用于判断被测程序的当前实现是否违反 AtomTracker 所判定的 atomic region 。
Taxonomy : atomicity region inference / atomicity violation detection / conflict serializability
Tag : hardware support / correct-run training / greedy strategy
generic(类似 conflict serializability) 不需要人工标注或任何有关程序语义的信息
# Atomicity Violation Survival
- 01
- Reading Papers - Kernel Concurrency06-01
- 02
- Linux Kernel - Source Code Overview05-01
- 03
- Linux Kernel - Per-CPU Storage05-01