5

我正在尝试重现 Dijkstra 在题为“协作顺序进程”的论文中编写的 ALGOL 60 代码，该代码是解决互斥锁问题的第一次尝试，语法如下：

begin integer turn; turn:= 1;
      parbegin
      process 1: begin Ll: if turn = 2 then goto Ll;
                           critical section 1;
                           turn:= 2;
                           remainder of cycle 1; goto L1
                 end;
      process 2: begin L2: if turn = 1 then goto L2;
                           critical section 2;
                           turn:= 1;
                           remainder of cycle 2; goto L2
                  end
      parend
end

所以我试图在 Promela 中重现上面的代码，这是我的代码：

#define true    1
#define Aturn true
#define Bturn false

bool turn, status;

active proctype A()
{   
    L1: (turn == 1); 
    status = Aturn;
    goto L1;
    /* critical section */
    turn = 1;

}

active proctype B()
{   
    L2: (turn == 2); 
    status = Bturn;
    goto L2;
    /* critical section */
    turn = 2;
}

never{ /* ![]p */ 
    if
    :: (!status) -> skip
    fi;
}

init
{   turn = 1;
    run A(); run B();
}

我要做的是，验证公平属性永远不会成立，因为标签 L1 无限运行。

这里的问题是我的 never claim 块没有产生任何错误，我得到的输出只是说我的语句从未到达..

这是 iSpin 的实际输出

spin -a  dekker.pml
gcc -DMEMLIM=1024 -O2 -DXUSAFE -DSAFETY -DNOCLAIM -w -o pan pan.c
./pan -m10000 
Pid: 46025

(Spin Version 6.2.3 -- 24 October 2012)
    + Partial Order Reduction

Full statespace search for:
    never claim             - (not selected)
    assertion violations    +
    cycle checks        - (disabled by -DSAFETY)
    invalid end states  +

State-vector 44 byte, depth reached 8, errors: 0
       11 states, stored
        9 states, matched
       20 transitions (= stored+matched)
        0 atomic steps
hash conflicts:         0 (resolved)

Stats on memory usage (in Megabytes):
    0.001   equivalent memory usage for states (stored*(State-vector + overhead))
    0.291   actual memory usage for states
  128.000   memory used for hash table (-w24)
    0.534   memory used for DFS stack (-m10000)
  128.730   total actual memory usage


unreached in proctype A
    dekker.pml:13, state 4, "turn = 1"
    dekker.pml:15, state 5, "-end-"
    (2 of 5 states)
unreached in proctype B
    dekker.pml:20, state 2, "status = 0"
    dekker.pml:23, state 4, "turn = 2"
    dekker.pml:24, state 5, "-end-"
    (3 of 5 states)
unreached in claim never_0
    dekker.pml:30, state 5, "-end-"
    (1 of 5 states)
unreached in init
    (0 of 4 states)

pan: elapsed time 0 seconds
No errors found -- did you verify all claims?

我已经阅读了有关never{..}块旋转的所有文档，但找不到我的答案（这里是链接），我也尝试过使用ltl{..}块（链接）但这只是给了我语法错误，即使它明确在文档中提到它可以在initand之外proctypes，有人可以帮我更正这段代码吗？

谢谢

4

1 回答 1

1

您重新定义了“真实”，这不可能是好的。我取消了重新定义，并且从未声明失败。但是，失败对您的目标无关紧要——“状态”的初始状态是“错误”，因此永不声明退出，这是一个失败。

此外，将 1 或 0 分配给 bool 是一种稍微不好的形式；改为分配 true 或 false - 或使用位。为什么不更密切地遵循 Dijkstra 代码 - 使用“int”或“byte”。在这个问题中，性能并不是一个问题。

如果您要调用“运行”，则不需要“活动” - 只需一个或另一个。

我对“流程 1”的翻译是：

proctype A ()
{
L1: turn !=2 ->
  /* critical section */
  status = Aturn;
  turn = 2
  /* remainder of cycle 1 */
  goto L1;
}

但我可能是错的。

于 2013-03-06T00:38:01.740 回答