model - 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.

您的模型包含一个永远挂起的进程， 但是 没有共享资源，没有其他进程持有它，没有循环等待等。换句话说，它只是一个无限长的时间内没有任何东西可以执行的进程，因为 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 “同时”执行指令 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

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