A forum for Spin users
You are not logged in.
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
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
Thank you very much for the explanation. I have a better understanding of an atomic sequence now.
Offline