TY - GEN

T1 - A partial order event model for concurrent objects

AU - Meseguer, José

AU - Talcott, Carolyn

N1 - Copyright:
Copyright 2020 Elsevier B.V., All rights reserved.

PY - 1999

Y1 - 1999

N2 - 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 T R o to the rewrite theory R specifying the desired system. The elements of T Ro are concurrent computations described as proofs modulo an equational theory of proof/computation equivalence. This paper builds a very intuitive alternate model εR, 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. The models are very general and can express both synchronous and asynchronous object computations. In the asynchronouscase the Baker-Hewitt eventmodel for actors appears as a special case of our model.

AB - 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 T R o to the rewrite theory R specifying the desired system. The elements of T Ro are concurrent computations described as proofs modulo an equational theory of proof/computation equivalence. This paper builds a very intuitive alternate model εR, 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. The models are very general and can express both synchronous and asynchronous object computations. In the asynchronouscase the Baker-Hewitt eventmodel for actors appears as a special case of our model.

UR - http://www.scopus.com/inward/record.url?scp=22644450258&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=22644450258&partnerID=8YFLogxK

U2 - 10.1007/3-540-48320-9_29

DO - 10.1007/3-540-48320-9_29

M3 - Conference contribution

AN - SCOPUS:22644450258

SN - 3540664254

SN - 9783540664253

T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

SP - 415

EP - 430

BT - CONCUR 1999, Concurrency Theory - 10th International Conference, Proceedings

PB - Springer-Verlag Berlin Heidelberg

T2 - 10th International Conference on Concurrency Theory, CONCUR 1999

Y2 - 24 August 1999 through 27 August 1999

ER -