Skip to main content

Transforming Threads into Actors: Learning Concurrency Structure from Execution Traces

  • Chapter
  • First Online:
Principles of Modeling

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

Abstract

The threads and shared memory model is still the most commonly used programming model. However, programs written using threads interacting with shared memory model are notoriously bug-prone and hard to comprehend. An important reason for this lack of comprehensibility is thread based programs obscure the natural structure of concurrency in a distributed world: actors executing autonomously with their own internal logic and interacting at arms length with each other. While actors encapsulate their internal state, enabling consistency invariants of the data structures to be maintained locally, thread-based programs use control-centric synchronization primitives (such as locks) that are divorced from the concurrency structure of a program. Making the concurrency structure explicit provides useful documentation for developers. Moreover, it may be useful for refactoring thread-based object-oriented programs into an actor-oriented programs based on message-passing and isolated state. We present a novel algorithm based on Bayesian inference that automatically infers the concurrency structure of programs from their traces. The concurrency structure is inferred as consistency invariants of program data, and expressed in terms of annotations on data fields and method parameters. We illustrate our algorithm on Java programs using type annotations in Java classes and suggest how such annotations may be useful.

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

Access this chapter

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. Agha, G.: Concurrent object-oriented programming. Commun. ACM 33(9), 125–141 (1990)

    Article  Google Scholar 

  2. Agha, G., Mason, I.A., Smith, S.F., Talcott, C.L.: A foundation for actor computation. J. Funct. Program. 7(1), 1–72 (1997)

    Article  MathSciNet  Google Scholar 

  3. Agha, G.A.: ACTORS - A Model of Concurrent Computation in Distributed Systems. MIT Press Series in Artificial Intelligence. MIT Press, Cambridge (1986)

    Google Scholar 

  4. Artho, C., Havelund, K., Biere, A.: High-level data races. In: NDDL 2003, pp. 82–93. ICEIS Press (2003)

    Article  Google Scholar 

  5. Artzi, S., Quinonez, J., Kieżun, A., Ernst, M.D.: Parameter reference immutability: formal definition, inference tool, and comparison. Autom. Softw. Eng. 16(1), 145–192 (2009)

    Article  Google Scholar 

  6. Astley, M., Sturman, D.C., Agha, G.: Customizable middleware for modular distributed software. Commun. ACM 44(5), 99–107 (2001)

    Article  Google Scholar 

  7. Biswas, S., Huang, J., Sengupta, A., Bond, M.D.: Doublechecker: efficient sound and precise atomicity checking. In: PLDI 2014. ACM (2014)

    Google Scholar 

  8. Boyapati, C., Lee, R., Rinard, M.C.: Ownership types for safe programming: preventing data races and deadlocks. In: OOPSLA 2002, pp. 211–230. ACM (2002)

    Article  Google Scholar 

  9. Burrows, M., Leino, K.R.M.: Finding stale-value errors in concurrent programs. Concurr. Pract. Exp. 16(12), 1161–1172 (2004)

    Article  Google Scholar 

  10. Charalambides, M., Dinges, P., Agha, G.A.: Parameterized, concurrent session types for asynchronous multi-actor interactions. Sci. Comput. Program. 115–116, 100–126 (2016)

    Article  Google Scholar 

  11. Clavel, M., et al.: Reflection, metalevel computation, and strategies. In: Clavel, M., et al. (eds.) All About Maude - A High-Performance Logical Framework. LNCS, vol. 4350, pp. 419–458. Springer, Heidelberg (2007). https://doi.org/10.1007/978-3-540-71999-1_14

    Chapter  Google Scholar 

  12. Clebsch, S., Drossopoulou, S., Blessing, S., McNeil, A.: Deny capabilities for safe, fast actors. In: Proceedings of the 5th International Workshop on Programming Based on Actors, Agents, and Decentralized Control, AGERE! 2015, pp. 1–12. ACM, New York (2015)

    Google Scholar 

  13. Cok, D.R.: OpenJML: JML for Java 7 by extending OpenJDK. In: Bobaru, M., Havelund, K., Holzmann, G.J., Joshi, R. (eds.) NFM 2011. LNCS, vol. 6617, pp. 472–479. Springer, Heidelberg (2011). https://doi.org/10.1007/978-3-642-20398-5_35

    Chapter  Google Scholar 

  14. Dinges, P., Agha, G.: Scoped synchronization constraints for large scale actor systems. In: Sirjani, M. (ed.) COORDINATION 2012. LNCS, vol. 7274, pp. 89–103. Springer, Heidelberg (2012). https://doi.org/10.1007/978-3-642-30829-1_7

    Chapter  Google Scholar 

  15. Dinges, P., Charalambides, M., Agha, G.: Automated inference of atomic sets for safe concurrent execution. In: Proceedings of the 11th ACM SIGPLAN-SIGSOFT Workshop on Program Analysis for Software Tools and Engineering, PASTE 2013, pp. 1–8. ACM, New York (2013)

    Google Scholar 

  16. Dinges, P., Charalambides, M., Agha, G.: Automated inference of atomic sets for safe concurrent execution. Technical report, UIUC, April 2013. http://hdl.handle.net/2142/43357

  17. Dolby, J., Hammer, C., Marino, D., Tip, F., Vaziri, M., Vitek, J.: A data-centric approach to synchronization. ACM TOPLAS 34(1), 4 (2012)

    Article  Google Scholar 

  18. Donkervoet, B., Agha, G.: Reflecting on aspect-oriented programming, metaprogramming, and adaptive distributed monitoring. In: de Boer, F.S., Bonsangue, M.M., Graf, S., de Roever, W.-P. (eds.) FMCO 2006. LNCS, vol. 4709, pp. 246–265. Springer, Heidelberg (2007). https://doi.org/10.1007/978-3-540-74792-5_11

    Chapter  Google Scholar 

  19. Erlang programming language. https://www.erlang.org

  20. Flanagan, C., Freund, S.N.: Atomizer: a dynamic atomicity checker for multithreaded programs. Sci. Comput. Program. 71(2), 89–109 (2008)

    Article  MathSciNet  Google Scholar 

  21. Flanagan, C., Freund, S.N.: FastTrack: efficient and precise dynamic race detection. In: Proceedings of the 2009 ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2009, pp. 121–133. ACM, New York (2009)

    Google Scholar 

  22. Flanagan, C., Freund, S.N., Yi, J.: Velodrome: a sound and complete dynamic atomicity checker for multithreaded programs. In: Proceedings of the 2008 ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2008, pp. 293–303. ACM, New York (2008)

    Google Scholar 

  23. Frølund, S., Agha, G.: A language framework for multi-object coordination. In: Nierstrasz, O.M. (ed.) ECOOP 1993. LNCS, vol. 707, pp. 346–360. Springer, Heidelberg (1993). https://doi.org/10.1007/3-540-47910-4_18

    Chapter  Google Scholar 

  24. Hammer, C., Dolby, J., Vaziri, M., Tip, F.: Dynamic detection of atomic-set-serializability violations. In: ICSE 2008, pp. 231–240. ACM (2008)

    Google Scholar 

  25. Hewitt, C., Bishop, P.B., Steiger, R.: A universal modular ACTOR formalism for artificial intelligence. In: Nilsson, N.J. (ed.) Proceedings of the 3rd International Joint Conference on Artificial Intelligence, Standford, CA, USA, 20–23 August 1973, pp. 235–245. William Kaufmann (1973)

    Google Scholar 

  26. Houck, C.R., Agha, G.: HAL: a high-level actor language and its distributed implementation. In: Shin, K.G. (ed.) Proceedings of the 1992 International Conference on Parallel Processing, University of Michigan, An Arbor, Michigan, USA, 17–21 August 1992, Volume II: Software, pp. 158–165. CRC Press (1992)

    Google Scholar 

  27. Huang, W., Milanova, A.: Inferring AJ types for concurrent libraries. In: FOOL 2012, pp. 82–88 (2012)

    Google Scholar 

  28. Lai, Z., Cheung, S.C., Chan, W.K.: Detecting atomic-set serializability violations in multithreaded programs through active randomized testing. In: ICSE 2010, pp. 235–244. ACM (2010)

    Google Scholar 

  29. Lee, E.A.: Model-driven development-from object-oriented design to actor-oriented design. In: Workshop on Software Engineering for Embedded Systems: From Requirements to Implementation (a.k.a. The Monterey Workshop) (2003)

    Google Scholar 

  30. Lee, E.A.: The problem with threads. Computer 39(5), 33–42 (2006)

    Article  Google Scholar 

  31. Lee, E.A., Liu, X., Neuendorffer, S.: Classes and inheritance in actor-oriented design. ACM Trans. Embed. Comput. Syst. 8(4), 29:1–29:26 (2009)

    Article  Google Scholar 

  32. Lightbend: Akka. https://akka.io

  33. Lightbend: Akka and the Java memory model. https://doc.akka.io/docs/akka/current/general/jmm.html

  34. Liu, P., Dolby, J., Zhang, C.: Finding incorrect compositions of atomicity. In: Proceedings of the 2013 9th Joint Meeting on Foundations of Software Engineering, ESEC/FSE 2013, pp. 158–168. ACM, New York (2013)

    Google Scholar 

  35. Lu, S., Park, S., Hu, C., Ma, X., Jiang, W., Li, Z., Popa, R.A., Zhou, Y.: MUVI: automatically inferring multi-variable access correlations and detecting related semantic and concurrency bugs. In: SOSP 2007, pp. 103–116. ACM (2007)

    Google Scholar 

  36. Lu, S., Park, S., Seo, E., Zhou, Y.: Learning from mistakes: a comprehensive study on real world concurrency bug characteristics. In: ASPLOS 2008, pp. 329–339. ACM (2008)

    Article  Google Scholar 

  37. Lu, S., Park, S., Zhou, Y.: Detecting concurrency bugs from the perspectives of synchronization intentions. IEEE Trans. Parallel Distrib. Syst. 23(6), 1060–1072 (2012)

    Article  Google Scholar 

  38. Lu, S., Tucek, J., Qin, F., Zhou, Y.: AVIO: detecting atomicity violations via access-interleaving invariants. IEEE Micro 27(1), 26–35 (2007)

    Article  Google Scholar 

  39. Milanova, A., Dong, Y.: Inference and checking of object immutability. In: Proceedings of the 13th International Conference on Principles and Practices of Programming on the Java Platform: Virtual Machines, Languages, and Tools, PPPJ 2016, pp. 6:1–6:12. ACM, New York (2016)

    Google Scholar 

  40. Negara, S., Karmani, R.K., Agha, G.A.: Inferring ownership transfer for efficient message passing. In: Cascaval, C., Yew, P. (eds.) Proceedings of the 16th ACM SIGPLAN Symposium on Principles and Practice of Parallel Programming, PPOPP 2011, San Antonio, TX, USA, 12–16 February 2011, pp. 81–90. ACM (2011)

    Google Scholar 

  41. Neykova, R., Yoshida, N.: Multiparty session actors. In: Kühn, E., Pugliese, R. (eds.) COORDINATION 2014. LNCS, vol. 8459, pp. 131–146. Springer, Heidelberg (2014). https://doi.org/10.1007/978-3-662-43376-8_9

    Chapter  Google Scholar 

  42. Palmskog, K., Hariri, F., Marinov, D.: A case study on executing instrumented code in Java PathFinder. In: Proceedings of JPF Workshop, JPF 2015 (2015)

    Article  Google Scholar 

  43. Papi, M.M., Ernst, M.D.: Compile-time type-checking for custom type qualifiers in Java. In: Companion to the 22nd ACM SIGPLAN Conference on Object-Oriented Programming Systems and Applications Companion, OOPSLA 2007, pp. 809–810. ACM, New York (2007)

    Google Scholar 

  44. Pearl, J.: Probabilistic Reasoning in Intelligent Systems: Networks of Plausible Inference. Morgan Kaufmann Publishers Inc., San Francisco (1988)

    MATH  Google Scholar 

  45. Srinivasan, S., Mycroft, A.: Kilim: isolation-typed actors for Java. In: Vitek, J. (ed.) ECOOP 2008. LNCS, vol. 5142, pp. 104–128. Springer, Heidelberg (2008). https://doi.org/10.1007/978-3-540-70592-5_6

    Chapter  Google Scholar 

  46. Sumner, W.N., Hammer, C., Dolby, J.: Marathon: detecting atomic-set serializability violations with conflict graphs. In: Khurshid, S., Sen, K. (eds.) RV 2011. LNCS, vol. 7186, pp. 161–176. Springer, Heidelberg (2012). https://doi.org/10.1007/978-3-642-29860-8_13

    Chapter  Google Scholar 

  47. Tomlinson, C., Kim, W., Scheevel, M., Singh, V., Will, B., Agha, G.: Rosette: an object-oriented concurrent systems architecture. SIGPLAN Not. 24(4), 91–93 (1989)

    Article  Google Scholar 

  48. Weeratunge, D., Zhang, X., Jagannathan, S.: Accentuating the positive: atomicity inference and enforcement using correct executions. In: OOPSLA 2011, pp. 19–34. ACM (2011)

    Article  Google Scholar 

Download references

Acknowledgements

The authors thank Peter Dinges, Farah Hariri, and Darko Marinov. This work is supported in part by the National Science Foundation under grants NSF CCF 14-38982 and NSF CCF 16-17401, and by AFOSR/AFRL Air Force Research Laboratory and the Air Force Office of Scientific Research under agreement FA8750-11-2-0084 for the Assured Cloud Computing at the University of Illinois at Urbana-Champaign.

Author information

Authors and Affiliations

Authors

Corresponding author

Correspondence to Gul Agha .

Editor information

Editors and Affiliations

Rights and permissions

Reprints and permissions

Copyright information

© 2018 Springer International Publishing AG, part of Springer Nature

About this chapter

Check for updates. Verify currency and authenticity via CrossMark

Cite this chapter

Agha, G., Palmskog, K. (2018). Transforming Threads into Actors: Learning Concurrency Structure from Execution Traces. In: Lohstroh, M., Derler, P., Sirjani, M. (eds) Principles of Modeling. Lecture Notes in Computer Science(), vol 10760. Springer, Cham. https://doi.org/10.1007/978-3-319-95246-8_2

Download citation

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

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-319-95245-1

  • Online ISBN: 978-3-319-95246-8

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics