互斥协议的安全性分析

0 引言

进程之间的间接制约在操作系统中通常叫互斥，互斥是系统设计的关键问题之一[2]，它保证了相互冲突的并发进程可以共享资源。本文介绍了安全性与活性的形式化定义，并针对其对状态序列没有做具体约束的不足，在行为时序逻辑中对其进行了重定义。然后，根据安全性和活性的形式化定义，对互斥协议的安全性进行了形式化的分析，证明了互斥协议是安全性而不是活性。

1 安全性与活性介绍

1977 年，美国科学家 Leslie Lamport 在验证多线程程序正确性的过程中，最早提出了将系统的性质分为安全性和活性两类，并给出了它们的非形式化定义：安全性：规定一些行为不会在系统中发生。活性：规定一些行为必须在系统中发生。

2 安全性与活性的形式化定义

在 1984 年，Lesile Lamport 第一次对安全性进行了形式化的定义，随后 Bowen Alpern 和 Fred B. Schneider 又进一步给出了活性的形式化定义。Lesile Lamport 是行为时序逻辑(temporallogic of action)[3]的创立者，而安全性和活性的定义主要也是由他提出或启发的，其中的很多概念都被他加入到了后来的行为时序逻辑当中。这使得安全性和活性能够方便地使用行为时序逻辑进行定义。因此下面首先介绍安全性和活性的原始定义，然后再以行为时序逻辑对它们进行更精确的定义。

3 互斥协议的安全性

现代计算机系统的中心方案包括多道程序设计、多处理和分布式处理，这些方案的基础以及操作系统设计的基础是并发，并发进程可以按照多种方式进行交。系统中的众多交互进程可能需要竞争使用资源，如对 I/O 设备的访问、主存中的一块空间或者一个文件等。此类交互中产生的重要问题就是互斥。互斥的定义通常为[10]：一组并发进程中的一个或多个程序段，因共享某一公有资源而导致它们必须以一个不允许交叉执行的单位执行。也就是说，不允许两个以上的共享该资源的并发进程同时进入临界区。互斥技术不但可以用于解决诸如共享资源竞争等冲突，还可以用于进程间同步，使它们可以协调合作[11]，例如著名生产者/消费者问题：一个进程向缓冲中写入/添加数据，另外一个或若干个进从缓冲中读取数据。

4 结束语

安全性和活性是两类最基本的属性，它们所确保的系统性质是完全不同的。由于对于安全性和活性的验证使用的是不同的技术，因此区分一个属性是安全性还是活性是十分必要的。研究属性的分类、定义和分析技术，对于系统的形式化分析具有重要的意义。后续的研究可以在本文工作的基础上，对于一些典型的系统属性进行分析，同时也可以探索安全性和活性在实际系统验证中的应用新途径。