# An Overview of PROMELA

• Print
This chapter is from the book

## Atomic Sequences

The simplest compound statement is the atomic sequence. A simple example of an atomic sequence is, for instance:

```atomic {       /* swap the values of a and b */
tmp = b;
b = a;
a = tmp
}
```

In the example, the values of two variables a and b are swapped in a sequence of statement executions that is defined to be uninterruptable. That is, in the interleaving of process executions, no other process can execute statements from the moment that the first statement of this sequence begins to execute until the last one has completed.

It is often useful to use atomic sequences to initialize a series of processes in such a way that none of them can start executing statements until the initialization of all of them has been completed:

```init {
atomic {
run A(1,2);
run B(2,3)
}
}
```

Atomic sequences may be non-deterministic. If, however, any statement inside an atomic sequence is found to be unexecutable (i.e., blocks the execution), the atomic chain is broken and another process can take over control. When the blocking statement becomes executable later, control can non-deterministically return to the process, and the atomic execution of the sequence resumes as if it had not been interrupted.

Note carefully that without atomic sequences, in two subsequent statements such as

```nfull(qname) -> qname!msg0
```

or

```qname?[msg0] -> qname?msg0
```

the second statement is not necessarily executable after the first one is executed. There may be race conditions when access to the channels is shared between several processes. In the first example, another process can send a message to the channel just after this process determined that it was not full. In the second example, another process can steal away the message just after our process determined its presence. On the other, it would be redundant to write

```atomic { qname?[msg0] -> qname?msg0 }
```

since this is equivalent to the single statement

```qname?msg0
```