Advertisement

Deadlock Detection for Actor-Based Coroutines

  • Keyvan Azadbakht
  • Frank S. de Boer
  • Erik de Vink
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 10951)

Abstract

The actor-based language studied in this paper features asynchronous method calls and supports coroutines which allow for the cooperative scheduling of the method invocations belonging to an actor. We model the local behavior of an actor as a well-structured transition system by means of predicate abstraction and derive the decidability of the occurrence of deadlocks caused by the coroutine mode of method execution.

Keywords

Deadlock detection Predicate abstraction Actor Cooperative scheduling Transition system 

References

  1. 1.
    Agha, G.: Actors: A Model of Concurrent Computation in Distributed Systems. The MIT Press, Cambridge (1986)Google Scholar
  2. 2.
    Wasser, N., Hähnle, R., Bubel, R.: Abstract Interpretation. Deductive Software Verification – The KeY Book. LNCS, vol. 10001, pp. 167–189. Springer, Cham (2016).  https://doi.org/10.1007/978-3-319-49812-6_6CrossRefGoogle Scholar
  3. 3.
    Azadbakht, K., Bezirgiannis, N., de Boer, F.S.: Distributed network generation based on preferential attachment in ABS. In: Steffen, B., et al. (eds.) SOFSEM 2017. LNCS, vol. 10139, pp. 103–115. Springer, Cham (2017).  https://doi.org/10.1007/978-3-319-51963-0_9CrossRefGoogle Scholar
  4. 4.
    Azadbakht, K., Bezirgiannis, N., de Boer, F.S., Aliakbary, S.: A high-level and scalable approach for generating scale-free graphs using active objects. In: Proceedings of the 31st Annual ACM Symposium on Applied Computing, pp. 1244–1250. ACM (2016)Google Scholar
  5. 5.
    Ball, T., Majumdar, R., Millstein, T., Rajamani, S.K.: Automatic predicate abstraction of C programs. In: Conference on Programming Language Design and Implementation, pp. 203–213 (2001)Google Scholar
  6. 6.
    Conway, M.E.: Design of a separable transition-diagram compiler. Commun. ACM 6(7), 396–408 (1963)CrossRefGoogle Scholar
  7. 7.
    de Boer, F.S., et al.: 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).  https://doi.org/10.1007/978-3-642-35861-6_7CrossRefGoogle Scholar
  8. 8.
    de Boer, F.S., Clarke, D., Johnsen, E.B.: A complete guide to the future. In: De Nicola, R. (ed.) ESOP 2007. LNCS, vol. 4421, pp. 316–330. Springer, Heidelberg (2007).  https://doi.org/10.1007/978-3-540-71316-6_22CrossRefGoogle Scholar
  9. 9.
    de Boer, F.S., Jaghoori, M.M., Laneve, C., Zavattaro, G.: Decidability problems for actor systems. In: Koutny, M., Ulidowski, I. (eds.) CONCUR 2012. LNCS, vol. 7454, pp. 562–577. Springer, Heidelberg (2012).  https://doi.org/10.1007/978-3-642-32940-1_39CrossRefGoogle Scholar
  10. 10.
    Finkel, A., Schnoebelen, Ph.: Well-structured transition systems everywhere!. Theoret. Comput. Sci. 256(1), 63–92 (2001)MathSciNetCrossRefGoogle Scholar
  11. 11.
    Giachino, E., Henrio, L., Laneve, C., Mastandrea, V.: Actors may synchronize, safely! In: 18th International Symposium on Principles and Practice of Declarative Programming, pp. 118–131 (2016)Google Scholar
  12. 12.
    Giachino, E., Laneve, C., Lienhardt, M.: A framework for deadlock detection in core ABS. Softw. Syst. Model. 15(4), 1013–1048 (2016)CrossRefGoogle Scholar
  13. 13.
    Graf, S., Saidi, H.: Construction of abstract state graphs with PVS. In: Grumberg, O. (ed.) CAV 1997. LNCS, vol. 1254, pp. 72–83. Springer, Heidelberg (1997).  https://doi.org/10.1007/3-540-63166-6_10CrossRefGoogle Scholar
  14. 14.
    Henrio, L., Laneve, C., Mastandrea, V.: Analysis of synchronisations in stateful active objects. In: Polikarpova, N., Schneider, S. (eds.) IFM 2017. LNCS, vol. 10510, pp. 195–210. Springer, Cham (2017).  https://doi.org/10.1007/978-3-319-66845-1_13CrossRefGoogle Scholar
  15. 15.
    Hewitt, C.: Description and theoretical analysis (using schemata) of planner: a language for proving theorems and manipulating models in a robot. Technical report, Massachusetts Institute of Technology Cambridge Artificial Intelligence Lab (1972)Google Scholar
  16. 16.
    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., de Boer, F.S., Bonsangue, M.M. (eds.) FMCO 2010. LNCS, vol. 6957, pp. 142–164. Springer, Heidelberg (2011).  https://doi.org/10.1007/978-3-642-25271-6_8CrossRefGoogle Scholar
  17. 17.
    Johnsen, E.B., Owe, O., Creol, I.C.Yu.: A type-safe object-oriented model for distributed concurrent systems. Theoret. Comput. Sci. 365(1–2), 23–66 (2006)Google Scholar
  18. 18.
    Kamburjan, E., Din, C.C., Chen, T.-C.: Session-based compositional analysis for actor-based languages using futures. In: Ogata, K., Lawford, M., Liu, S. (eds.) ICFEM 2016. LNCS, vol. 10009, pp. 296–312. Springer, Cham (2016).  https://doi.org/10.1007/978-3-319-47846-3_19CrossRefGoogle Scholar
  19. 19.
    Kerfoot, E., McKeever, S., Torshizi, F.: Deadlock freedom through object ownership. In: 5th International Workshop on Aliasing, Confinement and Ownership in Object-Oriented Programming (2009)Google Scholar
  20. 20.
    Sirjani, M.: Rebeca: theory, applications, and tools. In: de Boer, F.S., Bonsangue, M.M., Graf, S., de Roever, W.-P. (eds.) FMCO 2006. LNCS, vol. 4709, pp. 102–126. Springer, Heidelberg (2007).  https://doi.org/10.1007/978-3-540-74792-5_5CrossRefGoogle Scholar

Copyright information

© Springer International Publishing AG, part of Springer Nature 2018

Authors and Affiliations

  • Keyvan Azadbakht
    • 1
    • 2
  • Frank S. de Boer
    • 1
  • Erik de Vink
    • 1
    • 3
  1. 1.Centrum Wiskunde en InformaticaAmsterdamThe Netherlands
  2. 2.Leiden UniversityLeidenThe Netherlands
  3. 3.Eindhoven University of TechnologyEindhovenThe Netherlands

Personalised recommendations