spin - 如何在 promela/SP 中建模此代码？

Question

下面的算法试图在两个进程 P1 和 P2 之间强制互斥，每个进程都运行下面的代码。您可以假设最初 sema = 0。

while true do{
atomic{if sema = 0
then sema:= 1
else
 go to line 2}
critical section;
sema:= 0;
  }

如何在 promela/SPIN 中建模此代码？

谢谢你。

Answer 1

这应该很简单：

active proctype P() {
  bit sema = 0;

  do
    :: atomic {
         sema == 0 -> sema = 1
       }

       // critical section

       sema = 0
  od
}

可能你不需要do循环，如果在你的代码中你只需要它来进行一些主动等待。原子块只有在设置为 0 时才可执行sema，然后立即执行。Spin 有一个内置的被动等待语义。