Promela中N个进程之间的锁定答案

【问题标题】：Lock between N Processes in PromelaPromela中N个进程之间的锁定
【发布时间】：2017-11-02 18:24:35
【问题描述】：

我正在尝试在 promela 中为我的一个项目建模以进行模型检查。在那，我在网络中有 N 个节点。因此，对于每个节点，我都在制作一个流程。像这样的：

init {
byte proc;
atomic {
    proc = 0;
    do
    :: proc < N ->
        run node (q[proc],proc);
        proc++
    :: proc >= N ->
        break
    od
}
}

所以，基本上，这里的每个“节点”都是模拟我网络中每个节点的进程。现在，Node Process 有 3 个线程，它们在我的原始实现中并行运行，并且在这三个线程中，我在某个部分有锁定，因此三个线程不会同时访问关键部分。所以，在 promela 中，我做了这样的事情：

proctype node (chan inp;byte ppid)
{
   run recv_A()
   run send_B()
   run do_C()
}

所以这里的recv_A、send_B 和do_C 是在网络中每个节点上并行运行的三个线程。现在，问题是，如果我使用 atomic 将锁放在 recv_A、send_B、do_C 中，那么它将把锁锁在所有 3*N 进程上，而我想要一个锁，以便将锁应用于三个一组。也就是说，如果process1的（运行recv_A的主节点进程）recv_A在它的CS中，那么只有process1的send_B和do_C应该被禁止进入CS，而不是process2的recv_A、send_B、do_C。有没有办法做到这一点？

【问题讨论】：

标签： verification model-checking promela spin

【解决方案1】：

你有几个选择，都围绕着实现某种N个进程之间的互斥算法：

黑白烘焙算法的实现可通过here 获得。但是请注意，这些算法-可能除了 Peterson 的算法-往往很复杂，并且可能使您的系统验证变得不切实际。

一种比较简单的方法是使用 Test & Set Algorithm，但是在 trying 部分中仍然使用atomic .这是取自here 的示例实现。

bool lock = false;
int counter = 0;

active [3] proctype mutex()
{
  bool tmp = false;

trying:
  do
    :: atomic {
       tmp = lock;
       lock = true;
       } ->
       if
          :: tmp;
          :: else -> break;
       fi;
  od;

critical:
    printf("Process %d entered critical section.\n", _pid);
    counter++;
    assert(counter == 1);
    counter--;

exit:
    lock = false;
    printf("Process %d exited critical section.\n", _pid);

goto trying;
}

#define c0 (mutex[0]@critical)
#define c1 (mutex[1]@critical)
#define c2 (mutex[2]@critical)
#define t0 (mutex[0]@trying)
#define t1 (mutex[1]@trying)
#define t2 (mutex[2]@trying)
#define l0 (_last == 0)
#define l1 (_last == 1)
#define l2 (_last == 2)
#define f0 ([] <> l0)
#define f1 ([] <> l1)
#define f2 ([] <> l2)

ltl p1 { []   !(c0  &&  c1)  && !(c0 && c2) && !(c1 && c2)}
ltl p2 { []((t0 || t1 || t2) -> <> (c0 || c1 || c2)) }
ltl p3 {
        (f0 -> [](t0 -> <> c0))
        &&
        (f1 -> [](t1 -> <> c1))
        &&
        (f2 -> [](t2 -> <> c2))
        };

在您的代码中，您应该为每组3 相关线程使用不同的lock 变量。锁争用仍会在全局级别发生，但在临界区中工作的某些进程不会导致其他进程等待，而不是属于同一线程组的进程。

另一个想法是利用通道实现互斥：让每组线程共享一个公共的异步通道，该通道最初包含一个token 消息。每当这些线程中的一个想要访问临界区时，它都会从通道中读取。如果token 不在通道内，它会一直等待直到它变得可用。否则，它可以在临界区继续前进，并在完成后将token 放回共享通道。

proctype node (chan inp; byte ppid)
{
   chan lock = [1] of { bool };
   lock!true;

   run recv_A(lock);
   run send_B(lock);
   run do_C(lock);
};

proctype recv_A(chan lock)
{
    bool token;
    do
        :: true ->

            // non-critical section code
            // ...

            // acquire lock
            lock?token ->

            // critical section
            // ...

            // release lock
            lock!token

            // non-critical section code
            // ...
    od;
};

...

这种方法可能是最简单的开始，所以我会先选择这个。但是请注意，我不知道这会如何影响验证期间的性能，这很可能取决于Spin 在内部如何处理通道。此解决方案的完整代码示例可以在文件channel_mutex.pml 中找到here。

最后，请注意您可能希望将 mutual exclude、progress 和 lockout-freedom LTL 属性添加到您的模型中以确保其行为正确。 here 提供了这些属性定义的示例，here 提供了代码示例。

【讨论】：