Abstract
We present a decision algorithm for the following problem: given a specification, does there exist a concurrent program which both satisfies the specification and which can be implemented in hardware-available operations in a straightforward manner, i.e, without long correctness proofs, and without introducing excessive blocking and/or centralization? In case our decision algorithm answers “yes,” we also present a synthesis method to produce such a program. We consider specifications expressed in branching time temporal logic. Our result gives a way of classifying specifications as either “easy to implement” or “difficult to implement,” and can be regarded as the first step towards a notion of “implementation complexity” of specifications.
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
Anderson, J.H., Moir, M.: Universal constructions for multi-object operations. In: Symposium on Principles of Distributed Computing (1995)
Anuchitanukul, A., Manna, Z.: Realizability and synthesis of reactive modules. In: Dill, D.L. (ed.) CAV 1994. LNCS, vol. 818, pp. 156–169. Springer, Heidelberg (1994)
Attie, P.C., Emerson, E.A.: Synthesis of concurrent systems for an atomic read/atomic write model of computation (extended abstract). In: Fifteenth Annual ACM Symposium on Principles of Distributed Computing, May 1996, pp. 111–120. ACM Press, New York (1996)
Attie, P.C., Emerson, E.A.: Synthesis of concurrent systems for an atomic read/write model of computation. ACM Trans. Program. Lang. Syst. 23(2), 187–242 (2001); Extended abstract appears in ACM Symposium on Principles of Distributed Computing PODC 1996 (1996)
Browne, M.C., Clarke, E.M., Grumberg, O.: Characterizing finite kripke structures in propositional temporal logic. Theoretical Computer Science 59, 115–131 (1988)
Courtois, P.J., Heymans, H., Parnas, D.L.: Concurrent control with readers and writers. Communications of the ACM 14(10), 667–668 (1971)
Dijkstra, E.W.: A Discipline of Programming. Prentice-Hall Inc., Englewood Cliffs (1976)
Dill, D.L., Wong-Toi, H.: Synthesizing processes and schedulers from temporal specifications. In: Clarke, E., Kurshan, R.P. (eds.) CAV 1990. LNCS, vol. 531, pp. 272–281. Springer, Heidelberg (1991)
Emerson, E.A.: Temporal and modal logic. In: Van Leeuwen, J. (ed.) Handbook of Theoretical Computer Science. Formal Models and Semantics, vol. B. The MIT Press/Elsevier (1990)
Emerson, E.A., Clarke, E.M.: Using branching time temporal logic to synthesize synchronization skeletons. Sci. Comput. Program. 2, 241–266 (1982)
Harris, T.L., Fraser, K., Pratt, I.: A practical multi-word compare-and-swap operation. In: IEEE Symposium on Distributed Computing (2002)
Katz, S.: Temporary stability in parallel programs. Tech. Rep., Computer Science Dept., Technion, Haifa, Israel (1986)
Kupferman, O., Madhusudan, P., Thiagarajan, P.S., Vardi, M.Y.: Open systems in reactive environments: Control and synthesis. In: Palamidessi, C. (ed.) CONCUR 2000. LNCS, vol. 1877, pp. 92–107. Springer, Heidelberg (2000)
Kupferman, O., Vardi, M.Y.: Synthesis with incomplete information. In: 2nd International Conference on Temporal Logic, Manchester, July 1997, pp. 91–106. Kluwer Academic Publishers, Dordrecht (1997)
Manna, Z., Wolper, P.: Synthesis of communicating processes from temporal logic speciications. ACM Trans. Program. Lang. Syst. 6(1), 68–93 (1984); Also appears in Proceedings of the Workshop on Logics of Programs, Yorktown-Heights, N.Y. LNCS. Springer, Heidelberg (1981)
Moir, M.: Transparent support for wait-free transactions. In: Workshop on Distributed Algorithms (1997)
Pnueli, A., Rosner, R.: On the synthesis of a reactive module. In: Proceedings of the 16th ACM Symposium on Principles of Programming Languages, pp. 179–190. ACM, New York (1989)
Pnueli, A., Rosner, R.: On the synthesis of asynchronous reactive modules. In: Ronchi Della Rocca, S., Ausiello, G., Dezani-Ciancaglini, M. (eds.) ICALP 1989. LNCS, vol. 372, pp. 652–671. Springer, Heidelberg (1989)
Shavit, N., Touitou, D.: Software transactional memory. In: ACM Symposium on Principles of Distributed Computing, Ontario, Canada (1995)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2003 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Attie, P.C. (2003). On the Implementation Complexity of Specifications of Concurrent Programs. In: Fich, F.E. (eds) Distributed Computing. DISC 2003. Lecture Notes in Computer Science, vol 2848. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-39989-6_11
Download citation
DOI: https://doi.org/10.1007/978-3-540-39989-6_11
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-20184-7
Online ISBN: 978-3-540-39989-6
eBook Packages: Springer Book Archive