Abstract
The notion of equifairness, strengthening the familiar notion of fairness, is introduced as a scheduling policy of non-determinism and concurrency. Under this notion, it is infinitely often the case that the number of selections of each of a family of infinitely-often jointly-enabled processes is equal. A proof rule for proving strong equifair-termination is introduced, applied to examples and shown to be (semantically) complete.
Typed by: Barbara J. White
World-trade Visiting Scientist on a sabbatical leave from the Technion, Haifa, Israel. (Work of the 2nd author was partially supported by the Fund for Aiding Research, The Technion)
This is a preview of subscription content, log in via an institution to check access.
Preview
Unable to display preview. Download preview PDF.
References
K.R. Apt and E.R. Olderog, Proof Rules and Transformations Dealing with Fairness, TR 82-47, LITP, University of Paris 7, October 1982. To appear in Science of Computer Programming.
K.R. Apt, A. Pnueli and J. Stavi, Fair Termination Revisited with Delay, Proceedings of 2nd conference on foundations of software technology and theoretical computer science (FST-TCS), Bangalore, India, December 1982. Also: TR 82-51, LITP, Univ. of Paris 7, October 1982.
E.W. Dijkstra, A Discipline of Programming, Prentice Hall, Englewood Cliffs, N.J., 1976.
O. Grümberg, N. Francez, A complete proof-rule for (weak) equifairness. IBM T.J. Watson Research Center RC-9634, October 1982 (submitted for publication).
O. Grümberg, N. Francez, J.A. Makowsky and W.P. de Roever, A Proof Rule for Fair Termination of Guarded Commands, Proc. of the Int. Symp. on Algorithmic Languages, Amsterdam, October 1981, North-Holland, 1981.
D. Lehmann, A. Pnueli and J. Stavi, Impartiality, Justice and Fairness: the Ethics of Concurrent Termination, Proc. ICALP 81, in: Lecture notes in computer science 115 (S. Even, O. Kariv — eds.), Springer 1981.
D. Park, A Predicate Transformer for Weak Fair Iteration, Proc. 6 IBM Symp. on Math. Foundation of Computer Science, Hakone, Japan, 1981.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1984 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Grümberg, O., Francez, N., Katz, S. (1984). A complete proof rule for strong equifair termination. In: Clarke, E., Kozen, D. (eds) Logics of Programs. Logic of Programs 1983. Lecture Notes in Computer Science, vol 164. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-12896-4_367
Download citation
DOI: https://doi.org/10.1007/3-540-12896-4_367
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-12896-0
Online ISBN: 978-3-540-38775-6
eBook Packages: Springer Book Archive