Skip to main content
SpringerLink
Log in

A Theory of State-based Parallel Programming: Part 1

  • Conference paper
4th Refinement Workshop

Part of the book series: Workshops in Computing ((WORKSHOPS COMP.))

Abstract

This paper presents the first part of a theory for developing totally correct parallel programs. The emphasis of both specification and program is on the states, rather than actions, of the system. We stress the constructive approach in the development, by means of refinement and decomposition. A compositional proof system is investigated to support decomposition. It is shown to be sound in a computational model. Two examples are included to illustrate the compositionality of the proof system and the use of the methods in constructing an implementation.

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

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 39.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. M. Abadi and L. Lamport. The existence of refinement mappings. Research report 29, Digital System Research Center 1988.

    Google Scholar 

  2. M. Abadi and L. Lamport. Composing specifications Research report, Digital System Research Center 1989.

    Google Scholar 

  3. K.R. Apt. Ten years of Hoare’s logic: a survey-part II: nondeterminism. Theoretical Computer Science 28 83–109 1984.

    Article  MathSciNet  MATH  Google Scholar 

  4. K.R. Apt and G.D. Plotkin. countable nondeterminism and random assignment. Journal of the ACM 33 4 724–767 1986.

    Article  MathSciNet  MATH  Google Scholar 

  5. B. Alpern and F. Schneider. Defining liveness. Info. Proc. Lett. 21 181–185.

    Google Scholar 

  6. R.J.R. Back. A calculus of refinement for program derivations. Acta Informatica 25 593–624, Springer-Verlag 1988.

    Google Scholar 

  7. P. Cousot and R. Cousot. A language independent proof of the soundness and completeness of generalized Hoare logic. Inform. and Comput. 80165–191 1989.

    Google Scholar 

  8. W.P. de Roever. The guest for compositionality. in Proc:IFIP Working Conf The Role of Abstract Models in Computer Science North-Holland, 1985.

    Google Scholar 

  9. D. Grosvenor and A. Robinson. An evaluation of Rely-Guarantee. draft 1989.

    Google Scholar 

  10. E.C.R. Hehner. Predicative programming parts 1 and 2. Commun. ACM 27, 2 134–151 1984.

    Article  MathSciNet  MATH  Google Scholar 

  11. He, Jifeng. A simulation approach to verification of compiling specification of ProCoS level 0 programming language. ESPRIT 3104 ProCoS 1990.

    Google Scholar 

  12. C.A.R. Hoare et al. Laws of programming. Commun. ACM 30, 8 672–686 1987.

    Article  MathSciNet  MATH  Google Scholar 

  13. C.B. Jones. Development methods for computer programs including a notion of interference. DPhil. Thesis, Oxford University Computing Laboratory, 1981.

    Google Scholar 

  14. C.B. Jones. Tentative steps towards a development method for interfering programs. ACM Trans. Program. Lang. Syst. 5, 4, 596–619 1983.

    Article  MATH  Google Scholar 

  15. R.M. Keller. Formal verification of parallel programs Commun. ACM 19 371–384 1976.

    Article  MATH  Google Scholar 

  16. L. Lamport. Proving the correctness of multiprocess programs. IEEE Trans. on Software Engineering 1 1977.

    Google Scholar 

  17. L. Lamport. The Hoare logic of concurrent programming. Acta Inform. 14 21–37 1980.

    Article  MathSciNet  MATH  Google Scholar 

  18. C. Morgan, P.H.B. Gardiner and K. Robinson. On the Refinement Calculus. Oxford University Computing Laboratory, Technical Monograph PRG-70, 1988.

    Google Scholar 

  19. S. Owicki and D. Gries. An axiomatic proof technique for parallel programs. Acta Inform. 6 319–340 Springer-Verlag 1976.

    Google Scholar 

  20. E.-R. Olderog and C.A.R. Hoare. Specification-oriented semantics for communicating processes. Acta Informatica 23 9–66 Springer-Verlag 1986.

    Google Scholar 

  21. S. Owicki. A consistent and complete deductive system for the verification of parallel programs. Proceedings of 8th Annual ACM Symposium on Theory of Computing. Hershey, Pennsylvania, USA 1976.

    Google Scholar 

  22. G.D. Plotkin. A structural approach to operational semantics. Computer Science Department, Aarhus University, Technical Report, DAIMI FN-19,1981.

    Google Scholar 

  23. F.B. Schneider and G.R. Andrews. Concepts for Concurrent Pro-gramming. LNCS, Springer-Verlag

    Google Scholar 

  24. C. Stirling. A generalization of Owicki-Gries’s Hoare logic for a concurrent while language. Theoretical Computer Science 58 347–359 1988.

    Article  MathSciNet  MATH  Google Scholar 

  25. K. Stolen. Development of Parallel Programs on Shared Data-structures. Ph.D Thesis, Computer Science Department, Manchester University, 1990.

    Google Scholar 

  26. J.C.P. Woodcock and B. Dickinson. Using VDM with Rely and Guarantee-conditions, experiences from a real project. 2nd VDMEurope Symposium, Dublin, Ireland, LNCS 328, Springer-Verlag, 1988.

    Google Scholar 

  27. Xu Qiwen and He Jifeng. Towards a theory of interfering programs. Draft, Oxford University Computing Laboratory, 1990.

    Google Scholar 

  28. J. Zwiers. Compositionality, Concurrency and Partial Correctness. LNCS 321 1989.

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Programming Research Group, Oxford University Computing Laboratory, 8-11 Keble Road, Oxford, OX1 3QD, England, UK

    Xu Qiwen & He Jifeng

Authors
  1. Xu Qiwen
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. He Jifeng
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Department of Computing Science, University of Glasgow, G12 8QQ, Glasgow, Scotland

    Joseph M. Morris PhD

  2. Lloyd’s Register House, Lloyd’s Register of Shipping, 29 Wellesley Road, CR0 2AJ, Croydon, Surrey, UK

    Roger C. Shaw

Rights and permissions

Reprints and permissions

Copyright information

© 1991 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Qiwen, X., Jifeng, H. (1991). A Theory of State-based Parallel Programming: Part 1. In: Morris, J.M., Shaw, R.C. (eds) 4th Refinement Workshop. Workshops in Computing. Springer, London. https://doi.org/10.1007/978-1-4471-3756-6_15

Download citation

  • DOI: https://doi.org/10.1007/978-1-4471-3756-6_15

  • Publisher Name: Springer, London

  • Print ISBN: 978-3-540-19657-0

  • Online ISBN: 978-1-4471-3756-6

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation