2020, Vol. 31
2. 中国空间技术研究院, 北京 100094;
3. 计算机科学国家重点实验室(中国科学院 软件研究所), 北京 100190
2. China Academy of Space Technology, Beijing 100094, China;
3. State Key Laboratory of Computer Science(Institute of Software, Chinese Academy of Sciences), Beijing 100190, China
实时操作系统是航天领域必不可少的基础软件系统.操作系统负责管理计算机的各类硬件资源, 操作系统中任何一个小错误都可能导致致命故障.任务管理是操作系统中必不可少的核心功能, 任务管理的核心操作为任务调度.在这种实时操作系统中, 对其可靠性的保证极其重要, 对程序进行形式化建模并对模型进行验证, 是目前在高可信计算机领域中一种严格的可靠性保证方法.形式化验证方法是用数学的方法对程序进行形式化规约、建模和验证性质的过程, 从而发现程序中的错误和测试方法无法得到的潜在隐患.
操作系统的需求是设计和实现的起点, 操作系统的可靠性非常重要.本文对航天领域某实时操作系统的任务管理从用户角度在需求层进行形式化规约和验证, 提出了一种基于任务列表集合的验证方法.用的验证语言为Coq, 最终在需求层证明该操作系统的正确性.由于篇幅限制, 本文只介绍任务调度和用户操作中最具代表性的任务创建操作的建模和性质验证工作, 并在验证过程中对提出的性质中的其中一条进行形式化验证.
1 相关工作目前, 国内外有许多关于操作系统内核上的模型层和代码实现层的形式化验证的研究.模型层的形式化验证和代码实现层的形式化验证大有不同:模型层建模只需描述对模型状态产生影响的需求功能行为和操作语义, 不必考虑具体的代码实现细节, 不涉及对代码的建模分析; 代码层的建模需将实现代码语义转换为验证工具能识别的验证语句, 必须涉及实现细节[1, 2].Gerwin Klein等人利用定理证明器Isabelle/HOL对seL4内核进行模型层和代码层的形式化验证, 包括内存管理模块、并发管理模块、IO管理模块的建模, 证明了实现代码的性质和模型层有一致性[1].Gu等人在代码层建立并发操作系统内核模型并进行分模块验证, 该模型是可扩展的体系结构, 建模并进行验证的模块包括物理内存管理、虚拟内存管理、共享内存管理、共享队列库、线程管理[3].Feng等人就验证整个复杂软件系统可靠性的问题, 针对不同的模块在验证时使用的验证逻辑可能不同的原因, 因此采用对特定模块采用特定验证方法的方式, 分别验证可靠性, 最后将这些模块连接在一起, 验证整个系统的可靠性[4].Fu等人利用基于依赖保证的模拟方法对并发程序转换进行了验证, 验证了并发程序的编译和优化、并发对象的线性化和原子性[5].Xu等人利用Coq对操作系统内核进行建模验证, 提出了一种操作系统内核验证框架, 并利用该框架证明了μC/OS-Ⅱ的优先级反转自由[6].Chen等人利用Coq建立通用设备模型, 对可中断的操作系统内核和设备驱动程序进行验证[7, 8].Shao等人利用断言语言对并发线程管理代码进行建模验证, 建立的模型为两层框架, 允许线程修改自己的线程控制块, 提出类Hoare逻辑系统验证带硬件中断的抢占式多任务并发系统, 并且使用定理证明工具Coq证明提出的逻辑系统的可靠性[9, 10].Ma等人提出了结构拆分方法以及分离内存和数据结构形状的方法, 实现对某航天器操作系统内核复杂数据结构的形式化定义[11].June等人在中断并发条件下对任务调度行为证明其正确性, 作者只对影响调度决策的部分建模, 对模型产生影响的只有两个因素:正在执行的任务和中断处理标志性事件[12].Cao等人提出了VST-Floyd半自动策略以及层次演算方法, 该策略在Coq工具中展示如何指定、编程、验证和组合模型层, 在实际的编程语言中实例化层次演算, VST-Floyd采用前向验证的思路, 用于顺序代码的验证[13].Zou等人利用验证工具Coq对并发文件系统实现细粒度的验证, 将文件系统并发操作进行线性化分析, 提出一种通过辅助机制用来指定、实现和验证具有原子接口的并发文件系统的框架[14].Wang等人通过提出一个显示的内存推理机制来推理内存划分在多线程程序运行过程中的变化, 验证了线程调度、上下文切换及创建和退出操作的性质, 实现了对线程部分功能细粒度的验证[15].Ma等人在μC/OS-Ⅱ上对消息队列机制中涉及的几个内部函数进行代码层形式化规范式编写, 证明了共享数据结构的不变性[16].Gu等人对空间操作系统SpaceOS内核状态建模为状态机, 描述内核的数据结构并对提出的8条性质进行形式化验证, 证明了内核的正确性[17].Simon等人为证明seL4实现代码与可执行的规范的精化, 提出了一个形式化的Isabelle/HOL框架.该框架在代码层完成对seL4的高性能c实现正确实现可执行规范的形式化的机器检查证明[18].Qiao等人利用event-B工具对航天器内存管理算法和代码进行验证, 验证了模型具有实际内存块的连续、无重叠等性质[19].
上面学者对操作系统内核的某些模块形式化验证做了大量工作, 但是对任务管理模块的需求层的建模和验证工作不够完善.Shao等人和June等人仅对任务调度行为建模和验证, 缺乏对任务管理模块中其他系统操作的验证, 如任务创建、任务删除、任务挂起等操作.Tan利用建模工具event-B对任务管理进行建模, 由于event-B工具的特性, 当针对一个任务创建操作的建模涉及多种任务状态情况时, 需定义多个关联函数, 增加了建模的复杂性和工作量[20].在对一个涉及多种任务状态的操作进行建模时, Coq具有更强的表达能力, 可以仅用一个函数完成对该操作的建模.因此, 本文利用Coq对任务管理中涉及的操作系统任务调度等一系列任务管理操作进行准确清晰地形式化建模, 并降低了验证工作量.
2 基于Coq的任务管理需求层模型建立本文所建立的模型将上层用户操作以及操作系统中的任务调度模型化, 当执行用户操作时, 会改变任务控制块内容以及系统的整体状态.除此之外, 在满足某些特定条件下, 会对操作系统中系统调度进行调用.本文的创新之处为:将所有任务TCB结构连接成任务TCB列表, 并放入系统整体状态结构中, 并且能够实时更新任务TCB列表, 使得任何任务都可以访问其他任务TCB内容但又不能修改其他任务TCB, 在任何操作下的执行都能保证可靠性, 以及保证在整个系统运行期间总体的任务TCB列表与任务TCB保持一致性.除此之外, 系统整体状态结构中包含所有状态的任务名列表, 为后续的验证工作提供方便.在本文所建立的模型中, 任务调度为不涉及时间片的可抢占调度方式.需求层模型建模涉及任务TCB内容(用TData表示)、系统整体状态结构(用TList表示)和对任务执行的操作(用c表示), 任务TCB和任务集合状态初始化start.
模型为四元组:(TCB, TList, c, start).在本模型中没有考虑内存分配的具体操作, 只用内存分配是否成功来表示内存的分配情况.模型中涉及的基本数据类型定义以及操作定义介绍如下.
2.1 基本数据类型定义模型的任务类型Tasks、任务状态TaskStatus、任务的优先级Priority是确定下来的内容.我们将其中Tasks和TaskStatus用归纳方法定义它们的类型.Priority定义为整数类型, 并通过一个判断函数限定Priority的范围.模型中的任务TCB用一个包含TCB属性——任务名、任务状态、任务优先级、延时时间、创建任务标志、删除任务标志、任务挂起标志、任务恢复标志、任务延时标志、任务重启标志、任务调度标志、轮转剩余时间清零标志和更新优先级标志的数据结构TData来表示.总体任务集合状态用一个包含未创建任务列表、就绪任务列表、执行任务列表、挂起任务列表、阻塞任务列表、延时任务列表、挂起延时任务列表、挂起阻塞任务列表、当前最大优先级、当前最大优先级对应的任务列表以及所有任务TCB列表的数据结构TList表示.在Coq中, 定义具体数据类型如下所示:
定义1(任务集(多个不同任务类型的集合)).在模型中将任务类型设置为21个.这21个任务的任务状态为: 1个正在执行的任务、3个未创建的任务、2个就绪态的任务、3个延时态任务、3个挂起态任务、3个阻塞态任务、3个挂起延时态任务、3个挂起阻塞态任务.未创建任务、就绪态任务、延时态任务、挂起态任务、阻塞态任务、挂起延时态任务、挂起阻塞态任务的优先级分别大于、等于和小于正在执行任务的优先级.2个就绪态任务优先级分别小于和等于正在执行任务的优先级.由于初始化时正在执行的任务肯定为最高优先级的任务, 所以不存在就绪任务优先级大于正在执行任务的情况.这些任务的定义模拟了模型任务集合的一般状态, 若新加入没有定义好的任务, 则需将该新任务添加到Tasks中并改变初始化的系统整体状态集合中.这些任务的定义代表系统初始化后的一般状态(初始化后一般状态见第2.3.2节).在Coq中定义如下:
Inductive Tasks: Type:=
|t1: Tasks |t2: Tasks |t3: Tasks |t4: Tasks |t5: Tasks |t6: Tasks |t7: Tasks |t8: Tasks |t9: Tasks |t10: Tasks|t11: Tasks
|t12: Tasks |t13: Tasks |t14: Tasks |t15: Tasks |t16: Tasks |t17: Tasks |t18: Tasks |t19: Tasks|t20: Tasks |t21: Tasks.
t1~t21是所有任务的id, 这些任务在使用之前必须被分配内存.
定义2(任务状态集(多种任务状态类型的集合)).在模型行中涉及8种任务状态类型, 在Coq中定义所有任务状态如下:
Inductive TaskStatus: Type:=
|uncreat: TaskStatus |executing: TaskStatus |ready: TaskStatus |delay: TaskStatus |block: TaskStatus|suspend: TaskStatus |suspend_delay: TaskStatus |suspend_block: TaskStatus.
分别表示未创建、执行、就绪、延时、阻塞、挂起、挂起延时和挂起阻塞8种任务状态类型.
定义3(任务优先级集合(多种任务优先级类型的集合)).本模型支持任务优先级的个数为64个:Priority= 0...63.在Coq中定义时将优先级定义为无符号整数类型并通过判断函数pri_ritional判断Priority是否为0~63的整数, 任务优先级定义如下:
Definition priority:=nat.
在本模型中, 任务优先级的数值越大, 任务优先级越低.
定义4(单个任务TCB结构(单个任务控制块数据结构)).任务TCB内容包含一个任务的所有私有属性. TCB中包含的这些标志通过定义一个数据结构来实现每个任务属性的管理.在Coq中定义如下:
Record TData:=
mkTData{
TL: Tasks; TS: TaskStatus; TP:priority; TDtime: nat; creatFlag: nat; deleteFlag:nat; suspendFlag: nat; resumeFlag: nat; delayFlag:nat; restartFlag: nat; scheduleFlag: nat; clearTickFlag:nat; updatePriorityFlag: nat; }.
其中, TL∈Tasks表示任务名, TS∈TaskStatus表示该任务的状态, TP∈Priority为任务的优先级, TDtime∈nat表示延时时间.creatFlag∈nat表示创建任务的标志:如果creatFlag=1, 表示可以创建任务, 当创建完成后, creatFlag要置为0;creatFlag=0表示任务已经创建, 不能够重新创建.deleteFlag∈nat表示删除任务的标志:如果deleteFlag=1, 表示任务不是未创建状态, 可以执行删除操作, 删除操作完成后要置为0;如果deleteFlag=0, 表示任务为未创建状态, 不可以执行删除操作.suspendFlag∈nat为任务挂起标志:suspendFlag=1表示可以执行挂起操作, 挂起操作执行后要置为0;如果suspendFlag=0, 表示不可以执行挂起操作.resumeFlag∈nat为任务恢复标志:如果resumeFlag=1, 表示可以执行任务恢复操作, 执行完任务恢复操作后置为0;resumeFlag=0表示不可以执行任务恢复操作.delayFlag∈nat为任务延时标志:delayFlag=1表示可以执行任务延时, 在任务延时操作执行后置为0;delayFlag=0表示不可以执行任务延时操作.restartFlag∈nat为任务重启操作:restartFlag=1表示可以执行任务重启操作, 在执行完任务重启后置为0;restartFlag=0表示不可以执行任务重启操作.scheduleFlag∈nat为任务调度标志:scheduleFlag=1表示可以执行任务调度, 在执行完任务调度操作之后置为0;scheduleFlag=0表示不可以执行任务调度操作.clearTickFlag∈nat为轮转剩余时间清零标志:clearTickFlag=1表示可以将轮转剩余时间清零, 清零完成后置为0;clearTickFlag=0表示不可以将轮转剩余时间清零.updatePriorityFlag∈nat为更新优先级标志:updatePriorityFlag=1表示可以更新优先级, 更新完成后置为0;updatePriorityFlag=0表示不可以更新优先级.
定义5(系统整体状态集合(系统整体状态数据结构)).系统整体状态集合(TList)包含模型中所有任务状态列表的集合、记录最高优先级和最高优先级对应的任务名列表以及所有任务TCB列表.TList中包含各个任务状态的列表, 用来记录每一个任务所属的状态列表, 每当有任务更改其TCB信息时, 都会更新任务状态列表, 任务状态列表的作用为对模型进行验证时方便统计, 例如统计所有任务列表的总数应为初始状态定义的任务个数, 并且任何两个任务状态列表都不包含相同任务名, 保证每个任务只有一个任务状态.TList中包含的最高优先级和最高优先级对应的任务名列表, 用来判断在经过某任务操作后是否执行任务调度.例如, 最高优先级大于正在执行的任务就会触发任务调度.TList中包含的任务TCB列表用来实时记录所有任务的TCB信息, 保证实时更新任务TCB信息.整体的TList能够保证在进行操作时能够获得正确的任务TCB信息以及在涉及任务调度时能够获得正确的上下文任务.
在Coq中定义系统整体状态数据结构TList如下:
Record TList:=
mkTList{
uncreatList: listTasks; executingList: listTasks; readyList: listTasks; delayList:listTasks; blockList: listTasks; suspendList: listTasks; suspend_delay_List: listTasks; suspend_block_List: listTasks; TminP: priority; TminPL: listTasks; TminPTL: list_TData; }.
其中, uncreatList为所有任务中未创建任务的任务名列表; executingList为所有任务中正在执行任务的任务名列表, 理论上, 在已经初始化所有任务并且正在执行的任务只有一个, 则不论进行何种操作, 正在执行的任务都只有一个; readyList为所有任务中就绪任务的任务名列表; delayList为所有任务中睡眠任务的任务名列表; blockList为所有任务中阻塞的任务名列表; suspendList为所有任务中挂起的任务名列表; suspend_delay_List为所有任务中睡眠挂起的任务名列表; suspend_block_List为所有任务中阻塞挂起的任务名列表; TminP为当前就绪列表中最大优先级; TminPL为最大优先级TminP对应的任务列表; TminPTL为所有任务的TCB列表.
2.2 具体任务操作定义本文要验证的某实时操作系统的特点为:每个任务周期性执行, 支持基于优先级的可抢占任务调度.用户对任务的操作包括任务创建、任务删除、任务挂起、任务延时、任务阻塞、任务调度、任务恢复、任务重启的8个操作.任务管理能够实现这些用户操作.在我们验证的操作系统中要求任务具有就绪、未创建、运行、阻塞、睡眠、挂起、阻塞挂起、睡眠挂起这8个状态.8种状态之间的转换图如图 1所示.
|
Fig. 1 Task conversion process 图 1 任务转换过程 |
2.2.1 任务调度
本操作系统中的调度为基于优先级的可抢占的调度策略.用户是无法看到任务调度过程的.基础的基于优先级的任务调度为将最高优先级就绪任务转换为运行态, 这种情况下, 在执行任务调度之前是没有任何任务正在运行的.这个任务调度过程为选择就绪态任务中最高优先级任务运行, 将该任务的状态修改为执行态, 更新就绪态任务的最高优先级任务.基于优先级的可抢占任务调度不同于不可抢占式的任务调度, 这种调度在执行任务调度之前可以有任务正在运行, 当就绪态任务列表中最高优先级任务的优先级大于正在执行任务的优先级时, 任务调度可以将CPU等资源从正在执行的任务中抢占过来给就绪态任务中的最高优先级任务.该调度过程为将正在执行任务修改为就绪态, 将最高优先级任务状态修改为运行态, 更新就绪任务中最高优先级任务.
在模型中, 用一个函数表示任务调度过程.任务调度函数只针对总体状态列表中当前最大优先级任务进行操作, 当有新任务被创建或已有任务被删除、挂起、阻塞等操作会使整个系统状态发生变化, 并且可能会触发任务调度.任务调度函数的输入参数有两个, 分别为单个任务TCB内容TData(设为m)、系统整体状态集合TList(设为t), 输出参数为3个, 分别为执行某操作后的任务TCB内容、执行某操作后的系统整体状态集合和是否执行成功操作的bool类型标志.
根据单个任务TCB中任务的执行状态是否为ready以及单个任务TCB中优先级是否大于正在执行任务的优先级, 将任务调度分为4种情况.用Coq形式化定义任务调度过程如下.
Definition scheduleTasks(m:TData)(t:TList):(Tdata*TList*bool):=(*任务调度操作*)
match (TS m, scheduleFlag m, isnil_Task(remove_one(TL m)(TminPLt)),
isnil_Task(executingList t)) with
1. |(ready, 1, true, true)⇒(trans_TD(m)(executing)(0), trans_TL(add(TL m)(executingList t))(remove_one(TL m)(readyList t))(finmin(remove_TData m(TminPTL t)))((min_list(finmin (remove_TData m(TminPTL t)))(remove_TData m(TminPTL t))))(add_TData(trans_TD(m)(executing)(0))(remove_TData m(TminPTL t))), true) (*情况1*)
2. |(ready, 1, false, true)⇒(trans_TD(m)(executing)(0), trans_TL(add(TL m)(executingList t))(remove_one (TL m)(readyList t))(TminP t)(remove_one(TL m)(TminPL t))(add_TData(trans_TD(m)(executing)(0)) (remove_TData m (TminPTL t))), true) (*情况2*) |(ready, 1, true, false)⇒ match min_pri(TP m)(TP(map1(fstTasks(executingList t))(TminPTL t))) with
3. |true⇒(trans_TD(m)(executing)(0), trans_TL(add(TL m)nil)(add(TL(map1(fstTasks(executingList t)) (TminPTL t)))(remove_one(TL m)(readyList t)))(finmin(remove_TData m(add_TData(change(map1 (fstTasks(executingList t))(TminPTL t))(ready))(remove_TData(map1(fstTasks(executingList t)) (TminPTL t))(TminPTL t)))))(min_list(finmin(remove_TData m(add_TData(change(map1(fstTasks (executingList t))(TminPTL t))(ready))(remove_TData(map1(fstTasks(executingList t))(TminPTL t)) (TminPTL t)))))(remove_TData m(add_TData(change(map1(fstTasks(executingList t))(TminPTL t)) (ready))(remove_TData(map1(fstTasks(executingList t))(TminPTL t))(TminPTL t)))))(add_Tdata (trans_TD (m)(executing)(0))(remove_TData m(TminPTL t)), true) (*情况3*)
4. |false⇒(m, t, false) (*情况4*)
end
5. |(_, _, _, _)⇒(m, t, false) (*情况4*)
end (*任务调度操作完成*)
上面的Coq代码定义中, isnil_Task判断一个任务该列表是否为空, remove_one表示从任务列表中删除一个任务, trans_TD表示修改任务TCB的任务状态和任务调度标志位, trans_TL表示修改整体任务状态集合中正在执行任务列表、就绪列表、最高优先级的值、最高优先级任务列表、所有任务TCB列表, fin_min表示从任务TCB列表中找到最大优先级, add_TData表示向任务TCB列表中添加任务TCB, remove_TData表示从任务TCB列表中移除一个任务TCB, map1表示从任务TCB列表中查找已知任务名对应的该任务TCB的结构.任务调度函数可归纳为4种情况, 具体的说明如下.
(1) 情况1
当TData的任务状态为ready并且为最高优先级任务、调度任务标志为1, 系统整体状态执行列表为空, 系统整体状态集合中最大优先级任务列表删除任务m后列表为空时:执行任务调度后, 将m的状态改为executing, 调度任务标志改为0, 修改总体任务集合t的内容, 将t的readyList列表删除m的任务名, 将m的任务名加入到t的executingList中, 将t的最高优先级、最高优先级对应的任务列表更新、将t的所有任务TCB列表删除m并添加修改后的m.
(2) 情况2
当TData的任务状态为ready并且为最高优先级任务、调度任务标志为1, 系统整体状态执行列表为空, 系统整体状态集合中最大优先级任务列表删除任务m后列表不为空时:执行任务调度后, 将m的状态改为executing, 调度任务标志改为0, 修改总体任务集合t的内容, 将t的readyList列表删除m的任务名, 将m的任务名加入到t的executingList中, 将t的最高优先级对应的任务列表删除任务m的任务名、将t的所有任务TCB列表删除m并添加修改后的m.
(3) 情况3
当TData的任务状态为ready且为最高优先级任务、调度任务标志为1, 系统整体执行状态列表不为空, Tdata的任务优先级大于正在执行任务优先级, 系统整体状态集合中最大优先级任务列表删除任务m后列表为空时, 发生抢占式调度, 具体操作为:将m的状态改为executing, 调度任务标志为0, 将t的readyList列表删除m的任务名, 将t的executingList列表置空并将m的任务名加入到executingList中, 将正在执行任务名添加到readyList列表, 更新最高优先级和最高优先级任务名列表, 删除t的所有任务TCB列表中的m和正在执行任务, 之后添加更新后的m和更新后的正在执行任务.
(4) 情况4
除上面情况外, 执行任务调度后单个任务控制块内容m和系统整体状态t不改变.
2.2.2 任务创建任务创建是用户操作, 在任务创建的过程中会调用任务调度.当用户对一个任务执行创建任务操作, 如果该任务已经被创建, 则不做任何操作; 如果任务没有被创建, 则为该任务分配内存, 初始化其任务控制块, 将该任务状态修改为就绪态并插入就绪列表.之后比较其优先级与就绪列表中最高优先级:若小于最高优先级, 则结束完成创建操作; 若大于最高优先级, 则更改就绪列表最高优先级, 并且新的最高优先级大于正在执行任务的优先级, 则触发调度完成创建操作; 若等于最高优先级, 则在就绪列表最高优先级任务中插入新创建的任务.
在Coq中任务创建函数的两个参数为任务TCB内容TData(命名为m), 系统整体状态集合TList(命为t).根据单个任务TCB执行状态以及该任务与正在执行任务的关系将任务创建分为5种情况, 任务创建的5种情况用Coq形式化定义如下.
Definition creatTask(m:TData)(t:TList):(TData*TList*bool):=(*创建任务操作*)
match (TS m, pri_r(TP m), creatFlag m, min_pri(TP m)(TminP t), min_eqpri(TP m)(TminP t)) with
|(uncreat, true, 1, true, false)⇒
match min_pri(TP m)(TP(map1(fstTasks(executingList t))(TminPTL t))) with
1. |true⇒(trans_TD1 m ready 0, scheduleTasks(trans_TD1 m ready 0)(trans_TL1(remove_one(TL m) (uncreatList t))(add(TL m)(readyList t))(TP m)(TL m::nil)(add_TData(trans_TD1 m ready 0) (remove_TData m(TminPTL t))), true)) (*情况1*)
2. |false⇒((trans_TD1 m ready 0), trans_TL1(remove_one(TL m)(uncreatList t))(add(TL m)(readyList t)) (TP m)(TL m::nil)(add_TData(trans_TD1 m ready 0)(remove_TData m(TminPTL t))), true) (*情况2*)
end
3. |(uncreat, true, 1, false, true)⇒((trans_TD1 m ready 0), trans_TL1(remove_one(TL m)(uncreatList t)) (add(TL m)(readyList t))(TminP t)(cons(TL m)(TminPL t))(add_TData(trans_TD1 m ready 0) (remove_TData m(TminPTL t))), true) (*情况3*)
4. |(uncreat, true, 1, false, false)⇒((trans_TD1 m ready 0), transTL1(remove_one(TL m)(uncreatList t)) (add(TL m)(readyList t))(TminP t)(TminPL t)(add_TData(trans_TD1 m ready 0)(remove_TData m (TminPTL t))), true) (*情况4*)
5. |(_, _, _, _, _)⇒(m, t, false) (*情况5*)
end (*创建任务操作完成*)
上面的Coq代码中, pri_r用来判断函数优先级是否在0~63之间, min_pri判断第1个参数优先级的值是否小于第2个参数优先级, min_eqpri判断两个参数优先级是否相等, trans_TD1用来修改任务TCB中的任务状态和创建标志位, trans_TL1用来修改整体状态集合中的未创建列表、就绪列表、最高任务优先级、最高优先级任务列表、所有任务TCB列表, add_TData表示向任务TCB列表中添加任务TCB, remove_TData表示从任务TCB列表中移除一个任务TCB.定义的任务创建函数可归纳为5种情况, 具体的说明如下.
(1) 情况1
新创建任务的优先级大于正在执行任务的优先级, 触发调度.更新的具体内容为:修改m的任务状态为ready, 修改m的任务创建标志为0, t的未创建任务名列表删除m对应的任务名、向t的就绪任务名列表中添加m对应的任务名、更新t的最高优先级为m的优先级, 更新最高优先级任务为m的任务名、将t的总体TCB列表中的m删除并添加更新后的m.然后, 以更新后的m和更新后的t作为参数触发调度函数完成任务创建.
(2) 情况2
新创建的任务m优先级大于系统整体状态集合t中的最高优先级, 并且新创建任务优先级不大于正在执行任务的优先级, 则经过创建函数操作后, 更新任务TCB内容和系统整体状态集合.更新的具体内容为:修改m的任务状态为ready, 修改m的任务创建标志为0, t的未创建任务名列表删除m对应的任务名、向t的就绪任务名列表中添加m对应的任务名、更新t的最高优先级为m的优先级, 更新最高优先级任务为m的任务名、将t的总体TCB列表中的m删除并添加更新后的m, 完成任务创建.
(3) 情况3
新创建的任务m的优先级和总体任务集合t的最高优先级相等, 则经过任务创建后, 更新任务TCB内容和总体任务集合.更新具体实现为:将m的任务状态设置为ready, 将m的任务创建标志修改为0, 将t的未创建任务名列表删除m的任务名, 将t的就绪任务名列表添加m的任务名, 将最高优先级任务名列表添加m的任务名, 将t的总体TCB列表中的m删除并添加更新后的m, 完成任务创建.
(4) 情况4
新创建的任务m的优先级小于总体任务集合t的最高优先级, 则更新的过程为:将m的任务状态设置为ready, 将m的任务创建标志设置为0, 将t的未创建任务名列表删除m的任务名, 将t的就绪任务名列表添加m的任务名, 将t的总体TCB列表中的m删除并添加更新后的m, 完成任务创建.
(5) 情况5
除上述4种情况外, 执行创建操作后单个任务m和系统整体状态t都不改变.
2.2.3 初始化任务TCB以及系统整体状态本文给出21个任务的初始化单个任务TCB内容s1~s8_3, 代表了任务初始化的一般情况.其中:s1任务代表正在执行中的任务; 任务s2_1~s2_3分别代表未创建任务, 且优先级分别大于、等于、小于执行态任务的优先级; s3_1, s3_2分别代表就绪态任务, 且优先级分别等于、小于执行态任务优先级; s4_1~s4_3分别代表睡眠态任务, 且优先级分别大于、等于、小于执行态任务的优先级; s5_1~s5_3分别代表挂起态任务, 且优先级分别大于、等于、小于执行态任务的优先级; s6_1~s6_3分别代表阻塞态任务, 且优先级分别大于、等于、小于执行态任务的优先级; s7_1~s7_3分别代表阻塞挂起态, 且优先级分别大于、等于、小于执行态任务的优先级; s8_1~s8_3分别代表睡眠挂起态, 且优先级分别大于、等于、小于执行态任务优先级.并且根据初始化的任务给出整体任务状态startlist, 整体任务状态startlist由系统整体状态数据结构TList构成.在这个初始化的状态中, 正在执行任务是最高优先级任务且只有一个, 就绪列表中没有任务优先级高于正在执行任务的优先级, 且一个任务只对应一个优先级.在初始化时满足静态性质的要求.具体的Coq定义如下.
Definition s1:=mkTData(t1)(executing)(8)(0)(1)(1)(1)(1)(1)(0)(1)(1)(1).
Definition s2_1:=mkTData(t2)(uncreat)(1)(0)(1)(1)(1)(1)(1)(1)(1)(1)(1).
Definition s2_2:=mkTData(t3)(uncreat)(8)(0)(1)(1)(1)(1)(1)(1)(1)(1)(1).
Definition s2_3:=mkTData(t4)(uncreat)(9)(0)(1)(1)(1)(1)(1)(1)(1)(1)(1).
Definition s3_1:=mkTData(t5)(ready)(8)(0)(0)(1)(1)(1)(1)(1)(1)(1)(1).
Definition s3_2:=mkTData(t6)(ready)(10)(0)(0)(1)(1)(1)(1)(1)(1)(1)(1).
Definition s4_1:=mkTData(t7)(delay)(1)(8)(0)(1)(1)(0)(1)(1)(1)(1)(1).
Definition s4_2:=mkTData(t8)(delay)(8)(8)(0)(1)(1)(0)(1)(1)(1)(1)(1).
Definition s4_3:=mkTData(t9)(delay)(11)(8)(0)(1)(1)(0)(1)(1)(1)(1)(1).
Definition s5_1:=mkTData(t10)(suspend)(5)(0)(0)(1)(0)(1)(1)(1)(1)(1)(1).
Definition s5_2:=mkTData(t11)(suspend)(8)(0)(0)(1)(0)(1)(1)(1)(1)(1)(1).
Definition s5_3:=mkTData(t12)(suspend)(12)(0)(0)(1)(0)(1)(1)(1)(1)(1)(1).
Definition s6_1:=mkTData(t13)(block)(1)(0)(0)(1)(1)(1)(0)(1)(1)(1)(1).
Definition s6_2:=mkTData(t14)(block)(8)(0)(0)(1)(1)(1)(0)(1)(1)(1)(1).
Definition s6_3:=mkTData(t15)(block)(13)(0)(0)(1)(1)(1)(0)(1)(1)(1)(1).
Definition s7_1:=mkTData(t16)(suspend _block)(1)(0)(0)(1)(0)(1)(0)(1)(1)(1)(1).
Definition s7_2:=mkTData(t17)(suspend_block)(8)(0)(0)(1)(0)(1)(0)(1)(1)(1)(1).
Definition s7_3:=mkTData(t18)(suspend_block)(14)(0)(0)(1)(0)(1)(0)(1)(1)(1)(1).
Definition s8_1:=mkTData(t19)(suspend_delay)(1)(8)(0)(1)(0)(0)(1)(1)(1)(1)(1).
Definition s8_2:=mkTData(t20)(suspend_delay)(8)(8)(0)(1)(0)(0)(1)(1)(1)(1)(1).
Definition s8_3:=mkTData(t21)(suspend_delay)(15)(8)(0)(1)(0)(0)(1)(1)(1)(1)(1).
Definition startlist:=mkTList(t2::(t3::(t4::nil)))(t1::nil)(t5::(t6::nil))(t7::(t8::(t9::nil)))(t13::(t14::(t15::nil))) (t10::(t11::(t12::nil)))(t19::(t20::(t21::nil)))(t16::(t17::(t18::nil)))(8)(t5::nil)(cons1 s1 (cons1 s2_1(cons1 s2_2 (cons1 s2_3(cons1 s3_1(cons1 s3_2(cons1 s4_1(cons1 s4_2(cons1 s4_3(cons1 s5_1(cons1 s5_2(cons1 s5_3 (cons1 s6_1(cons1 s6_2(cons1 s6_3(cons1 s7_1(cons1 s7_2(cons1 s7_3 nil1)))))))))))))))))).
2.3 性质证明对于第2节建立的任务管理模型, 对于如何保证模型与实际操作系统的需求层模型保持一致性问题, 本文通过研究实际操作系统的性质, 针对本文的模型提出几条与实际操作系统一样的性质.若通过定理证明工具Coq得出这几条性质在本文建立的模型中能够正确的被证明, 那么说明本文建立的模型是正确的.本文提出的6条性质包含2条静态定义的性质和4条需证明的动态性质, 静态定义的性质是在建模过程中已经定义好的满足要求的性质, 动态性质为在模型运行过程中需要动态证明的性质.
2.3.1 定义时已经满足的静态性质在建立模型时, 对于任务优先级, 在数据结构中只设置一个优先级, 对任务执行何种操作都能保证一个任务只对应一个优先级.任务数据结构中设置状态标志位的目的为标识任务当前所处的状态, 对任务执行一个操作时, 首先判断标志位状态.例如对一个就绪态任务执行创建操作, 该任务当前未创建标志位creatFlag=0时表示已经创建完成, 再次执行创建操作不成功.
本文所提到的2条静态性质如下.
(1) 一个任务只能定义一个优先级, 以任务创建为例进行形式化定义如下:
Theorem priority_equal: forall (x:TData)(y:TData),
y=firstarg(creatTask x startlist)→TP x=TP y.
(*对任何任务进行创建操作, 操作执行完成后, 该任务优先级与操作执行前的优先级都相同*)
上面定理中的函数firstdarg表示返回类型为(TData*TList*bool)的第1个参数的值, 类型即为TData.上面的定理表示对任何任务进行创建操作, 该任务操作完成后优先级与操作执行前优先级都相同.
(2) 模型不存在重复同一操作的情况, 在定义时通过设置每一个任务执行某操作时的标志来保证这种情况不存在, 以任务重启为例进行形式化描述如下:
Theorem unchange_Flag: forall (x:TData)(z:TData),
z=first arg(restartTask(firstarg(restartTask x startlist))(secondarg(restartTask x startlist)))
→equal_Flag(firstarg(restartTask x startlist))(z)=true.
(*对任何任务执行一次重启操作和执行两次重启操作后该任务标志位都相同*)
上面定理中, z表示对同一执行两次重启操作得到的新任务状态, 函数equal_Flag的作用为比较两个类型为TData的任务所有任务标志是否完全相同.该定理说明对任何任务, 对其执行两次重启操作和执行一次重启操作后任务的所有标志位都相同, 表明模型不存在重复同一操作的情况, 即使存在, 该任务状态也不改变.
上述几种定义时已经满足的静态性质在建立模型中已经被实现, 对TCB内容数据结构以及初始化时已经被定义好, 因此能够保证模型在整个运行过程中都满足这些性质.
2.3.2 需证明的动态性质动态进行任务管理时需检验的性质.
性质1. 无论对任何队列进行何种操作, 一个任务只能对应一个任务状态, 即任何两个任务列表都不相交.
本文以任务创建操作为例验证对s2_2任务执行创建操作后每两个状态列表都不相交.在Coq中对性质1提出的定理如下.
Theorem list_uncross: forall x:TList, x=secondarg(creatTask s2_1 startlist)→
NoDup(uncreatList x)(executingList x)(readyList x)(delayList x)(blockList x)(suspendList x)(suspend_delay_ List x)(suspend_block_List x)=false. (*所有任务状态列表两两之间都没有相交任务*)
NoDup的作用是判断各个任务状态列表是否有相交项.NoDup的具体定义如下:
Definition NoDup(a b c d e f g h:listTasks):bool:=
match (intersect a(b++c++d++e++f++g++h))with
|true⇒true
|false⇒
match (intersect b(c++d++e++f++g++h))with
|true⇒true
|false⇒
match (intersect c(d++e++f++g++h)) with
|true⇒true
|fasle⇒match (intersect d(e++f++g++h)) with
|true⇒true
|false⇒match (intersect e(f++g++h)) with
|true⇒true
|false⇒match (intersect f(g++h)) with
|true⇒true
|false⇒match (intersect g h) with
|true⇒true
|false⇒false
end end end end end end end
上面定理和定义中, 符号“++”表示连接两个任务列表, 函数intersect判断两个列表是否包含相同的元素, 返回值为bool类型, 包含相同元素返回true; 否则返回false.上面定理中的函数secondarg表示返回类型为(TData*TList*bool)的第2个参数的值, 类型即为TList.上面定理中的函数length表示计算列表中总共有的元素个数.上述的函数在后面其他性质中是同样的含义.
上面的定理给出:通过对s2进行创建操作, 判断操作后的整体状态列表中所有任务状态列表是否有相交的元素, 通过上面的证明过程, 得到每两种任务状态列表都不含相同元素.同理, 对其他任务进行其他用户操作都能够证明上面定理, 本文不做叙述.
性质2.任何操作过后, 正在执行的任务永远只有一个.
本文以任务创建为例对s2_1执行创建操作, 在Coq中对性质2提出的定理如下:
Theorem executing_account: forall x y: TList, x=secondarg(creatTask s2_1 startlist)→length(executingList x)=1. (*length计算列表长度*)
性质3.无论做何种操作, 任务列表中任务的总数都等于初始化的任务总个数.
本文以任务延时为例对s1执行延时操作, 在Coq中对性质3提出的定理如下:
Theorem list_invari_account5: forall x: TList, x=secondarg(resumeTask s1 startlist)→length(uncreatList x)+ length(readyList x)+length(executingList x)+length(delayList x)+length(blockList x)+length(suspendList x)+ length(suspend_delay_List x)+length(suspend_block_List x)=21.
(*所有类型任务列表相加总数为初始化的任务总数*)
性质4.在任务调度中, 被选择进行任务调度的任务永远为就绪态任务集中优先级最高的任务.
本文以任务删除为例对s1执行删除操作, 在Coq中对性质4提出的定理如下:
Theorem min_Task: forall x: TList, x=secondarg(deleteTasks s3 startlist)→ compare(map1(fstTasks(executingList x))(TminPTL x))x=true.
(*compare函数的功能为比较一个正在执行的任务优先级是否大于就绪任务最高优先级*)
定理中的compare函数的功能为比较两个任务的优先级大小:若第1个任务优先级大于第2个任务, 则返回bool类型的true; 否则返回false.
上面4种动态性质在Coq中的实现代码由于篇幅太长, 本文只针对性质一给出证明过程:在系统整体状态startlist已经定义好的情况下, 进行创建、删除、延时、恢复、重启、挂起操作后每两个状态列表都不相交.
3 基于Coq的任务管理需求层模型形式化验证 3.1 形式化验证性质1在Coq中对第2.3.2节提出的性质1的定理形式化证明如下.
1. Proof. (*开始证明*)
2. intros. (*将所有变量、公式引入上下文环境中*)
3. unfold intersect. (*展开判断两个列表是否含相同元素的函数intersect的定义*)
4. simpl. (*化简, false=false∧false=false∧false=false∧false=false∧false=false∧false=false∧false=false的目标*)
5. tauto. (*自动化简*)
6. Qed. (*证明结束*)
证明过程分为6步:第1步通过Proof告知Coq工具证明开始; 第2步用intros规则将变量公式引入上下文环境中方便后续过程查找变量; 第3步用unfold规则对自定义的判断两个列表是否含有相同元素的函数进行展开; 第四步用simpl规则将展开的intersect函数应用到上下文中并化简得到false=false∧false=false∧false= false∧false=false∧false=false∧false=false∧false=false的目标; 第五步用tauto规则对第四步得到的目标自动化简; 第六步用Qed告知Coq证明过程结束, 完成一个完整证明.
除了上述的证明过程外, 初始化的系统状态中所有任务进行所有8种任务操作后, 系统都满足提出的6条基本性质.
3.2 证明结果在Coq中对模型进行第2.3.1节中的4条性质的验证, 结果表明, 在Coq中建立的模型满足4条性质.具体的代码统计见表 1.
|
Table 1 Coq code line statistics 表 1 Coq代码行统计 |
4 结论
本文介绍了利用Coq对星上计算机操作系统的任务管理模块的需求层建模, 模型中涉及任务调度以及任务管理等操作, 提出了一种基于任务状态列表集合的验证框架, 此框架包含建立的模型和对模型提出2条静态定义性质和4条需动态证明的性质, 并对4条需动态证明的性质进行验证.本文对其中一条动态性质形式化验证过程进行描述.验证结果表明, 需求层模型性质符合实际操作系统任务管理模型的性质.保证了需求层模型和实际操作系统的一致性.
但是本文建立的模型仍需完善.本文只在静态方面定义模型的基本操作, 没有涉及时间片的定义.在后续的工作中将添加进时间片, 利用时间自动机动态地建模, 并验证模型在基于时间的动态运行中是否仍然满足同实际操作系统任务管理相同的6条基本性质.本文的建模没有涉及代码层面的工作, 后续工作将对代码层的函数和算法进行建模和验证.
| [1] |
Klein G, Elphinstone K, Heiser G, Andronick J, Cock D, Derrin P, Elkaduwe D, Engerlhardt K, Kolanski R, Norrish M, Sewell T. seL4: Formal verification of an OS kernel. In: Proc. of the ACM SIGOPS 22nd Symp. on Operating Systems Principles. 2009. 207-220.
|
| [2] |
Gu RH, Koenig J, Ramananandro T, Shao Z, Wu XN, Weng SC, Zhang HZ, Guo Y. Deep specifications and certified abstraction layers. In: Proc. of the 42nd ACM Symp. on Principles of Programming Languages (POPL 2015). 2015. 595-608.
|
| [3] |
Gu RH, Shao Z, Chen H, Wu XN, Kim J, Sjoberg V, Costanzo D. CertiKOS: An extensible architecture for building certified concurrent OS kernels. In: Proc. of the 12th USENIX Symp. on Operating Systems Design and Implementation (OSDI 2016). 2016. 653-669.
|
| [4] |
Feng XF, Shao Z, Guo Y, Dong Y. Combining domain-specific and foundational logics to verify complete software systems. In: Proc. of the VSTTE 2008. 2008. 54-69.
|
| [5] |
Liang HJ, Feng XF, Fu M. A rely-guarantee-based simulation for verifying concurrent program transformations. In: Proc. of the 39th ACM Symp. on Principles of Programming Languages (POPL 2012). 2012. 455-468.
|
| [6] |
Xu FW, Fu M, Feng XF, Zhang XR, Zhang H, Li ZH. A practical verification framework for preemptive OS kernel. In: Proc. of the Int'l Conf. on Computer Aided Verification. Springer-Verlag, 2016. 57-59.
|
| [7] |
Barras B, Boutin S, Cornes C, Courant J, Coscoy Y, Delahaye D, de Rauglaudre D, Filliâtre JC, Giménez E, Herbelin H, Huet G, Laulhère H, Loiseleur P, Muñoz C, Murthy C, Parent C, Paulin C, Saïbi A, Werner B. The Coq Proof Assistant Reference Manual-Version V6.3. 1999.
|
| [8] |
Chen H, Wu XN, Shao Z, Lockerman J, Gu RH. Toward compositional verification of interruptible OS kernels and device drivers. In: Proc. of the 37th ACM SIGPLAN Conf. on Programming Language Design and Implementation (PLDI). 2016. 431-447.
|
| [9] |
Guo Y, Feng XF, Shao Z, Shi P. Modular verification of concurrent thread management. In: Proc. of the 10th Asian Symp. on Programming Languages and Systems (APLAS). 2012. 315-331.
|
| [10] |
Feng XF, Shao Z, Dong Y, Guo Y. Certifying low-level programs with hardware interrupts and preemptive threads. Journal of Automated Reasoning, 2009, 42(2-4): 301-347.
[doi:10.1007/s10817-009-9118-9] |
| [11] |
Ma D, Fu M, Qiao L, Feng XY. Formal specification and verification of complex kernel data structures. Journal of Chinese Computer Systems, 2019, 40(2): 359-366(in Chinese with English abstract).
[doi:10.3969/j.issn.1000-1220.2019.02.021] |
| [12] |
Andronick J, Lewis C, Matichuk D, Morgan C, Rizkallah C. Proof of OS Scheduling Behavior in the Presence of Interrupt-Induced Concurrency. Berlin: Springer-Verlag, 2016: 52-68.
|
| [13] |
Cao QX, Beringer L, Gruetter S, Dodds J, Appel AW. VST-Floyd:A separation logic tool to verify correctness of C programs. Journal of Automated Reasoning, 2018, 61(1-4): 1-56.
[doi:10.1007/s10817-018-9465-5] |
| [14] |
Zou M, Ding HR, Du D, Fu M, Gu RH, Chen HB. Using concurrent relational logic with helper for verifying the AtomFS file system. In: Zou M, Ding HR, Du D, Fu M, Gu RH, Chen HB, et al., eds. Proc. of the 27th ACM Symp. on Operating System Principles. Deerhurst Resort, 2019.
|
| [15] |
Wang HB, Guo Y, Chen YY. Verification multithreaded Code with dynamic thread creation and termination. Journal of Chinese Computer Systems, 2010, 31(8): 1637-1642(in Chinese with English abstract).
http://www.wanfangdata.com.cn/details/detail.do?_type=perio&id=xxwxjsjxt201008034 |
| [16] |
Ma JB, Fu M, Feng XY. Formal verification of the message queue communication mechanism in μC/OS-Ⅱ. Journal of Chinese Computer Systems, 2016, 37(6): 1179-1184(in Chinese with English abstract).
[doi:10.3969/j.issn.1000-1220.2016.06.012] |
| [17] |
Gu HB, Fu M, Qiao L, Feng XY. Formalization and verification of several global properties of SpaceOS. Journal of Chinese Computer Systems, 2019, 40(1): 141-148(in Chinese with English abstract).
http://www.wanfangdata.com.cn/details/detail.do?_type=perio&id=xxwxjsjxt201901026 |
| [18] |
Simon W, Gerwin K, Thomas S, June A, David C, Michael N. Mind the gap: A verification framework for low-level C. In: Berghofer S, Nipkow T, Urban C, Wenzel M, eds. Proc. of the 22nd TPHOLs. LNCS 5674, Springer-Verlag, 2009. 500-515.
|
| [19] |
Qiao L, Yang MF, Tan YL, Pu GG, Yang H. Formal verification of memory management system in spacecraft using Event-B. Ruan Jian Xue Bao/Journal of Software, 2017, 28(5): 1204-1220(in Chinese with English abstract).
http://www.jos.org.cn/1000-9825/5218.htm [doi:10.13328/j.cnki.jos.005218] |
| [20] |
Tan YL, Yang H, Qiao L. Formal modeling and verification of task-management requirement for SpaceOS2 on Event-B. Aerospace Control and Application, 2014, 40(4): 57-62(in Chinese with English abstract).
[doi:10.3969/j.issn.1674-1579.2014.04.011] |
| [11] |
马顶, 付明, 乔磊, 冯新宇. 复杂内核数据结构的形式化描述和验证. 小型微型计算机系统, 2019, 40(2): 359-366.
[doi:10.3969/j.issn.1000-1220.2019.02.021] |
| [15] |
王海波, 郭宇, 陈意云. 验证带有线程的动态创建和退出的多线程程序. 小型微型计算机系统, 2010, 31(8): 1637-1642.
http://www.wanfangdata.com.cn/details/detail.do?_type=perio&id=xxwxjsjxt201008034 |
| [16] |
马杰波, 付明, 冯新宇. μC/OS-Ⅱ中消息队列通信机制的形式化验证. 小型微型计算机系统, 2016, 37(6): 1179-1184.
[doi:10.3969/j.issn.1000-1220.2016.06.012] |
| [17] |
顾海博, 付明, 乔磊, 冯新宇. SpaceOS中若干全局性质的形式化描述和验证. 小型微型计算机系统, 2019, 40(1): 141-148.
http://www.wanfangdata.com.cn/details/detail.do?_type=perio&id=xxwxjsjxt201901026 |
| [19] |
乔磊, 杨孟飞, 谭彦亮, 蒲戈光, 杨桦. 基于Event-B的航天器内存管理系统形式化验证. 软件学报, 2017, 28(5): 1204-1220.
http://www.jos.org.cn/1000-9825/5218.htm [doi:10.13328/j.cnki.jos.005218] |
| [20] |
谭彦亮, 杨桦, 乔磊. 基于Event-B的SpaceOS2操作系统任务管理需求形式化建模与验证. 空间控制技术与应用, 2014, 40(4): 57-62.
[doi:10.3969/j.issn.1674-1579.2014.04.011] |