Spin informs you that your proctypes never reach the "end" state, which is of course true since they consist of endless loops. If this was not intended behavior, it would be a useful information. In your case, however, you might just tell Spin that the program is allowed to end in the state corresponding to the do-loop by adding an end label to your code, e.g.:
active proctype P1(){
endHere:
do
:: true->
y2 = y1 + 1;
(y1 == 0 || y2 < y1);
/* Entering critical section */
insideCritical++;
assert(insideCritical < 2);
insideCritical--;
/* Exiting critical section */
y2 = 0;
od
}
An end label is any label starting with "end". If your proctype ends in a state marked in such a way, Spin will not show you those warnings.