Abstract
A new framework for describing concurrent systems is presented. Rules for composing configurations of concurrent programs are represented by sequents Γ ⊢ρ Δ, where Γ and Δ are sequences of partially ordered sets (of events) and ρ is a matrix of monotone maps from the components of Γ to the components of Δ. Such a sequent expresses that whenever a configuration has certain specified subposets of events (Γ), then it extends to a configuration containing one of several specified subposets (Δ). The structural rules of Gentzen’s sequent calculus are decorated by suitable operations on matrices, where cut corresponds to product. The calculus thus obtained is shown to be sound with respect to interpretation in configuration structures [GG90]. Completeness is proven for a restriction of the calculus to finite sequents. As a case study we axiomatise the Java memory model, and formally derive a non-trivial property of thread-memory interaction.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
P. Cenciarelli. Event Structures for Java. In S. Drossopoulou, S. Eisenbach, B. Jacobs, G. Leavens, P. Mueller, and A. Poetzsch-Heffter, editors, Proceedings of the ECOOP 2000 Workshop on Formal Techniques for Java Programs, Cannes, France, June 2000.
P. Cenciarelli, A. Knapp, B. Reus, and M. Wirsing. An Event-Based Structural Operational Semantics of Multi-Threaded Java. In J. Alves-Foss, editor, Formal Syntax and Semantics of Java, 1523 LNCS. Springer, 1998.
R. J. van Glabbeek and U. Goltz. Refinement of Actions in Causality Based Models. In W.P. de Roever J. W. de Bakker and G. Rozenberg, editors, LNCS 430, pages 267–300. Springer-Verlag, 1990.
R. J. van Glabbeek and U. Goltz. Refinement of actions and equivalence notions for concurrent systems. Acta Informatica, 37:229–327, 2001.
J. Gosling, B. Joy, and G. Steele. The Java Language Specification. Addison-Wesley, 1996.
R. J. van Glabbeek and G. D. Plotkin. Configuration structures (extended abstract). In D. Kozen, editor, Proceedings of LICS’95, pages 199–209. IEEE Computer Society Press, June 1995.
M. Nielsen, G. D. Plotkin, and G. Winskel. Petri Nets, Event Structures and Domains: Part I. Theoretical Computer Science, 13(1):85–108, 1981.
G. Winskel. Event Structure Semantics of CCS and Related Languages. Springer LNCS, 140, 1982. Proceedings ICALP’82.
Glynn Winskel. Event Structures. In G. Rozemberg W. Brauer, W. Reisig, editor, Petri Nets: Applications and Relationships to Other Models of Concurrency, number 255 in LNCS. Springer-Verlag, 1987.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2002 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Cenciarelli, P. (2002). Configuration Theories. In: Bradfield, J. (eds) Computer Science Logic. CSL 2002. Lecture Notes in Computer Science, vol 2471. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-45793-3_14
Download citation
DOI: https://doi.org/10.1007/3-540-45793-3_14
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-44240-0
Online ISBN: 978-3-540-45793-0
eBook Packages: Springer Book Archive