# Spinroot

A forum for Spin users

You are not logged in.

## #1 2011-06-02 07:24:21

Usman
Member
Registered: 2011-05-20
Posts: 7

### help regarding atomicity

hi,

can you please elaborate the difference between these two following codes, as the use of atomic {} is not clear to me.
i used it to avoid interleaving but in 1st case it gives me my required results, where as in some cases the 2nd approach is better.please guide me in detail.
what is the difference in using atomic{} before do loop and using in do loop after implication sign.
i will be very grateful to you for responding.

First case

byte    turn = 1, x=0;

proctype p() {
atomic {do :: turn == 1 ->turn = 2;x=2;
od
}}

proctype q() {
atomic{ do :: (turn == 2) -> turn = 1; x=1;
od
}}

init {atomic{run q();run p()}}

2nd case

byte    turn = 1, x=0;

proctype p() {
do :: (turn == 1) -> atomic{turn = 2;x=2;
}od
}

proctype q() {
do :: (turn == 2) -> atomic{turn = 1; x=1;
}od
}

init {atomic{run q();run p()}}

Offline

## #2 2011-06-02 12:57:30

theo.ruys
Registered: 2010-11-18
Posts: 11

### Re: help regarding atomicity

The atomic construct can be used to make SPIN treat a sequence of statements as a single atomic instruction. The sequence of statements will execute as one indivisible unit, non-interleaved with any other process.

Suppose e1 is an boolean expression and s2 and s3 are Promela statements that are always executable (e.g., assignments, as in your example). Now consider

atomic { e1; s2; s3; }

If e1 is executable (i.e., the expression evaluates to non-zero), SPIN will execute the sequence e1; s2; s3; as a single transition. On the other hand,

e1; atomic { s2; s3; }

will be different. After the expression e1 has been taken, any other process can continue. When this process is scheduled
again, the atomic clause will be executed. However, due to the execution of the other process(es), e1 might not longer be true. The original atomic sequence has thus been splitted into two atomic sequences: e1, and atomic {s2; s3}.

Offline