Nuttx操作系统进程切换调度实时性的形式化验证

郝英华 王 瑞 李晓娟

1(首都师范大学信息工程学院 北京 100048) 2(首都师范大学高可靠嵌入式系统技术北京市工程研究中心,电子系统可靠性技术北京市重点实验室 北京 100048)

0 引 言

随着我国工业的快速发展，工业机器人[1]发挥的作用越来越重要。工业机器人控制系统是工业机器人的重要部分，控制操作机以完成指定的任务。操作系统处于工业机器人控制系统的核心地位，但是当前的工业机器人操作系统面对的一个大挑战就是实时性问题：目前流行的机器人操作系统ROS实时性不高，这在很大程度上限制了ROS的实际应用。为了满足实时性[2]需求，越来越多的工业机器人控制器开始使用实时操作系统作为软件核心。这些操作系统中最典型是：RTLinux[3]、Vxworks[4]、Window CE[5]、DSP/BIOS[6]等。它们都有着响应快速、稳定的优点，但很遗憾的是它们的源代码不开放，价格高昂，增加了开发成本。而Nuttx操作系统是一款开源的实时操作系统：代码完全对外开放，CPU可以被高优先级进程完全抢占，适应变化能力极强，它有极小的内存开销，支持多种硬件平台。

实时调度算法对操作系统的实时性有很大影响,它是提高系统实时性的关键技术。在Nuttx实时系统的进程调度中有三种调度策略:先来先服务，时间片轮转法以及零星调度。这三种调度策略均采用抢占式内核，使CPU总是响应优先级最高的进程，进而提高CPU利用率。先来先服务调度是Nuttx操作系统默认的调度，低优先级进程可以被高优先级进程抢占，实现实时抢占。时间片轮转调度中时间片被设置为20 ms，这使得CPU的切换次数以平均响应时间相对最优，提高CPU利用率。零星调度能够使零星任务根据服务器的预算值大小在高优先级和低优先级时之间进行转换，保证了在每个补充周期T内运行C的时间，使系统能够及时地响应零星任务。好的实时调度算法可以保证任务在其时限内完成，保证系统的实时性能。因此实时调度算法一直是人们研究的热点领域。文献[7]提出了一种称为准分区调度的新算法，它能够调度在同一个处理器上没有明确截止时间的零星任务。为了响应系统负载变化，该算法使用高效的调度策略在分配的EDF和类似全局的调度规则之间实现一种切换，动态地适应了系统变化。模拟结果表明，该策略具有非常低的抢占和开销，优于现有策略。文献[8]在调度器运行时允许修改策略的前提下，提出了四种调度策略，并使用VarySched调度器进行实验，评估了四种策略对应用程序运行时间的影响。评估结果表明，一个好的调度策略可以加速应用程序的运行，使程序更早地完成运行。在文献[9]中，作者提出一种抢占式操作系统内核的验证框架，并将该框架成功地运用到验证μC/OS-II操作系统的关键模块中，模块包括进程调度，中断处理程序，消息队列和互斥等。验证结果表明，μC/OS-II操作系统具有实时性，但它的限制是其C子集不允许功能指针，这需要高阶函数的逻辑支持。文献[10]首先对Web服务器端3种调度策略：先进先出、优先排队、加权公平排队进行简要概述和比较评估，然后基于优先排队和加权公平排队策略提出一种新的调度策略：加权公平排队。采用测试的方法对每种调度策略的执行时间和响应时间进行验证，验证结果表明：每种调度策略都有自己的优缺点，并且它们优势互补。以上文献中所用的测试方法都属于传统的测试方法，能给出准确的结果。但是，缺点是传统的测试依赖于测试条件，它们的有效性取决于测试用例的数量和条件，因此，验证结果具有不完备性。形式化验证从数学上完备地证明系统是否实现某些功能的方法，所以验证结果具有准确性和完备性。模型检测是一种常用于验证系统正确性的形式化方法之一，基本思想是用有限状态机(FSM)表示系统的状态转移结构，用时序逻辑表示设计的性质，如计算树逻辑和线性时序逻辑。有关模型检测方法的运用：文献[11]用形式化验证方法对任务的可调度性进行分析，并采用验证工具SCT(schedulability checking tool)与其他工具进行了比较，比较结果显示,SCT可以提供最为精确的分析结果，但同时也具有最长的分析时间。文献[12]采用Uppaal时间自动机对任务的可调度性进行建模与分析，结果表明，该建模方法是可扩展的，设计者可以根据它来对特定的系统进行设计验证。但是以上只是提供了一种方法，并未对某种具体的实时操作系统进行模型检测，我们可以借鉴为Nuttx操作系统的实时性进行验证。

综上，为了保证验证结果的完备性，本文采用模型检测的方法对Nuttx操作系统的调度策略进行实时性验证。首先提出在三种调度策略之间实行一种新的切换策略，使任务到达时能够根据自身的特点选择更适合的调度策略：让优先级相同的周期性任务选择时间片轮转调度，零星任务采用零星调度，其他的周期性任务默认先来先服务调度。同时采用模型检测的方法对Nuttx操作系统的三种调度策略之间的切换建立时间自动机模型，然后运用计算树逻辑公式描述需要验证的属性，最后在模型检测Uppaal[13-14]中进行验证。

1 时间自动机及CTL[15]公式

定义1Uppaal中的CTL公式

时间自动机[16-17]Uppaal使用计算树逻辑(CTL)公式来描述属性。该公式主要分为：状态公式和路径公式。其中，路径公式描述的是模型中路径或者轨迹，如表1所示。

表1 Uppaal 中路径公式

其中，公式inf{表达式}:y用来计算满足表达式所需要的最小时间y。公式sup:Task().response表示遍历系统模型的整个状态空间后得到的最小上界,也就是最坏响应时间。

2 Nuttx操作系统进程调度简介

Nuttx是一款实时开源的操作系统[18]。实时操作系统的核心是任务调度。只有保证进程能够在给定的时间内执行完成，才能保证Nuttx的实时性。在Nuttx操作系统中，总体上进程调度的过程如图1所示。

图1 进程调度过程示意图

• 当进程到来时，发送相应信号启动调度器。

• 调度器接收到该信号时，会根据不同的调度策略对进程进行相应的处理。

• 进程根据自己的调度策略运行，当运行完成后，会发送相应的信号通知调度器。

• 调度器接收到该信号，完成调度。

先来先服务调度：系统将先到达的进程调度到运行状态。在运行过程中，低优先级的进程是可以被高优先级的进程抢占，它是默认调度策略。

时间片轮转调度：在Nuttx操作系统中，时间片轮转法是为具有相同优先级的进程服务的。它将所有优先级相同的任务放到一个队列中，然后每个进程运行20 ms的时间片后，CPU进行上下文切换，当前进程放到队尾，新的队首进程进行一个时间片的运行。在切换过程中，运行完一个时间片的进程会放到blocklist队列中，直到下一次运行时才被移除blocklist队列。

零星调度：零星调度[19]服务器有一个补充周期、一个预算和两个优先级。当服务器有某些预算时，它处于高优先级，从预算时间中减去消耗的时间，预算用尽后立即进入低优先级，当服务器的时间被补充后，又重新进入高优先级。在一个周期T内：当时间小于预算budget_time时间时，进程每运行一段时间each_time就会丢失lost_time时间，并且这段时间该进程会一直处于高优先级。如果时间等于budget_time时，进程就会进入低优先级。若时间等于convert_time时，进程会补充前面丢失的lost_time时间。每补充一次lost_time，进程的优先级就会回到高优先级，并且这段时间可以看作是前半个周期T的对称运行。这就是Nuttx操作系统零星调度与其他调度不同的地方。它保证了每个进程在每个补充周期T内运行budget_time的时间，保证了系统的实时性。在每一个周期T中，其时间大小值如下所示：lost_time

图2 零星调度过程示意图

三种调度之间的切换：我们把所有的任务分为周期性任务和零星任务，让所有的优先级相同的周期性任务采用时间片轮转调度，零星任务采用零星调度，其他周期性任务默认先来先服务调度。当一个任务到达时，如果是同优先级周期任务，将其对应的变量m2设置为1，表示优先级相同任务，然后通过中间调度器找到它所对应的时间片轮转法；如果是零星任务，m3设置为1，对应到零星调度；将如果是普通的周期任务，m1设置为1，对应到先来先服务调度。不管处于哪种调度策略下的任务，都会发出一个信号，让当前正在运行的任务暂停，判断新来的任务优先级是否更高，若是，则切换到新来的任务，对CPU加锁，让其只运行当前优先级最高的任务，直至任务完成再执行暂停的任务，这就是实现切换策略的关键；若非，则执行当前的任务。具体切换过程如图3所示。

图3 切换过程示意图

3 Nuttx中切换调度的形式化建模

本部分对Nuttx系统的三种进程调度之间的切换过程进行了形式化描述。根据Nuttx系统进程间的调度过程建立了8个时间自动机模型，分别是任务模型(4个)、切换模型、先来先服务调度器模型、时间片调度器模型、零星调度器模型。我们给出了部分模型。这里我们重点介绍时间片轮转调度以及先来先服务调度策略之间的切换，其他调度过程间的切换此相似，不再赘述。

我们把任务标记为三种：把优先级相同的任务标记为m2，调用时间片轮转法；把零星任务标记为m3，采用零星调度法；其他任务标记为m1,默认调度先来先服务算法。

切换模型：如图4所示，当一个任务到达时，并且满足总的调度次数大于0时，发出ready!信号，如果m1等于1，它代表此任务采用先来先服务调度，立即发出fifo!信号,启动先来先服务调度器，m1立刻置0，代表该任务已成功找到对应的调度算法；如果m2等于1，它代表此任务采用时间片轮转调度，立即发出rr!信号,启动时间片轮转法调度器，m2立刻置0，代表该任务已成功找到对应的调度算法；如果m3等于1，它代表此任务采用零星调度，立即发出ss!信号,启动零星调度器，m2立刻置0，代表该任务已成功找到对应的调度算法。不管每种调度，任务到达时都会发出一个ready!信号，让当前正在运行的任务暂停，判断新来的任务优先级是否更高，若是，则切换到新来的任务，直至任务完成再执行暂停的任务；若非，则执行当前的任务。

图4 切换时间自动机

先来先服务模型：如果该任务采用先来先服务调度算法，如图5、图6所示。它主要有Task模型和Scheduler模型。Task模型主要有Idle、Ready、Running、Blocked、End、Error几种状态。当任务到达时，发出ready!信号，调用add()函数，该函数功能是将任务按照到达的先后顺序依次放到queue()队列中，时间t和响应时间response置0，m1置1，目的是通过切换器找到对应的先来先服务调度模型，同时任务的状态从Idle状态转换到Ready状态。先来先服务调度器模型接收到fifo?信号，首先会判断queue()队列的len值是否为1，如果为1，那说明当前只有该任务到达，满足numnber1大于0的条件，立即发出run!信号让该任务运行。任务接收到run?信号后，满足queue()队列的首元素时，会立即运行，并转换到Running状态，如果此时再有其他同类型任务到达，即满足m1等于1并且接收到fifo?信号后,调度器立即发出wait1!信号。任务接收到wait1?信号后，立即从Running状态转换为Blocked状态，此时调度器立刻发出run!信号。任务接收到run?信号，并且满足是queue()队列的首元素时，会重新运行转换到Running状态，实现高优先级抢占；如果不为1，那说明目前到达的任务不止1个，还会有其他非同类型任务已经到达，立即发出lock!信号。其他正在运行的任务接收lock?信号后，立即发出inform!信号。对应的调度器接收到inform?信号后，会一直等到高优先级非同类型任务运行完成后接收到unlock1?信号后，重新发出run!让目前queue()队列首元素运行，目的是实现同一时刻CPU只能运行一个任务。当先来先服务的任务数number1等于0时，如果其他非同类型任务还没有执行完，则发出unlock2!。其他非同类型接收到unlock?信号后，会立即运行，而当前调度器回到Init状态。当执行时间ax大于最好情况执行时间并且小于最坏情况执行时间时，任务运行完毕，发出done!信号，并调用remove()函数，将该任务从queue()队列移除，同时将success[]置1，表示该任务已经完成，响应时间response置0，此时任务进入到End状态，响应时间不变化。当时间t等于任务周期时，立即发出ready!信号，表示任务周期性来到，同时将时间t和response置0，success[]置0，并且调用add()函数，开始新一轮的调度。在任务模型中，只要时间t大于等于Deadlines[]，任务就会进入Error状态。

图5 先来先服务任务时间自动机

图6 先来先服务调度器时间自动机

时间片轮转模型：如果该任务采用时间片轮转调度算法，如图7、图8所示。在Nuttx系统中，时间片轮转调度是针对相同优先级的任务而进行的调度。所以在模型中，每个任务的优先级都是相同的，设计了两个跟图7一样的优先级相同的任务模型。它主要有Task模型和Scheduler模型。Task模型主要有Idle、Ready、Running、Blocked、End、Error几种状态。其他调度情况与先来先服务模型一致，这里不再赘述。重点介绍当运行时间ticks等于时间片值，任务运行一个时间片并且CPU允许上下文切换时，调度器发出stop!信号。任务接收到stop?信号后，调用change()函数。change()函数的作用是按照优先级大小将任务放到queue()队列的对应位置，让新的队首元素运行一个时间片的时间，并且任务从Running态转换到Blocked状态，cpu进行一次切换。若此时再有新的同类型任务到达，接收到rr?信号并且满足m2等于1的条件时，会立即发出wait!信号。任务接收到wait?信号后调用change()函数，进入到Blocked态,当满足队首元素时，再重新运行一个时间片的时间。

图7 时间片轮转任务间自动机

图8 时间片轮转调度器时间自动机

4 属性验证

在本节中，我们使用CTL公式描述这些属性，并且在Uppaal中对它们进行验证。Uppaal软件运行的计算机环境为：2.60 GHz的双核CPU，内存为4.00 GB。一级缓存为128 KB，二级缓存为512 KB，三级缓存为3.0 MB，内存工作频率为1 198 MHz。验证结果如表2、表3所示。

表2 属性描述以及验证结果 ms

表3 CPU最坏响应时间与截止时间 ms

属性1：对于任何一个待验证的系统而言，保证系统能够正常运行，不发生死锁是一个基本的前提，对于操作系统而言也是如此，它可以用如下CTL公式证明：A[ ] not deadlock。如表2所示，该属性被满足，这说明：说明整个系统不会出现死锁，该系统可以正常运行。

属性2：在进程调度过程中，同一时刻CPU只允许一个进程占用，不能允许多个进程同时运行：A[]Task(0).Running+Task(1).Running<=1。如表2所示，该属性被满足。这说明：整个系统在同一时刻CPU只允许一个任务运行。

属性3：进程在调度过程中，不超出截止时间，表明进程能够在不超出截止时间内完成，属性如下：A[] forall(i: pid_t ) not Task(i).Error。如表2所示，该属性在切换前不被满足，切换后得到满足。这说明：切换使得原本不能在截止时间内完成的任务完成了相应的操作，优化了实验结果。

属性4：每个进程，只要到达，就要在不超出截止时间内成相应的操作，这也是操作系统进程调度的实时性体现。属性用CTL公式可描述为：Task(i).Ready-->Task(i).End。如表2所示，该属性在切换前不被满足，切换后得到满足。这说明：切换使每个到达的任务都能完成相应的操作。

属性5：计算出每个进程从到达到完成的时间。该属性描述为：inf{success[i]==1}:time。如表2所示，我们根据该属性计算出CPU的平均响应时间，然后对切换前后的CPU平均响应时间进行比较，结果显示，切换后的平均响应时间小于切换前的平均响应时间。这说明：切换提高了CPU的平均响应时间。

属性6：计算出每个任务的最坏响应时间，与截止时间进行比较，进而保证任务在最坏情况下不超出截止时间而被完成，满足实时性。属性CTL描述如下：

sup:Task(0).response,Task(1).response,Task(2).response,Task(id).response。根据表3，我们对切换后的调度进行最坏响应时间与截止时间的比较，可以看出每种任务的最坏响应时间都不大于截止时间，这说明：切换使得任务能够在不超出给定的时间内完成相应的操作，满足了系统的实时性。

5 结 语

Nuttx是一款实时开源的操作系统，它能保证系统的实时性。因此对Nuttx系统的实时性进行验证很有必要。本文首次提出对以上三种调度策略进行切换，使得任务到达时能够根据自身的特点去选择适合自己的调度策略，以便得到更快的响应。首先对调度的切换过程进行了时间自动机建模，然后用计算树逻辑(CTL)公式描述了进程调度实时性的相关属性，最后在模型验证工具Uppaal中进行了验证。验证结果表明新的切换策略使得Nuttx操作系统在给定的时间内能够完成相应的操作，满足了实时性需求。本文对于测试和评估实时操作系统性能有一定的借鉴作用。Nuttx操作系统能够满足工业机器人控制系统的实时性需求，因此在工业机器人控制领域有着很好的应用前景。