Skip to main content
SpringerLink
Log in

Analysis of Synchronisations in Stateful Active Objects

  • Conference paper
  • First Online:
Integrated Formal Methods (IFM 2017)

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

Included in the following conference series:

Abstract

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.

This work was partially funded by the ANR project ANR-11-LABX-0031-01.

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

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 39.99
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.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

References

  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)

    Article  MathSciNet  MATH  Google Scholar 

  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

    Chapter  Google Scholar 

  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. Caromel, D., Henrio, L., Serpette, B.P.: Asynchronous sequential processes. Inf. Comput. 207(4), 459–495 (2009)

    Article  MathSciNet  MATH  Google Scholar 

  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

    Chapter  Google Scholar 

  6. Giachino, E., Henrio, L., Laneve, C., Mastandrea, V.: Actors may synchronize, safely! In: Proceedings of PPDP 2016. ACM (2016)

    Google Scholar 

  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. Giachino, E., Laneve, C., Lienhardt, M.: A framework for deadlock detection in core ABS. Softw. Syst. Model. 15(4), 1013–1048 (2016)

    Article  Google Scholar 

  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. Haller, P., Odersky, M.: Scala actors: unifying thread-based and event-based programming. Theoret. Comput. Sci. 410(2–3), 202–220 (2009)

    Article  MathSciNet  MATH  Google Scholar 

  11. Henrio, L., Laneve, C., Mastandrea, V.: Analysis of synchronisation patterns in stateful active objects. Research report, I3S; Inria - Sophia antipolis (2017). https://hal.archives-ouvertes.fr/hal-01542595

  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

    Chapter  Google Scholar 

  13. Kobayashi, N., Laneve, C.: Deadlock analysis of unbounded process networks. Inf. Comput. 252, 48–70 (2017)

    Article  MathSciNet  MATH  Google Scholar 

  14. Lucassen, J.M., Gifford, D.K.: Polymorphic effect systems. In: Proceedings of POPL 1988, pp. 47–57. ACM Press (1988)

    Google Scholar 

  15. Morris, B.: The Symbian OS Architecture Sourcebook: Design and Evolution of a Mobile Phone OS. Wiley, Hoboken (2007)

    Google Scholar 

  16. Niehren, J., Schwinghammer, J., Smolka, G.: A concurrent lambda calculus with futures. Theoret. Comput. Sci. 364(3), 338–356 (2006)

    Article  MathSciNet  MATH  Google Scholar 

  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

    Chapter  Google Scholar 

  18. Wyatt, D.: Akka Concurrency. Artima (2013)

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Université Côte d’Azur, CNRS, I3S, Sophia Antipolis, France

    Ludovic Henrio & Vincenzo Mastandrea

  2. University of Bologna, Bologna, Italy

    Cosimo Laneve

  3. INRIA-Focus, Sophia Antipolis, France

    Cosimo Laneve & Vincenzo Mastandrea

Authors
  1. Ludovic Henrio
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Cosimo Laneve
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Vincenzo Mastandrea
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Vincenzo Mastandrea .

Editor information

Editors and Affiliations

  1. Massachusetts Institute of Technology, Cambridge, Massachusetts, USA

    Nadia Polikarpova

  2. University of Surrey, Guildford, United Kingdom

    Steve Schneider

Rights and permissions

Reprints and permissions

Copyright information

© 2017 Springer International Publishing AG

About this paper

Cite this paper

Henrio, L., Laneve, C., Mastandrea, V. (2017). Analysis of Synchronisations in Stateful Active Objects. In: Polikarpova, N., Schneider, S. (eds) Integrated Formal Methods. IFM 2017. Lecture Notes in Computer Science(), vol 10510. Springer, Cham. https://doi.org/10.1007/978-3-319-66845-1_13

Download citation

  • DOI: https://doi.org/10.1007/978-3-319-66845-1_13

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-319-66844-4

  • Online ISBN: 978-3-319-66845-1

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation