[Home] [CV] [Publications]


Minus 1a5aa4f1c08b567c9107cba729de26bc87c17ab2b2f690eb45059193a1d6f587 A Partial Order Event Model for Concurrent Objects
Meseguer, J. and Talcott, C. L. - 1999

The increasing importance and ubiquity of distributed and mobile object systems makes it very desirable to develop rigorous semantic models and formal reasoning techniques to ensure their correctness. The concurrency model of rewriting logic has been extensively used by a number of authors to specify, execute, and validate concurrent object systems. This model is a true concurrency model, associating an algebra of proof terms RP to the rewrite theory R specifying the desired system. The elements of PR are concurrent computations described as proofs modulo an equational theory of proof/computation equivalence. This paper builds a very intuitive alternate model RE, also of a true concurrency nature, but based instead on the notion of concurrent events and a causality partial order between such events. The main result of the paper is the equivalence of these two models expressed as an isomorphism. Both models have straightforward extensions to similar models of infinite computations, in which infinite behavior properties such as fairness can be naturally expressed. The models are very general and can express both synchronous and asynchronous object computations. In the asynchronous case the Baker-Hewitt event model for actors appears as a special case of our model.