A Theory of State-based Parallel Programming: Part 1

  • Xu Qiwen
  • He Jifeng
Conference paper
Part of the Workshops in Computing book series (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.

Keywords

Europe Prefix sinO Cuted Prepar 

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. [AL88]
    M. Abadi and L. Lamport. The existence of refinement mappings. Research report 29, Digital System Research Center 1988.Google Scholar
  2. [AL89]
    M. Abadi and L. Lamport. Composing specifications Research report, Digital System Research Center 1989.Google Scholar
  3. [Ap84]
    K.R. Apt. Ten years of Hoare’s logic: a survey-part II: nondeterminism. Theoretical Computer Science 28 83–109 1984.MathSciNetCrossRefMATHGoogle Scholar
  4. [AP86]
    K.R. Apt and G.D. Plotkin. countable nondeterminism and random assignment. Journal of the ACM 33 4 724–767 1986.MathSciNetCrossRefMATHGoogle Scholar
  5. [AS85]
    B. Alpern and F. Schneider. Defining liveness. Info. Proc. Lett. 21 181–185.Google Scholar
  6. [Bk88]
    R.J.R. Back. A calculus of refinement for program derivations. Acta Informatica 25 593–624, Springer-Verlag 1988.Google Scholar
  7. [CC89]
    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. [dR85]
    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. [GR89]
    D. Grosvenor and A. Robinson. An evaluation of Rely-Guarantee. draft 1989.Google Scholar
  10. [He84]
    E.C.R. Hehner. Predicative programming parts 1 and 2. Commun. ACM 27, 2 134–151 1984.MathSciNetCrossRefMATHGoogle Scholar
  11. [He90]
    He, Jifeng. A simulation approach to verification of compiling specification of ProCoS level 0 programming language. ESPRIT 3104 ProCoS 1990.Google Scholar
  12. [Hoare et al 87]
    C.A.R. Hoare et al. Laws of programming. Commun. ACM 30, 8 672–686 1987.MathSciNetCrossRefMATHGoogle Scholar
  13. [Jo81]
    C.B. Jones. Development methods for computer programs including a notion of interference. DPhil. Thesis, Oxford University Computing Laboratory, 1981.Google Scholar
  14. [Jo83]
    C.B. Jones. Tentative steps towards a development method for interfering programs. ACM Trans. Program. Lang. Syst. 5, 4, 596–619 1983.CrossRefMATHGoogle Scholar
  15. [Ke76]
    R.M. Keller. Formal verification of parallel programs Commun. ACM 19 371–384 1976.CrossRefMATHGoogle Scholar
  16. [La77]
    L. Lamport. Proving the correctness of multiprocess programs. IEEE Trans. on Software Engineering 1 1977.Google Scholar
  17. [La80]
    L. Lamport. The Hoare logic of concurrent programming. Acta Inform. 14 21–37 1980.MathSciNetCrossRefMATHGoogle Scholar
  18. [MRG88]
    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. [OG76]
    S. Owicki and D. Gries. An axiomatic proof technique for parallel programs. Acta Inform. 6 319–340 Springer-Verlag 1976.Google Scholar
  20. [OH86]
    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. [Ow76]
    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. [P181]
    G.D. Plotkin. A structural approach to operational semantics. Computer Science Department, Aarhus University, Technical Report, DAIMI FN-19,1981.Google Scholar
  23. [SA]
    F.B. Schneider and G.R. Andrews. Concepts for Concurrent Pro-gramming. LNCS, Springer-VerlagGoogle Scholar
  24. [St88]
    C. Stirling. A generalization of Owicki-Gries’s Hoare logic for a concurrent while language. Theoretical Computer Science 58 347–359 1988.MathSciNetCrossRefMATHGoogle Scholar
  25. [St90]
    K. Stolen. Development of Parallel Programs on Shared Data-structures. Ph.D Thesis, Computer Science Department, Manchester University, 1990.Google Scholar
  26. [WD88]
    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. [XH90]
    Xu Qiwen and He Jifeng. Towards a theory of interfering programs. Draft, Oxford University Computing Laboratory, 1990.Google Scholar
  28. [Zw89]
    J. Zwiers. Compositionality, Concurrency and Partial Correctness. LNCS 321 1989.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1991

Authors and Affiliations

  • Xu Qiwen
    • 1
  • He Jifeng
    • 1
  1. 1.Programming Research GroupOxford University Computing LaboratoryOxfordEngland, UK

Personalised recommendations