Receiving message from channel as guard

Question

A: if
   :: q?a -> ...
   :: else -> ...
   fi

Note that a race condition is built-in to this type of code. How long should the process wait, for instance, before deciding that the message receive operation will not be executable? The problem can be avoided by using message poll operations, for instance, as follows:

The above citation comes from http://spinroot.com/spin/Man/else.html

I cannot understand that argumentation. Just Spin can decide on q?a: if q is empty then it is executable. Otherwise, it is blocking.

The given argument raised a race condition.

But, I can make the same argument:

byte x = 1;
A: if 
   :: x == 2 -> ...
   :: else -> ...
   fi

It is ok from point of Spin's view. But, I am asking, How long should the process wait, for instance, before deciding that the value of x will not be incremented by other process?

ivcha ivcha · Accepted Answer · 2017-03-28T03:54:57

The argumentation is sound with respect to the semantics of Promela and the selection construct. Note that for selection, if multiple guard statements are executable, one of them will be selected non-deterministically. This in turns implies the semantics such that selection (even though it can non-deterministally execute guards) needs to determine which guards are executable at the point of invocation of the selection statement.

The question about the race condition might make more sense when considering the semantics of selection and message receives. Note that race condition in this case means that the output of the selection might depend on the time for which it needs to invoke the receive (i.e. whether it finishes at a point at which there is a message in the channel or not). More specifically, for the selection statement, there should be no ambiguity in terms of feasible guards. Now, the message receive gets the message from the channel only if the channel is not empty (otherwise, it cannot finish executing and waits). Therefore, with respect to the semantics of receive, it is not clear whether it is executable before it is actually executed. In turn, else should execute if the receive is not executable. However, since else should execute only if ? is not executable, so to know if else is executable the program needs to know the future (or determine how much should it wait to know this, thus incurring the race condition).

Note that the argument does not apply to your second example:

byte x = 1;
A: if 
   :: x == 2 -> ...
   :: else -> ...
   fi

since here, to answer whether else is eligible no waiting is required (nor knowing the future), since the program can at any point determine if x == 2.

Receiving message from channel as guard

1 Answers