Skip to main content
SpringerLink
Log in

Concepts for concurrent programming

  • Chapter
  • First Online:
Current Trends in Concurrency

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

Abstract

Techniques for reasoning about safety properties of concurrent programs are discussed and implications for program design noted. The relationship between interference freedom and synchronization mechanisms is described. The methods are illustrated with a number of examples, including partial correctness of a bank simulation, and mutual exclusion, non-blocking, and deadlock freedom of a solution to the critical section problem.

These notes are excerpted from Concurrent Programming: Centralized and Distributed, by G.R. Andrews and F.B. Schneider, in preparation.

Supported by NSF grant DCR-8320274, a grant from the Office of Naval Research, and and IBM Faculty Development Award.

Supported by NSF grant DCR-8402090.

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. Alpern, B., and F.B. Schneider. Defining liveness. Information Processing Letters 21, (Oct. 1985), 181–185.

    Google Scholar 

  2. Andrews, G. and F.B. Schneider. Concepts and notations for concurrent programming. ACM Computing Surveys 15, 1 (March 1983), 3–43.

    Google Scholar 

  3. Ashcroft, E. Proving Assertions about Parallel Programs. Journal of Computer and System Sciences 10 1 (Feb. 1975), 110–135.

    Google Scholar 

  4. Ashcroft, E. Program verification tableaus. Technical Report CS-76-01. University of Waterloo, Waterloo, Ontario, Canada, Jan. 1976.

    Google Scholar 

  5. Ashcroft, E., and Z. Manna. Formalization of properties of parallel programs. Machine Intelligence 6, (1971), Edinburgh University Press, 17–41.

    Google Scholar 

  6. Barringer, Howard. A Survey of Verification Techniques for Parallel Programs. Lecture Notes in Computer Science Volume 191, Springer-Verlag, New York, 1985.

    Google Scholar 

  7. Ben Ari, M. Principles of Concurrent Programming. Prentice Hall International, Englewood Cliffs, N.J., 1982.

    Google Scholar 

  8. Brinch Hansen, P. Concurrent programming concepts. ACM Computing Surveys 5, 4 (Dec. 1973), 223–245.

    Google Scholar 

  9. Brinch Hansen, P. The Architecture of Concurrent Programs, Prentice Hall, Englewood Cliffs, N.J., 1977.

    Google Scholar 

  10. Burstall, R.M. Proving properties of programs by structural induction. Experimental Programming Reports, No. 17. DMIP, Edinburgh, 1968.

    Google Scholar 

  11. Clint, M. Program proving: Coroutines. Acta Informatica 2, 1 (1973), 50–63.

    Google Scholar 

  12. Constable, R.L. and M.J. O'Donnell. A Programming Logic. Winthrop Publishers, Cambridge, Mass., 1978.

    Google Scholar 

  13. de Bakker, J.W. Axiomatics of simple assignment statements. M.R. 94, Mathematisch Centrum, Amsterdam, 1968.

    Google Scholar 

  14. Dijkstra, E.W. A personal summary of the Gries-Owicki theory. EWD 554, in Selected Writings on Computing: A Personal Perspective, E.W. Dijkstra, Springer Verlag, New York, 1982.

    Google Scholar 

  15. On making solutions more and more fine-grained. EWD 622, in Selected Writings on Computing: A Personal Perspective, E.W. Dijkstra, Springer Verlag, New York, 1982.

    Google Scholar 

  16. Dijkstra, E.W. An Assertional Proof of a Protocol by G.L. Peterson. Technical Report EWD 779, Burroughs, Corp. Feb. 1981.

    Google Scholar 

  17. Fillman, R.E. and D.P. Friedman. Coordinated Computing Tools and Techniques for Distributed Software. McGraw Hill, New York, New York, 1983.

    Google Scholar 

  18. Floyd, R.W. Assigning meanings to programs. Proc. of Symposia in Applied Mathematics 19, 1967, 19–31.

    Google Scholar 

  19. Francez, N. Fairness. To appear. Springer Verlag, New York, 1986.

    Google Scholar 

  20. Goldstine, H.H. and J. von Neumann. Planning and coding of problems for an electronic computing instrument. Report for U.S. Ord. Dept. In A. Taub (ed.) Collected Works of J. von Neumann, New York, Pergamon, Vol. 5, 1965, 80–151.

    Google Scholar 

  21. Gries, D. The multiple assignment statement. IEEE Trans. on Software Engineering SE-4, 2 (March 1978), 87–93.

    Google Scholar 

  22. Halpern, Brent T. Verifying Concurrent Processes Using Temporal Logic. Lecture Notes in Computer Science Volume 129, Springer-Verlag, New York, 1982.

    Google Scholar 

  23. Hoare, C.A.R. An axiomatic basis for computer programming. CACM 12, 10 (Oct. 1969), 576–580.

    Google Scholar 

  24. Hoare, C.A.R. Towards a theory of parallel programming. In Operating Systems Techniques, C.A.R. Hoare and R. Perrot (eds.), Academic Press, New York, 1972.

    Google Scholar 

  25. Hoare, C.A.R. Parallel programming: An axiomatic approach. Computer Languages 1, 1975, Pergamon Press, 151–160.

    Google Scholar 

  26. Hoare, C.A.R. Communicating Sequential Processes. Prentice Hall, International, New Jersey, 1985.

    Google Scholar 

  27. Concurrent Euclid, The UNIX System, and Tunis. Addison-Wesley, Reading, Mass., 1983.

    Google Scholar 

  28. Holt, R.C., G.S. Graham, E.D. Lazowska, and M.A. Scott. Structured Concurrent Programming with Operating Systems Applications. Addison-Wesley, Reading, Mass., 1978.

    Google Scholar 

  29. Igarashi, S. An axiomatic approach to equivalence problems of algorithms with applications. Ph.D. thesis, University of Tokoyo, 1964.

    Google Scholar 

  30. Lamport, L. Towards a theory of correctness for multi-user data base systems. Technical Report CA-7610-0712, Massachusetts Computer Associates, Wakefield, Mass., Oct. 1976.

    Google Scholar 

  31. Lamport, L. Proving the correctness of multiprocess programs. IEEE Trans. on Software Engineering SE-3, 2 (March 1977), 125–143.

    Google Scholar 

  32. Lamport, L. The “Hoare Logic” of concurrent programs. Acta Informatica 14, (1980), 21–37.

    Google Scholar 

  33. The “Hoare Logic” of CSP and all that. ACM TOPLAS 6, 2 (April 1984), 281–296.

    Google Scholar 

  34. Lamport, L. Logical foundation. In Distributed Systems—Methods and Tools for Specification. (M. Paul and H.J. Siegert eds.), Lecture Notes in Computer Science Volume 190, Springer-Verlag, New York, 1985.

    Google Scholar 

  35. Lehman, D., A. Pnueli, and J. Stavi. Impartiality, justice and fairness: The ethics of concurrent termination. Proc. Eighth Colloquium on Automata, Languages and Programming, Lecture Notes in Computer Science Volume 115, Springer-Verlag, 1981, 264–277.

    Google Scholar 

  36. Levitt, K.N. The application of program-proving techniques to the verification of synchronization processes. Proc. AFIPS Fall Joint Computer Conference, AFIPS Press, 1972, 33–47.

    Google Scholar 

  37. McCarthy, J. Towards a mathematical science of computation. Proc IFIP Congress 1962, North Holland, Amsterdam, 1962, 21–28.

    Google Scholar 

  38. Morris, F.L. and C.B. Jones. An early program proof by Alan Turing. Annals of the History of Computing 6, 2 (April 1984), 139–143.

    Google Scholar 

  39. Naur, P. Proof of algorithms by general snapshots. BIT 6, 4, 310–316.

    Google Scholar 

  40. Axiomatic proof techniques for parallel programs. Ph.D. Thesis, Computer Science Department, Cornell University, Ithaca, New York, 1975.

    Google Scholar 

  41. An axiomatic proof technique for parallel programs I. Acta Informatica 6, (1976), 319–340.

    Google Scholar 

  42. Paul, M. and H.J. Siegert (eds.). Distributed Systems—Methods and Tools for Specification. Lecture Notes in Computer Science Volume 190, Springer-Verlag, New York, 1985.

    Google Scholar 

  43. Peterson, G.L. Myths about the mutual exclusion problem. Information Processing Letters 12, 3 (June 1981), 115–116.

    Google Scholar 

  44. Turing, A.M. Checking a large routine. Report of a Conference on High Speed Automatic Calculating Machines, University Mathematics Laboratory, Cambridge, 67–69.

    Google Scholar 

  45. Yanov, Yu I. Logical operator schemes. Kybernetika 1 (1958).

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Department of Computer Science, Cornell University, 14853, Ithaca, New York, U.S.A.

    Fred B. Schneider

  2. Department of Computer Science, University of Arizona, 85721, Tucson, Arizona, U.S.A.

    Gregory R. Andrews

Authors
  1. Fred B. Schneider
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Gregory R. Andrews
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

J. W. de Bakker W. -P. de Roever G. Rozenberg

Rights and permissions

Reprints and permissions

Copyright information

© 1986 Springer-Verlag Berlin Heidelberg

About this chapter

Cite this chapter

Schneider, F.B., Andrews, G.R. (1986). Concepts for concurrent programming. In: de Bakker, J.W., de Roever, W.P., Rozenberg, G. (eds) Current Trends in Concurrency. Lecture Notes in Computer Science, vol 224. Springer, Berlin, Heidelberg. https://doi.org/10.1007/BFb0027049

Download citation

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

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-16488-3

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

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation