Fairness and the axioms of control predicates. (English) Zbl 0647.68014
Summary: Many recent axiomatic definitions for structured programming languages include control predicates, at (S), and after (S), which are an abstraction of location counters. The usual axioms identify control locations so as to imply that “no time” (i.e., no state transition) is needed to pass from the end of one statement to the next, and in particular from the end of a loop body back to the test at the head of the loop.
Here, an axiomatic framework for control predicates is examined. It is shown that if all the axioms are to be maintained with common representation mappings, there are difficult new requirements which need to be satisfied by an implementation for fair concurrent models of computation. Several approaches to resolving the difficulty are considered, and in particular it is suggested to replace some axiom of the form \(P\Rightarrow Q\) by \(P\Rightarrow eventually(Q)\), where P and Q are control predicates, thereby separating control states previously identified.
Here, an axiomatic framework for control predicates is examined. It is shown that if all the axioms are to be maintained with common representation mappings, there are difficult new requirements which need to be satisfied by an implementation for fair concurrent models of computation. Several approaches to resolving the difficulty are considered, and in particular it is suggested to replace some axiom of the form \(P\Rightarrow Q\) by \(P\Rightarrow eventually(Q)\), where P and Q are control predicates, thereby separating control states previously identified.
MSC:
| 68Q60 | Specification and verification (program logics, model checking, etc.) |
| 68Q65 | Abstract data types; algebraic specification |
| 68N25 | Theory of operating systems |
Keywords:
fairness; concurrency; axiomatic semantics; structured programming languages; control predicatesReferences:
| [1] | S. S. Owicki and L. Lamport, Proving Liveness of Concurrent Programs,ACM-TOPLAS Vol. 4, No. 3 (July 1982). · Zbl 0483.68013 |
| [2] | L. Lamport, An Axiomatic Semantics of Concurrent Programming Languages, in:Logics and Models of Concurrent Systems (K. R. Apt-ed), Springer Verlag (1985). · Zbl 0582.68006 |
| [3] | L. Lamport, Control Predicates are Better than Dummy Variables for Reasoning about Program Control,ACM-TOPLAS, Vol. 10, No. 2, (April 1988). |
| [4] | L. Lamport, What It Means for a Concurrent Program to Satisfy a Specification: Why No One has Specified Priority,Proceedings of the 12th ACM-POPL, New Orleans (January 1985). |
| [5] | E. W. Dijkstra,A Discipline of Programming, Prentice Hall (1976). · Zbl 0368.68005 |
| [6] | N. Francez,Fairness, Springer Verlag (1986). |
| [7] | K. A. Apt and C. Delporte-Gallet, Syntax Directed Analysis of Liveness Properties of While Programs,Information and Control 68:223-253 (1986). · Zbl 0591.68016 · doi:10.1016/S0019-9958(86)80037-7 |
| [8] | C. A. R. Hoare, Communicating Sequential Processes,CACM Vol. 21, No. 8 (August 1978). · Zbl 0383.68028 |
| [9] | K. R. Apt, L. Bouge, and Ph. Clermont, Two Normal Form Theorems for CSP Programs,Information Processing Letters,26:165-171 (December 1987). · Zbl 0631.68026 · doi:10.1016/0020-0190(87)90001-9 |
| [10] | R. Kuiper and W. P. deRoever, Fairness Assumptions for CSP in a Temporal Logic Framework, TC2 Working Conference, Garmisch, W. Germany (June 1982). |
| [11] | O. Grumberg, N. Francez, and S. Katz, Fair Termination of Communicating Processes,Proceedings 3rd ACM-PODC, Vancouver, BC (August 1984). |
| [12] | S. Katz and D. Peled, Interleaving Set Temporal Logic,Proceedings of the 6th ACM-PODC, Vancouver, B.C. (August 1987). · Zbl 0718.03014 |
| [13] | E.-R. Olderog and K. R. Apt, Fairness in Parallel Programs: The Transformational Approach, TR8402, Inst. of Inf., Kiel U. (1984), in ACM-TOPLAS (to appear). · Zbl 0558.68015 |
| [14] | S. S. Owicki and D. Gries, An Axiomatic Proof Technique for Parallel Programs,Acta Informatica Vol. 6 (1976). · Zbl 0312.68011 |
| [15] | A. Pnueli, Application of Temporal Logic to the Specification and Verification of Reactive Systems, in:Current Trends in Concurrency (eds.) J. W. deBakker, W. P. deRoever, and G. Rozenberg, LNCS 244, Springer Verlag (1986). · Zbl 0607.68022 |
| [16] | R. J. J. Back and K. Kurki-Suonio, Serializability in Distributed Systems with Handshaking, TR CMU-CS-85-109, Carnegie-Mellon University, Pittsburgh (1985). · Zbl 0649.68020 |
| [17] | K. R. Apt, N. Francez, and S. Katz, Appraising Fairness in Languages for Distributed Programming,Proceedings of the 14th ACM Symposium on Principles of Programming Languages, Munich, West Germany (April 1987), also inDistributed Computing (to appear). · Zbl 0659.68023 |
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.
