Abstract
Already in Lamport’s bakery algorithm, integers are used for fair schedulers of concurrent processes. In this paper, we present the extension of a fair scheduler from ‘static control’ (the number of processes is fixed) to ‘dynamic control’ (the number of processes changes during execution). We believe that our results shed new light on the concept of fairness in the setting of dynamic control.
Chapter PDF
References
Apt, K.-R., Olderog, E.-R.: Verification of Sequential and Concurrent Programs, 2nd edn. Springer, Heidelberg (1997)
Bauer, J., Schaefer, I., Toben, T., Westphal, B.: Specification and verification of dynamic communication systems. In: Goossens, K., Petrucci, L. (eds.) ACSD, Turku, Finland. IEEE, Los Alamitos (2006)
Best, E.: Semantics of Sequential and Parallel Programs. Prentice Hall, Englewood Cliffs (1996)
Cook, B., Podelski, A., Rybalchenko, A.: Proving thread termination. In: PLDI. ACM Press, New York (2007)
Cousot, P., Cousot, R.: Abstract interpretation: A unified lattice model for static analysis of programs by construction or approximation of fixedpoints. In: POPL, pp. 238–252. ACM, New York (1977)
Dijkstra, E.W.: Guarded commands, nondeterminacy and formal derivation of programs. Comm. of the ACM 18, 453–457 (1975)
Francez, N.: Fairness. Springer, New York (1986)
Lamport, L.: A new solution of Dijkstra’s concurrent programming problem. Comm. of the ACM 17(8), 453–455 (1974)
Musuvathi, M., Quadeer, S.: Fair stateless model checking. In: PLDI (June 2008)
Olderog, E.R., Apt, K.R.: Fairness in parallel programs, the transformational approach. ACM TOPLAS 10, 420–455 (1988)
Plotkin, G.: A structural approach to operational semantics. J. of Logic and Algebraic Programming 60-61, 17–139 (2004)
Pnueli, A., Podelski, A., Rybalchenko, A.: Separating fairness and well-foundedness for the analysis of fair discrete systems. In: Halbwachs, N., Zuck, L.D. (eds.) TACAS 2005. LNCS, vol. 3440, pp. 124–139. Springer, Heidelberg (2005)
Podelski, A., Rybalchenko, A.: Transition invariants. In: LICS 2004, pp. 32–41. IEEE Computer Society, Los Alamitos (2004)
Podelski, A., Rybalchenko, A.: Transition predicate abstraction and fair termination. In: POPL, pp. 132–144. ACM, New York (2005)
Vardi, M.Y., Wolper, P.: An automata-theoretic approach to automatic program verification. In: LICS, pp. 332–344. IEEE Computer Society, Los Alamitos (1986)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2010 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Hoenicke, J., Olderog, ER., Podelski, A. (2010). Fairness for Dynamic Control. In: Esparza, J., Majumdar, R. (eds) Tools and Algorithms for the Construction and Analysis of Systems. TACAS 2010. Lecture Notes in Computer Science, vol 6015. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-12002-2_20
Download citation
DOI: https://doi.org/10.1007/978-3-642-12002-2_20
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-12001-5
Online ISBN: 978-3-642-12002-2
eBook Packages: Computer ScienceComputer Science (R0)