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.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
References
Agha, G.: Concurrent object-oriented programming. Commun. ACM 33(9), 125–141 (1990)
Agha, G., Mason, I.A., Smith, S.F., Talcott, C.L.: A foundation for actor computation. J. Funct. Program. 7(1), 1–72 (1997)
Agha, G.A.: ACTORS - A Model of Concurrent Computation in Distributed Systems. MIT Press Series in Artificial Intelligence. MIT Press, Cambridge (1986)
Artho, C., Havelund, K., Biere, A.: High-level data races. In: NDDL 2003, pp. 82–93. ICEIS Press (2003)
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)
Astley, M., Sturman, D.C., Agha, G.: Customizable middleware for modular distributed software. Commun. ACM 44(5), 99–107 (2001)
Biswas, S., Huang, J., Sengupta, A., Bond, M.D.: Doublechecker: efficient sound and precise atomicity checking. In: PLDI 2014. ACM (2014)
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)
Burrows, M., Leino, K.R.M.: Finding stale-value errors in concurrent programs. Concurr. Pract. Exp. 16(12), 1161–1172 (2004)
Charalambides, M., Dinges, P., Agha, G.A.: Parameterized, concurrent session types for asynchronous multi-actor interactions. Sci. Comput. Program. 115–116, 100–126 (2016)
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
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)
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
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
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)
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
Dolby, J., Hammer, C., Marino, D., Tip, F., Vaziri, M., Vitek, J.: A data-centric approach to synchronization. ACM TOPLAS 34(1), 4 (2012)
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
Erlang programming language. https://www.erlang.org
Flanagan, C., Freund, S.N.: Atomizer: a dynamic atomicity checker for multithreaded programs. Sci. Comput. Program. 71(2), 89–109 (2008)
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)
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)
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
Hammer, C., Dolby, J., Vaziri, M., Tip, F.: Dynamic detection of atomic-set-serializability violations. In: ICSE 2008, pp. 231–240. ACM (2008)
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)
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)
Huang, W., Milanova, A.: Inferring AJ types for concurrent libraries. In: FOOL 2012, pp. 82–88 (2012)
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)
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)
Lee, E.A.: The problem with threads. Computer 39(5), 33–42 (2006)
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)
Lightbend: Akka. https://akka.io
Lightbend: Akka and the Java memory model. https://doc.akka.io/docs/akka/current/general/jmm.html
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)
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)
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)
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)
Lu, S., Tucek, J., Qin, F., Zhou, Y.: AVIO: detecting atomicity violations via access-interleaving invariants. IEEE Micro 27(1), 26–35 (2007)
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)
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)
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
Palmskog, K., Hariri, F., Marinov, D.: A case study on executing instrumented code in Java PathFinder. In: Proceedings of JPF Workshop, JPF 2015 (2015)
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)
Pearl, J.: Probabilistic Reasoning in Intelligent Systems: Networks of Plausible Inference. Morgan Kaufmann Publishers Inc., San Francisco (1988)
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
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
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)
Weeratunge, D., Zhang, X., Jagannathan, S.: Accentuating the positive: atomicity inference and enforcement using correct executions. In: OOPSLA 2011, pp. 19–34. ACM (2011)
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
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2018 Springer International Publishing AG, part of Springer Nature
About this chapter
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)