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 ，基于一次已完成执行的运行时信息回溯探索分叉点。

DPOR
Taxonomy : 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 形式化定义

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$ 为 $s_1 \overset{t_1}{\rightarrow} s_2 ... \overset{t_n}{\rightarrow} s_{n + 1}$ ，并有如下助记符：

$S_i$ 表示 $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 ，且

# DPOR 算法

# ASE'07 - RAPOS

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

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