FSP语言学习（六）：Monitors 和条件 Synchronization

目录

1. 引言

2. Condition Synchronization

2.1 Car Park Model

2.2 Car Park Program

2.3 Condition Synchronization in Java

3. Semaphores

3.1 Modeling Semaphores

3.2 Semaphores in Java

4. 有界缓存

4.1 Bounded Buffer Model

4.2 Bounded Buffer Program

4.3 嵌套监控器问题

4.4 Monitor Invariants

---

1. 引言

监视器是用于并发编程的语言特性。监视器封装了数据，这些数据只能被监视器的访问程序观察和修改。一次只能有一个访问程序被激活。因此，一个访问程序对封装在监视器中的数据变量有互斥的访问权。监视器听起来应该很熟悉，因为我们已经在之前的学习中看到了监视器的概念，尽管使用了不同的术语解释。一个对象满足了监视器的数据访问要求，因为它封装了数据，如果声明为私有，则只能由对象的方法访问。这些方法可以被同步以提供互斥的访问。因此，监视器在Java中被简单地表示为一个拥有同步方法的类。

除了确保对其封装的数据的访问是互斥的，监控器还支持条件同步。条件同步，正如这个术语所暗示的，允许监控器阻塞线程，直到一个特定的条件成立，比如一个计数变成非零，一个缓冲区变成空或者新的输入变得可用。本篇博文介绍了监视器中的条件同步是如何建模的，以及如何在Java中实现的。

2. Condition Synchronization

我们用一个简单的例子来说明条件同步的问题。一个停车场需要一个控制器，它只允许汽车在停车场未满时进入，并且为了保持一致性，不允许汽车在停车场内没有汽车时离开。下图是我们对停车场进行Java模拟的一个快照。

它描述了停车场已满的情况，障碍物被放下，不再允许其他车辆进入。汽车的到达和离开是由不同的线程模拟的。在图中，出发的线程已经停止，以允许停车场满员。因此，到达线程被阻止，无法继续前进。

2.1 Car Park Model

对一个系统进行建模的第一步是决定哪些事件或动作是值得关注的。在停车场系统中，我们可以抽象出一些细节，如显示面板的旋转和显示线程的启动和停止。因此，我们省略了建模中与运行、旋转、暂停和终止线程有关的动作。相反，我们只关注两个动作：汽车到达停车场和汽车离开停车场。这些动作分别被命名为arrive和depart。

下一步是确定进程。这些进程是到达进程、离开进程和控制进入停车场的进程。

到达进程和离开进程都是微不足道的。它们分别试图产生一连串的到达行动和一连串的离开行动。

停车场控制必须只允许在停车场有空间时发生到达行动，在停车场有车时发生离开行动。这表达了其他进程在与停车场交互时必须满足的同步条件。

下图给出了停车场模型。CARPARKCONTROL进程使用索引状态SPACES来记录停车场的可用车位数量。上面描述的控制要求已经用FSP的保护动作结构进行了建模。因此，在状态SPACES[0]中，不接受到达动作，在状态SPACES[N]中，不接受离开动作。

在下图中，停车场系统的行为被描述为一个LTS。这个LTS是由上图的模型直接生成的。它清楚地表明，在必须发生离开动作之前，最多可以接受四个到达动作。

2.2 Car Park Program

我们的并发系统模型将系统中的所有实体表示为进程。

在把一个模型的行为实现为Java程序时，我们必须决定哪些实体是主动的，哪些是被动的。

所谓主动，我们指的是发起行动的实体；这被实现为一个线程。

所谓被动，我们指的是对行动作出反应的实体；这被实现为一个监视器。

正如我们将在随后的例子中看到的，在模型中哪些进程在实现中成为线程，哪些成为监视器，这个决定并不总是很明确。然而，在停车场的例子中，这个决定是明确的。发起到达和离开动作的进程ARRIVALS和DEPARTURES应该作为线程来实现。响应到达和离开动作的CARPARKCONTROL进程应该是一个监视器。下图描述了停车场程序的类结构。

为了简化类图，我们省略了由ThreadPanel管理的DisplayThread和GraphicCanvas线程。与程序的并发执行有关的类是两个Runnable类：Arrivals和Departures，以及控制到达和离开的CarPark Control 类。这些类的实例是由CarPark小程序start()方法创建的。

public void start() {CarParkControl c =new DisplayCarPark(carDisplay,Places);arrivals.start(new Arrivals(c));departures.start(new Departures(c));
}

Arrivals和Departures是ThreadPanel类的实例，carDisplay是CarParkCanvas的实例，如类图所示。

到达和离开类的代码列在下面的程序中。这些类使用ThreadPanel.rotate()方法，该方法将旋转显示段移动的度数作为其参数。如果停车场已满，CarParkControl类必须阻止到达线程对arrive()的激活，如果停车场已空，则阻止离开线程对depart()的激活。我们如何在Java中实现这一点？

class Arrivals implements Runnable {CarParkControl carpark;Arrivals(CarParkControl c) {carpark = c;}
public void run() {try {while(true) {ThreadPanel.rotate(330);carpark.arrive();ThreadPanel.rotate(30);}} catch (InterruptedException e){}}
}class Departures implements Runnable {CarParkControl carpark;Departures(CarParkControl c) {carpark = c;}public void run() {try {while(true) {ThreadPanel.rotate(180);carpark.depart();ThreadPanel.rotate(180);}} catch (InterruptedException e){}}
}

2.3 Condition Synchronization in Java

Java为每个监视器提供了一个线程等待集；实际上是每个对象，因为任何对象都可能有一个与之相关的监视器同步锁。以下方法是由Object类提供的，所有其他的类都是从Object类派生出来的。

public final void notify()

唤醒一个正在等待这个对象的等待集的单线程。

public final void notifyAll()

唤醒所有在此对象的等待集上等待的线程。

public final void wait() throws InterruptedException

等待另一个线程的通知。等待的线程会释放与监视器相关的同步锁。当被通知时，该线程必须等待重新获得监视器，然后再继续执行。

如果被当前不 "拥有 "监视器的线程（即之前没有通过执行同步方法或语句获得同步锁的线程）调用，则操作失败。我们指的是，当一个线程获得与监视器相关的互斥锁时，它就进入了监视器，当它释放锁时，就退出了监视器。从上面的定义可以看出，调用wait()的线程会退出监视器。这允许其他线程进入监视器，当满足适当的条件时，可以调用notify()或notifyAll()来唤醒等待的线程。下图中描述了wait()和notify()的操作。

使用FSP对一些条件条件和行动行为的受保护行动进行建模的基本格式如下所示：

FSP: when cond act -> NEWSTAT

使用Java实现条件cond和动作act的防护动作的相应格式如下：

Java: public synchronized void act() throws InterruptedException{while (!cond) wait();// modify monitor datanotifyAll()}

while循环是必要的，它可以确保当一个线程重新进入监视器时，cond确实被满足了。尽管调用wait()的线程可能已经被通知满足了cond，从而将其从监视器的等待集合中释放出来，但cond可能被另一个运行在等待线程被唤醒和重新进入监视器（通过获取锁）之间的线程所废止。

如果一个动作修改了监控器的数据，它可以调用notifyAll()来唤醒所有其他可能正在等待与该数据有关的特定条件的线程。如果不能确定只有一个线程需要被唤醒，那么调用notifyAll()比notify()更安全，以确保线程不会被不必要地等待。

回到停车场的例子，下面的程序中给出了CarParkControl监视器的实现。由于ARRIVALS线程被封锁等待空间，或者DEPARTURES线程被封锁等待汽车，而且这些条件是排他的，所以在任何时候只有一个线程可以在监视器队列中等待。因此，我们可以使用notify()而不是notifyAll()。请注意，我们已经将空间和容量变量变成了保护变量，而不是私有变量，这样它们就可以被派生自CarParkControl的显示类访问。

class CarParkControl {protected int spaces;protected int capacity;CarParkControl(n){capacity = spaces = n;}synchronized void arrive() throws InterruptedException {while (spaces==0) wait();--spaces;notify();}synchronized void depart() throws InterruptedException{while (spaces==capacity) wait();++spaces;notify();}
}

指导将进程模型翻译成Java监视器的一般规则如下:

监视器模型中的每个受保护的动作都被实现为一个同步方法，它使用while循环和wait()来实现保护。while循环的条件是对模型防护条件的否定。

监视器状态的变化是通过notify()或notifyAll()向等待的线程发出信号。

因此，在停车场模型中：

FSP: when(i>0) arrive->SPACES[i-1]

变成

Java: while (spaces==0) wait(); --spaces;

FSP: when(i<N) depart->SPACES[i+1]

变成

Java: while (spaces==N) wait(); ++spaces;

车场监视器的状态是整数变量空格。每个方法都会修改空格，因此，在每个方法的末尾都会用notify()发出变化的信号。

3. Semaphores

由Dijkstra（1968a）引入的semaphores是最早提出的处理进程间同步问题的机制之一。一个semaphore s是一个整数变量，只能取非负值。一旦s被赋予一个初始值，对s允许的唯一操作是up(s)和down(s)，定义如下：

down(s): when s>0 do decrement s;up(s): increment s

在Dijkstra的最初提议中，向下操作被称为P（代表荷兰语中passeren的第一个字母，意思是 "通过"）。上升操作被称为V（代表荷兰语单词vrijgeven的第一个字母，意思是 "释放"）。

Semaphores在许多操作系统和实时执行器的内核中被实现。上述semaphores的定义似乎意味着某种由down(s)进行的繁忙等待，直到s变成非零。事实上，在操作系统的内核中，semaphores通常是通过一个阻塞性的等待来实现的，如下所示：

down(s): if s>0 thendecrement selseblock execution of the calling processup(s):       if processes blocked on s thenawaken one of themelseincrement s

信号灯的实现通常是以先入先出(FIFO)队列的形式来管理进程，这些进程被down阻挡在信号灯上。up操作会唤醒队列头部的进程。在推理信号程序的正确性时，不应该依赖FIFO队列。

在下文中，我们将描述如何对信号灯进行建模，以及如何使用Java监视器来实现它们。然而，应该意识到，信号灯是一种低级的机制，有时用于实现高级的监视器结构，而不是像这里介绍的那样，出于教学的原因，反之亦然。

3.1 Modeling Semaphores

我们可以在FSP中描述的并发系统的模型是有限的，以确保它们可以被分析。因此，我们只能对取值范围有限的信号灯进行建模。如果超出了这个范围，那么这将被视为模型中的一个错误，如下所述：

const Max = 3
range Int = 0..MaxSEMAPHORE(N=0) = SEMA[N],
SEMA[v:Int]    = (up->SEMA[v+1]|when(v>0) down->SEMA[v-1]),
SEMA[Max+1]    = ERROR.

下图描述了信号灯的行为，其中的ERROR状态由state(-1)表示。事实上，由于FSP编译器会自动将未定义的状态映射到ERROR状态，我们可以省略最后一行描述，并将信号灯的模型更简洁地描述为：

SEMAPHORE(N=0) = SEMA[N],
SEMA[v:Int]    = (up->SEMA[v+1]|when(v>0) down->SEMA[v-1]).

这个模型直接来自上一节中对信号的第一个定义。只有当SEMAPHORE的值v大于0时，才接受down动作。向上的动作是不受保护的。SEMAPHORE可以在0...Max范围内取值，并且有一个初始值N。如果一个up动作导致Max被超过，那么SEMAPHORE就会进入ERROR状态。当SEMAPHORE被用在一个更大的模型中时，我们必须确保这个ERROR状态不会发生。作为一个例子，我们对使用信号灯来提供相互排斥进行建模。

下图描述了一个模型，其中三个进程p[1...3]使用一个共享的semaphore mutex来确保对一些资源的互斥访问。每个进程执行mutex.down动作来获得排他性访问，mutex.up动作来释放它。对资源的访问被建模为动作critical（用于访问共享资源的代码的关键部分）。每个进程的模型如下所示：

LOOP = (mutex.down->critical->mutex.up->LOOP).

复合进程SEMADEMO结合了进程和信号，在图中以图形方式描述，其定义如下：

||SEMADEMO = (p[1..3]:LOOP||{p[1..3]}::mutex:SEMAPHORE(1)).

请注意，对于互斥来说，semaphore必须被赋予初始值为1。第一个试图执行其关键动作的进程执行mutex.down动作，使mutex的值为零。在原进程通过mutex.up释放排他性之前，没有其他进程能够执行mutex.down。这可以从下图中的SEMADEMO标记的过渡系统中清楚地看到。

从上图中也可以看出，在SEMADEMO中没有ERROR状态可以达到，因为它没有出现在LTS中。事实上，信号的值不超过1（从LTS中，我们可以看到连续两个mutex.up动作而没有中间的mutex.down的跟踪不可能发生）。对于互斥来说，使用一个取值为0或1的二进制信号就足够了。

我们可以使用分析工具来机械地检查错误。当然，在这个例子中，我们可以通过设置Max为1并搜索错误来快速检查mutex是否曾经超过1。

3.2 Semaphores in Java

触发器是被动的对象，它对上、下的动作作出反应；它们不发起动作。因此，我们在Java中把semaphore实现为一个监视器类。上升和下降的动作成为同步方法。正如我们在第2节中看到的那样，模型中对向下动作的防护是用条件同步来实现的。实现信号灯的类在下个程序中列出。

public class Semaphore {private int value;public Semaphore (int initial){value = initial;}synchronized public void up() {++value;notify();}synchronized public void down() throws InterruptedException {while (value== 0) wait();--value;}
}

尽管程序中的down()方法通过递减值来改变监视器的状态，但我们并没有使用notify()来发出状态改变的信号。这是因为线程只等待semaphore的值被递增，而不等待值被递减。信号灯的实现并不检查增量时的溢出情况。这通常是由操作系统实现的信号灯的情况。在设计过程中，程序员有责任确保溢出不会发生。我们提倡使用可分析的模型来检查这种属性。

下图描述了上一部分中建模的信号灯演示程序的显示：

在其关键部分执行的线程由浅色段表示。每个线程的显示都是逆时针旋转的。在上图中，线程1正在其关键部分执行，线程2被阻塞，等待进入其关键部分，线程3已经完成其关键部分，正在执行非关键动作。每个线程下面的滑块可以调整线程执行关键动作的时间，而不是非关键动作。

如果所有三个线程在关键部分花费的总时间少于一整轮，那么就有可能让所有三个线程同时执行。换句话说，对关键资源的访问不需要有冲突。这种情况在实际系统中经常发生。只有在对共享资源的访问发生冲突时，相互排斥的机制才会生效。因此，在实际系统中，最好让关键部分的时间尽可能短，以减少冲突的可能性。

上图的显示背后的程序使用了与之前相同的ThreadPanel类；但是，它使用了一个不同的构造函数来创建具有多色段的显示。该类提供的接口，用本章中使用的方法进行了扩展，如下面程序所示。

public class ThreadPanel extends Panel {// construct display with title and rotating arc color cpublic ThreadPanel(String title, Color c) {...}// hasSlider == true creates panel with sliderpublic ThreadPanel(String title, Color c, boolean hasSlider) {...}// rotate display of currently running thread 6 degrees// return false when in initial color// return true when in second colorpublic static boolean rotate()throws InterruptedException {...}// rotate display of currently running thread by degreespublic static void rotate(int degrees)throws InterruptedException {...}// create a new thread with target r and start it runningpublic void start(Runnable r) {...}// stop the thread using Thread.interrupt()public void stop() {...}
}

下个程序列出了MutexLoop类，它为每个线程提供了run()方法。关键的（互斥的）动作是旋转()动作，当线段变为较浅的颜色时就会执行。当旋转的弧线是深色的时候，rotate()方法返回false，当浅色的时候返回true，这就表明了这一点。

class MutexLoop implements Runnable {Semaphore mutex;MutexLoop (Semaphore sema) {mutex=sema;}public void run() {try {while(true) {while(!ThreadPanel.rotate());mutex.down(); // get mutual exclusionwhile(ThreadPanel.rotate()); //critical actionsmutex.up(); //release mutual exclusion}} catch(InterruptedException e){}}
}

线程和信号是由applet start()方法以常规方式创建的。

public void start() {Semaphore mutex = new DisplaySemaphore(semaDisplay,1);thread1.start(new MutexLoop(mutex));thread2.start(new MutexLoop(mutex));thread3.start(new MutexLoop(mutex));
}

其中thread1、thread2和thread3是ThreadPanel实例，semaDisplay是NumberCanvas的实例。

4. 有界缓存

缓冲器在并发系统中经常被用来平滑数据生产者和数据消费者之间的信息传输速率。例如，考虑一个键盘设备驱动程序，它向一个编辑程序提供在键盘上输入的字符。编辑器消耗字符的速度平均比一个人在键盘上输入的速度快得多。然而，有些字符的处理时间可能比其他的要长，例如，导致屏幕滚动的字符或调用格式化命令的键盘命令。当编辑器处理一个需要很长时间的字符时，有必要对键盘上的字符进行缓冲，否则就会丢失。这个缓冲区有时被称为 "领先键 "缓冲区。它是我们在下文中描述的那种缓冲器的一个例子。

在这一节中，我们对一个有边界的缓冲区进行建模和编程，它由固定数量的槽组成。项目由一个生产者进程放入缓冲区，由一个消费者进程移除。缓冲区的组织方式是，第一个放入的项目将是第一个取出的项目（FIFO）。

下图描述了我们的示例系统的显示情况，其中一个生产者进程通过一个五槽的缓冲区向一个消费者进程传递字符。缓冲区上方的小圆圈表示生产者进程可以放入一个字符的下一个空闲槽。缓冲区下面的圆圈表示消费者进程可以从中获取一个字符的下一个槽。读者可能会注意到这个例子和第2节中最初的停车场例子之间的相似性。事实上，同步的要求是一样的。生产者只有在有空闲的槽时才允许把一个字符放入缓冲区，而消费者进程只有在缓冲区中至少有一个字符时才能得到一个字符。这些正是对停车场的要求，如果我们用空间代替插槽，用汽车代替角色。这两个例子的不同之处在于缓冲区所执行的先进先出原则，与停车场不同的是，汽车可以占据任何空闲的空间，而且不需要按照到达顺序离开。

4.1 Bounded Buffer Model

有边界的缓冲区的生产者——消费者系统是一个处理数据项而不改变它们的程序的例子。此外，生产者、消费者和缓冲区本身的行为不受他们处理的项目的价值影响。换句话说，他们不测试这些数据项的值。这种行为被说成是与数据无关的。如果可以建立数据独立性，那么模型可以通过省略参数和数据结构的详细表示来简化。这将导致更小、更易操作的模型。下面第一张图中的get和put操作是没有参数的简单动作。下面第二张图中描述的有界缓冲区系统的LTS应该与停车场LTS进行比较，以看到这两个系统的同步行为的相似性。

4.2 Bounded Buffer Program

模型中的BUFFER在Java实现中成为一个监视器，具有同步的put和get方法（下面的程序）。我们将缓冲器的接口与它的实现分开，因为我们将在下一部分提供一个替代的实现。

public interface Buffer<E> {public void put(E o)throws InterruptedException; //put object into bufferpublic E get()throws InterruptedException; //get object from buffer
}public class BufferImpl<E> implements Buffer<E> {protected E[] buf;protected int in = 0;protected int out= 0;protected int count= 0;protected int size;public BufferImpl(int size) {this.size = size;buf = (E[])new Object[size];}public synchronized void put(E o) throws InterruptedException {while (count==size) wait();buf[in] = o;++count;in=(in+1) % size;notifyAll();}public synchronized E get() throws InterruptedException {while (count==0) wait();E o = buf[out];buf[out]=null;--count;out=(out+1) % size;notifyAll();return (o);}
}

缓冲区已经被实现为一个通用的类，可以缓冲任何类型的Java对象。缓冲区的数据结构是一个固定大小的数组buf，索引是in，指向下一个空闲槽，out指向下一个要清空的槽。这些索引是根据缓冲区的大小递增的。生产者和消费者程序的代码列在下面程序中。

class Producer implements Runnable {Buffer<Character> buf;String alphabet= "abcdefghijklmnopqrstuvwxyz";Producer(Buffer<Character> b) {buf = b;}public void run() {try {int ai = 0;while(true) {ThreadPanel.rotate(12);buf.put(alphabet.charAt(ai));ai=(ai+1) % alphabet.length();ThreadPanel.rotate(348);}} catch (InterruptedException e){}}
} class Consumer implements Runnable {Buffer<Character> buf;Consumer(Buffer<Character> b) {buf = b;}public void run() {try {while(true) {ThreadPanel.rotate(180);Character c = buf.get();ThreadPanel.rotate(180);}} catch(InterruptedException e ){}}
}

4.3 嵌套监控器问题

假设我们不希望在缓冲区监视器类的实现中直接使用条件同步，而是决定使用两个信号灯full和empty来反映缓冲区的状态。空信号计算空间的数量，并在put操作中被递减。当然，如果empty的值为0，那么put操作就会被阻止。同样地，full计算缓冲区中的项目数量，并在get操作中被递减。因此，如果full的值为0，那么get就会被阻塞。修改后的缓冲区类显示在下面程序中。

class SemaBuffer<E> implements Buffer<E> {protected E[] buf;protected int in = 0;protected int out= 0;protected int count= 0;protected int size;Semaphore full; //counts number of itemsSemaphore empty; //counts number of spacesSemaBuffer(int size) {this.size = size; buf = (E[])new Object[size];full = new Semaphore(0);empty= new Semaphore(size);}synchronized public void put(E o)throws InterruptedException {empty.down();buf[in] = o;++count;in=(in+1) % size;full.up();}synchronized public E get()throws InterruptedException{full.down();E o =buf[out];buf[out]=null;--count;out=(out+1) % size;empty.up();return (o);}
}

这个程序的semaphores取代了原始实现中的count变量，以及对count值的条件性等待和对其值变化的通知。下面是反映缓冲区实现变化的最新模型：

const Max = 5
range Int = 0..MaxSEMAPHORE(I=0) = SEMA[I],
SEMA[v:Int]    = (up->SEMA[v+1]|when(v>0) down->SEMA[v-1]).BUFFER = (put -> empty.down ->full.up ->BUFFER|get -> full.down ->empty.up ->BUFFER).PRODUCER = (put -> PRODUCER).
CONSUMER = (get -> CONSUMER).||BOUNDEDBUFFER = (PRODUCER|| BUFFER || CONSUMER||empty:SEMAPHORE(5)||full:SEMAPHORE(0))@{put,get}.

当我们用分析工具LTSA检查这个模型时，发现它报告了一个潜在的死锁，同时还有一个通往该死锁的行动轨迹，这时问题就出现了。

Composingpotential DEADLOCK
States Composed: 28 Transitions: 32 in 60ms
Trace to DEADLOCK:get

我们将在下一篇博客更详细地讨论死锁。然而，从本质上讲，它意味着一个系统无法取得进一步的进展，因为它没有可以采取的进一步行动。模型中的死锁可以在程序的演示版本中看到，启动消费者并让它阻塞，等待从空的缓冲区获得一个字符。当生产者被启动时，它不能将一个字符放入缓冲区。为什么呢？原因是使用了两层同步锁：第一层是对缓冲区监视器的互斥访问，第二层是对信号灯的互斥访问。

当消费者调用get时，它获得了Buffer监视器锁，然后通过调用full.down()检查缓冲区中是否有东西，从而获得了full信号的监视器锁。由于最初缓冲区是空的，对full.down()的调用会阻塞消费者线程（使用wait()），并释放full信号的监视器锁。然而，它并没有释放Buffer的监视器锁。因此，生产者不能进入监视器将一个字符放入缓冲区，所以生产者和消费者都不能取得任何进展——因此出现了死锁。上面描述的情况被称为嵌套的监视器问题。在Java中避免这种情况的唯一方法是通过精心设计。在我们的例子中，可以通过确保缓冲区的监视器锁在semaphores被减去后才被获取来消除死锁。

class FixedSemaBuffer<E> implements Buffer<E> {protected E[] buf;protected int in = 0;protected int out= 0;protected int count= 0; //only used for display purposesprotected int size;Semaphore full;  //counts number of itemsSemaphore empty; //counts number of spacesFixedSemaBuffer(int size) {this.size = size; buf = (E[])new Object[size];full = new Semaphore(0);empty= new Semaphore(size);}public void put(E o)throws InterruptedException {empty.down();synchronized(this){buf[in] = o; ++count; in=(in+1)%size;}full.up();}public E get()throws InterruptedException{full.down(); E o;synchronized(this){o =buf[out]; buf[out]=null;--count; out=(out+1)%size;}empty.up();return (o);}
}

考虑到缓冲区的变化，需要对模型的那些部分进行修改，如下所示：

BUFFER = (put -> BUFFER|get -> BUFFER).PRODUCER = (empty.down->put ->full.up ->PRODUCER).
CONSUMER = (full.down ->get ->empty.up->CONSUMER).

将信号灯动作从缓冲区进程移到生产者和消费者进程中，反映了实现中的变化，即信号灯动作是在监视器之外执行的（即在获得监视器锁之前）。如果这个修改后的模型被组成并最小化，它产生的LTS与原始模型完全相同。这让我们相信，我们修改后的有界缓冲区的信号实现与直接使用wait()和notify()的原始模型是等价的。

4.4 Monitor Invariants

监视器的不变性是一个关于它所封装的变量的断言。只要监视器内没有线程执行，这个断言就必须成立。因此，在线程释放监视器锁的任何时候，该不变式都必须为真——当线程从同步方法调用中返回时，以及当线程被wait()阻塞时。监视器正确性的正式证明可以通过证明监视器的构造函数建立了不变性，并且在每个访问方法的执行之后和wait()执行之前，不变性都成立。这样的方法需要一个编程逻辑，一个正式的逻辑系统，便于对程序执行做出精确的陈述。Greg Andrews（1991）在他的书中使用了这种方法。同样地，Fred Schneider（1997）在他的书中讨论了关于并发程序的形式化推导和推理。

我们选择了使用一种可用于机械证明的基于模型的方法。其缺点是，我们的机械证明只适用于特定的情况或模型，而Andrews使用的手工证明理论方法允许对一般情况进行正确性证明。例如，一个证明方法可以为一个有界缓冲区的所有尺寸建立监控的正确性，而不仅仅是一个特定的尺寸。然而，通常的情况是，如果一个特定情况的模型被证明是正确的，那么一般情况就可以通过归纳推断出来。

虽然我们没有在正式的正确性证明中使用不变式，但它们是有用的程序文件，有助于非正式的正确性推理。本篇开发的监控程序的不变式是：。

CarParkControl Invariant: 0 ≤ spaces ≤ N

停车场控制器的不变量简单地说，可用车位的数量必须总是大于或等于零，并且小于或等于停车场的最大规模（N）。

Semaphore Invariant: 0 ≤ value

semaphore不变性简单地断言，semaphore的值必须总是一个非负的值。

Buffer Invariant: 0 ≤ count ≤ sizeand 0 ≤ in < sizeand 0 ≤ out < sizeand in = (out + count) modulo size

有界缓冲区不变性断言，缓冲区内的项目数必须在零到大小的范围内，并且输入和输出的索引必须在零到大小1的范围内。它指出，输入索引必须总是 "领先 "于输出索引的计数项，其中领先意味着对大小进行加法。

不变量也被用来推理面向对象顺序程序中类的正确性。不变量被要求在每个方法执行后保持不变。并发程序的不同之处在于，在对象的监控锁被释放的任何时候，都有额外的责任来确定不变式的存在。这些额外的点是可以执行wait()的地方。