Control predicates are better than dummy variables for reasoning about program control

ABSTRACT

When explicit control predicates rather than dummy variables are used, the Owicki-Gries method for proving safety properties of concurrent programs can be strengthened, making it easier to construct the required program annotations.

REFERENCES

• 1: ASHCROFT, E. Proving assertions about parallel programs. J. Comput. $ystm. $ci. 10 (Jan. 1975), 110-135.
• 2: DIJKSTRA, E. W. Misra's proof for Lamport's mutual exclusion. Nov. 1985. EWD948.
• 3: FLOYD, R. W. Assigning meanings to programs. In Proceedings of the Symposium on Applied Math., Vol. 19 (1967), American Mathematical Society, pp. 19-32.
• 4: 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]
• 5: L. Lamport, An axiomatic semantics of concurrent programming languages, Logics and models of concurrent systems, Springer-Verlag New York, Inc., New York, NY, 1989
• 6: LAMPORT, L. A fast mutual exclusion algorithm. 1985. Submitted for publication.
• 7: LAMPORT, L. The 'Hoare logic' of concurrent programs. Acta Inf. ld, i (1980), 21-37.
• 8: LAMPORT, L. Proving the correctness of multiprocess programs. IEEE Trans. Softw. Eng. SE-3, 2 (March 1977), 125-143.
• 9: Leslie Lamport , Fred B. Schneider, Constraints: a uniform approach to aliasing and typing, Proceedings of the 12th ACM SIGACT-SIGPLAN symposium on Principles of programming languages, p.205-216, January 14-16, 1985, New Orleans, Louisiana, United States [doi>10.1145/318593.318640]
• 10: Leslie Lamport , Fred B. Schneider, The ``Hoare Logic'' of CSP, and All That, ACM Transactions on Programming Languages and Systems (TOPLAS), v.6 n.2, p.281-296, April 1984 [doi>10.1145/2993.357247]
• 11: OWICKI, S., AND GRIES, D. An axiomatic proof technique for parallel programs. Acta Inf. 6, 4 (1976), 319-340.
• 12: F B Schneider , G R Andrews, Concepts for concurrent programming, Current trends in concurrency. Overviews and tutorials, Springer-Verlag New York, Inc., New York, NY, 1986

INDEX TERMS

Primary Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING
      D.2.4 Software/Program Verification
          Subjects: Correctness proofs

Additional Classification:
  F. Theory of Computation
  F.3 LOGICS AND MEANINGS OF PROGRAMS

General Terms:
Theory, Verification