Abstract
In basic action systems, the choice among actions is not restricted. Fairness can be imposed to restrict this nondeterminism. Finitary fairness has been proposed as a further restriction of fairness: it models implementations closer, and allows problems to be solved for which standard fairness is not sufficient. We propose a method for expressing finitary fairness in action systems. We give two general transformations from a system in which some actions are marked as fair, into an equivalent system without fair actions. A theoretical justification is given, and the transformations are illustrated with two examples: alternating bit protocol and distributed consensus. The examples are developed by stepwise refinement in Event-B and are mechanically checked.
Access provided by Autonomous University of Puebla. Download to read the full chapter text
Chapter PDF
Similar content being viewed by others
References
Back, R.J.R.: Refinement calculus, part II: Parallel and reactive programs. In: de Bakker, J.W., de Roever, W.-P., Rozenberg, G. (eds.) REX 1989. LNCS, vol. 430, pp. 67–93. Springer, Heidelberg (1990)
Abrial, J.R.: Modeling in Event-B: System and Software Engineering. Cambridge University Press (2010)
Alur, R., Henzinger, T.A.: Finitary fairness. ACM Trans. Program. Lang. Syst. 20(6), 1171–1194 (1998)
Abrial, J.-R., Butler, M., Hallerstede, S., Voisin, L.: An open extensible tool environment for event-B. In: Liu, Z., Kleinberg, R.D. (eds.) ICFEM 2006. LNCS, vol. 4260, pp. 588–605. Springer, Heidelberg (2006)
Chandy, K.M., Misra, J.: Parallel Program Design: A Foundation. Addison-Wesley (1988)
Francez, N.: Fairness. Texts and Monographs in Computer Science. Springer (1986)
Lamport, L.: The temporal logic of actions. ACM Transactions on Programming Languages and Systems 16(3), 872–923 (1994)
Back, R., Xu, Q.: Refinement of fair action systems. Acta Informatica 35(2), 131–165 (1998)
Singh, A.K.: Program refinement in fair transition systems. Acta Informatica 30, 503–535 (1993)
Wabenhorst, A.: Stepwise development of fair distributed systems. Acta Informatica 39, 233–271 (2003)
Apt, K.R., Olderog, E.R.: Proof rules and transformations dealing with fairness. Sci. Comput. Program. 3(1), 65–100 (1983)
Fischer, M., Lynch, N., Paterson, M.: Impossibility of distributed consensus with one faulty process. Journal of the ACM 32, 374–382 (1985)
Bartlett, K.A., Scantlebury, R.A., Wilkinson, P.T.: A note on reliable full-duplex transmission over half-duplex links. Communications of the ACM 12(5), 260–261 (1969)
Wabenhorst, A.: A stepwise development of the alternating bit protocol. Technical Report PRG-TR-12-97, Oxford University Computing Laboratory (March 1997)
Feijen, W.H.J., van Gasteren, A.J.M.: On a Method of Multiprogramming. Springer (1999)
Sekerinski, E.: An algebraic approach to refinement with fair choice. Electronic Notes in Theoretical Computer Science 214, 51–79 (2008)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2013 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Sekerinski, E., Zhang, T. (2013). Finitary Fairness in Action Systems. In: Liu, Z., Woodcock, J., Zhu, H. (eds) Theoretical Aspects of Computing – ICTAC 2013. ICTAC 2013. Lecture Notes in Computer Science, vol 8049. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-39718-9_19
Download citation
DOI: https://doi.org/10.1007/978-3-642-39718-9_19
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-39717-2
Online ISBN: 978-3-642-39718-9
eBook Packages: Computer ScienceComputer Science (R0)