[go: up one dir, main page]
Skip to main content
Springer Nature Link
Log in

CCS: It’s not fair!

Fair schedulers cannot be implemented in CCS-like languages even under progress and certain fairness assumptions

  • Original Article
  • Published:
Acta Informatica Aims and scope Submit manuscript

Abstract

In the process algebra community it is sometimes suggested that, on some level of abstraction, any distributed system can be modelled in standard process-algebraic specification formalisms like CCS. This sentiment is strengthened by results testifying that CCS, like many similar formalisms, is Turing powerful and provides a mechanism for interaction. This paper counters that sentiment by presenting a simple fair scheduler—one that in suitable variations occurs in many distributed systems—of which no implementation can be expressed in CCS, unless CCS is enriched with a fairness assumption. Since Dekker’s and Peterson’s mutual exclusion protocols implement fair schedulers, it follows that these protocols cannot be rendered correctly in CCS without imposing a fairness assumption. Peterson expressed this algorithm correctly in pseudocode without resorting to a fairness assumption, so it furthermore follows that CCS lacks the expressive power to accurately capture such pseudocode.

This is a preview of subscription content, log in via an institution to check access.

Access this article

Log in via an institution

Subscribe and save

Springer+ Basic
$34.99 /Month
  • Get 10 units per month
  • Download Article/Chapter or eBook
  • 1 Unit = 1 Article or 1 Chapter
  • Cancel anytime
Subscribe now

Buy Now

Price excludes VAT (USA)
Tax calculation will be finalised during checkout.

Instant access to the full article PDF.

Institutional subscriptions

Fig. 1

Similar content being viewed by others

Notes

  1. In [4] a form of reasoning using a particularly strong global fairness assumption was integrated in the axiomatic framework of ACP, and shown to be compatible with the notion of weak bisimulation commonly taken as the semantic basis for CCS.

  2. The process \(E'\) with \(E' \mathop {=}\limits ^{{ def}} a.a.E' + b.0\) on the other hand really needs strong fairness.

  3. Also known as First Come First Served (FCFS).

  4. http://en.wikipedia.org/wiki/Scheduling_(computing).

  5. http://en.wikipedia.org/wiki/Completely_Fair_Scheduler.

  6. This relaxed requirement only serves to increase the range of acceptable schedulers, thereby strengthening our impossibility result. It by no means rules out a scheduler that schedules task \(t_1\) exactly once for each request \(r_1\) received.

  7. Our specification places no restrictions on the presence or absence of any additional occurrences of \(e\). This again increases the range of acceptable implementations.

  8. When assuming that this formula holds, \(F_{0}\) trivially satisfies the other properties required in Sect. 7: the system will always return to a state where it remains ready to accept the next request \(r\) until it arrives; in any partial run there are no more occurrences of \(t\) than of \(r\), and between each two occurrences of \(t\) the action \(e\) is scheduled.

  9. The output and internal actions of CCS\(^!\) are similar to the output and internal action of I/O automata [39]. However, the remaining actions of I/O automata are input actions that are totally under the control of the environment of the modelled system. In CCS, on the other hand, the default type of action is a synchronisation that can happen only in cooperation between a system and its environment.

  10. When assuming that these formulas hold, \(F_1|F_2\) trivially satisfies the other properties required of it: the system will always return to a state where it remains ready to accept the next request \(r_i\) until it arrives—hence for any numbers \(n_1\) and \(n_2\in \mathbb {N}\cup \{\infty \}\) there is at least one run of the system in which exactly that many requests of type \(r_1\) and \(r_2\) are received—and in any partial run there are no more occurrences of \(t_i\) than of \(r_i\).

  11. By definition \(Y\) does not contain non-blocking action.

  12. The CCS process \(a.0 | b.0\) has two transitions labelled \(a\), namely \(a.0 | b.0 \mathrel {\xrightarrow {\,\, a \,\,}} 0|b.0\) and \(a.0 | 0 \mathrel {\xrightarrow {\,\, a \,\,}} 0|0\). The only difference between these two transitions is that one occurs before the action \(b\) is performed by the parallel component and the other afterwards. In [57] we formalise a notion of an abstract transition that identifies these two concrete transitions.

  13. We only give the liveness property for process A; the one for process B is similar.

  14. Whether weak fairness suffices depends on the interpretation of enabledness (cf. Sect. 2).

  15. It differs in a crucial way, however, namely by treating each action as output. As a consequence, under fairness of actions the process \(F_1|F_2\) of Sect. 10 is guaranteed to perform each of the actions \(r_1\) and \(r_2\) infinitely often. To model a protocol where the action \(r_i\) is not forced to occur, a \(\tau \)-loop is inserted at each location where \(r_{i}\) is enabled.

  16. Fairness of components is a form of weak fairness, requiring that if a component from some point onwards is enabled in each state, an action from that component will eventually be scheduled. Here a component is enabled if an action from that component is enabled, possibly in synchronisation with an action from outside that component. Under this notion of fairness, the system \(E\) from Sect. 2, defined by \(E \mathop {=}\limits ^{{ def}} a.E + b.0\), is not ensured to do a \(b\) eventually. However, the composition \((E|\bar{b}.c.0)\backslash b\) is ensured to do a \(c\) eventually, because the component \(\bar{b}.c.0\) is enabled in every state.

  17. Here, we slightly deviate from standard notation [52], where \({}^\bullet u\) and \({u}^\bullet \) are usually plain sets, obtained from our multisets by abstracting from the multiplicities of their elements. We prefer to retain this information, so as to shorten various formulas.

References

  1. Aceto, L., Ingólfsdóttir, A., Larsen, K.G., Srba, J.: Modelling mutual exclusion algorithms. In: Reactive Systems: Modelling, Specification and Verification, pp. 142–158. Cambridge University Press (2007). doi:10.1017/CBO9780511814105.008

  2. Apt, K.R., Francez, N., Katz, S.: Appraising fairness in languages for distributed programming. Distrib. Comput. 2(4), 226–241 (1988). doi:10.1007/BF01872848

    Article  MATH  Google Scholar 

  3. Baeten, J.C.M., Bergstra, J.A.: Discrete time process algebra. Form. Asp. Comput. 8(2), 188–208 (1996). doi:10.1007/BF01214556

    Article  MATH  Google Scholar 

  4. Baeten, J.C.M., Bergstra, J.A., Klop, J.W.: On the consistency of Koomen’s fair abstraction rule. Theor. Comput. Sci. 51(1/2), 129–176 (1987). doi:10.1016/0304-3975(87)90052-1

    Article  MATH  MathSciNet  Google Scholar 

  5. Baeten, J.C.M., Bergstra, J.A., Klop, J.W.: Ready-trace semantics for concrete process algebra with the priority operator. Comput. J. 30(6), 498–506 (1987). doi:10.1093/comjnl/30.6.498

    Article  MATH  MathSciNet  Google Scholar 

  6. Baeten, J.C.M., Luttik, B., van Tilburg, P.: Reactive turing machines. In: Owe, O., Steffen, M., Telle, J.A. (eds.) Fundamentals of Computation Theory, pp. 348–359 (2011). doi:10.1007/978-3-642-22953-4_30

  7. Bergstra, J.A., Klop, J.W.: Algebra of communicating processes. In: de Bakker, J.W., Hazewinkel, M., Lenstra, J.K. (eds.) Mathematics and Computer Science, CWI Monograph 1, pp. 89–138. North-Holland, Amsterdam (1986)

    Google Scholar 

  8. Bergstra, J.A., Klop, J.W.: Verification of an alternating bit protocol by means of process algebra. In: Bibel, W., Jantke, K.P. (eds.) Mathematical Methods of Specification and Synthesis of Software Systems ’85, LNCS, vol. 215, pp. 9–23. Springer, Berlin (1986). doi:10.1007/3-540-16444-8_1

    Chapter  Google Scholar 

  9. Bolognesi, T., Brinksma, E.: Introduction to the ISO specification language LOTOS. Comput. Netw. 14, 25–59 (1987). doi:10.1016/0169-7552(87)90085-7

    Google Scholar 

  10. Bouali, A.: Weak and branching bisimulation in Fctool. Research Report RR-1575, Inria-Sophia Antipolis (1992). https://hal.inria.fr/inria-00074985/document

  11. Brookes, S.D., Hoare, C.A.R., Roscoe, A.W.: A theory of communicating sequential processes. J. ACM 31(3), 560–599 (1984). doi:10.1145/828.833

    Article  MATH  MathSciNet  Google Scholar 

  12. Cleaveland, R., Lüttgen, G., Natarajan, V.: Priority in process algebra. In: Bergstra, J.A., Ponse, A., Smolka, S.A. (eds.) Handbook of Process Algebra, chapter 12, pp. 711–765. Elsevier, Amsterdam (2001). doi:10.1016/B978-044482830-9/50030-8

    Chapter  Google Scholar 

  13. Corradini, F., Di Berardini, M.R., Vogler, W.: Fairness of actions in system computations. Acta Inform. 43(2), 73–130 (2006). doi:10.1007/s00236-006-0011-2

    Article  MATH  MathSciNet  Google Scholar 

  14. Corradini, F., Di Berardini, M.R., Vogler, W.: Liveness of a mutex algorithm in a fair process algebra. Acta Inform. 46(3), 209–235 (2009). doi:10.1007/s00236-009-0092-9

    Article  MATH  MathSciNet  Google Scholar 

  15. Corradini, F., Di Berardini, M.R., Vogler, W.: Time and fairness in a process algebra with non-blocking reading, LNCS. In: Nielsen, M., Kucera, A., Miltersen, P.B., Palamidessi, C., Tuma, P., Valencia, F.D. (eds.) Theory and Practice of Computer Science (SOFSEM’09), vol. 5404, pp. 193–204. Springer, Berlin (2009). doi:10.1007/978-3-540-95891-8_20

    Google Scholar 

  16. Corradini, F., Vogler, W., Jenner, L.: Comparing the worst-case efficiency of asynchronous systems with PAFAS. Acta Inform. 38(11/12), 735–792 (2002). doi:10.1007/s00236-002-0094-3

    Article  MATH  MathSciNet  Google Scholar 

  17. Costa, G., Stirling, C.: A fair calculus of communicating systems. Acta Inform. 21, 417–441 (1984). doi:10.1007/BF00271640

    Article  MATH  MathSciNet  Google Scholar 

  18. Costa, G., Stirling, C.: Weak and strong fairness in CCS. Inf. Comput. 73(3), 207–244 (1987). doi:10.1016/0890-5401(87)90013-7

    Article  MATH  MathSciNet  Google Scholar 

  19. Degano, P., De Nicola, R., Montanari, U.: CCS is an (augmented) contact free C/E system. In: Zilli, M.V. (ed.) Mathematical Models for the Semantics of Parallelism, LNCS, vol. 280, pp. 144–165. Springer, Berlin (1987). doi:10.1007/3-540-18419-8_13

    Chapter  Google Scholar 

  20. Dijkstra, E.W.: Over de sequentialiteit van procesbeschrijvingen (1962 or 1963). http://www.cs.utexas.edu/users/EWD/ewd00xx/EWD35.PDF. Circulated privately

  21. Dijkstra, E.W.: Cooperating sequential processes. In: Genuys, F. (ed.) Programming Languages: NATO Advanced Study Institute, pp. 43–112. Academic Press, London (1968)

    Google Scholar 

  22. Esparza, J., Bruns, G.: Trapping mutual exclusion in the box calculus. Theor. Comput. Sci. 153(1–2), 95–128 (1996). doi:10.1016/0304-3975(95)00119-0

    Article  MATH  MathSciNet  Google Scholar 

  23. Fehnker, A., van Glabbeek, R.J., Höfner, P., McIver, A.K., Portmann, M., Tan, W.L.: A process algebra for wireless mesh networks used for modelling, verifying and analysing AODV. Technical Report 5513, NICTA (2013). http://arxiv.org/abs/1312.7645

  24. Francez, N.: Fairness. Springer, Berlin (1986). doi:10.1007/978-1-4612-4886-6

    Book  MATH  Google Scholar 

  25. Gabbay, D.M., Pnueli, A., Shelah, S., Stavi, J.: On the temporal analysis of fairness. In: Abrahams, P.W., Lipton, R.J., Bourne, S.R. (eds.) Principles of Programming Languages (POPL ’80), pp. 163–173. ACM, New York (1980). doi:10.1145/567446.567462

    Google Scholar 

  26. Goldin, D.Q., Smolka, S.A., Attie, P.C., Sonderegger, E.L.: Turing machines, transition systems, and interaction. Inf. Comput. 194(2), 101–128 (2004). doi:10.1016/j.ic.2004.07.002

    Article  MATH  MathSciNet  Google Scholar 

  27. Gorla, D.: Towards a unified approach to encodability and separation results for process calculi. Inf. Comput. 208(9), 1031–1053 (2010). doi:10.1016/j.ic.2010.05.002

    Article  MATH  MathSciNet  Google Scholar 

  28. Groote, J.F., Ponse, A.: The syntax and semantics of \(\mu \)CRL. In: Ponse, A., Verhoef, C., van Vlijmen, S.F.M. (eds.) Algebra of Communicating Processes ’94, Workshops in Computing, pp. 26–62. Springer, Berlin (1995). doi:10.1007/978-1-4471-2120-6_2

    Chapter  Google Scholar 

  29. Hansson, H., Jonsson, B.: A calculus for communicating systems with time and probabitilies. In: Real-Time Systems Symposium (RTSS ’90), pp. 278–287. IEEE Computer Society (1990). doi:10.1109/REAL.1990.128759

  30. Hennessy, M., Regan, R.: A process algebra for timed systems. Inf. Comput. 117(2), 221–239 (1995). doi:10.1006/inco.1995.1041

    Article  MATH  MathSciNet  Google Scholar 

  31. Hoare, C.A.R.: Communicating Sequential Processes. Prentice Hall, Englewood Cliffs (1985)

    MATH  Google Scholar 

  32. Kindler, E., Walter, R.: Mutex needs fairness. Inf. Process. Lett. 62(1), 31–39 (1997). doi:10.1016/S0020-0190(97)00033-1

    Article  MathSciNet  Google Scholar 

  33. Kleinrock, L.: Analysis of a time-shared processor. Naval Res. Logist. Q. 11(1), 59–73 (1964). doi:10.1002/nav.3800110105

    Article  MATH  MathSciNet  Google Scholar 

  34. Lamport, L.: The temporal logic of actions. ACM Trans. Program. Lang. Syst. 16(3), 872–923 (1994). doi:10.1145/177492.177726

    Article  Google Scholar 

  35. Lauer, P.E., Torrigiani, P.R., Shields, M.W.: COSY: a system specification language based on paths and processes. Acta Inform. 12, 109–158 (1979). doi:10.1007/BF00266047

    Article  MATH  Google Scholar 

  36. van Leeuwen, J., Wiedermann, J.: Beyond the turing limit: evolving interactive systems. In: Pacholski, L., Ruzicka, P. (eds.) Theory and Practice of Informatics (SOFSEM ’01), LNCS, vol. 2234, pp. 90–109. Springer, Berlin (2001). doi:10.1007/3-540-45627-9_8

    Chapter  Google Scholar 

  37. Lehmann, D.J., Pnueli, A., Stavi, J.: Impartiality, justice and fairness: the ethics of concurrent termination. In: Even, S., Kariv, O. (eds.) Automata, Languages and Programming (ICALP), LNCS, vol. 115, pp. 264–277. Springer, Berlin (1981). doi:10.1007/3-540-10843-2_22

    Chapter  Google Scholar 

  38. Lüttgen, G., Vogler, W.: A faster-than relation for asynchronous processes. In: Larsen, K.G., Nielsen, M. (eds.) Concurrency Theory (CONCUR ’01), LNCS, vol. 2154, pp. 262–276. Springer (2001). doi:10.1007/3-540-44685-0_18

  39. Lynch, N., Tuttle, M.: An introduction to input, output automata. CWI-Quarterly. 2(3), 219–246. Centrum Voor Wiskunde en Informatica. Amsterdam, The Netherlands (1989)

  40. Milner, R.: Communication and Concurrency. Prentice Hall, Englewood Cliffs (1989)

    MATH  Google Scholar 

  41. Milner, R., Parrow, J., Walker, D.: A calculus of mobile processes, Part I + II. Inf. Comput. 100(1), 1–77 (1992). doi:10.1016/0890-5401(92)90008-4

    Article  MATH  MathSciNet  Google Scholar 

  42. Nagle, J.: On packet switches with infinite storage. RFC 970, Network Working Group (1985). http://tools.ietf.org/rfc/rfc970.txt

  43. Nagle, J.: On packet switches with infinite storage. IEEE Trans. Commun. 35(4), 435–438 (1987). doi:10.1109/TCOM.1987.1096782

    Article  Google Scholar 

  44. Olderog, E.-R.: Nets, Terms and Formulas: Three Views of Concurrent Processes and their Relationship. No. 23 in Cambridge Tracts in Theoretical Computer Science. Cambridge University Press, Cambridge (1991)

    Book  Google Scholar 

  45. Parrow, J.: Expressiveness of process algebras. ENTCS 209, 173–186 (2008). doi:10.1016/j.entcs.2008.04.011

    MathSciNet  Google Scholar 

  46. Peterson, G.L.: Myths about the mutual exclusion problem. Inf. Process. Lett. 12(3), 115–116 (1981). doi:10.1016/0020-0190(81)90106-X

    Article  MATH  Google Scholar 

  47. Plotkin, G.D.: A powerdomain for countable non-determinism (extended abstract). In: Nielsen, M., Schmidt, E.M. (eds.) Automata, Languages and Programming (ICALP ’82), LNCS, vol. 140, pp. 418–428. Springer, Berlin (1982). doi:10.1007/BFb0012788

    Chapter  Google Scholar 

  48. Pnueli, A.: The temporal logic of programs. In: Foundations of Computer Science (FOCS ’77), pp. 46–57. IEEE (1977). doi:10.1109/SFCS.1977.32

  49. Prasad, K.V.S.: A calculus of broadcasting systems. Sci. Comput. Program. 25(2–3), 285–327 (1995). doi:10.1016/0167-6423(95)00017-8

    Article  Google Scholar 

  50. Puhakka, A., Valmari, A.: Liveness and fairness in process-algebraic verification. In: Larsen, K.G., Nielsen, M. (eds.) Concurrency Theory (CONCUR’01), LNCS, vol. 2154, pp. 202–217. Springer, Berlin (2001). doi:10.1007/3-540-44685-0_14

    Google Scholar 

  51. Reed, G.M., Roscoe, A.W.: A timed model for communicating sequential processes. In: Kott, L. (ed.) Automata, Languages and Programming (ICALP ’86), LNCS, vol. 226, pp. 314–323. Springer, Berlin (1986). doi:10.1007/3-540-16761-7_81

    Chapter  Google Scholar 

  52. Reisig, W.: Petri Nets: An Introduction. EATCS Monographs on Theoretical Computer Science, vol. 4. Springer (1985). doi:10.1007/978-3-642-69968-9

  53. Vaandrager, F.W.: Expressiveness results for process algebras. In: de Bakker, J.W., de Roever, W.P., Rozenberg, G. (eds.) Proceedings REX Workshop on Semantics: Foundations and Applications, LNCS, vol. 666, pp. 609–638. Springer, Berlin (1993). doi:10.1007/3-540-56596-5_49

    Chapter  Google Scholar 

  54. Valmari, A., Setälä, M.: Visual verification of safety and liveness. In: Gaudel, M., Woodcock, J. (eds.) Industrial Benefit and Advances in Formal Methods (FME’96), LNCS, vol. 1051, pp. 228–247. Springer, Berlin (1996). doi:10.1007/3-540-60973-3_90

    Chapter  Google Scholar 

  55. van Glabbeek, R.J.: On specifying timeouts. In: Accetp. L., Gordon, A.D. (eds.) Short Contribution from the Worksho on Algebraic Process Calculi: The First Twenty Five Years and Beyond, ENTCS, vol. 162, pp. 112–223. Elsevier, Amsterdam (2005). doi:10.1016/j.entcs.2005.12.083

  56. van Glabbeek, R.J.: Musings on encodings and expressiveness. In: Luttik, B., Reniers, M.A. (eds.) Proceedings Combined 19th International Workshop on Expressiveness in Concurrency and 9th Workshop on Structured Operational Semantics, EPTCS, vol. 89, pp. 81–98. Open Publishing Association, London (2012). doi:10.4204/EPTCS389.7

  57. van Glabbeek, R.J., Höfner, P.: Progress, fairness and justness in process algebra. CoRR abs/1501.03268(2015). http://arxiv.org/abs/1501.03268

  58. van Glabbeek, R.J., Vaandrager, F.W.: Petri net models for algebraic theories of concurrency. In: Bakker,J.W., Nijman, A.J., Treleaven, P.C. (eds.) Parallel Architectures and Languages Europe (PARLE’97), vol. II:Parallel Languages, LNCS. Springer, Berlin (1987). doi:10.1007/3-540-17945-3_13

  59. van Glabbeek, R.J., Goltz, U., Schicke, J.W.: Abstract processes of place/transition systems. Inf. Process. Lett. 111(13), 626–633 (2011). doi:10.1016/j.ipl.2011.03.013

    Article  MATH  Google Scholar 

  60. Vogler, W.: Efficiency of asynchronous systems, read arcs, and the MUTEX-problem. Theor. Comput. Sci. 275(1–2), 589–631 (2002). doi:10.1016/S0304-3975(01)00300-0

    Article  MATH  MathSciNet  Google Scholar 

  61. Walker, D.J.: Automated analysis of mutual exclusion algorithms using CCS. Form. Asp. Comput. 1(1), 273–292 (1989). doi:10.1007/BF01887209

    Article  MATH  Google Scholar 

  62. Wegner, P.: Why interaction is more powerful than algorithms. Commun. ACM 40(5), 80–91 (1997). doi:10.1145/253769.253801

    Article  Google Scholar 

Download references

Acknowledgments

We gratefully thank the anonymous referees. Their reports showed deep insights in the material, and helped a lot to improve the quality of the paper. In particular, the link between our fair scheduler and Peterson’s mutual exclusion protocol was made by one of the referees.

Author information

Authors and Affiliations

  1. NICTA, Sydney, Australia

    Rob J. van Glabbeek & Peter Höfner

  2. UNSW, Sydney, Australia

    Rob J. van Glabbeek & Peter Höfner

Authors
  1. Rob J. van Glabbeek
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Peter Höfner
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding authors

Correspondence to Rob J. van Glabbeek or Peter Höfner.

Additional information

It is our great pleasure to dedicate this paper to Walter Vogler on the occasion of his 60th birthday. We have combined two of Walter’s main interests: Petri nets and process algebra. In fact, we proved a result about Petri nets that had been proven before by Walter, but in a restricted form, as we discovered only after finishing our proof. We also transfer this result to the process algebra CCS. Beyond foundational research in the theory of concurrent systems, Walter achieved excellent results in related subjects such as temporal logic and efficiency. In addition to being a dedicated researcher, he is also meticulous in all of his endeavours, including his writing. As a consequence his scientific papers tend to contain no flaws, which is just one of the reasons that makes reading them so enjoyable. It’s fair to say: “CCS Walter!”—Congratulations and Continuous Success!

NICTA is funded by the Australian Government through the Department of Communications and the Australian Research Council through the ICT Centre of Excellence Program.

Rights and permissions

Reprints and permissions

About this article

Check for updates. Verify currency and authenticity via CrossMark

Cite this article

van Glabbeek, R., Höfner, P. CCS: It’s not fair!. Acta Informatica 52, 175–205 (2015). https://doi.org/10.1007/s00236-015-0221-6

Download citation

  • Received:

  • Accepted:

  • Published:

  • Issue Date:

  • DOI: https://doi.org/10.1007/s00236-015-0221-6

Search

Navigation