基于静态分析的RTOS内核高级竞争检测

雷卡·派1 ·阿比舍克·辛格2 ·迪帕克·德索萨1 ·米纳克希·德索萨2 ·普拉提巴·普拉卡什1

1 引言

在多线程程序中，当两个用户指定的代码段（或“临界访问”）本应互斥地访问一组共享变量或数据结构体，却最终发生“重叠”或相互交错时，就会出现高层竞争。在执行过程中，高层竞争通常是导致原子性违反的原因，从而引起软件出现意外的错误行为。

本文的研究重点是实时操作系统（RTOS）内核API函数中发生的高层竞争，这些系统通常用于嵌入式软件。在单处理器核心上，应用程序的多个任务线程或中断服务例程（ISRs）以交错方式调用RTOS的内核API。检测RTOS内核API中的高层竞争既重要又具有挑战性。之所以重要，是因为这些RTOS内核广泛应用于航空航天、汽车和医疗领域的安全关键型嵌入式应用，此处的高层竞争可能导致严重不良后果。此外，内核（相对于应用程序）中的单个竞争可能会影响许多使用该内核的应用程序。最后，这一问题具有挑战性，因为这些内核 invariably 使用非标准同步机制，例如禁用/启用中断、挂起调度器，并且通常依赖于回调和软件中断（SWI）等专用线程的相对调度优先级。

目前用于查找嵌入式内核中高层竞争的技术通常依赖于基于模型检测的方法，因为在这种方法中更容易建模特定的同步和上下文切换语义。该方法通过构建一个“最通用”应用程序 A的模型，非确定性地调用所有内核API函数，并使用模型检测工具穷尽地搜索高层竞争。虽然这是一种精确度很高且误报率很低的方法，但它存在一些固有的缺点。首先，最通用的应用程序 A必须预先固定每种类型线程（任务、ISR等）的数量。除非有复杂且RTOS特定的元论证支持该选择的充分性，如 [16],中所述，否则这种选择可能导致分析的不健全性。例如，最通用的应用程序 A可能将任务线程数量固定为2，而某个高层竞争需要3个或更多任务线程才能触发。在这种情况下，模型检测器会不健全地声明该特定高层竞争不会发生。其次，即使线程数量固定，状态空间也可能过于庞大，导致模型检测器无法完成其搜索 [16]。

本文提出了一种基于代码静态分析的可靠且高效的解决方案。我们的技术基于最近在[6]中提出的不相交块概念。就像经典多线程程序中位于获取和释放公共锁之间的两段代码一样，在并发程序的控制流图中，如果两个（代码）块模式在程序执行过程中永远不会“重叠”，则它们构成一对不相交块。我们的高层竞争检测算法本质上对内核API函数进行不相交块分析，然后检查每一对冲突的关键访问是否被某对不相交块所“覆盖”。如果是，则分析判定该对访问永远不会涉及高层竞争。此结论与应用程序中运行的线程数量无关。

我们已在四个重要的现代RTOS内核上实现并评估了我们的方法。第一个是基于ARINC 653的印度主要航空公司的专有实时操作系统，用于管理其飞机的导航系统。出于保密原因，我们将该RTOS称为“P‐RTOS”，其特点是使用了优先级介于任务和中断服务例程之间的回调例程。另外三个是流行的开源实时操作系统——来自德州仪器的TI‐RTOS [15]、作为现代自动驾驶软件（如ArduPilot [1],）首选 RTOS的ChibiOS [7]，以及来自Real‐Time Engineers的FreeRTOS [5]。这些实时操作系统各自具有不同的特性，需要设计专门的分析方法。例如，TI‐RTOS的特点是使用软件中断（SWI），而ChibiOS允许让出和嵌套中断。我们的分析发现，在几秒钟的运行时间内，发现了除ChibiOS外的每种实时操作系统中存在的多个有害高层竞争，并且误报率较低。我们已与这些实时操作系统的开发者取得联系，其中许多问题他们已经修复或计划修复。

这项工作的初步版本已作为扩展摘要发表在[22]中。与该版本相比，本文增加了案例研究（ChibiOS）、更详细的定义以及正确性证明。

本文的组织结构如下。第2节通过P‐RTOS应用程序示例描述了内核中高层数据竞争的问题，并概述了我们的分析方法论。我们在第3节描述了带回调的中断驱动程序的语法与语义，并在第4节定义了高层竞争。第5节介绍了我们使用不相交块的竞争检测算法，第6节提出了针对P‐RTOS内核的分析技术。接下来的几节分别描述了我们将该方法应用于TI‐RTOS（第7节）、ChibiOS（第8节）和FreeRTOS（第9节）。第10节描述了我们开发的工具Rtos-Racer的实现及其在四个案例研究上的评估。最后，第11节讨论了相关工作，我们在第12节进行总结。

2 概述

我们首先通过一个来自P‐RTOS内核的示例，概述我们的技术。然后介绍所采用的一般方法论的概述。

2.1 动机示例

P‐RTOS应用程序可以创建一组线程，这些线程分为三种类型：任务、回调和中断服务例程。除了使用标准C语句外，线程还可以调用LockPreemption函数，该函数具有“锁定”或“禁用”其他任务线程抢占的效果；以及调用UnlockPreemption函数以允许任务线程进行抢占。线程以交错方式进行执行，并受到某些限制。首先，回调必须在执行前被“激活”。线程之间可能相互抢占，但需遵循以下规则：（a）当LockPreemption生效时，任务不能被其他任务抢占；（b）当LockPreemption生效时，回调不能执行；（c）中断服务例程和回调不能被抢占——一旦开始执行，就会一直运行到完成。

图 1 显示了P‐RTOS内核代码的一部分。内核API函数 ProcessResume以指向任务的进程控制块（PCB）的指针作为参数，首先确保给定任务处于延迟队列中（ WAITING状态）。然后将其从延迟队列移动到就绪队列。后一部分操作在 LockPreemption命令的作用域内完成。 Tick_ISR是一个处理定时器中断的ISR线程。其主要工作是递增节拍计数，然后激活 TimeDelay回调。该 TimeDelay回调本质上会扫描延迟队列，将唤醒时间已到的任务移至就绪队列。

作为开发人员，我们可以将 ProcessResume 中的第3‐9行标记为临界访问A。这段代码访问了延迟队列和就绪队列等内核结构，并且显然必须与其他对这些结构之一的临界访问“互斥地”执行，否则数据结构可能会进入不一致或错误的状态。类似地，TimeDelay 中的第2‐16行可以被视为对延迟队列和就绪队列以及节拍计数变量的一个临界访问B。

我们说，如果某个应用程序的执行过程中调用了这些内核例程，导致临界访问 A和B在执行中发生交错（或重叠），则发生了涉及这两个临界访问的高层竞争。

现在考虑一个包含两个任务P和Q的P‐RTOS应用程序。假设当前节拍计数（记录在内核变量Tick_Count中）值为100，任务Q位于延迟队列中，其唤醒时间为 101。当前正在运行的任务P调用了以任务Q作为参数的ProcessResume内核例程。第3行的检查通过，因为Q处于延迟队列中且其状态为WAITING。然而，在第5行尝试锁定抢占之前，发生了一个定时器中断，Tick_ISR开始执行，将节拍计数增加到101，并激活TimeDelay回调。由于抢占尚未被锁定，TimeDelay例程得以运行，并将任务Q从延迟队列移至就绪队列。当执行切回任务P时，它试图在第7行从延迟列表中移除Q。由于它试图移除一个不在列表中的任务，这将导致一个异常。

此场景表现出涉及临界访问A和B的高层竞争（注意在此场景中，代码段A和 B在时间上存在重叠）。此外，该竞争是有害的，因为我们达到了一种系统状态（即出现异常条件），而这种状态在两个临界访问以串行方式（即无重叠）serially 执行的任何执行过程中都无法达到。

我们现在描述报告高层竞争的技术。由ProcessResume中的第6‐9行和 TimeDelay中的第1‐16行组成的两个着色块构成了一对不相交块，因为根据执行语义，它们在执行过程中永远不会重叠。这是因为第一个块处于锁抢占的作用域内，因此不能被回调线程中断。类似地，第二个块作为回调线程的一部分，也不能被任何线程中断。我们的竞争检测算法本质上是检查临界访问A和B是否被不相交块的配对“覆盖”（详见第5节）。在此情况下，它们并未被覆盖，因此我们判定A和B可能存在高层竞争。

我们注意到，更好的编程规范应该是在第3行之前（而不是第5行）放置 lockpreem（以及在第11行之后对应地放置unlockpreem）。在这种情况下，临界访问将被不相交块所覆盖，我们的算法会判定这对访问是安全的。

我们注意到，在此示例中，开发人员识别这些问题并不十分困难。然而在实际中，由于多种原因，要正确处理这些问题并不容易。首先，尽管单个临界访问本身可能较容易识别，但由于代码上下文中的复杂控制流（例如，开发人员可能在调用包含临界访问代码的过程之前就已设置同步机制，代码周围可能存在循环和条件语句、嵌套或重复的同步命令，以及深层控制流中的让出操作），程序员很难确定该代码必须位于哪些同步块中。其次，程序员仅查看单个临界访问是不够的，她必须检查每一对冲突的关键访问，以确定它们所处的同步块，并确保至少有一对这样的块是互不重叠的。我们注意到，在本文分析的每个实时操作系统中，此类配对的数量都高达数千。因此，拥有一种能够自动排除大量安全配对，并将剩余配对提交给开发人员进行人工检查的工具是非常有用的。

2.2 方法论概述

我们现在概述在四个案例研究中所遵循的通用方法论。在以下描述中，我们将非正式地介绍一些术语，这些术语将在后续章节中进行更正式的定义。

假设我们有一个实时操作系统内核库R，它包含一组内核结构体和API函数。

1. 编程语言LR 。我们首先将一种并发编程语言 LR与实时操作系统内核R相关联，旨在捕捉使用R的应用程序的交错执行语义。该编程语言的语法及其基本指令的语义本质上与应用程序和内核API的宿主语言（通常是C语言）相同。然而，内核API可能会使用一些低级汇编宏，例如 disableint用于禁用中断，lockpreem用于防止某些线程的抢占，或 sysSwitch用于在线程之间切换上下文。这些宏在LR中被保留为高级命令。内核实际上为应用程序中的线程指定了执行语义，这种语义被捕捉在LR程序的操作语义中。

在现实生活中，应用程序的执行依赖于中断（例如定时器或其他设备产生的中断），这些中断可能在应用程序执行过程中的不同时间点发生。为了应对这一问题，我们对中断的具体发生时机进行抽象，并保守地允许在线程之间进行非确定性上下文切换，当然这要取决于中断是否被禁用等条件。我们还可以进一步抽象掉其他特性，例如任务线程之间的执行优先级，因为我们的关注点在于内核中的竞争问题，而对优先级建模对我们没有任何帮助。基于这些原因，我们所使用的语言 LR的语义可以是更精确原始语义的一个较弱版本（或保守的过近似）。

2. 定义高层竞争 。给定一个在LR中具有标记的临界访问的程序P，我们说，在P的一次执行中，如果两个冲突的关键访问(A, B)在该执行中发生时间重叠，则它们涉及一次高层竞争。类似地，如果在R的API中已标记了临界访问，我们可以说，R中的一对冲突的关键访问(A, B)是存在竞争的，如果存在某个R‐应用程序 A以及一次 A的执行在由 LR给出的语义中，它们涉及高层竞争；否则，对(A,B)是非竞争的。

3. 静态分析 。对于一个LR程序P，其临界访问已被标记，我们展示如何对其进行静态分析，以可靠地判定访问配对为非竞争的。该分析基于为语言LR识别不相交块模式。

4. R的高层竞争分析 。假设我们已经标记出R的API函数中的临界访问。我们将上述分析进行扩展，以可靠地声明R中某些访问配对为非竞争的，具体方法如下。我们首先在LR中创建一个最通用的“元”应用程序M，它表示一系列应用程序 A1, A2,…，使得如果R中的一对访问(A, B)存在竞争，则该竞争会在某个Ai中体现。我们的静态分析算法现在分析M，并可靠地声明R中的某些访问配对为非竞争的。

在接下来的几节（第3–6节）中，我们将针对第一个案例研究P‐RTOS详细遵循此方法论。对于其余的案例研究，我们将简要介绍该方法论中的关键步骤。

3 带回调的中断驱动程序

在接下来的几节中，我们将重点讨论P‐RTOS实时操作系统。在本节中，我们描述一种多线程编程语言，旨在捕捉内联调用内核例程的P‐RTOS应用程序的语义。这种语言对应于我们在方法论中所称的 LP-RTOS，但为了可读性和表述方便进行了大量简化。我们将其称为带回调的中断驱动程序语言（简称IDC）。

IDC程序具有固定数量的有限线程和固定数量的全局变量。每个线程属于以下三种类型之一：任务线程，类似于标准线程；ISR线程，表示中断服务例程；以及由ISR线程激活的回调线程。其中有一个主程序线程，它是一个任务线程，并且是初始时唯一被启用的任务线程。该主程序线程可以初始化变量，然后调用启动命令以启用调度器并开始执行。

任务线程可以被其他任务线程或回调线程抢占（当中断未被禁用且调度器未被挂起时），或被ISR线程抢占（当中断未被禁用时）。回调线程初始状态为禁用，可通过来自中断服务例程的激活命令启用。一旦激活，回调可以在中断未被禁用且调度器未被挂起时执行。ISR线程和回调线程不能被抢占，必须运行至结束。回调线程在执行结束后会被禁用，之后可通过来自中断服务例程的激活命令再次启用。

线程使用一组标准命令访问一组共享全局变量，这些命令包括形式为 x := e 的赋值语句、条件语句（if‐then‐else）、循环语句（while）等。任务线程还可以使用 lockpreem、unlockpreem（分别用于挂起和恢复调度器）以及 disableint、 enableint（分别用于禁用和启用中断）等命令。表1展示了在变量集V和线程集T上的一组基本语句cmdV,T。

形式化地，我们将IDC程序P表示为一个元组P =(V , T)，其中V是一个有限的整数变量集合， T是一个有限的命名线程集合。每个线程 t ∈ T 具有一种类型，该类型是任务、中断服务例程或回调中的一种，并具有一个关联的控制流图，其形式为 Gt=(Lt, st, instt)，其中 Lt是线程t的一个有限位置集合，st ∈Lt是线程t的起始位置，instt ⊆Lt × cmdV,T × Lt是线程t的一个有限指令集合。对于一条指令 ι= 〈l, c, l′ instt，我们将 l 和 l′ 分别称为 ι 的源位置和目标位置，tid(ι) 表示线程 t。对于函数 f : A → B，我们定义 f[a → b] 为函数 g : A → B，其中 g(a′)= f(a′) 当 a′ = a，否则 g(a′)= b。对于在变量V 上的布尔值或算术表达式 e，以及一个赋值 φ: V → Z，我们用 eφ 表示在赋值 φ 下求值 e 所得到的值。

图 2展示了一个包含主程序线程、一个名为consume的任务线程、一个名为 service-packet的中断服务例程线程和一个produce回调线程的IDC程序示例。当中断对应的数据包到达时，ISR线程运行，并激活produce回调，该回调将数据包转换为项目。然后consume线程消费项目，并确保在此期间锁定抢占。

我们使用标记迁移系统（LTS）来定义IDC程序的操作语义。设P=(V, T)为一个程序。我们定义一个对应于P的标记迁移系统（LTS）TP=(Q Σ, s ⇒)，其中

– Q 是一组状态，形式为 (pc, enab, rt, it, id, pl φ)，其中 pc ∈T → L 是程序计数器，给出每个线程的当前位置， φ ∈ V → Z 是变量的赋值，enab ⊆T 是启用的线程集合，rt ∈T 是当前运行的线程，it ∈ T 是当调度器被挂起时被中断的任务线程； id 和 pl 是布尔值，用于指示中断是否被禁用（id =true 表示禁用，id = false 表示未禁用）以及调度器是否被挂起（pl (true=表示挂起，pl ) false(表示未挂起）。

– 标签集合 Σ 是程序 P 的指令集 instP。

– 初始状态 s 为 (λt.st,{main}, main, main,true,true λx.0)。因此在初始状态中，所有线程都位于其入口位置，只有主线程是启用并运行的，被中断的任务线程设为 main（这是一个占位值，因为仅在调度器被挂起时使用），中断被禁用，调度器被挂起，且初始环境将所有变量设为 0。

– 对于指令 ι= 〈l, c, l′〉 ∈ instΣ，其中 tid(ι)=t，我们定义

(pc, enab,rt,it,id,pl φ) ⇒ι(pc′ , enab ′ , rt′ ,it′ ,id′ ,pl′, φ ′ ) iff 满足以下条件：

– t ∈enab;

– 如果rt是 ISR 或回调线程，则 t= rt。这确保了 ISR 和回调线程能够运行至完成。如果rt是任务线程，则表 t上的条件在表 2中针对不同的 id和 pl 值进行了定义。因此，如果运行中的线程是任务线程，则执行当前指令的线程 t可以是任意启用的线程（当中断未被禁用且调度器未被挂起时）；或是运行中的线程或 ISR 线程（当中断未被禁用但调度器被挂起时）；或仅能是运行中的线程（当中断被禁用时）。

– 根据命令c，必须满足以下条件： 如果c是跳过命令，则φ′= φ，id′=id且pl′= pl。如果c是启动命令，则t=主程序 并且φ′= φ。如果 c是一个形式为 assume(b)的命令，那么 bφ= true， φ′= φ，id′=id和pl′= pl。如果 c是一个形式为 x := e 的赋值语句，那么 φ′= φ[x → eφ]，id′=id和pl ′= pl。如果c是一个 activate(u)命令，那么 t必须是一个 ISR线程，u必须是一个回调线程， φ′= φ，id′=id，以及 pl′= pl。如果 c是一个 disableint 命令，那么 t必须是一个任务线程，φ ′= φ，id′= true和pl ′= pl。如果 c是一个 enableint 命令，那么 t必须是一个任务线程，φ ′= φ，id′=f alse和pl ′= pl。如果c是lockpreem命令，则t必须是任务线程，φ ′= φ，id′=id，且pl′=真。如果c是unlockpreem命令，则t必须是任务线程，φ ′= φ，id′=id，且pl′=假。

程序计数器 pc 和启用的线程集合 enab 按如下方式更新。如果 c 是 start，则 enab′= enab ∪{t ∈ T | t 是任务或中断服务例程}且 pc′= pc。如果c是激活(u)，那么enab′= enab ∪{u}且pc′= pc。如果 ι是t 的最后一条语句且t是回调，则enab′= enab {t}且pc′= pc[t → st]。如果 ι是t的最后一条语句且t是中断服务例程，则enab′= enab且pc′= pc[t → st]。在所有其他情况下，enab′= enab且pc′= pc[t → l′]。

– 此外，转换会设置新的运行中的线程rt′和被中断的任务it′，具体如下：如果t是ISR 线程，pl为真，且 ι是t的第一条指令，则it′= rt且rt′= t。如果t是ISR线程或回调线程，且 ι是t的最后一条指令，则it′=it，rt′=it。在所有其他情况下，rt′= t且it′=it。为简化起见，我们假设没有任何一条指令同时是某线程的第一条和最后一条指令。

执行 σ的 P 是一个有限的转换序列 σ= τ0, τ1,…, τn,(n ≥ 0)，使得存在一个来自 Q 的状态序列 q0,q1,…, qn+1，其中 q0= s 且 τi=(qi, ιi, qi+1) 对每个 0 ≤i ≤n 成立。我们称状态 q ∈Q 在程序 P 中是可到达的，如果存在一条 P 的执行通向状态q。

4 高层竞争

在本节中，我们描述了IDC程序背景下高层竞争的概念。尽管我们以IDC程序为例进行说明，但这些定义适用于任何具有交错语义的程序类别。

让我们将程序P中的块定义为P中两个语句之间的代码段。更正式地，一个块由控制流图（CFG）中线程t的两个位置(l, l′)和一个位置集合X组成，使得l, l′ ∈X。该块表示线程t中从l开始、在l′结束，并且始终保持在位置集合X内的路径段集合π。例如，在图2a所示示例程序的消费线程中，第4‐9行构成一个块，在该线程的控制流图中，我们用位置对(4, 9)和位置集合{4, 5, 6, 7, 8, 9}来表示它。此块中包含两条路径段。当位置集合X被理解为l和l′之间的中间位置（如上述情况）时，我们仅用( l, l′)来表示该块。

程序P中的临界访问是P中一个用户指定的代码块。如果临界访问A包含一条写入 v的语句，则称A是对变量 v的一次写操作。类似地，如果A包含一条读取 v的语句，则称A是对 v的一次读访问。临界访问是用户给定的输入，代表用户期望相对于对相同变量的其他临界访问能够“原子地”或“互斥地”执行的代码部分。

例如，在图2所示程序中，我们可以将 consume线程的第4‐9行标记为一个临界访问 A，它既读取又写入 items变量。类似地，produce线程的第1‐4行可被视为一个临界访问 B，它读取和写入 items和 packets。

最后，如果两个临界访问访问了同一个公共变量，并且其中至少有一个是对该变量的写操作，则称这两个临界访问是冲突的。

我们说，程序P中两个不同线程内的冲突的临界访问A和B涉及一个高层竞争 （或简单称为存在竞争），如果在P的某次执行中，它们在时间上发生重叠；也就是说，对应于其中一个临界访问的路径段在另一个临界访问对应的路径段的开始与结束之间某处开始。回到图2a的例子，临界访问A和B是冲突的（因为它们都写入 items），但它们并不存在竞争，因为在程序执行的任何情况下它们都不可能发生重叠。然而，如果将consume任务中的lockpreem和unlockpreem语句移除，则这两个访问现在可能重叠，从而产生竞争。例如，按以下行号序列执行（修改后的）程序：

主程序：1–4 。服务数据包： 1–3 。 。produce：1–3 。 。consume：1–4 。服务数据包：1–3 。 。produce： 1–3 。 。 。consume：5–8

由于 produce 中的块 B 与 consume 中的块 A 发生重叠，导致出现高层竞争。

我们将涉及临界访问A和B的竞争分类为有害的，如果存在一种执行情况，使得这两个临界访问发生重叠，并且该执行到达一个无法通过将这两个临界访问以串行方式依次执行所能到达的状态。一些论文（参见[11]）也将此条件称为原子性违反。上述竞争是有害的，因为程序到达了一个items值为0的状态，而在该执行的任何串行版本（即 A和B不重叠）结束时都无法到达这种状态。如果一个竞争不是有害的，则称其为良性的。

5 使用不相交块进行高层竞争检测

我们现在提出一种基于静态分析的算法，用于可靠地检测IDC程序中的高层竞争。该算法基于[6],中引入的不相交块概念，我们接下来将对其进行描述。

不相交块

我们从[6]中回顾到，不相交块是指在不同线程的控制流图中可以静态识别的代码块配对，根据这类程序的执行语义，这些代码块在程序执行过程中保证不会发生时间上的重叠。更准确地说，在程序P的每次执行中，若对应于代码块F和G中的路径片段（如果存在）在时间上从不重叠，则这两个代码块构成一对不相交块。因此，这些代码块在此意义上是“不相交”的。

一个块模式 F是表示一组符合该模式的块的描述。例如，对于IDC程序，我们可以将D模式块定义为任务线程中的一个块，该块以disableint开始，以 enableint结束，并且中间没有其他enableint。如果在某种特定编程语言的任意程序P中，当P的一个线程包含一个匹配模式 F的块F，而另一个线程包含一个匹配模式G的块G时，这两个块在P中是不相交的，则称这一对块模式(F, G)为不相交。我们将这样的一对模式称为不相交块模式。

我们为IDC程序类设计了一组不相交块模式，如图3所示。该图中的八对使用了六种不同的块模式：A D‐块是任务线程中的一个块，以disableint开始，以enableint结束，其间没有其他 enableint。I‐块（相应地 C‐块）是 ISR 线程（相应地 回调线程）的全部代码。S‐块是任务线程中以 lockpreem 开始并以 unlockpreem 结束的块。M‐块是从主线程开始到 start 语句之间的块。最后，T‐块是除主线程外的任务、回调或 ISR 线程的全部代码。我们声称，这八对模式中的每一对都是 IDC 程序的有效不相交块模式。

例如，让我们来看一下图3的g部分中的S和C‐块对。回到图2a的运行示例，其中consume的第4‐9行对应一个S‐块，而produce的第1‐4行则对应一个C‐块。图3g告诉我们，它们构成了程序中的一对不相交块。以下引理形式化了这一结论。

引理1 图3中的八对块模式构成IDC程序的有效不相交块模式。

证明 让我们考虑 (S,C)模式，如图 3g 所示。考虑一个包含两个线程的 IDC 程序 P，其中一个线程包含一个 S‐块 F，另一个线程包含一个 C‐块 G。为了说明 F 和 G 确实是不相交的，假设它们在某个 ρ执行过程中存在重叠P。那么要么是 F 块在 G 块开始之后、结束之前开始；要么情况相反。在第一种情况下，一旦 G 块开始执行，就必须运行至完成（因为根据 IDC 程序的语义，回调不能被抢占）。因此这种情况被排除。在第二种情况下，一旦任务线程执行了 lockpreem 命令，只有 ISR 线程可以抢占它。然而，一旦 ISR 线程完成，必须将控制权交还给被中断的任务线程，并且在任务线程解锁抢占之前，无法执行任何回调。我们注意到，ISR 线程不能使用 unlockpreem 命令。因此，这种情况也被排除。因此，S和C‐块构成了IDC程序的有效不相交块模式。

让我们考虑图3中(e)部分配对的另一个示例，该示例表明两个S‐块彼此不相交。再次使用与上述类似的论证，我们可以说，一旦一个任务线程处于S‐块之间，由于 lockpreem的语义，我们无法切换到另一个任务线程。可以使用类似的论证来证明其他配对构成了IDC程序的有效不相交块模式。

竞争检测算法

我们现在描述用于IDC程序的高层竞争检测算法。算法 1展示了该算法的概要。我们首先解释算法中使用的一些术语。

算法1 检测高层竞争

1: 过程 检测高层级竞争
Require: IDC程序 P和一组临界访问 CA，位于 P 中。
确保： 设置 H的潜在的高级竞争条件
2: H := ∅;
3:基于图 3中的模式对 P 中的每个线程执行不相交块分析；
4:对于 每个临界访问中的冲突对 (A，B) CA执行
5:如果 A和 B位于不同的线程中，并且未被一对不相交块覆盖那么
6: 声明(A,B)可能存在竞争；
7: H := H ∪{(A, B)};
8: else
9: 声明(A,B)为非竞争的；
return H

设P为一个程序，A和F为P中的块。我们说块F覆盖块A，如果对于A中的每条路径 π，在F中都存在一条路径 δ，其包含 π作为子路径。类似地，我们说一对块(F,G)覆盖程序P中的一对临界访问(A, B)，当且仅当F覆盖A且G覆盖B（或反之亦然）。例如，在图2a所示的程序中，临界访问A和B被一对不相交块覆盖，即S块（consume中的第 4‐9行）和C块（produce中的第1‐4行）。

基于图3的不相交块模式进行的不相交块分析，其含义如下。回顾图3可知，共有六种不同的块模式，分别标记为D、I、C、S、M和T。我们首先对给定的IDC程序P的每个线程进行数据流分析，以计算每条语句s必须属于的块模式集合。如果在该线程控制流图中所有到达语句s的初始路径上，s始终包含在一个 F‐块中，则称语句s必须属于某个块模式 F。通过此分析，我们可以（保守地）声明：若块A中的每条语句都必须属于某个 F‐块，则块A被一个 F‐块覆盖。现在，我们可以（再次保守地）利用这一点来判断：一对临界访问(A, B)被一对不相交块(F, G)覆盖。

定理1 算法 1是可靠的，即当它判定IDC程序P中的一对临界访问(A，B)为非竞争的时，这些访问确实是非竞争的。

证明 假设该算法判定程序P中的临界访问(A, B)是非竞争的。那么要么A和B属于同一线程，要么我们必须找到一对块(F, G)覆盖(A, B)，其中F是某个 F‐块，G是某个 G‐块，对应于图3中某个不相交块模式(F, G)。根据引理1，我们知道(F, G) 确实是程序P的一对不相交块。现在假设(A, B)存在竞争，则A和B必须出现在两个不同的 P 线程之间必须存在一个执行 ρ，使得它们在时间上发生重叠。但由于 (A, B) 被 (F,G) 被覆盖，因此块 F 和 G 也必须在 ρ 中发生重叠。但这与它们在 P 中互不相交的事实相矛盾。因此 (A,B) 不可能是竞争的。

6 分析P‐RTOS内核

让我们回到在P‐RTOS内核API中发现高层竞争的问题。假设开发者已在API函数中标记出一组临界访问。我们关心的是，是否存在涉及这些标记的临界访问的高层竞争，即是否存在某个P‐RTOS应用程序调用了内核API，并且存在某个该应用程序的执行过程中，两个冲突的关键访问发生重叠。

我们可以使用迄今为止开发的IDC程序框架来解决此问题，具体如下。对于任意自然数n，我们可以构造一个最一般(P-RTOS)应用程序(MGA) Pn，它是一个具有以下结构的IDC程序。它包含一个主线程，用于初始化内核变量，然后启动调度器；n个任务线程，每个任务线程在整体循环中非确定性地调用其中一个任务API函数；一个回调线程，在循环中非确定性地调用其中一个回调API函数，并以非确定性方式退出；以及一个 ISR线程，仅简单地调用Tick_ISR例程。P‐RTOS共有45个可从任务线程调用的API函数，以及23个可从回调中调用的API函数。P‐RTOS通常不使用ISR（除了Tick_ISR），而是依赖周期性任务来轮询IO缓冲区。图4展示了MGA P1。该MGA Pn具有如下性质：如果某个具有某些n个任务线程的P‐RTOS应用程序存在一次执行，其中出现了涉及内核 API中两个临界访问的高层竞争，则该MGA Pn可以编排出类似的竞争。

算法2 检测P‐RTOS内核中的高层竞争

1: procedure在P‐RTOS中检测高层竞争
要求： P‐RTOS内核APIs中的一组临界访问CA。
确保： 设置 H关于P‐RTOS内核中潜在的高层竞争
2: H := ∅;
3:基于图 3的模式对MGA P1中的每个线程执行不相交块分析；
4:对于 临界访问集合 CA中的每一对冲突对 (A,B)，执行以下操作
5:如果 (A,B)未被一对不相交块覆盖 则
6: 声明 (A,B{v10}为潜在竞争；
7: H := H ∪{(A, B)};
8: else
9: 声明 (A,B)为非竞争的；
return H

定理2 算法 2是可靠的，即如果它声明内核API中的一对临界访问是非竞争的，则这些访问永远不会涉及高层竞争。

**

基于静态分析的RTOS内核高级竞争检测

7 分析TI‐RTOS内核

在本节中，我们描述了将我们的方法论应用于检测TI‐RTOS内核中的高层竞争。

TI‐RTOS应用程序的特点是使用软件中断，以及通过禁用和启用各种类型的线程来实现细粒度的同步机制。

我们首先将TI‐RTOS应用程序的行为形式化为带软件中断的中断驱动程序（ IDS）。该语言对应于我们的方法论概述中描述的 LTI-RTOS。此语言中的应用程序包含三种类型的线程：任务、软件中断（SWI）和硬件中断（HWI）。任务线程是普通线程，SWI线程由任意线程通过编程方式触发，HWI线程是中断服务例程，由硬件触发。应用程序在主程序线程中开始执行。该主程序线程是一个任务线程，负责初始化全局变量并调用启动命令以启用任务和SWI调度器，同时使能中断。初始时仅任务线程和HWI线程被允许执行。任务线程可被其他任务线程抢占（当任务和SWI调度器已启用且中断已使能时），或被SWI线程抢占（当SWI调度器和中断已使能时），或被HWI线程抢占（当中断已使能时）。SWI线程可被其他SWI线程抢占（当SWI调度器和中断已使能时）或被HWI线程抢占（当中断已使能时）。HWI线程可被其他HWI线程抢占（当中断已使能时）。

除了表1中介绍的前四个基本命令外，该模型还允许IDS应用程序使用表3中所示的命令。

在图 5中，我们列出了为IDS程序类识别出的不相交块模式。根据这些程序的执行语义，显然这些是该程序类的有效不相交块模式。

现在讨论针对TI‐RTOS内核的竞争检测算法，其思路是将算法2应用于适当定义的 MGA。我们假设已在TI‐RTOS内核API中标识出临界访问。TI‐RTOS共有45个API函数，其中按照惯例，16个可用于任务线程，13个可用于SWI线程，12个可用于HWI线程。另有4个函数可由主线程使用。我们定义一个IDS程序Pi,j,k，表示一个MGA，定义如下： Pi,j,k包含一个主线程，用于初始化内核数据结构并启动调度器。它包含i个相同的任务线程，每个任务线程在循环中非确定性地调用其中一个任务API函数。它包含j个相同的 SWI线程，每个SWI线程在循环中非确定性地调用其中一个SWI API函数，并以非确定性退出。最后，它包含k个相同的HWI线程，每个HWI线程在循环中非确定性地调用其中一个HWI API函数，并以非确定性退出。图6描绘了MGA P1,1,1。

我们现在对“元”MGA P1,1,1运行算法 2，通过使用 MGA P1,1,1替代 P1,以及图 5中的不相交块模式。

8 分析ChibiOS内核

我们现在描述将我们的方法论应用于检测ChibiOS内核中的高层竞争[7]。

ChibiOS是一种紧凑且快速的实时操作系统，深受自动驾驶开发者欢迎[1]。该内核通过简单地禁用和启用中断来实现同步。此内核的一个关键区别特征是，即使中断被禁用，也允许任务让出。内核API函数在可被调用的上下文方面也具有相当复杂的调用约定。

我们将ChibiOS应用程序的行为形式化为带让出的中断驱动程序（IDY）。该语言中的程序由任务线程和ISR线程组成。IDY程序支持中断嵌套，从而导致ISR线程之间的潜在切换。其中有一个特殊的主线程，它是初始时唯一活跃的任务线程。主线程可以通过使用创建命令来创建其他线程以执行。

IDY程序在主线程中开始执行，初始化共享全局变量，然后创建其他线程，启用中断并使用 sysInit 命令启动调度器。当中断未被禁用时，任务线程可被其他任务线程或 ISR 线程抢占。即使中断被禁用，任务仍可以主动让出控制权。而 ISR 线程则不能让出，但当中断未被禁用时，可被其他 ISR 线程抢占。ISR 线程不会被任务线程抢占。

除了表1中介绍的前三个基本命令外，IDY程序还可以使用表4中列出的命令。

根据语言语义，我们列出图7中所示的不相交块模式。使用的七种块模式为：D、I、 ID、DS1,DS2,M和T。任务中的D模式表示被sysLock-sysUnlock命令包围且中间没有插入sysUnlock或sysSwitch命令的块。任务中被sysLock-sysUnlock包围但中间有sysSwitch的块将被拆分为两个块DS1和DS2。该

中，任务t1中的块DS1与任务t2中的块DS′ 1和DS′ 2成对不相交。类似地，t1中的块DS2与t2中的块DS′ 1和DS′ 2不相交。对于(e)和(f)中的不相交块也采用类似的解释。)

整个 ISR（相应地为任务）代码构成一个I（相应地为T）块。ID模式表示 ISR 中被 sysLockFromISR‐sysUnlockFromISR 命令包围且中间没有插入 sysUnlockFromISR 的块。M块从主线程的开始处起，直到线程创建为止。

块对 (a)–(c) 和 (g) 中代码的不相交性符合预期。(d)–(f) 中的情况需要一些解释。考虑 (d) 中的块。此情况假设任务 t1（在左侧模式中）可以在处于 sysLock‐sysUnlock 块内时让出（使用 sysSwitch 命令）。对于右侧的任务 t2也做了类似的假设。我们断言，任务 t1的子块 DS1与任务 t2的块 DS′ 1是不相交的。块 DS1被包含在 sysLock‐sysSwitch 内，且中间没有 sysUnlock 和 sysSwitch 命令。因此，根据 sysLock 命令的语义，当在 DS1中中断被禁用时，任务 t1不会被其他任务抢占。任务 t1的块 DS2也与任务 t2的块 DS′ 1不相交。此处，块 DS2被包含在 sysSwitch‐sysUnlock 内，且中间没有 sysSwitch 和 sysUnlock 命令。此外，sysSwitch 命令是在 sysLock 的上下文中执行的。因此，当任务 t1恢复控制权（在 sysSwitch 之后），其上下文将恢复到中断被禁用的状态（由于 DS1中的 sysLock），因此如上所述，该任务不会被抢占。对于任务 t2的块 DS′ 2 分别与任务 t1,的块 DS1和 DS2的不相交性，也可进行类似的推理。

不相交块模式(d)出现在ChibiOS内核API中，如图8所示。假设任务线程t调用 chThdWait(t1) API函数，而另一个任务线程t′调用chThdStart(t2)。调用chThdWait(t1)会将调用线程（在此为t）加入到线程t1的等待队列中，将t的状态更新为WTEXIT，从就绪队列中移除t，并最终选择下一个就绪的任务线程进行执行（第3–8行）。此时，线程t通过调用 chSysSwitch让出控制权给新线程（第9行）。当线程t恢复执行时，该API返回一个退出码 （第10–11行）。所有这些操作都在一个chSysLock‐chSysUnlock块内完成。当线程t′调用 chThdStart(t2)时，如果t′的优先级较小，则线程t2被放入就绪列表（第3–5行）。否则，线程t′被添加到就绪列表，同时t2成为新的运行中的线程（第3、6–9行）。此时，t′通过调用 chSysSwitch让出控制权给新的任务（第10行）。所有这些操作都在一个 chSysLock‐chSysUnlock块内完成（第2–11行）。

下一步是在ChibiOS内核中检测高层竞争。我们假设已知ChibiOS API函数中标记出的临界访问。我们设计了一种最通用的

。左侧的每个块与右侧的每个块均不相交)

应用程序 (MGA) Pi,j作为一个具有 i个任务线程（除主线程外）和 j个ISR线程的 IDY程序。主任务线程初始化共享内核数据结构，然后创建其他任务线程。每个任务线程和ISR线程非确定性地调用内核API函数。ChibiOS API函数分为三类，由后缀字母标识。无后缀的API可以从任务线程中调用。带有后缀‘S’的API必须在任务线程中的 sysLock-sysUnlock块内调用。带有后缀‘I’的API分别在任务线程和ISR线程的 sysLock-sysUnlock以及 sysLockFromISR-sysUnlockFromISR块内调用。这些API在任务线程上下文中调用时，应随后调用调度器。这些API被无限次调用。ChibiOS支持29个任务API和8个ISR API。该MGA P1,1如图 9所示。我们在该MGA上运行算法 2，使用图7中的不相交块模式，以可靠地声明关键访问对为非竞争的。

9 分析FreeRTOS内核

FreeRTOS应用程序的执行语义在[6]中被形式化为中断驱动程序（IDP）。IDP的结构比迄今为止描述的语言更简单。IDP程序仅允许任务线程和ISR线程，并对抢占施加了更简单的约束。此外，任务线程不能让出，中断也不能嵌套。然而，IDP程序除了使用常规的中断和调度器启用‐禁用命令外，还使用flags 进行同步。

在[6]中，作者构建了一个MGA P1,1,，包含一个任务线程和一个ISR线程，旨在查找FreeRTOS内核API中的低级数据竞争。该任务线程调用了37个任务API，而 ISR线程调用了12个特定于ISR的API。该论文识别出适用于IDP程序的八种不相交块模式。其中包括与我们讨论过的其他语言类似的模式，例如禁用‐启用块、调度器挂起‐恢复块、所有任务和ISR线程块。此外，该论文还使用了基于标志的块。块Ff是任务线程中将f设置为1并再恢复为0的语句之间的块。而块Cf在ISR线程中对应于检查f= 0是否成立的条件语句的then块。

我们现在可以使用我们的算法 2来检测FreeRTOS内核API中的高层竞争，方法是使用标记了临界访问的最一般应用 P1,1以及列出的不相交块 [6]。

10 实验评估

我们现在描述针对四个RTOS内核案例研究的竞争检测算法的实验评估。我们首先描述工具的实现，然后分析结果。

10.1 工具实现

我们已将竞态检测算法实现为一个名为 Rtos- Racer 的工具。该工具可在 https://bitbucket.org/rekhapai/hlr-tool/src/master/ 获取。图 10展示了该工具的示意图，给出了工具内的组件和工作流程。该工具分为三个阶段运行：(1) 预处理，(2) 分析， 以及 (3) 竞态报告，我们将在下文逐一描述。

预处理。对内核API函数进行了修改，以使其适用于不相交块分析。我们首先通过识别初始化代码（例如，在FreeRTOS启动时会创建一个空闲任务，该任务涉及访问许多共享内核变量，或在ChibiOS和TI‐RTOS中创建并初始化就绪队列等）来准备内核API函数，这些代码将作为主线程的一部分。这样做的目的是减少工具报告的误报数量。在初始化阶段，调度器尚未启动，因此对这些变量的访问不会导致竞争。

然后，API函数被手动标注了临界访问。这需要了解主要的内核数据结构以及内核 API如何修改这些结构体。

函数。每个内核的关键内核数据结构如图11所示。这四个内核都具有诸如就绪队列（用于准备执行的线程）、延时队列（用于被延迟的线程）、带指针的任务列表、定时器变量等结构体。P‐RTOS为符合ARINC653标准，还包含多个分区，但我们关注的是分区内的代码。对于TI‐RTOS，除了用于任务调度的状态组件（图中详细显示）外，还有用于软件中断和硬件中断的类似组件。这些变量和结构体构成了我们的“关注变量”。

如果一段代码在API函数中访问了一个或多个关注变量，并且我们认为它应该相对于其他对相同变量的临界访问“原子地”执行，则我们将该段代码标记为临界访问。对于每个临界访问，我们还需要标注它所访问的变量及其访问类型（读/写）。对于变量x的临界写访问，在访问开始处添加函数调用begin(“w:”, x)1，在其结束处添加end(“ w:”, x)1。例如，FreeRTOS中的vTaskResume API将一个任务从xSuspendedTaskList移除并插入到pxReadyTasksLists中。这是通过一段代码序列实现的，我们已将其标记为对这些列表的临界访问。在此临界访问开始时，我们添加begin(“w:w:”, xSuspendedTaskList,pxReadyTasksLists)。字符串“w:w:”表示对xSuspendedTaskList和 pxReadyTasksLists均进行写访问。该临界访问的结束由调用end(“w:w:”, xSuspendedTaskList,pxReadyTasksLists)来标识。读访问用字符串“r:”表示。有关标记的临界访问数量的详细信息见表5。标记了临界访问的修改后的代码作为输入传递给工具，进行进一步的预处理。

对于识别出的不相交块模式集合中的每个块模式，我们关联一个锁，该锁在块的开始处获取，在块的结束处释放。例如，对于图3中所示的S‐块模式，我们在 lockpreem之后插入一个acquire(S)语句，并在unlockpreem之前插入一个 release(S)语句。块模式列表及其对应的锁作为工具的输入提供。

我们的不相交块分析是一种过程内分析，因此我们将顶层函数内部调用的所有辅助函数调用进行内联。我们针对每种实时操作系统库中的所有重要API进行了分析。所分析的API数量为

每个实时操作系统在表5中给出。临界访问的标记、锁转换和内联构成了预处理阶段。

分析。 我们现在使用标准锁集分析 [19]来计算在每个语句处必须持有的锁的集合。在程序入口处，假设没有锁被持有。当遇到对 acquire(l) 的调用时，分析会在该调用的l out点添加锁。当遇到对 release(l) 的调用时，该调用在out点的锁集为在in点计算出的锁集中移除锁l后的结果。对于任何其他语句，将其语句in点的锁集复制到其out点。join操作仅仅是输入锁集的交集。不相交块分析在CIL框架 [17]中实现。分析器输出临界访问的列表以及在这些访问处必须持有的锁。

竞态报告。 完成不相交块分析后，我们可以进行高层竞争检测。对于每一对冲突的关键访问，我们保守地检查

10.2 分析结果

表 5显示了在四个RTOS内核上运行Rtos- Racer的结果。评估是在一台配备32 GB内存的Intel Core i7机器上进行的，系统为Ubuntu 16.04，报告的运行时间基于此配置。此处报告的运行时间是指不相交块分析以及shell脚本判断冲突对是否为竞争所花费的时间。该表显示了报告的潜在竞态数量，以及将报告的竞争分类为误报（在实际非抽象系统中并非竞争），并在真阳性中进一步区分出有害竞争。如果一对访问可能参与有害竞争，则我们将该访问对归类为有害的。此分类是手动完成的，我们将在下文更详细地描述这一过程。

误报。 我们从P‐RTOS中的一个误报示例开始。该工具报告了API函数 ProcessCreate和TimeDelay中临界访问之间的竞争，这两个函数都访问任务的 eState结构。然而，实际上ProcessCreate只能由主线程在初始化期间调用（此时 TimeDelay回调未激活），因此在实际系统中它们不可能发生竞争。

许多误报是由于将具有多个字段的数据结构抽象为单个变量所致。例如，在 FreeRTOS 中，我们将pxDelayedTaskList数据结构抽象为一个变量。因此，即使访问的是结构体的不同部分，我们的分析也会将其报告为存在竞争。这导致在 FreeRTOS 中出现了大量误报。

我们工具报告的 ChibiOS 中的所有竞争均为误报，这是由于临界访问的标记方式所致。问题出现在 chThdWaitAPI 函数中，我们在图 12中说明了该问题。该函数将当前线程（由 currp指向）放入指定线程（由 tp指向）的等待队列中，随后通过更新就绪列表并选择一个新的就绪任务来执行，使当前线程进入睡眠状态（(a) 中第 3–6 行）。因此，我们将第 3–6 行标记为对就绪列表的“写”临界访问。在预处理阶段，工具会内联 chSchGoSleepS API（(a) 中第 5 行），因此现在对就绪列表的临界访问范围变为第 3–10 行（见图12b）。调用 chSchGoSleepSAPI 将导致让出控制权给一个新任务（(b) 中第 9 行），因此没有任何块模式可以覆盖该临界访问（见图 12b）。因此，在整个临界访问期间没有公共锁被持有，工具便将其标记为就绪列表上的潜在竞争（rlist在

图 12b）。注意，在图 12b 中，对就绪列表的访问仅限于第 3–8 行，因此该竞争实为误报。可以通过先手动内联 chSchGoSleepS，然后准确重新标记临界访问来解决此问题，如图 12c 所示。现在该临界访问被 DS1‐块覆盖，工具将不会报告涉及此临界访问的任何竞争。

良性竞争。在P‐RTOS中一个真实但为良性的竞争示例是SetEvent函数中的临界访问。事件对象被用作任务之间的信号机制。一个任务调用SetEvent函数以通知其他任务某些数据已准备好供消费。该函数检查事件对象的flag 字段是否未设置，如果是，则使用 lockpreem命令禁用抢占，设置flag，重置与该事件关联的任务队列，并使用 unlockpreem命令重新启用抢占。此函数的完整代码（包括对flag的检查）被标记为临界访问。显然，在SetEvent中的这些访问之间存在竞争。然而，它并不会导致

任何原子性违规，因为交错执行这些临界访问的效果与串行执行相同。

TI‐RTOS 存在一个有趣的良性竞争场景，如下所述。当一个软件中断s1调用 Swi_self API函数时，它会非保护地读取curSwi变量。在此瞬间，一个高优先级的软件中断 s2可能抢占s1并继续调用 Swi_post。该 API 函数在写入curSwi变量之前先保存其内容。在从该调用返回时，它会恢复curSwi的旧值。所有这些操作都在中断被禁用的情况下完成。由于这种“保存并恢复”的机制，s1和s2中的两次访问不会导致任何原子性违规。

有害竞争。以一个有害竞争为例，在P‐RTOS的BufferSend和Tick_ISR函数中存在临界访问。当一个周期性任务调用BufferSend向一个满队列发送消息时，该函数会检查任务的下一次激活时间是否超过当前节拍计数，只有在此情况下才将任务放入延迟队列。然而，该检查并未禁用中断，因此Tick_ISR可能很快运行并增加节拍计数。考虑当前节拍计数为99且任务的下一次激活时间为100的情况。此时Tick ISR将时间增加至_100。当控制权返回到BufferSend时，它仍继续执行并将任务放入延迟队列。结果，当调度器下次尝试运行该周期性任务时，发现任务位于延迟队列而非就绪队列中。这种状态是这两个临界访问的任何串行执行都无法达到的。

在TI‐RTOS中，当发生以下场景时，共享结构readyQ上会出现有害的竞争。当一个任务t1通过调用Task_delete(t2)删除另一个就绪状态的任务t2时，可能会被软件中断抢占t1。删除t2的过程涉及访问readyQ结构。如果该软件中断调用了Task_setPri(t2)，它将更新readyQ以反映任务t2的新优先级。这两次访问导致了对readyQ结构的有害竞争。

我们已就这些内核中的竞争问题与相关开发者取得联系。P‐RTOS 中的 3 个有害竞争均已修复。在 TI‐RTOS 中，部分有害竞争涉及任务删除函数中的访问操作。内核开发者认为程序员不应在任务被删除时调用其他任务 API，因此不认为这是重要问题。在 FreeRTOS 中，一些问题已在我们工作之外得到修复。其余的竞争问题大多涉及队列注册表，他们认为无需修复。

讨论。 在本节中，我们展示了该工具能够将大量冲突的关键访问对过滤为非竞争的，平均过滤率达到97%。同时证实了ChibiOS内核不存在用户标注的竞争。该工具在报告实际竞态方面的准确率较高（即实际竞态 / 潜在竞态）。平均而言，仅有18%的潜在竞态为误报（即误报 / 潜在竞态）。通过仔细标记临界访问，还可以进一步降低误报率。此外，将结构体的字段视为“关注的访问”也可以降低报告的误报率。

我们工具的完整实现以及TI‐RTOS、ChibiOS和FreeRTOS的修改后并已标注的源代码可在https://bitbucket.org/rekhapai/hlr-tool/src/master/获取。

11 相关工作

我们重点关注关于sound竞态检测技术（即报告所有竞争的技术）的相关工作，并根据三种主要方法对这些研究进行组织。

经典并发程序的基于锁集的分析。Artho 等人[4]提出了“高级数据竞争”这一术语，并以原子方式访问一组共享变量的形式对其进行了非正式定义。他们定义了线程对共享变量集合的视图概念，并在两个线程存在视图不一致时标记潜在竞争。他们提供了一种基于锁集的算法，用于在执行过程中动态检测视图不一致。von Praun 和 Gross [25]以及 Pessanha 等人[8]扩展了[4]的基于视图的方法，以进行静态分析来检测高层竞争。针对经典并发程序中数据竞争的基于锁集的静态分析 [2,10,23,26]原则上可以扩展以处理高层竞争。然而，由于同步机制的特殊性质和非标准的切换语义，上述技术均不适用于中断驱动程序。中断驱动程序的静态分析。Regehr 和 Cooprider [18]描述了一种将中断驱动程序源到源转换为标准多线程程序的方法，并对转换后的程序进行数据竞争分析。然而，他们的转换在我们的场景下是不充分的。我们建议读者参考[6]了解此类方法固有的问题。Schwarz 等人 [20,21]提供了一种精确的数据流分析方法，用于检查中断驱动应用程序中的竞争，该方法能够处理基于标志的同步和中断驱动调度。尽管该技术能够检测所有竞争，但它仅适用于特定应用程序，而不适用于内核库。Sung 和其他作者[24]研究了具有不同优先级的中断服务例程形式的中断驱动应用程序，并执行基于区间的静态分析以检查断言。他们未处理库。Wang 等人[27]使用符号和动态分析相结合的方法分析中断驱动应用程序中的竞争。这是一种缺陷检测方法，无法保证检测所有可能的竞争。最后，Chopra 等人[6]提出了不相交块的概念以检测数据竞争，并对类似 Free‐RTOS 的中断驱动内核执行数据流分析。我们的工作扩展了不相交块的使用，以处理高层竞争，并且还为带有回调、软件中断和让出的新类型中断驱动程序识别出不相交块模式。

基于模型检测的方法。一些研究人员使用了诸如Slam、Blast和Spin等模型检测工具，以精确建模各种控制流和同步机制，并穷尽地检测错误[3,9,12–14,28]。所有这些方法都是针对特定的应用程序，而不是库。最后，相关工作[16]采用了一种模型检测方法，用于发现FreeRTOS内核v6.1.1中的所有高层竞争。他们使用专为此软件定制的元论证来限制引发竞争所需的线程数量。该方法仅处理25个API函数，总运行时间接近2小时。相比之下，我们的方法不需要内核特定的论证，且运行时间仅为几秒钟。

12 结论

本文提出了首个基于静态分析的综合方法，用于检测RTOS内核中的高层竞争。该方法具有可靠性高、效率高且误报率低的特点。我们认为，该方法可广泛适用于中断驱动型内核领域，而该领域中似乎存在大量正在使用的专用和专有内核。

在未来的工作中，我们希望研究将此方法扩展到使用多核（如TI‐RTOS）和多分区（如P‐RTOS中的隔离内核概念）的内核。