Reading Papers - Scheduling Control
# Scheduling Control
# PLDI'07 - ICB
ICB 即 iterative context-bounding ,区分抢占式和非抢占式的上下文切换,通过限制抢占式上下文切换的次数对被测程序的调度空间进行系统性的探索,在遏制状态空间爆炸的同时避免限制探索执行的深度。
PLDI'07 - Iterative Context Bounding for Systematic Testing of Multithreaded Programs
Taxonomy : scheduling control
Tag : scheduling control
KEY Idea :限制抢占式上下文切换的次数,但完全不限制非抢占式调度。
- 若发生调度时,让出 CPU 的线程是 runnable 的,则称此次上下文切换为 抢占式上下文切换 (preempting context switch, or preemption) ,例如时间片到期时。否则为非抢占式调度,例如阻塞等待资源时。
限制 preemption 的次数不会限制 model checker 深入探索状态空间的能力:正确实现的系统应当能在不存在 preemption 的情况下正常执行完成。
本文将访问不同状态的数量作为 coverage 的度量,而非传统的代码覆盖(行、分支、路径等)。在该度量上,ICB 比 depth-bounded dfs 要强上几个数量级。
ICB 搜索算法 :
ICB 迭代地增加 preemption bound :算法在探索 preemption 次数为 的执行之前,会先探索完所有 preemption 次数为 的执行。
ICB 能够找到触发错误所需的最小 preemption 次数。
ICB 认为程序中的每个线程都在执行一系列的步骤 (steps) ,每个步骤都涉及对共享变量的一次访问,在执行每个步骤之后都可以进行调度,因此可能的交错数是每个线程的执行步数的指数。
设线程数为 ,执行步数为 ,其中最多 个步骤是(潜在)阻塞的,设 preemption 次数固定为 ,则可能的交错数上界为 ,仅为执行步数 的多项式。考虑到 远小于 ,ICB 确实有效地遏制了状态空间爆炸。
事实上,在每次共享内存访问后都 enable preemption choice 是没有必要的,只需要在被测程序的每个同步操作之前插入调度点就足够了。本质上这是一种 partial reduction 策略,可以进一步缩小状态空间,并且不会遗漏任何错误,具体证明详见论文正文及附录。
ICB 讨论 :
对于给定的深度限制 ,depth-bounded search 可以保证被测程序在不超过 步的执行内没有错误。这种方法适用于 message-passing software ,但不适用于多线程程序,因为前者的感兴趣的行为和错误都出现在从初始状态出发后的少量步骤中。
本文认为,model checking 多线程程序类似于在 non-deterministic scheduler 上运行被测程序,然后系统性地探索 scheduler 做出的每个选择。
# PLDI'08 - RaceFuzzer
RaceFuzzer 利用已有静态检测工作报告的潜在错误来指导运行时刻的线程随机调度。
PLDI'08 - Race Directed Random Testing of Concurrent Programs
Taxonomy : scheduling control
Tag : scheduling control
Key Idea :存在许多已有工作利用静态的方法检测或预测 data race ,无需执行被测程序,但误报率很高。可以利用这些信息来指导动态的检测方法,发挥静态方法优势的同时规避其缺陷。
RaceFuzzer 的策略分为两个阶段:首先通过静态方法获取一系列有 potential data race 的 statement pair ,然后利用这些信息来指导运行时刻的线程随机调度。
在第一阶段,RaceFuzzer 实现了已有工作 hybrid-race detection 的算法。
在第二阶段,依次分别处理每个 statement pair :
通常情况下,RaceFuzzer 以朴素的方式进行随机调度。
如果某个线程执行到了某个 ,则将该线程挂起并标记为 postponed thread 。
如果某个线程执行到了某个 且已有其它 postponed thread ,则根据运行时信息(例如是否同时读写同一内存)判定是否存在 real race 。
- 发现 real race 之后,RaceFuzzer 会挂起其中一个线程并让另一个线程继续执行,观测该 potential race 是否引起了什么不好的事情。
如果一直没有发现 real race ,则这些线程会被持续挂起,直到所有线程都被挂起时随机唤醒一个线程以避免程序停滞。
如果没有 postponed thread 且没有线程可被调度,则判定存在死锁。
RaceFuzzer 不保证总能识别出 potential race 中的所有 real race(为什么?),也不能辨别良性的 data race 。
# ASPLOS'11 - PCT
PCT 即 probabilistic concurrency testing ,是一种随机化的并发调度算法。PCT 提供了在每次 test run 中找到某个并发错误的数学概率,因而重复独立运行 test run 能够将发现错误的概率提高到任意所期望的值。
ASPLOS'10 - PCT - A Randomized Scheduler with Probabilistic Guarantees of Finding Bugs
Taxonomy : scheduling control / probabilistic testing
Tag : scheduling control
Key Idea :并发错误通常仅涉及少数线程执行的少数指令之间的交互。
PCT 的设计旨在为深度较小的错误提供更好的保证:在每次 test run 中,PCT 专注于概率性地查找特定深度 的错误。
定义 ordering constraint 为调度中不同线程的指令之间的调用顺序约束。显然,一些约束可能会触发错误,而不同的约束可能会触发相同的错误。
定义并发错误的 深度 (depth) 为触发错误所需的 ordering constraints 的最小数量。直观地,深度越大的错误越难以被发现。
设被测程序最多创建 个线程、每个线程最多执行 条指令,则对于一个深度为 的 BUG ,PCT 在每次 test run 中以不小于 的概率找到此 BUG 。
PCT 调度算法 :
PCT scheduler 为每个线程维护一个优先级,仅调度具有最高优先级的、当前可运行的线程。换句话说,一个线程被调度当且仅当所有比它优先级更高的线程都被阻塞。
PCT 会在每次 test run 时将被测程序的某些程序点设为 priority change point ,并为每个点关联一个预定的优先级值。当线程执行到 priority change point 时,PCT 将当前线程的优先级更改为与之关联的优先级值。
具体地讲,设被测程序最多创建 个线程、每个线程最多执行 条指令,则对于一个深度为 的 BUG ,PCT 按如下方式工作:
初始时,将 个优先级值 随机分配给每个线程。
将 个 priority change point 随机分布在范围 内。不妨设第 个点位于第 条指令处,且其关联的优先级值为 。
根据优先级调度线程,并在某个线程执行到第 条指令时将其优先级更改为 。(?:是否应该为第一个执行到此处的线程?)
PCT 的调度是序列化的,即每一步只有一个线程在执行。
基于以下原因,在实践中 PCT 的表现可能比最坏界限更好:
同一个错误可能对应于多种不同的调度,这提高了发现错误的几率。
有时同一个 priority change point 落在多个程序点之一(或某个程序段范围内)就足以触发错误。
有时同一段有错误的代码段可能会被同一个或不同的线程重复执行多次,这提供了多个触发错误的机会。
# OSDI'14 - SKI (to-be-reread)
SKI 基于 PCT 算法扩展了对中断的支持,并且针对中断优化了 PCT 调度策略。
SKI 实现 :
TBD.
SKI 优化 :
Key Idea :在实践中,通过很少的 reschedule point 就能触发大多数并发错误;在实践中,通过少量线程和少量并发请求就能触发许多并发错误。
SKI 限制 reschedule point 仅会出现在 communication point 处,以避免测试冗余的调度。
- 定义 communication point 为一条指令,该指令会访问其它线程在测试期间访问的内存位置,并且其中存在至少一个写操作。
SKI 在每次运行期间跟踪 memory trace 并生成一组潜在的 communication point 。此过程不依赖于 sample run ,各次运行的潜在点集会被合并累积,可以视为一个迭代的学习过程,前次累积的点集会被用于下一次运行。
# SOSP'21 - Snowboard
Key Idea : overlapped memory access in different threads means potential concurrency bugs
- PMC : Potential Memory Communication
对于由其它 input generator (e.g. Syzkaller) 生成的每个系统调用序列,在单线程下,从固定的初始状态出发执行并记录 memory trace 。存在对相同地址的读写访问的输入被绑定为 PMC-Based Input Pair 。
基于 SKI ,将 PMC 作为 scheduling hint 使用,在 PMC 指令附近频繁 schedule 。
- 01
- Reading Papers - Kernel Concurrency06-01
- 02
- Linux Kernel - Source Code Overview05-01
- 03
- Linux Kernel - Per-CPU Storage05-01