Spinroot

A forum for Spin users

You are not logged in.

#1 2014-04-17 16:13:01

maryam
Member
Registered: 2012-03-27
Posts: 16

Confused about the result of using atomic sequence

Hi,

I have two following statements in the model (the program model is the self-composed model of a program with parallel composition):

   c_code{};
   (!lock);

The first statement is always followed by the second one. So, I wrapped these two statements as an atomic sequence as follows:

   atomic{
        c_code{};
        (!lock);
   }

As expected, the number of states were decreased for concurrent programs (when lock is zero, the sequence is executed indivisibly).
But, the result for sequential programs was surprising, where the number of states were increased a bit little! I cannot understand why?!

many thanks in advance

Offline

#2 2014-04-18 04:41:39

spinroot
forum
Registered: 2010-11-18
Posts: 691
Website

Re: Confused about the result of using atomic sequence

a c_code statement is always treated as global -- meaning that it allows no partial order reduction to be applied.
and similarly an atomic statement is treated as global (as a whole) if it contains at least one global statement.
so it could be that some statements in your atomic sequence could be executed under partial order reduction rules if you omit the atomic sequence, but not if you group it with a global statement into a single sequence.  in that case the number of states reached could increase

Offline

#3 2014-04-18 11:05:06

maryam
Member
Registered: 2012-03-27
Posts: 16

Re: Confused about the result of using atomic sequence

Thank you very much for the explanation. I have a better understanding of an atomic sequence now.

Offline

Board footer

Powered by FluxBB