PROMELA：这会是一个僵局的例子吗？

Posted 2021-05-03

这会是一个僵局的例子吗？

active proctype test(){

     bool one;
     byte x;

     one;
     x = x+11;
}

答案

不，不。

遵循维基百科所示的list of necessary conditions for a deadlock：

当且仅当以下所有条件同时存在于系统中时，才会出现资源上的死锁情况：

• Mutual exclusion:必须以非共享模式保存至少一个资源。否则，在必要时不会阻止进程使用资源。在任何给定的时刻，只有一个进程可以使用该资源。
• 保持并等待或资源保留：进程当前持有至少一个资源并请求其他进程持有的其他资源。
• 没有preemption：资源只能由持有它的进程自愿释放。
• 循环等待：每个进程必须等待另一个进程持有的资源，而该进程又等待第一个进程释放资源。通常，有一个等待进程的set，P = {P1，P2，...，PN}，这样P1正在等待P2持有的资源，P2正在等待P3持有的资源，依此类推，直到PN为止。等待P1持有的资源。

这四个条件被称为Coffman条件，这些条件来自Edward G. Coffman, Jr.在1971年的一篇文章中的第一次描述

你的模型包含一个永远挂起的进程，但是没有共享资源，没有其他进程持有它，没有循环等待等等。换句话说，它只是一个无限量执行的进程时间，因为one默认被分配false，并且评估false的表达总是在Promela中阻塞。

---

下面是一个简单的死锁示例，取自今年早些时候的"Spin: Introduction" held at University of Trento讲座。

file：mutex_simple_flaw2.pml

bit x, y;
byte cnt;


active proctype A() {
again:
  x = 1;
  y == 0; /* waits for process B to end: if y != 0, the execution of this
             statement is blocked here */
  cnt++;
  /* critical section */
  printf("Process A entered critical section.\n");
  assert(cnt == 1);
  cnt--;

  printf("Process A exited critical section.\n");
  x = 0;
  goto again
}


active proctype B() {
again:
  y = 1;
  x == 0;

  cnt++;
  /* critical section */
  printf("Process B entered critical section.\n");
  assert(cnt == 1);
  cnt--;

  printf("Process B exited critical section.\n");
  y = 0;
  goto again
}

当进程A和B“同时”执行指令x = 1和y = 1时，这个模型陷入僵局。

这通过以下验证搜索来见证，该搜索表示存在无效的结束状态，其对应于满足所有Coffman条件的执行轨迹：

~$ spin -search -bfs mutex_simple_flaw2.pml

pan:1: invalid end state (at depth 2)
pan: wrote mutex_simple_flaw2.pml.trail

(Spin Version 6.4.8 -- 2 March 2018)
Warning: Search not completed
    + Breadth-First Search
    + Partial Order Reduction

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

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

Stats on memory usage (in Megabytes):
    0.000   equivalent memory usage for states (stored*(State-vector + overhead))
    0.291   actual memory usage for states
  128.000   memory used for hash table (-w24)
  128.195   total actual memory usage



pan: elapsed time 0 seconds

由Spin发现的违规执行追踪如下：

~$ spin -t -p -g -l mutex_simple_flaw2.pml

using statement merging
  1:    proc  1 (B:1) mutex_simple_flaw2.pml:24 (state 1)   [y = 1]
        y = 1
  2:    proc  0 (A:1) mutex_simple_flaw2.pml:7 (state 1)    [x = 1]
        x = 1
  3:    proc  0 (A:1) mutex_simple_flaw2.pml:8 (state 2)    [((y==0))]
    transition failed
spin: trail ends after 3 steps
#processes: 2
        x = 1
        y = 1
        cnt = 0
  3:    proc  1 (B:1) mutex_simple_flaw2.pml:25 (state 2)
  3:    proc  0 (A:1) mutex_simple_flaw2.pml:8 (state 2)
2 processes created

---

您的模型也会导致“无效的结束状态”。但是，这并不意味着它必然是死锁，它只意味着执行跟踪在进程到达其代码块结束之前终止。根据所建模的系统，这并不总是一个实际问题。