Reasoning about nonatomic operations

ABSTRACT

A method is presented that permits assertional reasoning about a concurrent program even though the atomicity of the elementary operations is left unspecified. It is based upon a generalization of the dynamic logic operator [α]. The method is illustrated by verifying the mutual exclusion property for a two-process version of the bakery algorithm.

REFERENCES

• 1: E. A. Ashcroft. Proving Assertions About Parallel Programs. J. Comput. Sys. Sci. 10 (Jan. 1975), 110-135.
• 2: David Harel, First-Order Dynamic Logic, Springer-Verlag New York, Inc., Secaucus, NJ, 1979
• 3: 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]
• 4: Robert M. Keller, Formal verification of parallel programs, Communications of the ACM, v.19 n.7, p.371-384, July 1976 [doi>10.1145/360248.360251]
• 5: Leslie Lamport, A new solution of Dijkstra's concurrent programming problem, Communications of the ACM, v.17 n.8, p.453-455, Aug. 1974 [doi>10.1145/361082.361093]
• 6: L. Lamport. Proving the Correctness of Multiprocess Programs. IEEE Trans. on Soft. Eng. SE-3 2, 2 (Mar. 1977), 125-143.
• 7: L. Lamport. The 'Hoare Logic' of Concurrent Programs. Acta Informatica 14 (1980), 21-37.
• 8: Leslie Lamport, Specifying Concurrent Program Modules, ACM Transactions on Programming Languages and Systems (TOPLAS), v.5 n.2, p.190-222, April 1983 [doi>10.1145/69624.357207]
• 9: 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]
• 10: S. Owicki and D. Gries. An Axiomatic Proof Technique for Parallel Programs. Acta Informatica 6, 4 (1976), 319-340.
• 11: Susan Owicki , Leslie Lamport, Proving Liveness Properties of Concurrent Programs, ACM Transactions on Programming Languages and Systems (TOPLAS), v.4 n.3, p.455-495, July 1982 [doi>10.1145/357172.357178]
• 12: A. Pnueli. The Temporal Logic of Programs. Proc. of the 18th Symposium on the Foundations of Computer Science, Nov. 1977, 46-57.