Three processes share a global variable x$,$ and each process $($named P; in a mixed syntax$)$ performs the following:

int k; $/*$ local variable $*/$

for $($k $=0$; k $<mtext\; id="EditorElement\_84075"></mtext><mn\; id="EditorElement\_84076">5</mn>$; k$++)\{$

LOAD$($x$)$; INCREMENT$($x$)$; STORE$($x$)$; $\}$

That is$,$ each process executes $$x$++$;$$ five times, but each assignment is realized in three steps using its own local register. Now consider the following parallel program:

x $=0$;

run P$()$; run P$()$; run P$()$;

Can the final value of x be as small as $1$ or $2?$ Check possible outcomes using Spin, explain the results, and generalize them.

Hint:

$1.$ Model the three processes and the main $($init$)$ program in Prolmela $-$by implementing the behavior of LOAD, INCREMENT, and STORE using the constructs of Promela $($e$.$g$.$ local variables$).$

$2.$ Suppose you think x can be $3$ but not less. Then you should: a$.$ verify that x$==3$ is a possible outcome upon termination. $-$ This can be done by asserting that, when only one process $($the main process$)$ remains active after three run P$()$; x cannot be $3.-$The number of active processes can be obtained by the $\_$nr$\_$pr special variable or by counting them explicitly. $$b$.$ Verify that x$<mn\; id="EditorElement\_85060">3</mn>$ is not a possible outcome upon termination.