Advertisement

Specifications and proofs for abstract data types in concurrent programs

  • Susan S. Owicki
II. Program Verification
Part of the Lecture Notes in Computer Science book series (LNCS, volume 69)

Abstract

Shared abstract data types, such as queues and buffers, are useful tools for building well-structured concurrent programs. This paper presents a method for specifying shared types in a way that simplifies concurrent program verification. The specifications describe the operations of the shared type in terms of their effect on variables of the process invoking the operation. This makes it possible to verify the processes independently, reducing the complexity of the proof. The key to defining such specifications is the concept of a private variable: a variable which is part of a shared object but belongs to just one process. Shared types can be implemented using an extended form of monitors; proof rules are given for verifying that a monitor correctly implements its specifications. Finally, it is shown how concurrent programs can be verified using the specifications of their shared types. The specification and proof techniques are illustrated with a number of examples involving a shared bounded buffer.

Keywords

Auxiliary Variable Data Abstraction Procedure Call Concurrent Program Concurrent Process 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. [Brinch Hansen 73]
    P. Brinch Hansen. Operating Systems Principles. Prentice Hall, Englewood Cliffs, New Jersey, (1973).Google Scholar
  2. [Brinch Hansen 75]
    P. Brinch Hansen. The programming language concurrent Pascal. IEEE Trans. on Software Eng., SE-1 No. 2, (June, 1975), pp. 199–207.Google Scholar
  3. [Good and Ambler 75]
    D.I. Good and A.L. Ambler. Proving systems of concurrent processes synchronized with message buffers. Draft, (1975).Google Scholar
  4. [Guttag 75]
    J.V. Guttag. The specification and application to programming of abstract data types. Ph.D. thesis, Computer Science, University of Toronto, (Sept. 1975).Google Scholar
  5. [Guttag et al 76]
    J.V. Guttag, E. Horowitz, D.R. Musser. Abstract data types and software validation. Univ. of Southern California Information Sciences Institute report 76–48, (August, 1976).Google Scholar
  6. [Hoare 69]
    C.A.R. Hoare. An axiomatic basis for computer programming. Comm. ACM 12, 10 (Oct. 1969), pp. 576–583.Google Scholar
  7. [Hoare 71]
    C.A.R. Hoare. Procedures and parameters—an axiomatic approach. Symp. on the Semantics of Algorithmic Languages, Springer, Berlin-Heidelberg-New York, (1971), pp. 102–116.Google Scholar
  8. [Hoare 72]
    C.A.R. Hoare. Proof of correctness of data representations. Acta Informatica 1 (1972), pp. 271–281.Google Scholar
  9. [Hoare 73]
    C.A.R. Hoare. A structured paging system. Computer J. 16, 3 (1973), pp. 209–215.Google Scholar
  10. [Hoare 74]
    C.A.R. Hoare. Monitors: an operating system structuring concept. Comm. ACM 17, 10 (Oct. 1974), pp. 549–556.Google Scholar
  11. [Howard 76]
    J.H. Howard. Proving monitors. Comm. ACM 19, 5 (May 1976), pp. 273–279.Google Scholar
  12. [Lamport 75]
    L. Lamport. Formal correctness proofs for multiprocess algorithms. Proc. Second Int. Symp. on Programming, April 1976.Google Scholar
  13. [Liskov and Zilles 75]
    B.H. Liskov and S. Zilles. Specification techniques for data abstractions. IEEE Trans. on Software Eng. SE-1, 1 (March 1975), pp. 7–19.Google Scholar
  14. [Liskov and Berzins 76]
    B.H. Liskov and V. Berzins. An appraisal of program specifications. Computation Structures Group Memo 141, M.I.T. (July 1976).Google Scholar
  15. [Manna 74]
    Z. Manna and A. Pnueli. Axiomatic approach to total correctness of programs. Acta Informatica 3 (1974) pp. 243–263.Google Scholar
  16. [Neumann 75]
    P.G. Neumann, L. Robinson, K.N. Levitt, R.S. Boyer, A.R. Saxena. A provably secure operating system. Stanford Research Institute, Menlo Park, California (June 1975).Google Scholar
  17. [Owicki 76]
    S.S. Owicki. A consistent and complete deductive system for the verification of parallel programs. Proc. 8 th ACM Symp. on Theory of Computing, (May 1976), pp. 73–86.Google Scholar
  18. [Owicki and Gries 76a]
    S.S. Owicki and D. Gries. Verifying properties of parallel programs: an axiomatic approach. Comm. ACM 19, 5 (May 1976), pp. 280–285.Google Scholar
  19. [Owicki and Gries 76b]
    S.S. Owicki and D. Gries. An axiomatic proof technique for parallel programs I, Acta Informatica 6 (1976) pp. 319–340.Google Scholar
  20. [Parnas 72]
    D.L. Parnas. A technique for the specification of software modules, with examples. Comm. ACM 15, 5 (May 1972), pp. 330–336.Google Scholar
  21. [Schorre 75]
    V. Schorre. A program verifier with assertions in terms of abstract data. Systems Development Corporation report SP 3841, Santa Monica, California.Google Scholar
  22. [Shaw 76]
    M. Shaw. Abstraction and verification in Alphard: design and verification of a tree handler. Computer Science Department, Carnegie-Mellon University, (June 1976).Google Scholar
  23. [Spitzen 75]
    J. Spitzen and B. Wegbreit. The verification and synthesis of data structures. Acta Informatica 4 (1975), pp. 127–144.Google Scholar
  24. [Wulf 76]
    W.A. Wulf, R.L. London, and M. Shaw. An introduction to the construction and verification of Alphard programs. IEEE Trans. on Software Eng., SE-2, 4 (December, 1976), pp. 253–265.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1979

Authors and Affiliations

  • Susan S. Owicki
    • 1
  1. 1.Digital Systems Laboratory Departments of Electrical Engineering and Computer ScienceStanford UniversityStanford

Personalised recommendations