Skip to main content
SpringerLink
Log in

Coordinating Multicore Computing

  • Chapter
  • First Online:
Formal Methods for Multicore Programming (SFM 2015)

Part of the book series: Lecture Notes in Computer Science ((LNPSE,volume 9104))

  • 652 Accesses

Abstract

Traditional models of concurrency resort to peculiarly indirect means to express interaction and study its properties. Formalisms such as process algebras/calculi, concurrent objects, actors, shared memory, message passing, etc., all are primarily action-based models that provide constructs for the direct specification of things that interact, rather than a direct specification of interaction (protocols). Consequently, interaction in these formalisms becomes a derived or secondary concept whose properties can be studied only indirectly, as the side-effects of the (intended or coincidental) couplings or clashes of the actions whose compositions comprise a model.

Treating interaction as an explicit first-class concept, complete with its own composition operators, allows to specify more complex interaction protocols by combining simpler, and eventually primitive, protocols. Reo [4, 7, 8, 15] serves as a premier example of such an interaction-based model of concurrency. In this paper, we describe Reo and its compiler. We show how exogenous coordination in Reo reflects an interaction-centric model of concurrency where an interaction (protocol) consists of nothing but a relational constraint on communication actions. In this setting, interaction protocols become explicit, concrete, tangible (software) constructs that can be specified, verified, composed, and reused, independently of the actors that they may engage in disparate applications.

This paper complements the first author’s lecture at the \(15^{th}\) International School on Formal Methods for the Design of Computer, Communication and Software Systems in Bertinoro, Italy, June 2015, and collects previously published material (notably [9]).

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

Access this chapter

Log in via an institution
eBook
USD 16.99
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 16.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Notes

  1. 1.

    By this anthropomorphic expression we simply mean that a component does not contain any piece of code that directly contributes to determine the entities that it composes with, or the specific protocol that coordinates its own interactions with them.

  2. 2.

    In fact, this characterization is not very accurate for values of \(k>1\). Work out what happens for \(k=2\), for instance.

  3. 3.

    In fact, constraint automata do not have the expressiveness required to directly represent context sensitivity. Other more expressive semantic models, including more sophisticated automata models, have been devised for this purpose [29, 34]. A recent work shows that, although constraint automata cannot directly represent context sensitivity, it is possible to encode context sensitivity using constraint automata as well [52, 61].

  4. 4.

    Of course, in a distributed memory setting, the concurrency primitives are different, but message passing communication primitives used in such settings still constitute an action-based model of concurrency, for which our subsequent argument still holds.

References

  1. CADP home page. http://www.inrialpes.fr/vasy/cadp/

  2. Extensible Coordination Tools home page. http://reo.project.cwi.nl/cgi-bin/trac.cgi/reo/wiki/Tools

  3. mCRL2 home page. http://www.mcrl2.org

  4. Reo home page. http://reo.project.cwi.nl

  5. Vereofy home page. http://www.vereofy.de/

  6. Agha, G.: Actors: A Model of Concurrent Computation in Distributed Systems. MIT Press, Cambridge (1986)

    Google Scholar 

  7. Arbab, F.: Reo: a channel-based coordination model for component composition. Math. Struct. Comput. Sci. 14(3), 329–366 (2004)

    Article  MathSciNet  MATH  Google Scholar 

  8. Arbab, F.: Abstract behavior types: a foundation model for components and their composition. Sci. Comput. Program. 55(1–3), 3–52 (2005)

    Article  MathSciNet  MATH  Google Scholar 

  9. Arbab, F.: Puff, the magic protocol. In: Agha, G., Danvy, O., Meseguer, J. (eds.) Formal Modeling: Actors, Open Systems, Biological Systems. LNCS, vol. 7000, pp. 169–206. Springer, Heidelberg (2011)

    Chapter  Google Scholar 

  10. Arbab, F., Aştefănoaei, L., de Boer, F.S., Dastani, M., Meyer, J.-J., Tinnermeier, N.: Reo connectors as coordination artifacts in 2APL systems. In: Bui, T.D., Ho, T.V., Ha, Q.T. (eds.) PRIMA 2008. LNCS (LNAI), vol. 5357, pp. 42–53. Springer, Heidelberg (2008)

    Chapter  Google Scholar 

  11. Arbab, F., Baier, C., de Boer, F.S., Rutten, J.J.M.M.: Models and temporal logical specifications for timed component connectors. Softw. Syst. Model. 6(1), 59–82 (2007)

    Article  Google Scholar 

  12. Arbab, F., Chothia, T., Meng, S., Moon, Y.-J.: Component connectors with QoS guarantees. In: Murphy, A.L., Vitek, J. (eds.) COORDINATION 2007. LNCS, vol. 4467, pp. 286–304. Springer, Heidelberg (2007)

    Chapter  Google Scholar 

  13. Arbab, F., Chothia, T., van der Mei, R., Meng, S., Moon, Y.-J., Verhoef, C.: From coordination to stochastic models of QoS. In: Field and Vasconcelos [35], pp. 268–287

    Google Scholar 

  14. Arbab, F., Kokash, N., Meng, S.: Towards using Reo for compliance-aware business process modeling. In: Margaria, T., Steffen, B. (eds.) ISoLA 2008. CCIS, vol. 17, pp. 108–123. Springer, Heidelberg (2008)

    Chapter  Google Scholar 

  15. Arbab, F., Mavaddat, F.: Coordination through channel composition. In: Arbab, F., Talcott, C. (eds.) COORDINATION 2002. LNCS, vol. 2315, pp. 22–39. Springer, Heidelberg (2002)

    Chapter  Google Scholar 

  16. Arbab, F., Meng, S.: Synthesis of connectors from scenario-based interaction specifications. In: Chaudron, M.R.V., Ren, X.-M., Reussner, R. (eds.) CBSE 2008. LNCS, vol. 5282, pp. 114–129. Springer, Heidelberg (2008)

    Chapter  Google Scholar 

  17. Arbab, F., Meng, S., Moon, Y.-J., Kwiatkowska, M.Z., Qu, H.: Reo2MC: a tool chain for performance analysis of coordination models. In: van Vliet, H., Issarny, V. (eds.) ESEC/SIGSOFT FSE, pp. 287–288. ACM, New York (2009)

    Google Scholar 

  18. Arvind, D.A., Pingali, K., Chiou, D., Sendag, R., Yi, J.: Programming multicores: do applications programmers need to write explicitly parallel programs? IEEE Micro 30(3), 19–33 (2010)

    Article  Google Scholar 

  19. Baeten, J.C.M., Weijland, W.P.: Process Algebra. Cambridge University Press, Cambridge (1990)

    Book  MATH  Google Scholar 

  20. Baier, C.: Probabilistic models for Reo connector circuits. J. Univers. Comput. Sci. 11(10), 1718–1748 (2005)

    Google Scholar 

  21. Baier, C., Blechmann, T., Klein, J., Klüppelholz, S.: Formal verification for components and connectors. In: de Boer, F.S., Bonsangue, M.M., Madelaine, E. (eds.) FMCO 2008. LNCS, vol. 5751, pp. 82–101. Springer, Heidelberg (2009)

    Chapter  Google Scholar 

  22. Baier, C., Blechmann, T., Klein, J., Klüppelholz, S.: A uniform framework for modeling and verifying components and connectors. In: Field and Vasconcelos [35], pp. 247–267

    Google Scholar 

  23. Baier, C., Blechmann, T., Klein, J., Klüppelholz, S., Leister, W.: Design and verification of systems with exogenous coordination using vereofy. In: Margaria, T., Steffen, B. (eds.) ISoLA 2010, Part II. LNCS, vol. 6416, pp. 97–111. Springer, Heidelberg (2010)

    Chapter  Google Scholar 

  24. Baier, C., Klein, J., Klüppelholz, S.: Modeling and verification of components and connectors. In: Bernardo, M., Issarny, V. (eds.) SFM 2011. LNCS, vol. 6659, pp. 114–147. Springer, Heidelberg (2011)

    Chapter  Google Scholar 

  25. Baier, C., Sirjani, M., Arbab, F., Rutten, J.J.M.M.: Modeling component connectors in Reo by constraint automata. Sci. Comput. Program. 61(2), 75–113 (2006)

    Article  MathSciNet  MATH  Google Scholar 

  26. Baier, C., Wolf, V.: Stochastic reasoning about channel-based component connectors. In: Ciancarini, P., Wiklicky, H. (eds.) COORDINATION 2006. LNCS, vol. 4038, pp. 1–15. Springer, Heidelberg (2006)

    Chapter  Google Scholar 

  27. Bergstra, J.A., Klop, J.W.: Process algebra for synchronous communication. Inf. Control 60, 109–137 (1984)

    Article  MathSciNet  MATH  Google Scholar 

  28. Blechmann, T., Baier, C.: Checking equivalence for Reo networks. Electr. Notes Theor. Comput. Sci 215, 209–226 (2008)

    Article  Google Scholar 

  29. Bonsangue, M.M., Clarke, D., Silva, A.: Automata for context-dependent connectors. In: Field and Vasconcelos [35], pp. 184–203

    Google Scholar 

  30. Bonsangue, M.M., Izadi, M.: Automata based model checking for reo connectors. In: Arbab, F., Sirjani, M. (eds.) FSEN 2009. LNCS, vol. 5961, pp. 260–275. Springer, Heidelberg (2010)

    Chapter  Google Scholar 

  31. Clarke, D., Costa, D., Arbab, F.: Modelling coordination in biological systems. In: Margaria, T., Steffen, B. (eds.) ISoLA 2004. LNCS, vol. 4313, pp. 9–25. Springer, Heidelberg (2006)

    Chapter  Google Scholar 

  32. Clarke, D., Costa, D., Arbab, F.: Connector colouring I: Synchronisation and context dependency. Sci. Comput. Program. 66(3), 205–225 (2007)

    Article  MathSciNet  MATH  Google Scholar 

  33. Clarke, D., Proença, J., Lazovik, A., Arbab, F.: Channel-based coordination via constraint satisfaction. Sci. Comput. Program. 76(8), 681–710 (2011)

    Article  MATH  Google Scholar 

  34. Costa, D.: Formal models for context dependent connectors for distributed software components and services. Ph.D. thesis, Vrije Universiteit Amsterdam (2010). http://dare.ubvu.vu.nl//handle/1871/16380

  35. Field, J., Vasconcelos, V.T. (eds.): COORDINATION 2009. LNCS, vol. 5521. Springer, Heidelberg (2009)

    MATH  Google Scholar 

  36. Fokkink, W.: Introduction to Process Algebra. Texts in Theoretical Computer Science, An EATCS Series. Springer, Berlin (1999)

    MATH  Google Scholar 

  37. Grabe, I., Jaghoori, M.M., Aichernig, B.K., Baier, C., Blechmann, T., de Boer, F.S., Griesmayer, A., Johnsen, E.B., Klein, J., Klüppelholz, S., Kyas, M., Leister, W., Schlatte, R., Stam, A., Steffen, M., Tschirner, S., Xuedong, L., Yi, W.: Credo methodology: modeling and analyzing a peer-to-peer system in credo. Electr. Notes. Theor. Comput. Sci. 266, 33–48 (2010)

    Article  Google Scholar 

  38. Groote, J.F., Mathijssen, A., Reniers, M.A., Usenko, Y.S., van Weerdenburg, M.: The formal specification language mCRL2. In: Brinksma, E., Harel, D., Mader, A., Stevens, P., Wieringa, R. (eds.) MMOSS. Dagstuhl Seminar Proceedings, vol. 06351. Internationales Begegnungs- und Forschungszentrum fuer Informatik (IBFI), Schloss Dagstuhl, Germany (2006)

    Google Scholar 

  39. Hamberg, R., Vaandrager, F.: Using model checkers in an introductory course on operating systems. Oper. Syst. Rev. 42(6), 101–111 (2008)

    Article  Google Scholar 

  40. Hoare, C.A.R.: Communicating Sequential Processes. Prentice-Hall, Upper Saddle River (1985)

    MATH  Google Scholar 

  41. Izadi, M., Bonsangue, M.M., Clarke, D.: Modeling component connectors: synchronisation and context-dependency. In: Cerone, A., Gruner, S. (eds.) SEFM, pp. 303–312. IEEE Computer Society, Los Alamitos (2008)

    Google Scholar 

  42. Izadi, M., Bonsangue, M.M., Clarke, D.: Büchi automata for modeling component connectors. Softw. Syst. Model. 10(2), 183–200 (2011)

    Article  Google Scholar 

  43. Izadi, M., Movaghar, A.: Failure-based equivalence of constraint automata. Int. J. Comput. Math. 87(11), 2426–2443 (2010)

    Article  MathSciNet  MATH  Google Scholar 

  44. Jongmans, S.-S., Arbab, F.: Overview of thirty semantic formalisms for Reo. Sci. Ann. Comput. Sci. 22(1), 201–251 (2012)

    MathSciNet  Google Scholar 

  45. Jongmans, S.-S.T.Q., Arbab, F.: Global consensus through local synchronization. In: Canal, C., Villari, M. (eds.) ESOCC 2013. CCIS, vol. 393, pp. 174–188. Springer, Heidelberg (2013)

    Chapter  Google Scholar 

  46. Jongmans, S.-S., Arbab, F.: Modularizing and specifying protocols among threads.In: Proceedings of PLACES 2012. EPTCS, vol. 109, pp. 34–45. CoRR (2013)

    Google Scholar 

  47. Jongmans, S.-S., Arbab, F.: Toward sequentializing overparallelized protocol code. In: Proceedings of ICE 2014. EPTCS, vol. 166, pp. 38–44. CoRR (2014)

    Google Scholar 

  48. Jongmans, S.-S., Arbab, F.: Can high throughput atone for high latency in compiler-generated protocol code? In: Proceedings of FSEN 2015. Springer (in press)

    Google Scholar 

  49. Jongmans, S.-S.T.Q., Halle, S., Arbab, F.: Automata-based optimization of interaction protocols for scalable multicore platforms. In: Kühn, E., Pugliese, R. (eds.) COORDINATION 2014. LNCS, vol. 8459, pp. 65–82. Springer, Heidelberg (2014)

    Chapter  Google Scholar 

  50. Jongmans, S.-S., Halle, S., Arbab, F.: Reo: a dataflow inspired language for multicore.In: Proceedings of DFM 2013, pp. 42–50. IEEE (2014)

    Google Scholar 

  51. Jongmans, S.-S., Santini, F., Arbab, F.: Partially-distributed coordination with Reo.In: Proceedings of PDP 2014, pp. 697–706. IEEE (2014)

    Google Scholar 

  52. Jongmans, S.-S.T.Q., Krause, C., Arbab, F.: Encoding context-sensitivity in reo into non-context-sensitive semantic models. In: De Meuter, W., Roman, G.-C. (eds.) COORDINATION 2011. LNCS, vol. 6721, pp. 31–48. Springer, Heidelberg (2011)

    Chapter  Google Scholar 

  53. Kemper, S.: SAT-based verification for timed component connectors. Electr. Notes Theor. Comput. Sci. 255, 103–118 (2009)

    Article  Google Scholar 

  54. Kemper, S.: Compositional construction of real-time dataflow networks. In: Clarke, D., Agha, G. (eds.) COORDINATION 2010. LNCS, vol. 6116, pp. 92–106. Springer, Heidelberg (2010)

    Chapter  Google Scholar 

  55. Klein, J., Klüppelholz, S., Stam, A., Baier, C.: Hierarchical modeling and formal verification. An industrial case study using reo and vereofy. In: Salaün, G., Schätz, B. (eds.) FMICS 2011. LNCS, vol. 6959, pp. 228–243. Springer, Heidelberg (2011)

    Chapter  Google Scholar 

  56. Klüppelholz, S., Baier, C.: Symbolic model checking for channel-based component connectors. Electr. Notes Theor. Comput. Sci 175(2), 19–37 (2007)

    Article  MATH  Google Scholar 

  57. Koehler, C., Lazovik, A., Arbab, F.: ReoService: coordination modeling tool. In: Krämer et al. [64], pp. 625–626

    Google Scholar 

  58. Kokash, N., Krause, C., de Vink, E.P.: Data-aware design and verification of service compositions with Reo and mCRL2. In: SAC 2010: Proceedings of the 2010 ACM Symposium on Applied Computing, pp. 2406–2413. ACM, New York (2010)

    Google Scholar 

  59. Kokash, N., Arbab, F.: Formal behavioral modeling and compliance analysis for service-oriented systems. In: de Boer, F.S., Bonsangue, M.M., Madelaine, E. (eds.) FMCO 2008. LNCS, vol. 5751, pp. 21–41. Springer, Heidelberg (2009)

    Chapter  Google Scholar 

  60. Kokash, N., Arbab, F.: Applying Reo to service coordination in long-running business transactions. In: Shin, S.Y., Ossowski, S. (eds.) SAC, pp. 1381–1382. ACM, New York (2009)

    Google Scholar 

  61. Kokash, N., Arbab, F., Changizi, B., Makhnist, L.: Input-output conformance testing for channel-based service connectors. In: Aceto, L., Mousavi, M.R. (eds.) PACO. EPTCS, vol. 60, pp. 19–35 (2011)

    Google Scholar 

  62. Kokash, N., Krause, C., de Vink, E.P.: Verification of context-dependent channel-based service models. In: de Boer, F.S., Bonsangue, M.M., Hallerstede, S., Leuschel, M. (eds.) FMCO 2009. LNCS, vol. 6286, pp. 21–40. Springer, Heidelberg (2010)

    Chapter  Google Scholar 

  63. Kokash, N., Krause, C., de Vink, E.P.: Time and data-aware analysis of graphical service models in Reo. In: Fiadeiro, J.L., Gnesi, S., Maggiolo-Schettini, A. (eds.) SEFM, pp. 125–134. IEEE Computer Society (2010)

    Google Scholar 

  64. Krämer, B.J., Lin, K.-J., Narasimhan, P. (eds.): ICSOC 2007. LNCS, vol. 4749. Springer, Heidelberg (2007)

    Google Scholar 

  65. Lazovik, A., Arbab, F.: Using Reo for service coordination.In: Krämer et al. [64], pp. 398–403

    Google Scholar 

  66. Meng, S., Arbab, F.: On resource-sensitive timed component connectors. In: Bonsangue, M.M., Johnsen, E.B. (eds.) FMOODS 2007. LNCS, vol. 4468, pp. 301–316. Springer, Heidelberg (2007)

    Chapter  Google Scholar 

  67. Meng, S., Arbab, F.: QoS-driven service selection and composition. In: Billington, J., Duan, Z., Koutny, M. (eds.) ACSD, pp. 160–169. IEEE (2008)

    Google Scholar 

  68. Milner, R. (ed.): A Calculus of Communicating Systems. LNCS, vol. 92. Springer, Heidelberg (1980)

    MATH  Google Scholar 

  69. Milner, R.: Elements of interaction - turing award lecture. Commun. ACM 36(1), 78–89 (1993)

    Article  Google Scholar 

  70. Moon, Y.-J.: Stochastic models for quality of service of component connectors. Ph.D. thesis, Leiden University (2011)

    Google Scholar 

  71. Moon, Y.-J., Silva, A., Krause, C., Arbab, F.: A compositional semantics for stochastic Reo connectors. In: Mousavi, M.R., Salaün, G. (eds.) FOCLASA. EPTCS, vol. 30, pp. 93–107 (2010)

    Google Scholar 

  72. Sangiorgi, D., Walker, D.: PI-Calculus: A Theory of Mobile Processes. Cambridge University Press, New York (2001)

    MATH  Google Scholar 

  73. Schumm, D., Turetken, O., Kokash, N., Elgammal, A., Leymann, F., van den Heuvel, W.-J.: Business process compliance through reusable units of compliant processes. In: Daniel, F., Facca, F.M. (eds.) ICWE 2010. LNCS, vol. 6385, pp. 325–337. Springer, Heidelberg (2010)

    Chapter  Google Scholar 

  74. Wegner, P.: Coordination as comstrainted interaction (extended abstract). In: Hankin, C., Ciancarini, P. (eds.) COORDINATION 1996. LNCS, vol. 1061, pp. 28–33. Springer, Heidelberg (1996)

    Chapter  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Formal Methods, CWI, Science Park 123, 1098 XG, Amsterdam, The Netherlands

    Farhad Arbab & Sung-Shik T. Q. Jongmans

  2. Leiden Institute for Advanced Computer Science, Leiden University, Niels Bohrweg 1, 2333 CA, Leiden, The Netherlands

    Farhad Arbab

Authors
  1. Farhad Arbab
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Sung-Shik T. Q. Jongmans
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Farhad Arbab .

Editor information

Editors and Affiliations

  1. Università di Urbino "Carlo Bo", Urbino, Italy

    Marco Bernardo

  2. University of Oslo, Oslo, Norway

    Einar Broch Johnsen

Rights and permissions

Reprints and permissions

Copyright information

© 2015 Springer International Publishing Switzerland

About this chapter

Cite this chapter

Arbab, F., Jongmans, SS.T.Q. (2015). Coordinating Multicore Computing. In: Bernardo, M., Johnsen, E. (eds) Formal Methods for Multicore Programming. SFM 2015. Lecture Notes in Computer Science(), vol 9104. Springer, Cham. https://doi.org/10.1007/978-3-319-18941-3_2

Download citation

  • DOI: https://doi.org/10.1007/978-3-319-18941-3_2

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-319-18940-6

  • Online ISBN: 978-3-319-18941-3

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation