检测并发程序Bug：[PLDI2021] Canary: Practical Static Detection of Inter-thread Value-Flow Bugs

最近得研究下多任务并发程序的静态分析，于是看了这篇文章

总体来说，看是看懂了，但是… … 这篇文章所做的工作有点多啊… 实现起来不会很容易…

1. Canary: Practical Static Detection of Inter-thread Value-Flow Bugs

这篇文章是港科大团队发表在PLDI 2021，并发Bug缺陷检查。

首次将并发bug检测转化为source-sink可达性问题，有效减低冗余的线程交错处理。
提出值流图上的thread-modular算法来捕获数据和干扰(interference)依赖.
检测方法
- 值流相关的边被标注guard用于表示value-flow的条件。Canary通过遍历value-flow graph追踪source-sink属性，并利用SMT求解器来确定可行路径，最终检测并发缺陷。

实验结果表明Canary是precise/scalable/practical的，并且low false positives。

2. Introduction

并发bug查找很难
- 动态分析很难，因为线程间切换错综复杂，程序的可行路径爆炸。(静态分析已经很爆炸了…)
- 相比之下，静态分析有较好的覆盖率，但是求解近似解不够精确。
精确的针对并发程序的静态分析特别有挑战性
- 传统程序分析沿着CFG传播，比较冗余，再加上并发程序的混淆。使得追求高精度时，出现性能问题。
- interference dependence: 并发程序里额外的数据依赖(线程间共享内存)。捕获不同线程间的def-use关系能够有效剪枝冗余的线程间交互路径。
  - 这种依赖的求解本身就很有挑战性。
  - 关键的困难：精确的线程间指针别名分析。因为穷举式的计算指针信息并不够scalable。
- 另一方面，没必要去探索跟被检查的属性无关的线程间交错空间

Canary追踪值怎么通过data/interference dependence关系被store/load。

关键思想就是：通过On-Demand的方式追踪source-sink value flow来缓解并发bug检测的状态搜索空间爆炸问题。value flow只追踪跨线程相关的def-use关系。

术语：inter-thread value flow bugs，比如inter-thread use-after-free，NULL pointer dereference，double free，infomation leak。

图1所示，Canary有3个关键步骤：

thread-modular算法：在VFG上单独地捕获数据依赖和冲突依赖(interference dependence)
在相关的VFG边上编码可行路径，遵循sequential consistency的定义
- 冲突依赖边作为“tunnels”，用于on-demand值流搜索，值的流进/流出线程。
bug检查阶段，Canary使用interference-aware的VFG来检查source-sink属性，并将累积的guards扔给SMT求解器

值得注意的特性：

图遍历和SMT求解只会在source-sink值流上进行，降低开销。
value-flow生成清晰的bug报告，用于定位什么样的语句执行条件，导致并发错误。
- 很重要：能够有效帮助诊断bug的原因 (witness)

3. 简要

冲突依赖的定义：语句s1被另一条语句s2 interference dependent(冲突依赖)，如果s1对x的定义在s2被使用，并且s1，s2是并发执行的。

不仅要收集一般的路径条件约束，还要收集线程间语句的执行先后约束。

抽象域
- 线程id的集合T：每个线程t关联一个上下文敏感的fork点，由有限个函数F组成
- Label的集合L：每个label l表示CFG上的一个程序点
- 变量分为top-level变量的集合V，address-token变量的集合O
  - top-level：v在不同的guard条件下，可能指向不同的内存对象
  - address-token：o可以通过top-level指针变量，load，store语句间接访问

线程间的值流没有传递性，需要注意单线程内的执行顺序。

值流路径P = <v1@L1, …, vn@Ln >被认为是sequentially consistent，如果存在一个在program order <上的total order <，并且遵循下面的条件:

V(n-1)@L(n-1) 通过相同内存位置流向Vi@Li, 并且不会被重写 (2 <= i <= n)
对任意Li, Lj, 如果Li < Lj，那么Li < Lj。
- 也就是说 < ==> <

L1: *x = q;
L2: p = *y;// 是否 q@L1 能流向 p@L2
// 关键是确定x, y是否是别名// 核心思想就是
// 1. 捕获被逃逸的对象
// 2. 发现所有指向这些对象的指针变量

分析时需要编码必要的sequentially consistency axioms作为条件：

Memory Alias。变量x, y可能指向相同内存对象的条件
Load-Store Order。
- q@L1 能流向 p@L2
  - 通过相同的内存对象
  - 这块内存并不会被其它并发store语句重写

4. Thread-Modular Dependence Analysis

解决两个问题：

数据依赖 (VFG)
VFG上，别名的interference依赖

算法2个Phase

intra-thread数据依赖 (传统的数据流分析)
- Intra-procedural analysis
- inter-procedural analysis
inter-thread数据依赖 (Modular-Thread依赖分析)
- interference dependence analysis
  - 依赖边的计算
  - 依赖边上的guards计算

4.1 intra-thread数据依赖

此阶段的目的就是求解线程内的数据依赖边并计算它们的Guards。生成的VFG作为interference dependence analysis的输入。

计算间接流: q@*x=q -> p = *y, 这需要address-token变量O的指向信息。
数据依赖Guard：x，y指向相同内存对象o的条件 && L1到L2的分支条件

为了降低指向分析的开销，我们执行函数内的路径敏感指向分析[1]来解析局部数据依赖，指向分析沿着thread-call-graph自底向上进行分析。

求解数据依赖的基本规则：

intra-procedural分析 (参考文献[2])

标准的数据流分析[2], 逆后序 (reverse post-order) CFG计算指向信息Pts。

首先对函数F执行标准的转换
- 对通过引用传入函数的对象，引入辅助变量，以暴露函数参数的side-effects。
由于V是SSA形式，所以分析直接使用全局指向图 PG 来存储top-level变量V的指针信息
使用IN[L]和OUT[L]集合[2]来存储在语句L处，address-token变量O所传播的指针信息
- 4种指针操作：alloc，assign，load，store
- 图6给出的规则能够找到间接值流

inter-procedural分析

Trans(F)摘要了函数F的formal-in和formal-out之间指向分析的副作用。它表示了input/output的行为，抽象掉函数内的细节。

当分析调用点的时候，我们会去使用procedural transfer function来推理callee对实参的副作用。这里并不需要推理fork点的参数传递(之后再处理)。

此阶段的VFG包含对后续interference dependence analysis很重要的指针信息。

标识escaped objects：比如共享内存位置；通过在VFG上找到不同线程可能可访问的内存对象。

Interference-dependence分析

此阶段的目的 就是识别VFG上所有可能的interference-dependence边, 并计算修饰这些边的guards。

核心的问题就是确定：跨越不同线程，介于*x = q; p = *y之间的(q@L1, p@L2)边依赖。当然我们也需要确定L1和L2之间的order（如下图所示的等式右侧两个条件的^）

Interference-dependence的条件：共享内存，escaped objects

接下来就是，通过有效的算法来：

计算escaped objects集合EspObj
- escape analysis
指向这些集合的变量Pted(o), o in EspObj
- 通过遍历VFG来找到从o可达的节点

注意：新引入的interference-dependence边可能会扩大EspObj和Pted集合的大小。这就会导致又会存在一些新的interference-dependence，intra-thread-data-dependence边。这叫cyclic-dependence-problem。

因此VFG和interference-dependence分析是相互影响的，于是我们通过迭代最终达到不动点(没有更多的value-flow被生成，EspObj，Pted集合也不更新)。

所以这个方法并不严格来说是inter-thread的分析，因为它也会迭代地更新intra-thread的data-dependence，但是这个方法确实是thread-modular的。

Dependence-guard计算

别名约束Guard：介于*x = q; p = *y之间的(q@L1, p@L2)边依赖
- 约束1: x, y可能指向相同内存对象的；VFG上从内存o到节点x和y之间的guard累积
- 约束2: 语句L1到语句L2在CFG上的分支条件Guard
load-store约束Guard: 根据sequential consistency
- 如果一个Store变量q@L1流向Load变量p@L2，那么需要保证L1 < L2
- L1到L2之间没有其它的并发Store

总结

Thread-Modular的好处是不用穷举所有的可执行路径。

约束只在Bug检查阶段去求解，避免激进的求解开销。

只路径敏感地推理共享内存对象，而非使用穷举式昂贵的指针分析。

5. Guarded Reachability Detection

上述interference-aware VFG构建好之后，bug检查就被转换成guarded图可达性问题。

检测阶段

偏序值流搜索
约束求解

问题

怎么定位program order是否违反
- 考虑控制流
  - 值流路径两个连续节点L1，L2，如果存在一条合理的从L1到L2的CFG路径
- 同步控制语义 (这里只考虑fork, join, 其它的同步原语也是使用类似的框架)
  - 父线程fork操作之前节点的order < 子线程所有节点的order
  - 父线程join操作之后节点的order > 被join子线程所有节点的order
- 编码值流路径上每两个连续的节点的order约束 PO(i)
  - 所以整个值流路径的Order约束就是值流路径上所有PO(i)的与 (1<= i <= k-1, k为value flow path路径长度)
怎么有效地求解修饰Value-Flow路径上的约束
- 整个值流路径的Guards记为All = PO ^ Guards
  - 值流路径上program order记为PO, def-use边的条件记为Guards
- 经观察发现，可能生成的约束串非常大，需要优化
  - 使用semi-decision procedures过滤掉很明显冲突的约束；降低计算/内存开销
  - 不同source-sink路径约束相互独立的，我们可以并行求解
  - 对于复杂的公式，我们充分利用cube and conquer parallel SMT solving strategy来求解约束
    - ???what?

6. 实现

支持大多数C/C++特性：类，动态内存分配，引用，虚函数
- 数组元素被认为是同一个变量，比如Arr[k] 被认为是 Arr[0]
使用may-happen-in parallel (MHP) analysis剪枝一些不可行的线程间值流
- ??? what?
使用Steensgaard来构造thread-call-graph
使用CHA来解析虚函数调用

unsound的决策

尽可能低误报找到bug，所以潜在漏报
展开循环两次，忽略内联汇编
手动模型化部分C/C++库
假定函数的不同参数互相不为别名
- ???
比较工具
- 与SABER，FSAM比较
测试项目
- Firefox
- MariaDB
- MySQL
比较指标
- 值流构造
- 并发bug检测
  - Scalability
  - Precision
- 检测真实并发bug
4小时9百万行，平均误报26.67%，发现19个被开发者确认，之前没被发现的并发bug，14个被修复
- 20核，Intel® Xeon® CPU E5-2698 v4 @ 2.20GHz, 256GB物理内存, Ubuntu-16.04
- ???
工业要求是每百万行代码5-10小时，误报率低于30%[3]

仍然需要做的：

支持更多的同步语义
- Unlock/lock, signal/notify
扩展relaxed memory model, 比如TSO/PSO
自定义decision procedures，用于提升约束求解的效率
- 一大长串公式还是太耗性能。。。

参考

[1] Qingkai Shi, Xiao Xiao, Rongxin Wu, Jinguo Zhou, Gang Fan, and Charles Zhang. 2018. Pinpoint: Fast and Precise Sparse Value Flow Analysis for Million Lines of Code. In Proceedings of the 39th ACM SIGPLAN Conference on Programming Language Design and Implemen tation (Philadelphia, PA, USA) (PLDI 2018). Association for Computing Machinery, New York, NY, USA, 693–706. https://doi.org/10.1145/3192366.3192418

[2] Ben Hardekopf and Calvin Lin. 2009. Semi-Sparse Flow-Sensitive Pointer Analysis. In Proceedings of the 36th Annual ACM SIGPLAN SIGACT Symposium on Principles of Programming Languages (Savannah, GA, USA) (POPL ’09). Association for Computing Machinery, New York, NY, USA, 226–238. https://doi.org/10.1145/1480881.1480911

[3] Al Bessey, Ken Block, Ben Chelf, Andy Chou, Bryan Fulton, Seth Hallem, Charles Henri-Gros, Asya Kamsky, Scott McPeak, and Dawson Engler. 2010. A Few Billion Lines of Code Later: Using Static Analysis to Find Bugs in the Real World. Commun. ACM 53, 2 (Feb. 2010), 66–75. https://doi.org/10.1145/1646353.1646374