Reading Papers - Partial Order Reduction

# Introduction

在并发测试领域，对于 model checking 、并发调度、以及其它需要探索状态空间的技术而言，状态空间爆炸始终是必须面对的挑战。partial order reduction (POR) 是一种用于缩小状态空间的技术，其核心思想是利用并发执行中 transition 、指令、事件的 可交换性 (commutativity) 。非形式化地讲，对于一个并发调度的事件序列（或子序列），交换其中一些事件的相对顺序不会改变程序的执行结果，那么这些调度是等价的，可以将其舍去，从而缩小探索的状态空间。

KEY Idea of POR ：对于一组相互独立的 transition（例如它们分属于几个相互之间不存在交互的进程），改变其排列顺序不会改变其最终执行结果。

POR 包括 persistent set 和 sleep set 两类互补的技术：

persistent set 利用程序的静态信息，
sleep set 利用测试运行时在过去的搜索中所获得的信息，

(VeriSoft:)从 POR 的视角看待状态空间，存在两种不同类型的冗余探索（？什么意思）：

explorations of any interleaving of a single finite partial ordering of transitions of the system, reaching the same state.
exporations of different finite partial orderings of transitions, reaching the same state.

Wikipedia - Partial Order Reduction (opens new window)

LNCS'96 - Partial-Order Methods for the Verification of Concurrent Systems (opens new window)

# Traditional Techniques

# LNCS'96 - Godefroid *

Godefroid (opens new window) 在其博士论文中提出并系统地介绍了 partial order reduction 的相关概念。

LNCS'96 - Partial-Order Methods for the Verification of Concurrent Systems
Taxonomy : model checking / concurrency testing / partial order reduction
Tag : persistent set / sleep set

# Transition Independency

Godefroid 将并发程序建模为 transition system ，具体形式化定义略。

若两个 transition $t_1$ 和 $t_2$ 满足以下条件，则称其为一组 independent transitions ：

independent transitions can neither disable nor enable each other;
commutativity of enabled independent transitions ：对于系统的任意状态 $s$ ，若 $t_1,\ t_2$ 均为 enabled ，则存在唯一的 $s'$ 满足 $s \overset{t_1t_2}{\Rightarrow} s' \land s \overset{t_2t_1}{\Rightarrow} s'$ 。

可以利用 independent transitions 的概念来定义 execution trace（即 sequence of states and transitions）之间的等价性：对于两个执行 $E_1$ 和 $E_2$ ，若 $E_2$ 可以通过（多次）交换 $E_1$ 中相邻的一组 independent transitions 得到，则称 $E_1$ 和 $E_2$ 是等价的。

随后，等价的 execution trace 可以被聚合为等价类，在探索状态空间时只需探索每个等价类中的一个 trace 即可。

检查系统中的每一对 transition 是否相互独立是不现实的，但实践中仍然存在一些易于检查的语法判断条件。直觉地，我们可以分别考虑控制依赖和数据依赖，例如：

若 active for (?) $t_1,\ t_2$ 的进程集不相交，即 $active(t_1) \cap active(t_2) = \emptyset$ ，则二者必互相独立。
若 $t_1,\ t_2$ 可访问的对象集不相交，则二者必互相独立。

# Persistent Set

考虑当前程序执行到某个状态 $s$ 处，设 $T_{enabled}(s)$ 为此时全体 enabled transitions 的集合。对于 $T(s) \subseteq T_{enabled}(s)$ ：

若从 $s$ 出发的任意 与 $T(s)$ 无关的 non-empty transition sequence $t_1t_2...t_n\ (\forall i \in [1,\ n],\ t_i \notin T(s))$

s \overset{t_1}{\rightarrow} s_1 \overset{t_2}{\rightarrow} s_2\ \cdots \overset{t_n}{\rightarrow} s_n\ (\forall i \in [1,\ n],\ t_i \notin T(s))

均有 $t_n$ 与 $\forall t \in T(s)$ 互相独立，则称 $T(s)$ 是 $s$ 上的一个 persistent set 。

Intuitively, a subset T of the set of transitions enabled in a state s of the system is called persistent in s, if all transitions not in T that are enabled in s, or in a state reachable from s through transitions not in T, are independent with all transitions in T. In other words, whatever one does from s, while remaining outside of T, does not interact with or affect T.

persistent-set selective search 的策略很简单：在探索每个状态时不再枚举所有可能的后继 transition ，而是仅考虑当前的 persistent set 中的 transition ，从而减小算法的状态空间。

persistent-set selective search 的伪代码如下所示：

Initiallze:
    Stack is empty;
    H is empty;
    push (s0) onto Stack;
Loop:
    while Stack is NOT EMPTY do {
        pop(s) from Stack;
        if s is NOT already in H then {
            enter s in H;
            T = Perslstent_Set(s);
            for all t in T do {
                s' = succ(s) after t; /* t is executed */
                push (s') onto Stack;
            }
        }
    }

关键在于如何对于给定的状态 $s$ 如何计算 $\text{Perslstent\_Set}(s)$ 。

$T_{enabled}(s)$ 是 $s$ 上的一个 trivial persistent set ，因为不存在不在该集合中的 enabled transition 使其能构造出需要判定的 sequence 。然而使用该集合是没有意义的，事实上使算法退化为 exhausted model checking 。

Godefroid 给出了三个计算 persistent set 的算法，依次更加精确，(VeriSoft:)致力于找到最小的 non-empty persistent set 。

Algorithm 1. Conflicting Transitions

算法 1 依据如下定义，随意选取当前状态下的一个 enabled transition $t$ ，然后将与 $t$ conflict / parallel / use can-be-dependent opts 的 transitions 都加入 persistent set 中，重复该过程直到无法加入新的 enabled transition 为止：

称 transition $t_1$ 和 $t_2$ conflict 当且仅当 $pre(t_1) \cap pre(t_2) \ne \emptyset$ ；
称 transition $t_1$ 和 $t_2$ parallel 当且仅当 $active(t_1) \cap active(t_2) = \emptyset$ ；
称 operation $op_1$ 和 $op_2$ can-be-dependent 当且仅当存在某个系统状态 $s$ 使得 $op_1$ 和 $op_2$ 在 $s$ 上 dependent 。

证明算法 1 返回的结果一定是一个 persistent set ：证明略。

Algorithm 2. Overman's Algorithm

算法 2 相比于算法 1 更精确，考虑了 disabled transitions ，考虑了每个进程在其当前局部状态下能访问的 transitions 。

算法 2 选取当前状态下的一个 enabled transition $t$ ，考虑 active for $t$ 的所有进程 $P_i$ 所构成的集合 $P$ ，然后迭代地将可能与 $P$ 中进程产生干扰的所有进程加入 $P$ 中。

具体地讲，对于 $\forall P_i \in P$ ，设进程 $P_i$ 当前的局部状态为 $s(i)$ ，则对于所有从 $s(i)$ 出发的 transition $t$ ，即 $\forall t,\ s(i) \in pre(t)$ ，将满足以下条件之一的所有进程都加入 $P$ 中：

active for $t$ ；
active for $t'$ ，其中 $t$ 和 $t'$ parallel 或 use can-be-dependent opts 。

证明算法 2 返回的结果一定是一个 persistent set ：证明略。

Algorithm 3. Stubborn Sets

算法 3 相比于算法 2 更精确，还考虑了系统中各进程的内部结构信息。

TBD.

# Sleep Set

考虑给定系统状态 $s$ 上的一个 persistent set $T(s)$ ，可能存在 independent transitions $t_1,\ t_2 \in T(s)$ ，则连续调度 $t_1t_2$ 和 $t_2t_1$ 会到达相同的状态。sleep set 的目标就是消除此类冗余调度：在从 $s$ 出发执行 $t_1$ 到达 $s_1$ 后，将 $t_2$ 加入 $s_1.SleepSet$ 以避免立即执行 $t_2$ 。

更精确地讲，状态 $s$ 上的 sleep set 是此时 enabled but will not be executed from $s$ 的全体 transitions 的集合，记为 $s.SleepSet$ 。

考虑在搜索过程中如何动态计算 sleep set 。初始时 $s_0.Sleep = \emptyset$ ；对于给定的状态 $s$ ，其后继状态的 sleep set 按如下方法计算：

从 $T(s)$ 中随意选择一个 transition $t_1$ ，执行有 $s \overset{t_1}{\Rightarrow} s'$ ，则 $s'.Sleep$ 为 $s.Sleep$ 中所有与 $t_1$ independent 的 transitions 。
从 $T(s)$ 中选择下一个 transition $t_2$ ，执行有 $s \overset{t_2}{\Rightarrow} s''$ ，则 $s''.Sleep$ 为 $s.Sleep \cup \{t_1\}$ 中所有与 $t_2$ independent 的 transitions 。
……

换句话说，后继状态的 sleep set 从 $s.Sleep$ 开始，将从 $s$ 出发已探索的所有 $t$ 列入暂停执行的范围，并将与 $t$ dependent 的 transitions 重新激活（因为 dependency 导致后续探索不再冗余）。

The general rule is thus that the sleep set associated with a state s' reached by a transition t from a state s is the sleep set that was obtained when reaching s augmented with all transitions already taken from T, and purged of all transitions that are dependent with t in s.

sleep-set-augmented persistent-set selective search 的伪代码如下所示，其中 $H(s).Sleep$ 表示 $s$ 在 $H$ 中且搜索已结束（？）时被赋予存储的 sleep set ：

Initiallze:
    Stack is empty;
    H is empty;
    s0.Sleep = EMPTY_SET;
    push (s0) onto Stack; 
Loop:
    while Stack is NOT EMPTY do {
        pop(s) from Stack;
        if s is NOT already in H then {
            enter s in H;
            T = Perslstent_Set(s) \ s.Sleep;
        } else {
            T = {t | t ∈ H(s).Sleep && t ∉ s.Sleep};
            s.Sleep = s.Sleep ∩ H(s).Sleep;
            H(s).Sleep = s.Sleep;
        }
        for all t in T do {
            s' = succ(s) after t; /* t is executed */
            s'.Sleep = {t' ∈ s.Sleep | (t, t') are independent in s}
            push (s') onto Stack;
            s.Sleep = s.Sleep ∪ {t}
        }
    }

# Improved Techniques

# POPL'05 - DPOR

DPOR 在运行时刻动态地计算 persistent set ，基于一次已完成执行的运行时信息回溯探索分叉点。

POPL'05 - Dynamic Partial-Order Reduction for Model Checking Software
Taxonomy : stateless model checking / concurrency testing / partial order reduction
Tag : dynamic partial order reduction

传统的 POR 技术利用静态信息构建 persistent set ，并在运行时刻结合 sleep set 来减少状态空间的冗余探索。然而静态方法具有精确度不足的本质缺陷。为解决该挑战，本文提出了 dynamic partial order reduction (DPOR) 技术，在运行时刻动态地计算 persistent set 。

persistent set 的本质是回答 which operations on which shared objects each process might execute in the future 这一问题。许多并发程序具有输入不确定性（例如用户输入），迫使静态方法采取保守策略（例如对于下标不确定性的数组访问，将整个数组视为 the same memory entry），大幅降低了 POR 技术减小状态空间的能力。

DPOR 先随意地完成一次完整的执行，在执行期间收集线程交互信息（例如共享内存读写），并据此标记 backtracking point（即存在 alternative transitions 的程序点），以在随后的测试中进行回溯探索。

DPOR 以随意的方式处理 non-determinism ，这里的意思似乎是：仅保证最终能探索到所有的不等价路径，而不关心其探索顺序。

# DPOR 形式化定义

DPOR 的形式化语义基于 POR 和 VeriSoft 的定义。在此基础上有：

定义并发程序的状态为全局的 共享状态 (shared state) 和每个进程的 局部状态 (local state) 所构成的集合，记为 $s = \braket{g,\ ls}\ (g \in SharedState,\ ls \in LocalStates)$ 。

记号 $ls(p)$ 表示 $ls$ 中进程 $p$ 的 local state 。
记号 $ls[p := l]$ 表示将 $ls$ 中进程 $p$ 的 local state 替换为 $l$ 所得的状态。

定义 transition $t$ 为从某个（全局）状态出发转换到另一个（全局）状态的动作，其含义为选定进程执行一个 visible op 紧接着一组有限个 invisible op ，直到该进程的下一个 visible op 之前结束。

记号 $t_{p,\ l}$ 表示进程 $p$ 处在 local state $l$ 时所执行的 transition $t$ 。
称 transition $t_{p,\ l}$ 在状态 $s = \braket{g,\ ls}$ 上 enabled ，当且仅当 $l = ls(p)$ 且 $t_{p,\ l}(g)$ is defined（？）。
记号 $proc(t)$ 表示正在执行 transition $t$ 的进程 $p$ ，即 $proc(t_{p,\ l}) \equiv p$ 。本文假设每个进程的 transitions 互不相交。

对于给定的状态 $s = \braket{g,\ ls}$ ，记号 $next(s,\ p) = t_{p,\ ls(p)}$ 表示在状态 $s$ 下进程 $p$ 下一步要执行的（唯一的）transition 。

若存在某个状态使得 transition $t_1$ 和 $t_2$ 同时 enabled ，则称 $t_1$ 和 $t_2$ may be co-enabled with each other 。

定义 transition sequence $S = t_1t_2...t_n$ ，使得存在状态 $s_1, s_2, ..., s_{n + 1}$ 满足 $s_1 \overset{t_1}{\rightarrow} s_2 ... \overset{t_n}{\rightarrow} s_{n + 1}$ ，并有如下助记符：

$S_i$ 表示 transition $t_i$ ；
$S.t$ 表示用一个额外的 transition $t$ 扩展 $S$ ；
$dom(S)$ 表示 $\{1,\ 2,\ ...,\ n\}$ ；
$pre(S,\ i)$ 表示 $s_i$ ，其中 $i \in dom(S)$ ；
$last(S)$ 表示 $s_{n + 1}$ ；
同一 transition $t$ 可以在 $S$ 中多次出现，记为 $t_i = t_j$ ；

定义 transition sequence $S$ 上的 happens-before relation $\rightarrow_S$ 如下：

若 $i < j$ 且 $S_i$ 和 $S_j$ dependent ，则 $i \rightarrow_S j$ 。

对于 $i \in dom(S)$ 和进程 $p$ ，若以下两个条件之一成立，则有 $i \rightarrow_S p$ ：

$proc(S_i) = p$ ；
$\exists k \in \{i + 1,\ ...,\ n\},\ i \rightarrow_S k \land proc(S_k) = p$ 。

相反地， $i \not \rightarrow_S p$ 意味着： $S_i$ 不是 $p$ 的 transition ，且对于任意的 $k > i$ ，要么 $S_i$ 和 $S_k$ 相互独立，要么 $S_i$ 和 $S_k$ 属于不同线程。

# DPOR 算法

在具体的算法实现中，还需为每个状态 $s$ 维护一个集合 $backtrack(s)$ ，用于

设 $Explore(S)$ 为算法主程序，接收输入 transition sequence $S$ ，则 DPOR 算法的工作流程如下：

意会吧，这太难读懂了。。暂时放弃了，和自己和解，以后再说。。

# ASE'07 - RAPOS

RAPOS 将 DPOR 的思想引入 randomized model checking ，在分叉点对偏序集进行更加均匀的随机采样。

ASE'07 - Effective Random Testing of Concurrent Programs
Taxonomy : stateless model checking / randomized model checking / concurrency testing / partial order reduction
Tag : dynamic partial order reduction
Preceding Work : POPL'05 - DPOR

randomized model checking ：受时间和空间资源的限制，model checking 不可能穷竭一个真实程序的状态空间；然而，传统的 model checking 算法通常遵循 DFS 、BFS 或其它的固定搜索策略，在有限时间下容易陷入到状态空间的局部当中。在路径分叉时使用随机策略可以有效改善此问题。

自然地，简单的随机策略是不合理的：许多路径交错是等价的，然而每个偏序集的大小并不相同，简单随机采样会导致不同偏序集的采样频率差别很大（而有 bug 的路径通常属于概率小的偏序集）。

然而，DPOR 技术并不能直接与 randomized model checking 相结合：POPL'05 - DPOR 中提出的算法需要获取指令之间的依赖关系，天然地要求对局部空间进行穷竭搜索，在随机策略下我们无法收集此类依赖关系。

RAPOS 沿用 DPOR 中对 POR 以及并发程序执行的形式化定义。

RAPOS 动态维护两个集合 $schedulable$ 和 $scheduled$ ，对于当前所处状态 $s$ ：

$schedulable$ 是状态 $s$ 处 enabled transitions 的一个子集：集合 $enabled(s) \setminus schedulable$ 包含所有希望延迟执行的 transitions ，延迟直到其 dependent transitions 被执行为止，类似于传统 POR/DPOR 中的 sleep set 。
$scheduled$ 是从 $schedulable$ 中随机选取的某个非空子集，其中所有的 transition 都相互独立：该集合事实上是算法即将调度的 transition 集，也即状态 $s$ 处的某个偏序集。

RAPOS 的工作流程如下：

初始时，令 $schedulable = enabled(s_0)$ ，然后循环执行以下动作直至不存在任何 enabled transition 。
从 $schedulable$ 中随机选取 $scheduled$ ，然后令其中包含的线程自由执行，即不控制这些 transitions 的执行顺序。
在 $scheduled$ 中的 transitions 全部执行完毕后，将 $enabled(s) \setminus schedulable$ 中已满足条件的 transitions 作为新的 $schedulable$ 集合，继续延迟剩余 transitions 的执行。

随机选取 $scheduled$ 的方法为：首先随机选取一个 transition $t$ 加入 $scheduled$ ，然后遍历每个 $t' \in schedulable$ ，若 $t'$ 与 $scheduled$ 中已有的所有 transition 相互独立，则将 $t'$ 也加入 $scheduled$ 。

# FSE'09 - Symbolic Pruning

Symbolic Pruning

SSS
Taxonomy : concurrency testing / --
Tag : --
Preceding Work : POPL'05 - DPOR

#Research #Paper Reading #Concurrency #Concurrency Testing #Partial Order Reduction

← Reading Papers - Scheduling Control Reading Papers - Coverage Criteria for Concurrency Testing→