A case for allowing modification of global variables by certain types of synchronized actions

[kpjo...@illinois.edu]

There are two scenarios I can think of where I feel that PRISM should allow synchronized actions (or at least what PRISM considers to be synchronized actions) to modify global variables. I would like to know your thoughts on this. In both scenarios I am referring to DTMCs, I am not sure if my reasoning will apply to these types of models.

Scenario 1:

A module 'foo' has a named action 'bar' that modifies a global variable. This name is only present for giving the action a name to distinguish it from other actions in this module. No other modules have an action named 'bar'.

In this scenario, the action, though named, is NOT a synchronized action. Therefore it should be allowed to modify the global variable.

Scenario 2:

Modules 'm1' and 'm2' have a synchronized action 'act'. The action in 'm1' modifies a global variable. The corresponding action in 'm2' does not modify this same global variable.

In this scenario since both modules do not try to simultaneously modify the same global variable, there is no possibility of a data race. Further, because preconditions are checked before the action is performed, there is no possibility of an action changing the global variable while the other action is checking its precondition.

[Christos Kloukinas]

I imagine that if they allow labelled transitions to modify global variables, then one can write transitions that attempt to modify the same variables with different values:

module A

 [sync] true -> (a' = 3);

endmodule

module B

 [sync] true -> (a' = 2);

endmodule

So they'd need to check that the same-labelled transitions are modifying sets of variables whose intersection is empty - seems simpler to just forbid it.

Cheers

--
You received this message because you are subscribed to the Google Groups "PRISM model checker" group.
To unsubscribe from this group and stop receiving emails from it, send an email to prismmodelchec...@googlegroups.com.
To post to this group, send email to prismmod...@googlegroups.com.
Visit this group at https://groups.google.com/group/prismmodelchecker.
For more options, visit https://groups.google.com/d/optout.

[Joachim Klein]

Hi,

Indeed, that would be a useful relaxation of the global variable
handling. I've opened an issue at
https://github.com/prismmodelchecker/prism/issues/50. You might want to
have a look at the
https://github.com/kleinj/prism/tree/flexible-global-writes branch as
well, where both scenarios above should work - apart from the part where
a conflict is only avoided due to the guards not overlapping. See the
issue for some more explanation.


Cheers,
Joachim