Skip to main content
SpringerLink
Log in

Reasoning about atomic objects

  • Conference paper
  • First Online:
Formal Techniques in Real-Time and Fault-Tolerant Systems (FTRTFT 1988)

Part of the book series: Lecture Notes in Computer Science ((LNCS,volume 331))

Abstract

Atomic transactions are a widely-accepted technique for organizing activities in reliable distributed systems. In most languages and systems based on transactions, atomicity is implemented through atomic objects, which are typed data objects that provide their own synchronization and recovery. This paper describes new linguistic mechanisms for constructing atomic objects from non-atomic components, and it formulates proof techniques that allow programmers to verify the correctness of such implementations.

This research was sponsored by the Defense Advanced Research Projects Agency (DOD), ARPA Order No. 4976, monitored by the Air Force Avionics Laboratory Under Contract F33615-84-K-1520. The views and conclusions contained in this document are those of the authors and should not be interpreted as representing the official policies, either expressed or implied, of the Defense Advanced Research Projects Agency or the US Government.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. K.R. Apt, N. Francez, and W.P. De Roever. A Proof System for Communicating Sequential Processes. ACM Transactions on Programming Languages and Systems 2(3):359–385, July, 1980.

    Article  Google Scholar 

  2. P.A. Bernstein and N. Goodman. A survey of techniques for synchronization and recovery in decentralized computer systems. ACM Computing Surveys 13(2):185–222, June, 1981.

    Article  Google Scholar 

  3. E. Best and B. Randell. A Formal Model of Atomicity in Asynchronous Systems. Acta Informatica 16(1):93–124, 1981.

    Article  Google Scholar 

  4. G. Dixon and S.K. Shrivastava. Exploiting Type Inheritance Facilities to Implement Recoverability in Object Based Systems. In Proceedings of the 6th Symposium in Reliability in Distributed Software and Database Systems. March, 1987.

    Google Scholar 

  5. K.P. Eswaran, J.N. Gray, R.A. Lorie, and I.L. Traiger. The Notion of Consistency and Predicate Locks in a Database System. Communications ACM 19(11):624–633, November, 1976.

    Article  Google Scholar 

  6. J.E. Richardson and M.J. Carey. Programming Constructs for Database System Implementation in EXODUS. In ACM SIGMOD 1987 Annual Conference, pages 208–219. May, 1987.

    Google Scholar 

  7. M.P. Herlihy, N.A. Lynch, M. Merritt, and W.E. Weihl. On the correctness of orphan elimination algorithms. In 17th Symposium on Fault-Tolerant Computer Systems. July, 1987. Abbreviated version of MIT/LCS/TM-329.

    Google Scholar 

  8. I. Greif, R. Seliger, and W.E. Weihl. Atomic Data Abstractions in a Distributed Collaborative Editing System. In Proceedings of the 13th Annual ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages, pages 160–172. January, 1986.

    Google Scholar 

  9. D. Gries. The Science of Programming. Spinger-Verlag, New York, 1981.

    Google Scholar 

  10. J.V. Guttag, J.J. Horning, and J.M. Wing. The Larch Family of Specification Languages. IEEE Software 2(5):24–36, September, 1985.

    Google Scholar 

  11. M.P. Herlihy. A quorum-consensus replication method for abstract data types. ACM Transactions on Computer Systems 4(1), February, 1986.

    Google Scholar 

  12. M.P. Herlihy and J.M. Wing. Avalon: Language Support for Reliable Distributed Systems. In The Seventeenth International Symposium on Fault-Tolerant Computing, pages 89–94. July, 1987. Also available as CMU-CS-TR-86-167.

    Google Scholar 

  13. M.P. Herlihy and J.M. Wing. Axioms for concurrent objects. In Fourteenth ACM Symposium on Principles of Programming Languages, pages 13–26. January, 1987.

    Google Scholar 

  14. C.A.R. Hoare. An Axiomatic Basis for Computer Programming. Communications of the ACM 12(10):576–583, October, 1969.

    Article  Google Scholar 

  15. C.A.R. Hoare. Proof of Correctness of Data Representations. Acta Informatica 1(1):271–281, 1972.

    Article  Google Scholar 

  16. J. Hooman and W.-P. de Roever. The Quest Goes On: A Survey of Proof Systems For Partial Correctness of CSP. Lecture Notes in Computer Science 224: Current Trends in Concurrency. Springer-Verlag, 1986, pages 343–395.

    Google Scholar 

  17. L. Lamport. Time, clocks, and the ordering of events in a distributed system. Communications of the ACM 21(7):558–565, July, 1978.

    Article  Google Scholar 

  18. L. Lamport. Specifying Concurrent Program Modules. ACM Transactions on Programming Languages and Systems 5(2):190–222, April, 1983.

    Article  Google Scholar 

  19. B.H. Liskov, and R. Scheifler. Guardians and actions: linguistic support for robust, distributed programs. Transactions on Programming Languages and Systems 5(3):381–404, July, 1983.

    Article  Google Scholar 

  20. B.H. Liskov and J.V. Guttag. Abstraction and Specification in Program Development. The MIT Press, 1986.

    Google Scholar 

  21. N. Lynch. A Concurrency Control For Resilient Nested Transactions. Technical Report MIT/LCS/TR-285, Laboratory for Computer Science, 1985.

    Google Scholar 

  22. N. Lynch and M. Merritt. Introduction to the Theory of Nested Transactions. In Proceedings of the International Conference on Database Theory. Rome, Italy, September, 1986. Sponsored by EATCS and IEEE.

    Google Scholar 

  23. Z. Manna and A. Pnueli. Verification of concurrent Programs, Part I: The Temporal Framework. Technical Report STAN-CS-81-836, Dept. of Computer Science, Stanford University, June, 1981.

    Google Scholar 

  24. J.E.B. Moss. Nested Transactions: An Approach to Reliable Distributed Computing. Technical Report MIT/LCS/TR-260, Laboratory for Computer Science, April, 1981.

    Google Scholar 

  25. S. Owicki and D. Gries. Verifying Properties of Parallel Programs: An Axiomatic Approach. Communications of the ACM 19(5):279–285, May, 1976.

    Google Scholar 

  26. C.H. Papadimitriou. The serializability of concurrent database updates. Journal of the ACM 26(4):631–653, October, 1979.

    Article  Google Scholar 

  27. D.P. Reed. Implementing atomic actions on decentralized data. ACM Transactions on Computer Systems 1(1):3–23, February, 1983.

    Article  Google Scholar 

  28. A.Z. Spector, J. Butcher, D.S. Daniels, D.J. Duchamp, J.L. Eppinger, C.E. Fineman, A. Heddaya, and P.M. Schwarz. Support for Distributed Transactions in the TABS prototype. IEEE Transactions on Software Engineering 11(6):520–530, June, 1985.

    Google Scholar 

  29. B. Stroustrup. The C++ Programming Language. Addison Wesley, 1986.

    Google Scholar 

  30. W.E. Weihl. Specification and implementation of atomic data types. Technical Report TR-314, Massachusetts Institute of Technology Laboratory for Computer Science, March, 1984.

    Google Scholar 

  31. W.E. Weihl, and B.H. Liskov. Implementation of resilient, atomic data types. ACM Transactions on Programming Languages and Systems 7(2):244–270, April, 1985.

    Article  Google Scholar 

  32. C.T. Wilkes and R.J. LeBlanc. Rationale for the design of Aeolus: a systems programming language for an action/object system. Technical Report GIT-ICS-86/12, Georgia Inst. of Tech. School of Information and Computer Science, Dec. 1986.

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Computer Science Department, Carnegle Mellon University, 15213-3890, Pittsburgh, Pennsyivania, U.S.A.

    Maurice P. Herlihy & Jeannette M. Wing

Authors
  1. Maurice P. Herlihy
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Jeannette M. Wing
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

M. Joseph

Rights and permissions

Reprints and permissions

Copyright information

© 1988 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Herlihy, M.P., Wing, J.M. (1988). Reasoning about atomic objects. In: Joseph, M. (eds) Formal Techniques in Real-Time and Fault-Tolerant Systems. FTRTFT 1988. Lecture Notes in Computer Science, vol 331. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-50302-1_14

Download citation

  • DOI: https://doi.org/10.1007/3-540-50302-1_14

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-50302-6

  • Online ISBN: 978-3-540-45965-1

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation