PROMELA: Would this be an example of a deadlock?

Would this be an example of a deadlock?

active proctype test(){

     bool one;
     byte x;

     one;
     x = x+11;
}

IMHO, no.

Follows the list of necessary conditions for a deadlock as illustrated by Wikipedia:

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.

Your model includes a process that hangs forever, but there is no shared resource, there is no other process holding it, there is no circular wait, etc. In other words, it is just a process which has nothing to execute for an infinite amount of time, because one is assigned false by default, and an expression evaluating to false is always blocking in Promela.

---

A simple deadlock example, taken from the lecture "Spin: Introduction" held at University of Trento earlier this year, follows.

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
}

This model incurs in a deadlock when processes A and B "contemporarily" execute the instructions x = 1 and y = 1.

This is witnessed by the following verification search, which signals the existence of an invalid end state, which corresponds to an execution trace satisfying all of the Coffman conditions:

~$ 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

The offending execution trace, found by Spin, follows:

~$ 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

---

Your model results in an "invalid end state" too. However, this does not mean that it is necessarily a deadlock, it only means that the execution trace terminates before the processes reach the end of their block of code. Depending on the system being modeled, this is not always an actual problem.