model - PROMELA：这会是死锁的例子吗？

恕我直言，不。

当且仅当系统中同时满足以下所有条件时，才会出现资源死锁情况：

互斥：至少一个资源必须以不可共享的方式持有。否则，不会阻止进程在必要时使用资源。在任何给定时刻，只有一个进程可以使用该资源。

持有并等待或资源持有：一个进程当前持有至少一个资源并请求其他进程持有的额外资源。

无抢占：资源只能由持有它的进程自愿释放。

循环等待：每个进程必须等待一个被另一个进程占用的资源，而另一个进程又在等待第一个进程释放该资源。一般来说，有一组等待进程，P = {P1, P2, ..., PN}，这样 P1 正在等待 P2 持有的资源，P2 正在等待 P3 持有的资源，依此类推，直到 PN等待 P1 持有的资源。

这四个条件在 1971 年Edward G. Coffman, Jr. 的文章中首次描述时被称为科夫曼条件。

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

下面是一个简单的僵局示例，取自今年早些时候在特伦托大学举办的“Spin: Introduction”讲座。

文件： 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

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

model - PROMELA：这会是死锁的例子吗？

问题描述

解决方案

推荐阅读