JM233333's Blog
  • Programming Languages

    • C
    • UNIX-C
    • Python
  • Algorithms and Data Structures

    • Data Structure
    • Fundamental Algorithms
    • Graph Theory
  • GNU Toolchain

    • Bash
    • gdb
  • Development Environment

    • Ubuntu
    • QEMU
  • Development Tools

    • Git
    • VSCode
  • Operating Systems

    • Principles of Operating Systems
    • Xv6
    • Linux Kernel
  • Software Testing and Analysis

    • Software Testing
    • Software Analysis
    • Program Verification
  • LeetCode
  • XJTUOJ
  • Programming

    • Is Parallel Programming Hard
  • System

    • System Performance
  • Others

    • ...
  • Paper Reading

    • Model Checking
    • Fuzzing
    • Symbolic Execution
  • 3D Game Programming

    • 3D Mathematics
  • Miscellaneous

JM233333

弱小可怜又无助的学术废物
  • Programming Languages

    • C
    • UNIX-C
    • Python
  • Algorithms and Data Structures

    • Data Structure
    • Fundamental Algorithms
    • Graph Theory
  • GNU Toolchain

    • Bash
    • gdb
  • Development Environment

    • Ubuntu
    • QEMU
  • Development Tools

    • Git
    • VSCode
  • Operating Systems

    • Principles of Operating Systems
    • Xv6
    • Linux Kernel
  • Software Testing and Analysis

    • Software Testing
    • Software Analysis
    • Program Verification
  • LeetCode
  • XJTUOJ
  • Programming

    • Is Parallel Programming Hard
  • System

    • System Performance
  • Others

    • ...
  • Paper Reading

    • Model Checking
    • Fuzzing
    • Symbolic Execution
  • 3D Game Programming

    • 3D Mathematics
  • Miscellaneous
  • model-checking

  • fuzzing

  • symbolic-execution

  • verification

  • concurrency-testing

    • Reading Papers - Concurrency Testing Overview
    • Reading Papers - Data Race Detection
    • Reading Papers - Atomicity Violation
    • Reading Papers - Scheduling Control
    • Reading Papers - Partial Order Reduction
      • Introduction
      • Traditional Techniques
        • LNCS'96 - Godefroid *
      • Improved Techniques
        • POPL'05 - DPOR
        • ASE'07 - RAPOS
    • Reading Papers - Coverage Criteria for Concurrency Testing
  • crash-consistency

  • kernel-testing

  • others

  • Reading Papers 00 - Related Works
  • Reading Papers 01 - Model Checking
  • Reading Papers 03 - Symbolic Execution
  • Reading Papers 04 - Verification
  • Reading Papers 02 - Crash Consistency
  • Reading Papers 10 - System Design
  • Reading Papers 20 - Others
  • FUCK-ELF
  • paper-reading
  • concurrency-testing
JM233333
2023-04-01
5957

Reading Papers - Partial Order Reduction

Creative Commons

# 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 t1t_1t1​ 和 t2t_2t2​ 满足以下条件,则称其为一组 independent transitions :

  • independent transitions can neither disable nor enable each other;

  • commutativity of enabled independent transitions :对于系统的任意状态 sss ,若 t1,t2t_1,\ t_2t1​, t2​ 均为 enabled ,则存在唯一的 s′s's′ 满足 s⇒t1t2s′∧s⇒t2t1s′s \overset{t_1t_2}{\Rightarrow} s' \land s \overset{t_2t_1}{\Rightarrow} s's⇒t1​t2​s′∧s⇒t2​t1​s′ 。

可以利用 independent transitions 的概念来定义 execution trace(即 sequence of states and transitions)之间的等价性:对于两个执行 E1E_1E1​ 和 E2E_2E2​ ,若 E2E_2E2​ 可以通过(多次)交换 E1E_1E1​ 中相邻的一组 independent transitions 得到,则称 E1E_1E1​ 和 E2E_2E2​ 是等价的。

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

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

  • 若 active for (?) t1,t2t_1,\ t_2t1​, t2​ 的进程集不相交,即 active(t1)∩active(t2)=∅active(t_1) \cap active(t_2) = \emptysetactive(t1​)∩active(t2​)=∅ ,则二者必互相独立。

  • 若 t1,t2t_1,\ t_2t1​, t2​ 可访问的对象集不相交,则二者必互相独立。

# Persistent Set

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

若从 sss 出发的任意 与 T(s)T(s)T(s) 无关的 non-empty transition sequence t1t2...tn(∀i∈[1,n],ti∉T(s))t_1t_2...t_n\ (\forall i \in [1,\ n],\ t_i \notin T(s))t1​t2​...tn​ (∀i∈[1, n], ti​∈/​T(s))

s→t1s1→t2s2⋯→tnsn(∀i∈[1,n],ti∉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))s→t1​s1​→t2​s2​ ⋯→tn​sn​ (∀i∈[1, n], ti​∈/​T(s))

均有 tnt_ntn​ 与 ∀t∈T(s)\forall t \in T(s)∀t∈T(s) 互相独立,则称 T(s)T(s)T(s) 是 sss 上的一个 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;
            }
        }
    }

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

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

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

Algorithm 1. Conflicting Transitions

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

  • 称 transition t1t_1t1​ 和 t2t_2t2​ conflict 当且仅当 pre(t1)∩pre(t2)≠∅pre(t_1) \cap pre(t_2) \ne \emptysetpre(t1​)∩pre(t2​)​=∅ ;

  • 称 transition t1t_1t1​ 和 t2t_2t2​ parallel 当且仅当 active(t1)∩active(t2)=∅active(t_1) \cap active(t_2) = \emptysetactive(t1​)∩active(t2​)=∅ ;

  • 称 operation op1op_1op1​ 和 op2op_2op2​ can-be-dependent 当且仅当存在某个系统状态 sss 使得 op1op_1op1​ 和 op2op_2op2​ 在 sss 上 dependent 。

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

Algorithm 2. Overman's Algorithm

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

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

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

  • active for ttt ;

  • active for t′t't′ ,其中 ttt 和 t′t't′ parallel 或 use can-be-dependent opts 。

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

Algorithm 3. Stubborn Sets

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

TBD.

# Sleep Set

考虑给定系统状态 sss 上的一个 persistent set T(s)T(s)T(s) ,可能存在 independent transitions t1,t2∈T(s)t_1,\ t_2 \in T(s)t1​, t2​∈T(s) ,则连续调度 t1t2t_1t_2t1​t2​ 和 t2t1t_2t_1t2​t1​ 会到达相同的状态。sleep set 的目标就是消除此类冗余调度:在从 sss 出发执行 t1t_1t1​ 到达 s1s_1s1​ 后,将 t2t_2t2​ 加入 s1.SleepSets_1.SleepSets1​.SleepSet 以避免立即执行 t2t_2t2​ 。

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

考虑在搜索过程中如何动态计算 sleep set 。初始时 s0.Sleep=∅s_0.Sleep = \emptysets0​.Sleep=∅ ;对于给定的状态 sss ,其后继状态的 sleep set 按如下方法计算:

  • 从 T(s)T(s)T(s) 中随意选择一个 transition t1t_1t1​ ,执行有 s⇒t1s′s \overset{t_1}{\Rightarrow} s's⇒t1​s′ ,则 s′.Sleeps'.Sleeps′.Sleep 为 s.Sleeps.Sleeps.Sleep 中所有与 t1t_1t1​ independent 的 transitions 。

  • 从 T(s)T(s)T(s) 中选择下一个 transition t2t_2t2​ ,执行有 s⇒t2s′′s \overset{t_2}{\Rightarrow} s''s⇒t2​s′′ ,则 s′′.Sleeps''.Sleeps′′.Sleep 为 s.Sleep∪{t1}s.Sleep \cup \{t_1\}s.Sleep∪{t1​} 中所有与 t2t_2t2​ independent 的 transitions 。

  • ……

换句话说,后继状态的 sleep set 从 s.Sleeps.Sleeps.Sleep 开始,将从 sss 出发已探索的所有 ttt 列入暂停执行的范围,并将与 ttt 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).SleepH(s).SleepH(s).Sleep 表示 sss 在 HHH 中且搜索已结束(?)时被赋予存储的 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=\braketg,ls(g∈SharedState,ls∈LocalStates)s = \braket{g,\ ls}\ (g \in SharedState,\ ls \in LocalStates)s=\braketg, ls (g∈SharedState, ls∈LocalStates) 。

  • 记号 ls(p)ls(p)ls(p) 表示 lslsls 中进程 ppp 的 local state 。

  • 记号 ls[p:=l]ls[p := l]ls[p:=l] 表示将 lslsls 中进程 ppp 的 local state 替换为 lll 所得的状态。

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

  • 记号 tp,lt_{p,\ l}tp,l​ 表示进程 ppp 处在 local state lll 时所执行的 transition ttt 。

  • 称 transition tp,lt_{p,\ l}tp,l​ 在状态 s=\braketg,lss = \braket{g,\ ls}s=\braketg, ls 上 enabled ,当且仅当 l=ls(p)l = ls(p)l=ls(p) 且 tp,l(g)t_{p,\ l}(g)tp,l​(g) is defined(?)。

  • 记号 proc(t)proc(t)proc(t) 表示正在执行 transition ttt 的进程 ppp ,即 proc(tp,l)≡pproc(t_{p,\ l}) \equiv pproc(tp,l​)≡p 。本文假设每个进程的 transitions 互不相交。

对于给定的状态 s=\braketg,lss = \braket{g,\ ls}s=\braketg, ls ,记号 next(s,p)=tp,ls(p)next(s,\ p) = t_{p,\ ls(p)}next(s, p)=tp,ls(p)​ 表示在状态 sss 下进程 ppp 下一步要执行的(唯一的)transition 。

若存在某个状态使得 transition t1t_1t1​ 和 t2t_2t2​ 同时 enabled ,则称 t1t_1t1​ 和 t2t_2t2​ may be co-enabled with each other 。

定义 transition sequence SSS 为 s1→t1s2...→tnsn+1s_1 \overset{t_1}{\rightarrow} s_2 ... \overset{t_n}{\rightarrow} s_{n + 1}s1​→t1​s2​...→tn​sn+1​ ,并有如下助记符:

  • SiS_iSi​ 表示 tit_iti​ ;

  • S.tS.tS.t 表示用一个额外的 transition ttt 扩展 SSS ;

  • dom(S)dom(S)dom(S) 表示 {1,2,...,n}\{1,\ 2,\ ...,\ n\}{1, 2, ..., n} ;

  • pre(S,i)pre(S,\ i)pre(S, i) 表示 sis_isi​ ,其中 i∈dom(S)i \in dom(S)i∈dom(S) ;

  • last(S)last(S)last(S) 表示 sn+1s_{n + 1}sn+1​ ;

  • 同一 transition ttt 可以在 SSS 中多次出现,记为 ti=tjt_i = t_jti​=tj​ ;

定义 transition sequence SSS 上的 happens-before relation →S\rightarrow_S→S​ 如下:

  • 若 i<ji < ji<j 且 SiS_iSi​ 和 SjS_jSj​ dependent ,则 i→Sji \rightarrow_S ji→S​j 。

对于 i∈dom(S)i \in dom(S)i∈dom(S) 和进程 ppp ,若以下两个条件之一成立,则有 i→Spi \rightarrow_S pi→S​p :

  • proc(Si)=pproc(S_i) = pproc(Si​)=p ;

  • ∃k∈{i+1,...,n},i→Sk∧proc(Sk)=p\exists k \in \{i + 1,\ ...,\ n\},\ i \rightarrow_S k \land proc(S_k) = p∃k∈{i+1, ..., n}, i→S​k∧proc(Sk​)=p 。

相反地,i̸→Spi \not \rightarrow_S pi​→S​p 意味着:SiS_iSi​ 不是 ppp 的 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→

最近更新
01
Reading Papers - File System Verification
03-01
02
LeetCode 0115 - Distinct Subsequences
02-13
03
Linux 00 - Introduction
02-01
更多文章>
Theme by Vdoing | Copyright © 2019-2023 JM233333 | CC BY-NC-SA 4.0
  • 跟随系统
  • 浅色模式
  • 深色模式
  • 阅读模式