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

Question

这是一个死锁的例子吗？

active proctype test(){

     bool one;
     byte x;

     one;
     x = x+11;
}

Answer 1

恕我直言，没有。

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

A deadlock situation on a resource can arise if and only if all of the following conditions hold simultaneously in a system:

Mutual exclusion: At least one resource must be held in a non-shareable mode. Otherwise, the processes would not be prevented from using the resource when necessary. Only one process can use the resource at any given instant of time.

Hold and wait or resource holding: a process is currently holding at least one resource and requesting additional resources which are being held by other processes.

No preemption: a resource can be released only voluntarily by the process holding it.

Circular wait: each process must be waiting for a resource which is being held by another process, which in turn is waiting for the first process to release the resource. In general, there is a set of waiting processes, P = {P1, P2, …, PN}, such that P1 is waiting for a resource held by P2, P2 is waiting for a resource held by P3 and so on until PN is waiting for a resource held by P1.

These four conditions are known as the Coffman conditions from their first description in a 1971 article by Edward G. Coffman, Jr.

您的模型包含一个永远挂起的进程，但是 没有共享资源，没有其他proces持有它，没有循环等待，等等。换句话说，它只是一个进程，无限长的时间内没有什么可执行的，因为默认情况下，one 被分配 false，并且计算为 false 的表达式始终在 Promela.

中阻塞

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

文件: 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"contemporarily"执行指令x = 1和[=时，该模型发生死锁19=].

下面的验证搜索证明了这一点，它表明存在 无效的结束状态 ，它对应于满足所有 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

您的模型也会产生 "invalid end state"。但是，这并不意味着它一定是死锁，它仅意味着执行跟踪在进程到达其代码块末尾之前终止。根据所建模的系统，这并不总是一个实际问题。

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

PROMELA: Would this be an example of a deadlock?

deadlock

model-checking

model

spin

promela