基于SPIN的Linux管道模型检测研究

速昱行 ，王金波

（1.中国科学院大学北京100190；2.中国科学院空间应用工程与技术中心北京100094）

为了适应航天事业的快速发展，完成繁杂的空间任务，对嵌入式软件系统的可靠性、稳定性等提出了更高的要求，Linux作为一款开源、可裁剪、可移植的操作系统逐渐被应用于国内外航天嵌入式领域。

对于航天任务而言，其特殊性决定了必须在研制阶段就确保星载嵌入式软件的可靠性，否则可能会造成灾难性的后果。例如，1997年火星“探路者”号在执行任务时，遇到系统频繁重启问题；1996年欧洲航天局发射的一架未载人的阿丽亚娜5号火箭，在发射升空40秒钟之后发生了爆炸。因此，对操作系统进行分析和验证是至关重要的。目前，对于操作系统的测试验证工作，尚无明确的标准和规范，主要的方法有以下几种[1-5]：

1）通过各种系统调用测试内核功能的安全性和正确性；

2）通过第三方的测试套件（工具）对内核进行测试；

3）各种性能测试，如实时性测试等。

针对已有测试手段只能尽可能多的找出错误和缺陷，形式化验证通过对系统所有行为状态的模拟，可以在早期便彻底的检测系统是否还存在其他问题。模型检测作为形式化验证的其中一支于近年来成功地应用在了通用操作系统的分析和验证中[4]，特别是与数字电路和通信协议有关的设计中。同时进程间通信（IPC）对操作系统的重要性不言而喻，因此对其进行模型检测非常有意义，也成为一个研究模型检测对操作系统验证的切入点。

1 模型检测和SPIN概述

形式化验证是基于用形式化语言描述的规格（specification）之上进行模型（model）分析和验证，从而发现系统中存在的不一致性、歧义性、不完整性和竞态条件的方法。其主要手段包括模型检测和定理证明。前者的应用范围限定在有限状态并发系统上，可以在有限的时间和空间内完全自动运行和终止；后者则被用于无限状态的推理，但只有其中一部分可以自动进行，但即使验证性质为真，却可能需要无限大的时间和内存。因此模型检测应用场景更加广泛，可以用在中等规模的计算机上运行[4]。

模型检测将建立的系统模型及性质作为检测工具的输入，一般通过深度优先遍历的方式进行状态空间搜索，从而判断属性正确与否。目前已经开发出的模型检测工具有很多[5]，如SMV、SPIN、JPF、Isabelle/HOL、MOPS等。模型检测一般经过以下3个步骤：

1）建模——抽象模型提取以及转化为能被检测工具接受的形式；

2）刻画——声明模型需要满足的性质；

3）验证——分析验证结果（错误轨迹）。

本文工作主要基于SPIN，其最大特点是采用了偏序规约、on the fly等技术[8]，从而状态空间的数目得以缩减，提高了检测效率。它的建模语言为Promela，可以用线性时态逻辑（LTL）和断言（assertion）来声明系统属性，支持随机、交互式和引导式模拟。SPIN的每个进程都被看作有限状态自动机来建模，实际并发系统的全局行为就通过计算这些自动机的异步交错积来得到：1）对LTL公式刻画的系统性质取反，得到Büchi自动机P；2）计算系统中每个进程的转移子系统的乘积，建立Büchi自动机S，得到模型代表的系统的全局行为；3）计算P与S的乘积；4）检查最后乘积得到的自动机，若其所能接受的语言为空，则表示系统满足所描述的性质，反之说明系统不满足原本定义的属性要求。具体在软件中操作的过程如图1直观所示，证明时序逻辑公式φ是否在模型M中成立（即证明M|=φ）。

图1 SPIN模型检测过程

Promela是SPIN的建模语言，其中包括的抽象对象有变量、消息、通道、进程、迁移和全局系统状态。消息通道支持会面点（rendezvous）或缓冲的（buffered）消息传递方式，实现同步或者异步通信。

2 Linux管道的分析验证

2.1 管道的描述

在Linux中，处于用户空间的进程拥有各自的地址空间，一般无法互相访问。然而多数场景下需要进程间进行相互通信，以完成系统的某些功能，如数据传输、数据共享、消息通知、进程控制等[7]。进程通过与内核及其它进程之间的互相通信来协调各自的行为。管道属于IPC中一种使用频率较高的通信手段，有匿名管道和命名管道之分。前者只能在父子进程或者兄弟进程之间使用，而后者打破了这种限制，提供了文件的路径来识别管道，从而实现在没有亲缘关系的进程之间通信，本文仅讨论匿名管道。管道从本质上说也是文件的一种，但它又和普通的文件有所区别，它是内核中一个大小固定的缓冲区。其具体实现的源代码位于＜fs/pipe.c>中，创建过程如图2所示。

图2 管道创建过程

1）父进程通过调用int pipe（int fd[2]）创建管道，这里得到的两个文件描述符fd[0]、fd[1]，分别指向管道的读端和写端，此时读端和写端皆指向父进程；

2）父进程通过调用fork（）创建子进程，子进程拷贝了父进程除某些资源之外的所有内容，包括上一步创建的管道，即子进程也有两个文件描述符指向同一管道；

3）随后，父进程关闭读端，子进程关闭写端，则前者向管道中写入数据，而后者就可以将管道中的数据读出，这样就实现了进程间通信。

管道使用的过程中可能会面临问题有：缓冲区的溢出，即当要写入的数据大于缓冲区大小时，数据的丢失；阻塞问题，读写进程在未满足自身读写要求时，可能会陷入死等状态；还有管道破裂，即读写进程关闭不一致的情况；以及数据写入可能不保证原子性等等。文献[13]提出了一种建模方法，本文针对其中的疏漏和不完善进行了研究和改进。

2.2 管道的建模

根据管道通信思想和源代码的研读，结合SPIN的使用特点，用有限状态自动机（FSA）描述模型。将管道、管道读端以及写端看作3个实体，建立3个相应的FSA，3个实体的交互，必然涉及到消息传递以及共享变量状态改变，加上迁移条件的复杂性和耦合性，加大了建模的难度。文献[13]中的模型存在如下等问题：只使用了全局变量，迁移关系不完整，模型粒度不够细化以及模型耦合关系复杂，现介绍另外一种改进方案。

2.2.1 管道模型

在Linux中，管道的实现并没有使用专门的数据结构，而是借助了文件系统的file结构和虚拟文件系统的索引节点inode。在此不展开探讨，仅仅对其抽象状态进行讨论。管道通过系统调用pipe（）创建后，可进行读写操作，此时通过同步管道内容管道进行进程间通信。在此期间，管道状态可能是写状态或者是读状态，而且在读写端都未正式结束前，管道的状态可能在两个状态间相互转化。当读者或者写者结束时，管道进入预关闭状态，直到没有读者和写者，管道正式关闭。期间，若读者提前退出，写者还未完成，则管道破裂。如果缺少了管道读写状态这一相互转化的重要过程，也就是说，管道创建以后只能进行单一的读或者写，这与实际情况是不符合的。

同时，尽管单独把管道抽象成为一个实体，但其状态变迁主要是依据读写端的状态变化完成，而不是管道主动变迁的结果，因此读写端的操作指令应当存在读写端所代表实体中，而不是作为管道状态的触发条件。这样的设计使实体间交互关系更加清楚，耦合性降低，同时也更符合设计逻辑。具体的过程见图3所示。

图3 管道模型

2.2.2 管道读端

如果某个进程要读取管道中的数据，那么该进程应当及时关闭fd[1]，以避免意外错误的发生。读端进程通过调用read（）系统调用读取管道内容，读端实体进入READ状态，此时分两种情况，阻塞方式（NOBLOCK==0）和非阻塞方式读取（NOBLOCK==1）。

阻塞方式下：

1）如果管道中有数据（len>0）并且请求数据rdata不为0时，read操作时返回能够读取到的字节数。请求数据大于管道容量的，则返回管道中现有所有数据len；若请求字节数不大于管道容量，则返回现有所有数据或者请求的字节数；

2）如果管道中数据为0并且请求数据不为0时，若写端文件描述符未关闭则进入等待状态WAIT；

3）若管道中数据为0，写端文件描述符关闭，则返回0，进入结束状态FINISH；

4）阻塞等待的读端进程在管道有数据写入时再次进入读取状态READ；

5）当请求数据读取完成后，进入完成FINISH状态。

非阻塞方式下：

1）如果管道中有数据并且请求数据不为0时，read操作时返回能够读取到的字节数；

2）若管道中数据为0，若管道写端被关闭，则返回0；若写端未关闭则返回-1；进入FINISH状态。

读取结束，文件描述符关闭后，读者计数器置0。具体的变迁过程如图4所示。

图4 管道读端模型

2.2.3 管道写端

因为缓冲区大小固定，管道写端的情况相对更加复杂。写进程写入数据前需要关闭读端，即close（fields[0]）。当写进程向管道中写入时，它利用标准的库函数write（），系统根据库函数传递的文件描述符，可找到该文件的file结构。file结构中指定了用来进行写操作的函数（即写入函数）地址，同时需要满足管道没有被读进程占用。写进程进入数据写入状态时，同样分为阻塞和非阻塞两种情况。

阻塞情况下：

1）只有缓冲区未满的情况下，才能写入数据。当写入数据wdata小于管道总长度buf时，保证写入的原子性atomic，如果此时当前可容纳长度小于写入数据时，写进程进入阻塞状态WAIT，直到可以一次性写入；而当写入数据大于管道总长度时，不再保证写入过程的原子性，只要管道未满，就写入数据，否则进入阻塞状态WAIT直到数据写完；

2）当数据写入完毕，进入FINISH状态；

非阻塞情况下：

1）同样也只有在管道未满状态下写入数据。当写入数据wdata小于管道总长度buf时，保证写入原子性，如果当前可容纳长度大于写入长度，则一次性写入，否则直接返回；

2）当写入数据wdata大于管道总长度buf时，若管道未满，则写入可容纳数据；若管道已满则返回错误；

在写入过程中，如果读端完毕，关闭了文件描述符，则管道宣布破裂，产生信号SIGPIPE，返回-1。具体如图5所示。

图5 管道写端模型

2.2.4 模型的Promela描述

3个实体分别为进程

各进程初始状态分别为

对用到的状态作枚举说明

mtype={UNCREATED， CREATED， IsREAD，WRITTEN，ReadyCLOSE，BROKEN，CLOSE，UNWRITE，UNREAD，READ，WRITE，WAIT，FINISH}。

限于篇幅，同样以管道部分Promela代码为例，如图6。新的建模方法中，管道部分加入了WRITTEN和READ状态的相互转化，同时剥离了管道和读写端的操作联系，状态迁移仅由读写端状态和文件描述符状态（读写端计数）给出，如下：

同时由于管道状态与读写端进程是同步关系，定义消息通道

mtype为枚举类型，代表读写端状态；byte代表读写端计数，即文件描述符。这样的做法使管道状态与读写端进程更能保持同步变化，比单纯用全局变量更加精确，全局变量在SPIN中并不能保证同步。

对读写端，为了减少状态数，read和write操作返回值不同的情况将由打印信息printf（）给出，但都归为FINISH状态。提高了程序可读性，减少了模型检测过程中系统的存储状态数，从而模型的复杂程度也得到简化。

增加和细化的迁移条件，使新模型更加完善；对原建模方法当中的错误迁移条件进行了勘误，如读写端进程是先结束，再关闭文件描述符，计数减少。

图6 管道Promela部分代码

3 实验结果分析及改进

实验中，属性用LTL表达式进行描述，作为SPIN的输入。

1）首先，是其有界性。即管道数据长度len，不能超过管道总长度buf，否则将会导致缓冲区溢出。用 ltl公式描述为 ltl p1{[]（len ＜ =buf）}，[]表示always。检测结果表明性质满足。

图7 ltl属性验证

2）其次，验证读写端不能同时占用管道，即读端状态为READ，写端状态为WRITE。用ltl公式描述 为 ltl p2{[]!（Reader_State==READ&&Writer_State==WRITE）}。

检验的结果表明，系统不满足性质，经过反例查验，Reader_State==READ和Writer_State==WRITE可以同时成立，这与实际情况并不相符。原因在于同步机制，内核会利用一定的机制同步对管道的访问，为此，内核使用了锁、等待队列和信号。而本方法在管道到读写进程状态只是使用了全局变量，致使读写端进程状态没有得到更新，为了更好的模拟实际情况，给出改进措施：

a.增加同步通道

这样管道状态变化可以及时与读写进程通信，通知读写进程。实际上，管道状态和读写进程状态是互相制约，同步转换的。

b.为读写端实体各增加一个PAUSE状态，与WAIT状态区分，以读端为例

图8 改进读端模型

3）最后，通过更改初始参数，模拟不同的情况，验证可终止性，得到系统不同的结束状态。也可用ltl 公 式 {＜ >（Reader_State == FINISH &&Writer_State==FINISH&&Pipe_State==CLOSE）}来检验。当违反属性时，SPIN生成反例trail文件，可以沿错误路径再次进行模拟，得到反例情况。

SPIN模拟输出的结果格式如图9所示，具体所有结果列于表1。

图9 SPIN模拟输出结果

表1 各实体终止状态

第一种情况代表管道读写端正确读取（或读取实际可读数据）和写入数据后关闭；

第二种情况代表写端写入数据时，读端关闭，管道宣布破裂；

第三种情况表明管道以非阻塞形式打开，但管道为空，读者返回-1；

第四种情况表明管道以非阻塞形式打开，写入数据大于缓冲区总长度且管道已满或者写入数据小于缓冲区长度但管道不足以容纳；

第五种情况表明管道以阻塞形式打开，写端写入完成，但读端进入了等待读取数据的情况。实际上读取进程也可能工作得比写进程快，当写进程还未关闭前，读进程读空管道数据进入了等待状态，只有等待新的数据被写入。这种情况对应于实际编程中打开了文件描述符，而操作结束后，忘记close的情况，应当引起注意。

4 结 论

本文基于实际工作中的测试需要，对操作系统验证方法进行了调研。简要介绍了形式化方法中的模型检测，并对模型检测工具SPIN及其编程语言Promela进行了详细描述。基于SPIN，对Linux进程间通信手段之一的管道进行了建模分析，对前人有关研究工作进行了改进、细化和补充完善。希望能够抛砖引玉，对操作系统验证工作有所帮助和启发。