3

Can anyone explain to me the order of what happens in the following?

if
 :: a_channel??5 -> // do A
 :: value_1 == value_2 -> // do B
fi;

So basically how I understand it is that for the statement to be executable, 5 needs to be in the channel. I understand that 5 will then be removed from the channel as a result(if it is indeed in the channel). What I don't undertstand is when 5 will be removed. Will 5 be removed after the statement is executed or will it be removed before during the check for execution.

Promela ref link for receiving: http://spinroot.com/spin/Man/receive.html

Rajdeep
  • 2,246
  • 6
  • 24
  • 51

1 Answers1

3

Assume a_channel??5 is contained in the body of some process P_i.

Will 5 be removed after the statement is executed or will it be removed before during the check for execution.

The "check for execution" is a necessary but not sufficient condition for the removal of 5 from the channel. The other, necessary, condition is that P_i is selected for execution and executes the statement a_channel??5.

A more detailed answer.

The statement a_channel??5 is a statement that it is not always executable. It is executable only when 5 is in channel. (e.g. if 5 was in the channel, but it has been removed [e.g. by someone else], a_channel??5 is no longer executable)

After each time a process P_i executes an atomic (set of) instruction(s), the scheduler may decide to pre-empt it and to allow some other process P_j with some executable instruction to continue.

When a process P_i reaches a non-executable statement, it is always immediately pre-empted by the scheduler. In this case, it is an error condition if there is no other process P_j with some immediately executable instruction that can be scheduled for execution (i.e. the famous "invalid end state" error).

If statement a_channel??5 is executable and process P_i is selected for execution (or keeps going), then a_channel??5 executes atomically and it immediately removes the (first occurrence) of the value 5 from the channel.

Patrick Trentin
  • 7,126
  • 3
  • 23
  • 40
  • In the updated example above (assuming 5 is already in the channel), statement a_channel??5 might be atomically executed removing 5 from the channel, but does that mean it has to now do A ? Or can it still do B if value_1 == value_2 (i.e. 5 would be removed but it does B instead). – Rajdeep Oct 19 '19 at 16:37
  • Thanks for the detailed explanation by the way! – Rajdeep Oct 19 '19 at 16:47
  • 1
    @Rajdeep According to the above explanation, the removal of `5` requires the **execution** of `a_channel??5`. According to the **branching** semantics, the execution of a **guard** is followed by the execution of its body `// do A`. Therefore, if process `P_i` selects the guard `a_channel??5` then it cannot execute neither `value_1 == value_2` nor `// do B`, unless the *if statement* is contained in some **loop** and next time it reaches the same branch it makes a different choice. – Patrick Trentin Oct 20 '19 at 03:29
  • 1
    @Rajdeep Perhaps a simpler example than `a_channel??5` is to look at what happens when another expression with side effects is used as a guard, like for example`x = x + 1`. Would you expect `x` to be incremented even when its branch is not taken? Of course not! As an exercise, you can use *LTL* model checking to formally verify this. – Patrick Trentin Oct 20 '19 at 03:42
  • Ah I understand now, thanks alot for the explanation !! – Rajdeep Oct 21 '19 at 01:57