Dissecting ThreadSanitizer Algorithm

本文深入剖析 ThreadSanitizer(V2) 检测 Data Race 背后的算法原理。

Introduction

ThreadSanitizer(AKA TSan) 是一个集成在 GCC 和 Clang 中的动态分析工具，能够检测 C++ 代码中大多数的数据竞争 (data race) 。它由编译时插桩和运行时库两部分组成，通过编译和链接时添加参数 -fsanitize=thread，就可以在运行时检测 data race 。

Data Race

TSan 是检测 data race 的动态分析工具。我们先看下 data race 指的是什么？

Data Race：两个线程 concurrently 访问了同一个内存位置 (memory location)，并且两个线程的访存操作中至少一个是写操作。

注：关于 race condition 和 data race 的区别，见 Race Condition vs. Data Race – Embedded in Academia

例如下述代码：两个线程并发地修改整型全局变量 Global 存在 data race。两个线程执行结束后，全局变量 Global 的值可能是 1 也可能是 2。如果是在读写 STL 容器时存在 data race，则可能导致更严重的后果，比如内存破坏、程序崩溃。

int Global;

void Thread1() {
  Global = 1;
}

void Thread2() {
  Global = 2;
}

根据 data race 的定义，判断代码中是否存在 data race 需要考虑 3 个条件：

  1. 两个线程访问的是否为同一个 memory location
  2. 两个线程的访存操作中至少有一个是写操作
  3. 两个线程的访存操作是否 concurrent

其中前两个条件很容易判断，所以检测 data race 的要解决的关键问题就是怎么判断两个访存操作是否 concurrent ！

Happen-Before & Concurrent

在介绍如何判断两次访问操作是否是 concurrent 之前，我们需要先引入 happen-before 的定义。

Happen-before 的定义最开始是在 Lamport, L., 1978. Time, clocks, and the ordering of events in a distributed system 中给出的，描述的是分布式系统中事件之间的一种偏序关系。

一个分布式系统是由一系列 processes 组成的，每个 process 又由一系列事件组成， 不同的 process 之间是通过收发消息进行通信的。

Happen-before 关系（记作 $\rightarrow$）的定义：

  1. 如果事件 $a$ 和事件 $b$ 是在同一个 process 中的事件，并且 $a$ 早于 $b$ 发生，那么 $a \rightarrow b$

  2. 如果事件 $a$ 和事件 $b$ 是不同 process 中的事件，且 $b$ 是 $a$ 发送的消息的接收者，那么 $a \rightarrow b$

  3. Happen-before 关系是一种严格偏序关系 (strict partial order)，即满足 transitive, irreflexive and antisymmetric

    1. Transitive。对于任意事件 $a,b ,c$，如果 $a \rightarrow b$ 且 $b \rightarrow c$，那么有 $a \rightarrow c$
    2. Irreflexive。对于任意事件 $a$，都有 $a \nrightarrow a$
    3. Antisymmetric。对于任意事件 $a,b$，如果 $a \rightarrow b$，那么有 $b \nrightarrow a$

下面通过一个例子对 happen-before 进行说明：

上图是对一个分布式系统的某一次 trace：

那么对于上图分布式系统 trace：

理解了 happen-before 的定义后，我们给出 concurrent 的定义：如果 $a \nrightarrow b$ 且 $b \nrightarrow a$，那么称 $a$ 和 $b$ 是 concurrent 的。

这样我们就能够将判断两次访存操作之间是否 concurrent 转化为了判断两次访存操作之间是否存在 happen-before 关系。

那么如何判断两次访存操作之间是否存在 happen-before 关系呢？答案是 Vector Clock。在介绍 Vector Clock 之前，我们需要先了解下 Lamport Logical Clock。

Lamport Logical Clock

Lamport logical clock 算法是由 Leslie Lamport 在 Lamport, L., 1978. Time, clocks, and the ordering of events in a distributed system 中提出的一种简单的逻辑时钟算法，用于描述分布式计算机系统中事件的偏序关系。

算法如下：

  1. 每个 Process $P_i$ 都持有一个逻辑时钟 $Clock_i$，process $P_i$ 在每次本地事件发生之前，都将 $Clock_i$ 自增 1
  2. Process $P_i$ 向其他 Process 发送消息时，先执行步骤 1，然后将 $Clock_i$ 的值包含在消息中一并发送出去
  3. Process $P_j$ 接收到 Process $P_i$ 发送来的消息时，获取消息中携带的 $Clock_i$ 的值，与自身的 $Clock_j$ 取最大值，然后在认为收到消息之前将 $Clock_j$ 自增 1

根据 lamport logical clock 算法流程和 happen-before 定义易得：对于任意两个事件，如果事件 $a$ happen-before 事件 $b$，那么 $Clock(a) < Clock(b)$。

下面通过例子来说明 lamport logical clock 算法流程：

但是 lamport logical clock 是存在局限性的：

例如 $Clock_p(p1)= 1 < 2 = Clock_q(q2) $，但是实际上 $p_1$ happen-before $p_2$ 是不成立！也就是说，事件 $p_1$ 和事件 $p_2$ 之间谁都可能早于另外一个事件发生。

我们前面将 data race 检测问题转化为了判断两次访存操作之间是否存在 happen-before 关系的问题。但是由于 lamport logical lock 的局限性，我们不能直接将 lamport logic clock 应用于 data race 的检测。

Vector Clock

Colin Fidge 和 Friedemann Mattern 提出的 vector clock 解决了 lamport logic clock 的上述局限性

vector clock 算法如下：

下面还是通过一个例子来说明 vector clock 的算法流程：

Vector clock 解决了 lamport logical clock 的局限性，满足如下性质：

即 $p_a \rightarrow q_b \quad \textup{iff} \quad VC_p(a) < VC_q(b)$

Vector clock 上的偏序关系如下：

根据 $p_a \rightarrow q_b \quad \textup{iff} \quad VC_p(a) < VC_q(b)$ 这个性质，我们就能使用 vector clock 来判断两次访存操作之间是否存在 happen-before 关系，即能够基于 vector clock 算法来检测多线程程序中的 data race。

Data Race Detection

我们前面在介绍 lamport logic clock 和 vector clock 时都是以分布式系统中的事件之间序关系为背景进行介绍的。

实际上多线程程序也可以看作是一个分布式系统。我们对上述 vector clock 算法稍加修改，就可以应用于检测多线程程序中的 data race：

下面还是通过一个例子来说明如何应用 vector clock 检测多线程程序中的 data race：

ThreadSanitizer Internals

ThreadSanitizer 检测 data race 的思想其实就是基于 vector clock 算法的，只不过在实现时做了一些取舍。比如对于每一个变量 $x$，ThreadSanitizer 不会记录所有线程最近一次对变量 $x$ 的读写，ThreadSanitizer 只会记录最近 4 次对变量 $x$ 的读写。

ThreadSanitizer 由编译时插桩和运行时库两部分组成。

例如，本文最开始提到的全局变量数据竞争的代码片段使用 ThreadSanitizer 插桩后的代码变为如下所示：

int global;

void Thread1() {
  __tsan_func_entry(__builtin_return_address(0));
  __tsan_write4(&global);
  global = 1;
  __tsan_func_exit();
}

void Thread2() {
  __tsan_func_entry(__builtin_return_address(0));
  __tsan_write4(&global);
  global = 2;
  __tsan_func_exit();
}

注意到：在 global = 1 和 global = 2 之前都插入了对 __tsan_write4 的函数调用。

启用 ThreadSanitizer 后，在程序运行过程中，每一个线程都会保存一个 vector clock，每 8-bytes 的应用程序内存都对应有 4 个 8-bytes 的 shadow word。每个 shadow word 都用于记录一次访问操作，记录 TID（线程 id）、Epoch（访存操作发生时线程 TID 此时的 local time）、Pos:Size（标识本次访存访问的是当前 8-bytes 的哪几个 bytes）、IsWrite（标识本次访存操作是读还是写）。

每次读写变量 $x$ 时，由于程序被 ThreadSanitizer 插桩，所以在执行读写操作之前，都会调用函数 __tsan_read 或 __tsan_write，在__tsan_read 和 __tsan_write的函数实现中，首先找到变量 $x$ 所在的 8-bytes 内存区域。然后找到这 8-bytes 内存所对应的 4 个 shadow word，检查当前这一次对变量 $x$ 的读写与shadow word 中记录的最近 4 次读写是否存在 data race。最后更新 shadow word 的内容，记录本次对变量 $x$ 的读写，保证 shadow word 记录的是最近 4 次对变量 $x$ 的读写。

完整的 ThreadSanitizer 算法的伪代码如下所示：

def HandleMemoryAccess(thread_state, tid, pc, addr, size, is_write, is_atomic):
  shadow_mem = MemToShadow(addr) # the type of shadow_mem is uint64_t*
  IncrementThreadClock(tid)
  LogEvent(tid, pc)
  new_shadow_word = ShadowWord(tid, CurrentClock(tid), addr, size, is_write, is_atomic)
  stored = false
  for i in range(0, 4):
    raced = UpdateOneShadowState(thread_state, shadow_mem, i, new_shadow_word, stored)
    if raced:
      return
  if not stored:
    # Evict a random Shadow Word
    shadow_mem[Random(4)] = store_word # Atomic

def UpdateOneShadowState(shadow_mem, idx, new_shadow_word, stored):
 old_shadow_word = shadow_mem[idx] # Atomic
 # The old state is empty
 if old_shadow_word == 0:
   if not stored:
     StoreIfNotYetStored(shadow_mem[idx], store_word)
     stored = true
   return false
 # Is the memory access equal to the previous?
 if AccessedSameRegion(old_shadow_word, new_shadow_word):
   if SameThreads(old_shadow_word, new_shadow_word): # same thread
     if IsRWWeakerOrEqual(old_shadow_word, new_shadow_word):
       StoreIfNotYetStored(shadow_mem[idx], store_word)
       stored = true
     return false
   if HappensBefore(old_shadow_word, thread_state):
       return false
   if IsBothReadsOrAtomic(old_shadow_word, new_shadow_word):
     return false
   # race!
   ReportRace(old_shadow_word, new_shadow_word)
   return true
 # Do the memory access intersect?
 if AccessedIntersectingRegions(old_shadow_word, new_shadow_word):
   if SameThreads(old_shadow_word, new_shadow_word):
     return false
   if IsBothReadsOrAtomic(old_shadow_word, new_shadow_word):
     return false
   if HappensBefore(old_shadow_word, thread_state):
     return false
   # race!
   ReportRace(old_shadow_word, new_shadow_word)
   return true
 # The accesses do not intersect, do nothing
 return false

def StoreIfNotYetStored(shadow_mem, store_word):
  *shadow_mem = store_word # Atomic
  store_word = 0

def IsRWWeakerOrEqual(old_shadow_word, new_shadow_word):
 return (old_shadow_word.is_atomic > new_shadow_word.is_atomic) ||
        (old_shadow_word.is_atomic == new_shadow_word.is_atomic &&
         !old_shadow_word.is_write >= !new_shadow_word.is_write)

def HappensBefore(old_shadow_word, thread_state):
  return thread_state.vector_clock.get(old_shadow_word.tid) >= old_shadow_word.epoch

References

  1. Lamport, L., 1978. Time, clocks, and the ordering of events in a distributed system.Communications of the ACM,21(7), pp.558-565.
  2. Cormac Flanagan and Stephen N. Freund. 2009. FastTrack: efficient and precise dynamic race detection. (PLDI ‘09)
  3. Finding races and memory errors with GCC instrumentation. (GNU Tools Cauldron 2012)
  4. AddressSanitizer, ThreadSanitizer and MemorySanitizer – Dynamic Testing Tools for C++. (Google Test Automation Conference)
  5. https://en.wikipedia.org/wiki/Lamport_timestamp
  6. https://en.wikipedia.org/wiki/Vector_clock