Constructing correct and efficient concurrent programs

ABSTRACT

A method is presented for programming correct and efficient cooperation in a set of sequential modules, on the basis of an invariant assertion, by means of formal and static deductions. For each sequential module, the pre- and post-assertions are computed from the invariant. Whereas the pre-assertion gives the synchronizing condition required before execution in order to preserve the invariant, the post-assertion expresses the “contribution” of this execution. Other assertions, called firing conditions, are derived which connect that contribution to the needs of waiting processes as expressed in their synchronizing conditions. A sequential module and its synchronizing and firing conditions are then integrated in a high-level synchronizing construct close to conditional critical regions, but allowing explicit control over the synchronizing conditions to be reevaluated at the exit for process resumption. Three levels of static elimination of useless condition reevaluations are then presented. These eliminations essentially use the information contained in firing conditions; they are shown to preserve partial correctness. The combined use of the notation and of the techniques proposed is illustrated through three examples.

REFERENCES

• 1: Brinch Hansen P. 1972. A comparison of two synchronizing concepts. Acta Informatica 1, 3 (1972), 190-199.
• 2: Per Brinch Hansen, Concurrent Programming Concepts, ACM Computing Surveys (CSUR), v.5 n.4, p.223-245, Dec. 1973 [doi>10.1145/356622.356624]
• 3: Per Brinch Hansen, Operating System Principles, Prentice Hall PTR, Upper Saddle River, NJ, 1973
• 4: Burstall R. 1974. Program proving as hand simulation with a little induction, Proc. IFIP Congress 74, North-Holland, 1974, 308-312.
• 5: Roy H. Campbell , A. Nico Habermann, The specification of process synchronization by path expressions, Operating Systems, Proceedings of an International Symposium, p.89-102, April 23-25, 1974
• 6: Cooprider L. W., P. J. Courtois, F. Heymans and D. L. Parnas 1974. Information streams sharing a finite buffer: other solutions, Information Processing Letters 3 (1974), 16-21.
• 7: Edsger W. Dijkstra, Letters to the editor: go to statement considered harmful, Communications of the ACM, v.11 n.3, p.147-148, March 1968 [doi>10.1145/362929.362947]
• 8: Dijkstra E. W. 1968b. A constructive approach to the problem of program correctness, BIT 8 (1968), 174-186.
• 9: Dijkstra E. W. 1968c. Cooperating sequential processes, in F. Genuys (ed.), Programming Languages, Academic Press, New York, 1968.
• 10: Dijkstra E. W. 1972. Information streams sharing a finite buffer, Information Processing Letters 1 (1972), 179-180.
• 11: Dijkstra E. W. 1974a. A simple axiomatic basis for programming language constructs, Indagationes Mathematicae 36 (1974), 1-15.
• 12: Dijkstra E. W. 1974b. Guarded commands, non-determinacy and a calculus for the derivation of programs, Rep. EWD418, Burroughs, The Netherlands, 1974.
• 13: Floyd R. W. 1967. Assigning meanings to programs, in J. T. Schwartz (ed.), Mathematical Aspects of computer science, Proc. Symp. Applied Maths, vol. 19, American Math. Soc., Providence, 1967.
• 14: Donald Irvin Good, Toward a man-machine system for proving program correctness, 1970
• 15: A. Nico Habermann, Synchronization of communicating processes, Communications of the ACM, v.15 n.3, p.171-176, March 1972 [doi>10.1145/361268.361277]
• 16: C. A. R. Hoare, An axiomatic basis for computer programming, Communications of the ACM, v.12 n.10, p.576-580, Oct. 1969 [doi>10.1145/363235.363259]
• 17: Hoare C. A. R. 1973a. Towards a theory of parallel programming, in C. A. R. Hoare and R. H. Perrott (eds), Operating Systems Techniques, Academic Press, New York, 1973.
• 18: Hoare C. A. R. 1973b. Recursive data structures, CS-73-400, Computer Sci. Dept., Stanford Univ., 1973.
• 19: C. A. R. Hoare, Monitors: an operating system structuring concept, Communications of the ACM, v.17 n.10, p.549-557, Oct. 1974 [doi>10.1145/355620.361161]
• 20: Shigeru Igarashi , Ralph L. London , David C. Luckham, Automatic program verification I: a logical basis and its implementation., Stanford University, Stanford, CA, 1973
• 21: James Cornelius King, A program verifier, 1970
• 22: Donald E. Knuth, Structured Programming with go to Statements, ACM Computing Surveys (CSUR), v.6 n.4, p.261-301, Dec. 1974 [doi>10.1145/356635.356640]
• 23: Levitt K. N. 1972. The application of program proving techniques to the verification of synchronization processes, AFIPS Proc. FJCC, vol.41, 1972, 33-47.
• 24: Michel Sintzoff, Calculating properties of programs by valuations on specific models, Proceedings of ACM conference on Proving assertions about programs, p.203-207, January 06-07, 1972, Las Cruces, New Mexico, United States

INDEX TERMS

Primary Classification:
  D. Software
  D.3 PROGRAMMING LANGUAGES
      D.3.3 Language Constructs and Features
          Subjects: Concurrent programming structures

Additional Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING
      D.2.3 Coding Tools and Techniques

General Terms:
Languages

Keywords:
Assertion generation, Concurrent programming, Correctness, Operating systems, Program construction, Run-time efficiency, Static optimization, Structured programming