Object-based commutativity analysis for real-time applications

The semantic specification of an object's methods can be used to determine their commutativity properties. The commutative method group, introduced in our earlier work, captures these commutativity properties in terms of groups of methods that commute, as opposed to pairs of methods This paper outlines how method group commutativity can be used to increase concurrency in distributed and real-time applications. This paper presents the conceptual foundations of our analysis techniques for determining group commutativity. We show that our formal analysis techniques are able to derive a greater degree of commutativity when the semantics of object methods are weakened. This formal procedure is supported by the PVS theorem prover. Using a set of examples, we demonstrate the effectiveness of our approach in detecting increased commutativity when object semantics are weakened.