FSP语言学习：解决同步问题—死锁、干扰

1. 学前回顾

2. 什么是死锁

2.1 The Coffman conditions

3. The bounded buffer in FSP

4. Modelling semaphores in FSP

4.1 FSP信号量模型的死锁问题

4.2 Correcting the bounded buffer behaviour

5. 案例学习

5.1 Deadlock-free philosophers

1. 学前回顾
我们在上一篇文章中学习了如何使用FSP对并行运行的processes建模。但是由于多线程或者多进程会有共享的资源空间，它们可能同时访问同一个共享资源，这就是竞态条件。当多个线程或多个进程在争抢资源的时候，它们就会互相干扰，即运行结果取决于最后一个访问资源的线程或进程。为了防止竞态条件的发生，我们会给共享资源加锁，来控制访问，但是当多个进程互相等待对方释放资源时，就会发生死锁。

我们这篇文章会学习如何使用FSP对存在同步问题的系统进行建模，以帮助我们发现系统潜在的死锁或者干扰问题。

2. 什么是死锁
我们首先需要认识什么是死锁，什么是活锁，以及死锁产生的条件。

发生死锁的情景是，多个进程相互占有对方的资源的锁，而又相互等待对方释放锁。此时若无外力干预，这些进程则一直处理阻塞的假死状态，形成死锁。

发生活锁的情景是，多个进程在拿到资源却又相互谦让，即释放资源不执行操作。这使得资源在多个进程之间轮转却得不到实际的执行，这就是活锁。

2.1 The Coffman conditions
Coffman conditions 是四个充分必要条件，当四个条件都满足时发生死锁。

Serially reusable resources: the processes involved must share some reusable resources between themselves under mutual exclusion.

Incremental acquisition: processes hold on to resources that have been allocated to them while waiting for additional resources.

No preemption: once a process has acquired a resource, it can only release it voluntarily—it cannot be forced to release it.

Wait-for cycle: a cycle exists in which each process holds a resource which its successor in the cycle is waiting for.

3. The bounded buffer in FSP

那么我们该如果解决死锁问题呢。在Java编程中，我们有有界缓冲区的概念。首先我们学习使用monitor来控制有界缓冲区，即生产者进程将项目放入缓冲区，并由消费者进程以先进先出(FIFO)的方式从缓冲区中取出。由于缓冲区由一个个固定的槽组成，只有在有空闲槽的情况下，生产者进程才可以将项目放入缓冲区；否则调用生产者将被阻塞。另一方面，只有当缓冲区中有这样的项目时，才能从缓冲区中删除该项目；否则，消费者将被阻塞。

那么我们如何使用FSP描述有界缓冲区呢，我们来看一个例子：

BUFFER(N=5) = COUNT[0],
COUNT[i:0..N]
    = ( when (i COUNT[i+1]
      | when (i>0) get -> COUNT[i-1]
      ).

PRODUCER = (put -> PRODUCER).
ConSUMER = (get -> CONSUMER).

||BOUNDEDBUFFER = (PRODUCER || BUFFER(5) || CONSUMER).

通过阅读上面的表达式，我们发现这正是描述了生产者能将项目加入缓冲区，和消费者能从缓冲区取出项目的条件。但是我们的模型忽略了很多细节，我们不考虑这些项目到底是什么，我们只描述了生产者和消费者在有界缓冲区的交互行为，这种抽象恰恰是FSP语言的优点，帮助我们将模型的重点聚焦在进程的并发上。

我们之前就说过，FSP语言是经过严格定义的，比某些编程语言还有准确。下面我们就将它的表达式与java语句进行对比。

FSP

when cond act -> NEWSTAT

Java

public synchronized void act() throws InterruptedException 
{
    while (!cond) wait();
    //modify monitor data
    notifyAll();
}

通过观察，可以看到FSP语言的监控器很好的映射了Java监控器。Java监视器中的 while (!cond) wait () 语句。被FSP语言简洁的表达了出来。

但我们需要注意，FSP的抽象级别是高于Java语言的，所以对于FSP语言，cond就是i，即缓冲区的大小，再细节的东西它就不予考虑。

而对于Java语言来说，消费者进程能get的cond是 buffer.size() == 0。

while (buffer.size() == 0) wait();

4. Modelling semaphores in FSP

另外一种控制有界缓冲区的方法是使用信号量，即我们会使用更短的 up 和 down 代替 signal 和wait。在下面的学习中，我们用信号量 empty 代表缓冲区空阻塞消费者，使用 full 代表缓冲满阻塞生产者。

那么我们如何使用FSP去描述信号量 empty 和 full 呢，我们将 empty 信号量初始化为N，代表着此时缓冲区还能被生产者放入项目N次。而 full 信号量被初始化为0，代表着调用缓冲区的进程被阻塞。

假设我们最初的缓冲区是空的。于是我们可以对put，empty 信号量从N递减，full 信号量从0递增。而对于get, full 信号量是从当前值递减的，empty 信号量是从当前值递增的。

具体的表达式为：

const N = 5
range Int = 0..N

SEMAPHORE(I=0) = SEMA[I],
SEMA[v:Int] = ( when (v 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(N)
                  ||  full:SEMAPHORE(0)
                  ).

4.1 FSP信号量模型的死锁问题
但是上面的模型是有问题的，当缓冲区为空时，启用get转换。但是get请求会随即被挂起，因为此时信号量是0无法再减少。而且，put动作被禁用了，因为已经执行了get，监视器锁定了缓冲区。

这个问题又被成为 nested monitor problem。它的发生是因为同时满足四个 coffman conditions。它发生在信号量保护的缓冲区而不是原始缓冲区的原因是，信号量解决方案引入了 Incremental acquisition（第二个 coffman condition）：进程在等待额外的资源时，会持有已分配给它们的资源。通过执行get，进程获得缓冲区的锁，然后尝试索要 full 信号量。

4.2 Correcting the bounded buffer behaviour

为了解决上面的问题，我们需要重新设计缓冲区，我们给进程缓冲区的锁是有条件的，只有当信号量被进程获取后才能给予进程缓冲区的锁：

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

上面这种设计已经可以消除死锁，但是依然存在问题，比如当缓冲区被填满一半时，一个信号量被一个进程的 get 或 set 获取，另一个进程就会因为获取不到另一边的信号量而被阻塞。比如，当进程1执行 put 获取了 full 信号量，进程2在执行 get 时就要等待 full 信号量被进程1释放。这虽然不会造成死锁，但会降低效率。所以我们需要一个更有效的设计，即将信号量的获取权给予生产者和消费者。

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

5. 案例学习

五位哲学家共用一张圆桌。每个人的一生都是在思考和吃饭之间交替度过的。桌子中央放着一大盘意大利面。哲学家吃一份意大利面需要两把叉子。不幸的是，由于学哲学的收入不如学计算机高，哲学家们只能负担得起5个分叉。每对夫妇之间放一个叉子，他们同意每对夫妇只使用他们的右边和左边的叉子。

在这个系统中，叉子就是被共享的资源。它被多个哲学家拿起放下。

FORK = (get -> put -> FORK).

哲学家每次需要两把叉子。过程是他准备吃饭，于是坐下来，拿起两个叉子，吃意大利面，放下两个叉子，最后站起来，准备重新开始思考哲学：

PHIL = (sitdown -> right.get -> left.get -> eat
        -> left.put -> right.put -> arise -> PHIL).

最后，为了把这五位哲学家和五把叉子放在一起，我们使用了以下复合进程：

||DINERS(N=5) =
    forall [i:0..N-1]
      ( phil[i]:PHIL
      || {phil[i].left,phil[((i-1)+N)%N].right}::FORK
      ).

注：((i-1)+N)%N 是渐减N的模。

但是上面这个模型是存在死锁的，这是因为哲学家坐成一个圈，每个人都想得到他右边的叉子造成的，即第四个 coffman condition —— wait-for cycle：在这个周期中，每个进程都持有一个资源，而它的后继进程正在等待这个资源。为了解决这个问题我们就要取消 wait-for cycle。

5.1 Deadlock-free philosophers

wait-for cycle 是由于所有哲学家都在同一时间需要右边的刀叉造成的，要解决这个问题，一种方法就是让他们有不同的行为。比如，让奇数的哲学家先拿起他们的右叉，偶数的哲学家先拿起他们的左叉：

PHIL(I=0)
    = ( when (I%2 == 0)
            sitdown -> left.get -> right.get
            -> eat -> left.put -> right.put
            -> arise -> PHIL
      | when (I%2 == 1)
            sitdown -> right.get -> left.get
            -> eat -> left.put -> right.put
            -> arise -> PHIL
      ).

以上就是FSP语言在解决并发进程同步问题的建模帮助。

FSP语言学习：解决同步问题—死锁、干扰

Java相关栏目本月热门文章