Nothing Special   »   [go: up one dir, main page]
Skip to main content
Springer Nature Link
Log in

Hoare-Style compositional proof systems for reactive shared variable concurrency

  • Conference paper
  • First Online:
Foundations of Software Technology and Theoretical Computer Science (FSTTCS 1997)

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

Abstract

A new compositional logic for verifying safety properties of shared variable concurrency is presented, in which, in order to characterize infinite computations, a Hoare-style I/pre/post format is used where I expresses the communication interface, enabling the characterization of reactive programs. This logic relates to the Rely/Guarantee paradigm of Jones [11], in that Rely/Guarantee formulae can be expressed within our formalism. As novel feature we characterize prefixes of computations through so-called time-diagrams, a mapping from a discrete total wellfounded ordering to states, and combine these with action predicates (already introduced in old work of, e.g., Lamport) in order to obtain a compositional formalism. The use of time diagrams enables the expression of strongest postconditions and strongest invariants directly within the assertion language, instead of through encoding within the natural numbers. A proof of Dekker's mutual exclusion algorithm is given.

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. P. Aczel. On an inference rule for parallel composition. unpublished note, 1993.

    Google Scholar 

  2. F.S. de Boer, U. Hannemann and W.-P. de Roever. A compositional proof system for shared variable concurrency. to appear at FME '97, LNCS, 1997.

    Google Scholar 

  3. H. Barringer, R. Kuiper, and A. Pnueli. Now you may compose temporal logic specifications. In 16th ACM symposium on Theory of Computation, pages 51–63, 1984.

    Google Scholar 

  4. F.S. de Boer, J.N. Kok, C. Palamidessi, and J.J.M.M. Rutten. The failure of failures: Towards a paradigm for asynchronous communication. In Proceedings of Concur '91, Lecture Notes in Computer Science, Vol. 527, pages 111–126, 1991.

    Google Scholar 

  5. S. Brookes. A fully abstract semantics of a shared variable parallel language. In Proceedings 8th Annual IEEE Symposium on Logic in Computer Science, IEEE Computer Society Press, pages 98–109, 1993.

    Google Scholar 

  6. S.D. Brookes, C.A.R. Hoare and A.W. Roscoe. A Theory of Communicating Sequential Processes. JACM 31(7), pp. 560–599, 1984.

    Article  MATH  MathSciNet  Google Scholar 

  7. S.A. Cook. Soundness and completeness of an axiom system for program verification. In SIAM J. on Computing 7, pp. 70–90, 1978.

    Article  MATH  Google Scholar 

  8. R.W. Floyd. Assigning meaning to Programs. Mathematical Aspects of Computer Science XIX, American Mathematical Society, 1967.

    Google Scholar 

  9. E.C.R. Hehner, C.A.R. Hoare. A more complete model of Communicating Processes. TCS 26, pp. 134–120, 1983.

    Article  MathSciNet  Google Scholar 

  10. J. Hooman. Specification and compositional verification of real-time systems. Lecture Notes in Computer Science, Vol. 558, 1992.

    Google Scholar 

  11. C.B. Jones. Development methods for computer programs including a notion of interference. PhD thesis, Oxford University Computing Laboratory, 1981.

    Google Scholar 

  12. L. Lamport. Verification and specification of concurrent programs. In A Decade of Concurrency (eds. J.W de Bakker, W.-P. de Roever and G. Rozenberg), Lecture Notes in Computer Science, Vol. 803, 1993.

    Google Scholar 

  13. J. Misra and K.M. Chandy. Proofs of networks of processes. IEEE Transactions on Software Engeneering, 7(7):417–426, 1981.

    MATH  MathSciNet  Google Scholar 

  14. P. Pandya: Compositional Verification of Distributed Programs. Ph. D. Thesis, University of Bombay, 1988.

    Google Scholar 

  15. P. Pandya and M. Joseph: P-A logic — a compositional proof system for distributed programs. Distributed Computing, Vol. 5, pp. 37–54, 1991.

    Article  MATH  MathSciNet  Google Scholar 

  16. W.-P. de Roever, F.S. de Boer, U. Hannemann, J. Hooman, Y. Lakhnech, P. Pandya, M. Poel, H. Schepers, Q. Xu and J. Zwiers. State-Based Proof Theory of Concurrency: from Noncompositional to Compositional Methods. to appear 1998.

    Google Scholar 

  17. K. StØlen. Development of Parallel Programs on Shared Data-structures. PhD thesis, Computer Science Department, Manchester University, 1990.

    Google Scholar 

  18. N. Sounderarajan. Axiomatic semantics of communicating sequential processes. TOPLAS, 6:647–662, 1984.

    Article  Google Scholar 

  19. N. Sounderarajan. A proof technique for parallel programs. Theoretical Computer Science, Vol. 31, pp. 13–29, 1984.

    Article  MathSciNet  Google Scholar 

  20. J.V. Tucker and J.I. Zucker. Program correctness over abstract data types, with error-state semantics. In CWI Monograph Series, vol. 6, Centre for Mathematics and Computer Science/North-Holland, 1988.

    Google Scholar 

  21. S. Owicki and D. Gries. An axiomatic proof technique for parallel programs. In Acta Informatika, 6:319–340, 1976.

    Article  MATH  MathSciNet  Google Scholar 

  22. Q. Xu. A theory of state — based parallel programming. PhD thesis, Oxford University Computing Laboratory, 1992.

    Google Scholar 

  23. Q. Xu, W.-P. de Roever and J. He. Relyguarantee method for verifying shared variable concurrent programs. Formal Aspects of Computing 1997 (To appear).

    Google Scholar 

  24. C.C. Zhou and C.A.R. Hoare. Partial Correctness of CSP. Proc. IEEE Int. Conf. on Distributed Computer Systems, pp. 1–12, 1981.

    Google Scholar 

  25. J. Zwiers, W.-P. de Roever and P. van Emde Boas: Compositionality and concurrent networks: soundness and completeness of a proofsystem. Technical Report 57, University of Nijmegen, The Netherlands, 1984.

    Google Scholar 

  26. J. Zwiers. Compositionality, Concurrency, and Partial Correctness. Lecture Notes in Computer Science, Vol.321, Springer-Verlag, 1989.

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Department of Computer Science, Utrecht University, P.O. Box 80.089, 3508, TB Utrecht, The Netherlands

    F. S. de Boer

  2. Institut für Informatik und Praktische Mathematik II, Christian-Albrechts-UniversitÄt zu Kiel, Preusserstrasse 1-9, 24105, Kiel, Germany

    U. Hannemann & W. -P. de Roever

Authors
  1. F. S. de Boer
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. U. Hannemann
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. W. -P. de Roever
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

S. Ramesh G Sivakumar

Rights and permissions

Reprints and permissions

Copyright information

© 1997 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

de Boer, F.S., Hannemann, U., de Roever, W.P. (1997). Hoare-Style compositional proof systems for reactive shared variable concurrency. In: Ramesh, S., Sivakumar, G. (eds) Foundations of Software Technology and Theoretical Computer Science. FSTTCS 1997. Lecture Notes in Computer Science, vol 1346. Springer, Berlin, Heidelberg. https://doi.org/10.1007/BFb0058036

Download citation

  • DOI: https://doi.org/10.1007/BFb0058036

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

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

  • Online ISBN: 978-3-540-69659-9

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation