Semantics Based Commutativity Analysis of Object Methods
2005-03-04
Loading...
View/Download File
Persistent link to this item
Statistics
View StatisticsJournal Title
Journal ISSN
Volume Title
Title
Semantics Based Commutativity Analysis of Object Methods
Authors
Published Date
2005-03-04
Publisher
Type
Report
Abstract
Traditional analysis and usage of operation commutativity relies on pairwise commutativity relationships. In contrast, this paper presents method group commutativity, which specifies the conditions under which operations in a method group will commute. Method group commutativity can be practically applied to efficiently support distributed object caching and concurrency control. A formal definition of commutativity, in terms of Hoare logic expressions, guides the development of a methodology to create a method commutativity specification from an object's semantic specification. This methodology uses the PVS theorem prover for analysis and validation of commutativity properties. The use of formal methods, together with suitable tools, provides a more complete understanding of method commutativity relationships as compared to existing approaches. Our approach also provides a unified representation of both forward and backward commutativity properties. The methodology is also expanded to express weakened semantics in the method commutativity specification to enable greater commutativity.
Keywords
Description
Related to
Replaces
License
Series/Report Number
Funding information
Isbn identifier
Doi identifier
Previously Published Citation
Suggested citation
Eberhard, John; Tripathi, Anand. (2005). Semantics Based Commutativity Analysis of Object Methods. Retrieved from the University Digital Conservancy, https://hdl.handle.net/11299/215647.
Content distributed via the University Digital Conservancy may be subject to additional license and use restrictions applied by the depositor. By using these files, users agree to the Terms of Use. Materials in the UDC may contain content that is disturbing and/or harmful. For more information, please see our statement on harmful content in digital repositories.