代码之家 › 专栏 › 技术社区 › Carol

Promela中N个进程之间的锁定

spin promela model-checking verification

2

Carol · 技术社区 · 7 年前

我试图在promela中为我的一个项目建模,以进行模型检查。其中,网络中没有N个节点。因此,对于每个节点,我都在做一个过程。类似这样:

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

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

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

这里recv_A,send_B和do_C是在网络中的每个节点上并行运行的三个线程。现在,问题是,如果我使用原子在recv\u A,send\u B,do\u C中设置锁,那么它将在所有3*N进程上设置锁,而我想要一个锁,这样锁将应用于三个组。也就是说,如果process1的(从中运行recv\u A的主节点进程)recv\u A在其CS中,则只应禁止process1的send\u B和do\u C进入CS,而不应禁止process2的recv\u A、send\u B和do\u C。有方法做到这一点吗?

1 回复 | 直到 7 年前

1

0

Patrick Trentin 7 年前

你有几个选择,都围绕着实现某种 :

实现 黑色(&A);白色烘焙算法 可用 here . 然而,请注意,这些算法 -也许除了彼得森的一个- 往往比较复杂,可能会使系统的验证不切实际。

有点简单 方法是在 测试(&A);集合算法 然而,它仍然使用 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))
        };

在代码中,应该使用不同的 lock 每组的变量 3 临界截面 不会导致属于同一线程组的其他进程等待。

另一个想法 渠道为了实现互斥:让每组线程共享一个公共线程异步最初包含一个的通道 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 .

最后,请注意,您可能需要添加 相互排斥 , 进步和 锁定自由 LTL 属性,以确保其行为正确。这些属性的定义示例可用 here 并提供了一个代码示例 here .