Abstract
We Propose a method of constructing concurrent programs in which the synchronization skeleton of the program is automatically synthesized from a high-level (branching time) Temporal Logic specification. The synchronization skeleton is an abstraction of the actual program where detail irrelevant to synchronization is suppressed. For example, in the synchronization skeleton for a solution to the critical section problem each process’s critical section may be viewed as a single node since the internal structure of the critical section is unimportant. Most solutions to synchronization problems in the literature are in fact given as synchronization skeletons. Because synchronization skeletons are in general finite state, the propositional version of Temporal Logic can be used to specify their properties.
Originally published in: Kozen, D. (ed.) Logic of Programs. LNCS, vol. 131, pp. 52-71. Springer, Heidelberg (1982).
This is a preview of subscription content, log in via an institution to check access.
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
Ben-Ari, H.: Personal communication (198l)
Ben-Ari, M., Halpern, J., Pnueli, A.: Finite Models for Deterministic Propositional Logic. In: Proceedings 8th Int. Colloquium on Automata, Languages, and Programmlng (to appear, 1981)
Ben-Ari, M., Manna, Z., Pnueli, A.: The Temporal Logic of Branching Time. In: 8th Annual ACM Sympo on Principles of Programming Languages (1981)
Clarke, E.M.: Program Invariants as Fixpoints. In: 18th Annual Symp. on Foundations of Computer Science (1977)
Emerson, E.A., Clarke, E.M.: Characterizing Correctness Properties of Parallel Programs as Fixpoints. In: Proceedings 7th Int. Colloquium on Automata, Languages, and Programming. LNCS, vol. 85. Springer (1981)
Emerson, E.A., Halpern, J.: A New Decision Procedure for the Temporal Logic of Branching Time. Harvard Univ. (unpublished manuscript, 1981)
Flon, L., Suzuki, N.: The Total Correctness of Parallel Programs. SIAM J. Comp. (to appear, 1981)
Gabbay, D., Pnueli, A., et al.: The Temporal Analysis of Fairness. In: 7th Annual ACM Symp. on Principles of Progremmlng Languages (1980)
Hughes, G., Cresswell, M.: An Introduction to Modal Logic, Methuen, London (1968)
Lamport, L.: “Sometime” is Sometimes “Not Never”. In: 7th Annual ACM Symp. on Principles of Prgramming Languages (1980)
Laventhal, M.: Synthesis of Synchronization Code for Data Abstractions, Ph.D. Thesis, M.I.T (June 1978)
Park, D.: Fixpolnt Induction and Proofs of Program Properties. In: Mitchie, D. (ed.) Machine Intelligence 5. Edinburgh University Press (1970)
Pratt, V.: A Practical Decision Method for Propositional Dynamic Logic. In: I0th ACM Symp. on Theory of Computing (1977)
Ramamritham, K., Keller, R.: Specification and Synthesis of Synchronizers. In: 9th International Conference on Parallel Processing (1980)
SmuIIyan, R.M.: First Order Logic. Springer, Berlin (1968)
Tarskl, A.: A Lattice-Theoretical Fixpoint Theorem and Its Applications. Pacific J. Math. 5, 285–309 (1955)
Tarjan, R.: Depth First Search and Linear Graph Algorithms. SIAM J. Comp. 1(2), 146–160 (1972)
Wolper, P.: Synthesis of Communicating Processes From Temporal Logic Specifications. Stanford Univ. (unpublished manuscript, 1981)
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 2008 Springer-Verlag Berlin Heidelberg
About this chapter
Cite this chapter
Clarke, E.M., Emerson, E.A. (2008). DESIGN AND SYNTHESIS OF SYNCHRONIZATION SKELETONS USING BRANCHING TIME TEMPORAL LOGIC. In: Grumberg, O., Veith, H. (eds) 25 Years of Model Checking. Lecture Notes in Computer Science, vol 5000. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-69850-0_12
Download citation
DOI: https://doi.org/10.1007/978-3-540-69850-0_12
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-69849-4
Online ISBN: 978-3-540-69850-0
eBook Packages: Computer ScienceComputer Science (R0)