Analysis of Synchronisations in Stateful Active Objects

  • Ludovic Henrio
  • Cosimo Laneve
  • Vincenzo MastandreaEmail author
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 10510)


This paper presents a static analysis technique based on effects and behavioural types for deriving synchronisation patterns of stateful active objects and verifying the absence of deadlocks in this context. This is challenging because active objects use futures to refer to results of pending asynchronous invocations and because these futures can be stored in object fields, passed as method parameters, or returned by invocations. Our effect system traces the access to object fields, thus allowing us to compute behavioural types that express synchronisation patterns in a precise way. The behavioural types are thereafter analysed by a solver that discovers potential deadlocks.


  1. 1.
    Ameur-Boulifa, R., Henrio, L., Kulankhina, O., Madelaine, E., Savu, A.: Behavioural semantics for asynchronous components. J. Logical Algebr. Methods Program. 89, 1–40 (2017)MathSciNetCrossRefzbMATHGoogle Scholar
  2. 2.
    Boer, F.S., Bravetti, M., Grabe, I., Lee, M., Steffen, M., Zavattaro, G.: A petri net based analysis of deadlocks for active objects and futures. In: Păsăreanu, C.S., Salaün, G. (eds.) FACS 2012. LNCS, vol. 7684, pp. 110–127. Springer, Heidelberg (2013). doi: 10.1007/978-3-642-35861-6_7 CrossRefGoogle Scholar
  3. 3.
    Boyapati, C., Lee, R., Rinard, M.C.: Ownership types for safe programming: preventing data races and deadlocks. In: Proceedings of the OOPSLA 2002 (2002)Google Scholar
  4. 4.
    Caromel, D., Henrio, L., Serpette, B.P.: Asynchronous sequential processes. Inf. Comput. 207(4), 459–495 (2009)MathSciNetCrossRefzbMATHGoogle Scholar
  5. 5.
    Flores-Montoya, A.E., Albert, E., Genaim, S.: May-happen-in-parallel based deadlock analysis for concurrent objects. In: Beyer, D., Boreale, M. (eds.) FMOODS/FORTE 2013. LNCS, vol. 7892, pp. 273–288. Springer, Heidelberg (2013). doi: 10.1007/978-3-642-38592-6_19 CrossRefGoogle Scholar
  6. 6.
    Giachino, E., Henrio, L., Laneve, C., Mastandrea, V.: Actors may synchronize, safely! In: Proceedings of PPDP 2016. ACM (2016)Google Scholar
  7. 7.
    Giachino, E., Kobayashi, N., Laneve, C.: Deadlock analysis of unbounded process networks. In: Baldan, P., Gorla, D. (eds.) CONCUR 2014. LNCS, vol. 8704, pp. 63–77. Springer, Heidelberg (2014). doi: 10.1007/978-3-662-44584-6_6 Google Scholar
  8. 8.
    Giachino, E., Laneve, C., Lienhardt, M.: A framework for deadlock detection in core ABS. Softw. Syst. Model. 15(4), 1013–1048 (2016)CrossRefGoogle Scholar
  9. 9.
    Gkolfi, A., Din, C.C., Johnsen, E.B., Steffen, M., Yu, I.C.: Translating active objects into colored petri nets for communication analysis. In: Proceedings of the FSEN 2017. LNCS. Springer (2017)Google Scholar
  10. 10.
    Haller, P., Odersky, M.: Scala actors: unifying thread-based and event-based programming. Theoret. Comput. Sci. 410(2–3), 202–220 (2009)MathSciNetCrossRefzbMATHGoogle Scholar
  11. 11.
    Henrio, L., Laneve, C., Mastandrea, V.: Analysis of synchronisation patterns in stateful active objects. Research report, I3S; Inria - Sophia antipolis (2017).
  12. 12.
    Johnsen, E.B., Hähnle, R., Schäfer, J., Schlatte, R., Steffen, M.: ABS: a core language for abstract behavioral specification. In: Aichernig, B.K., Boer, F.S., Bonsangue, M.M. (eds.) FMCO 2010. LNCS, vol. 6957, pp. 142–164. Springer, Heidelberg (2011). doi: 10.1007/978-3-642-25271-6_8 CrossRefGoogle Scholar
  13. 13.
    Kobayashi, N., Laneve, C.: Deadlock analysis of unbounded process networks. Inf. Comput. 252, 48–70 (2017)MathSciNetCrossRefzbMATHGoogle Scholar
  14. 14.
    Lucassen, J.M., Gifford, D.K.: Polymorphic effect systems. In: Proceedings of POPL 1988, pp. 47–57. ACM Press (1988)Google Scholar
  15. 15.
    Morris, B.: The Symbian OS Architecture Sourcebook: Design and Evolution of a Mobile Phone OS. Wiley, Hoboken (2007)Google Scholar
  16. 16.
    Niehren, J., Schwinghammer, J., Smolka, G.: A concurrent lambda calculus with futures. Theoret. Comput. Sci. 364(3), 338–356 (2006)MathSciNetCrossRefzbMATHGoogle Scholar
  17. 17.
    Sirjani, M.: Rebeca: theory, applications, and tools. In: Boer, F.S., Bonsangue, M.M., Graf, S., Roever, W.-P. (eds.) FMCO 2006. LNCS, vol. 4709, pp. 102–126. Springer, Heidelberg (2007). doi: 10.1007/978-3-540-74792-5_5 CrossRefGoogle Scholar
  18. 18.
    Wyatt, D.: Akka Concurrency. Artima (2013)Google Scholar

Copyright information

© Springer International Publishing AG 2017

Authors and Affiliations

  • Ludovic Henrio
    • 1
  • Cosimo Laneve
    • 2
    • 3
  • Vincenzo Mastandrea
    • 1
    • 3
    Email author
  1. 1.Université Côte d’Azur, CNRS, I3SSophia AntipolisFrance
  2. 2.University of BolognaBolognaItaly
  3. 3.INRIA-FocusSophia AntipolisFrance

Personalised recommendations