A Petri Net Based Modeling of Active Objects and Futures

• Autorzy: de Boer F. S. , Bravetti M. , Lee M. D. , Zavattaro G.

Identyfikatory

DOI

10.3233/FI-2018-1663

• Języki publikacji: EN

Abstrakty

EN

We give two different notions of deadlock for systems based on active objects and futures. One is based on blocked objects and conforms with the classical definition of deadlock by Coffman, Jr. et al. The other one is an extended notion of deadlock based on blocked processes which is more general than the classical one. We introduce a technique to prove deadlock freedom of systems of active objects. To check deadlock freedom an abstract version of the program is translated into Petri nets. Extended deadlocks, and then also classical deadlock, can be detected via checking reachability of a distinct marking. Absence of deadlocks in the Petri net constitutes deadlock freedom of the concrete system.

Słowa kluczowe

EN

Petri nets; active objects; deadlock analysis

• Wydawca: IOS Press
• Czasopismo: Fundamenta Informaticae
• Rocznik: 2018
• Tom: Vol. 159, nr 3
• Strony: 197--256
• Opis fizyczny: Bibliogr. 25 poz., rys., tab.

Twórcy

autor

de Boer F. S.

• Centrum Wiskunde and Informatica, Department of Software Engineering, Amsterdam, The Netherlands

autor

Bravetti M.

• Department of Computer Science and Engineering / Focus Team INRIA, University of Bologna, Bologna, Italy

autor

Lee M. D.

• Faculty of Mathematics, Astronomy and Physics (FAMAF), National University of Córdoba, Córdoba, Argentina

autor

Zavattaro G.

• Department of Computer Science and Engineering / Focus Team INRIA, University of Bologna, Bologna, Italy

Bibliografia

• [1] Armstrong J. Erlang. Communications of ACM, 2010. 53(9):68-75. doi:10.1145/1810891.1810910.
• [2] Haller P, Odersky M. Scala Actors: Unifying thread-based and event-based programming. Theoretical Computer Science, 2009. 410(2-3):202-220. URL https://doi.org/10.1016/j.tcs.2008.09.019.
• [3] Caromel D, Henrio L, Serpette BP. Asynchronous and deterministic objects. SIGPLAN Not., 2004. 39(1):123-134. doi:10.1145/982962.964012.
• [4] Edward G Coffman J, Elphick MJ, Shoshani A. System Deadlocks. ACM Computing Surveys, 1971. 3(2):67-78.
• [5] Johnsen EB, Owe O. An Asynchronous Communication Model for Distributed Concurrent Objects. Software and Systems Modeling, 2007. 2007. 6(1):39-58. doi:10.1007/s10270-006-0011-2.
• [6] Gul A Agha SFS Ian A Mason, Talcott CL. A foundation for actor computation. Journal of Functional Programming, 1997. 7(1):1-72. doi:10.1017/S095679689700261X.
• [7] Dijkstra EW. Cooperating sequential processes. In: Genuys F (ed.), Programming Languages: NATO Advanced Study Institute, pp. 43-112. Academic Press, 1968.
• [8] Holt RC. Some Deadlock Properties of Computer Systems. ACM Computing Surveys, 1972. 4(3):179-196. doi:10.1145/356603.356607.
• [9] de Boer FS, Bravetti M, Grabe I, Lee MD, Steffen M, Zavattaro G. A Petri Net Based Analysis of Deadlocks for Active Objects and Futures. In: Proceedings of 9th International Symposium on Formal Aspects of Component Software (FACS), volume 7684 of Lecture Notes in Computer Science. Springer, 2013 pp. 110-127. doi:10.1007/978-3-642-35861-6_7.
• [10] Ábrahám E, Grabe I, Grüner A, Steffen M. Behavioral interface description of an object-oriented language with futures and promises. Journal of Logic and Algebraic Programming, 2009. 78(7):491-518. URL https://doi.org/10.1016/j.jlap.2009.01.001.
• [11] Gordon AD, Hankin PD. A Concurrent Object Calculus: Reduction and Typing. In: Proceedings of 3rd International Workshop on High-Level Concurrent Languages (HLCL 1998), volume 16 no 3 of Electronic Notes in Theoretical Computer Science. Elsevier Science Publishers, 1998 pp. 248-264. URL https://doi.org/10.1016/S1571-0661(04)00145-8.
• [12] Abadi M, Cardelli L. A Theory of Objects. Monographs in Computer Science. Springer-Verlag, 1996. ISBN:0387947752.
• [13] Mayr E. Persistence of Vector Replacement Systems is Decidable. Acta Informatica, 1981. 15:309-318. URL https://doi.org/10.1007/BF00289268.
• [14] Karp R, Miller R. Parallel Program Schemata. Journal of Computer and system Sciences, 1969. 3(2):147-195. URL https://doi.org/10.1016/S0022-0000(69)80011-5.
• [15] Busi N, Zavattaro G. Deciding reachability problems in Turing-complete fragments of Mobile Ambients. Mathematical Structures in Computer Science, 2009. 19(6):1223-1263. URL https://doi.org/10.1017/S0960129509990181.
• [16] Agha G, de Cindio F, Rozenberg G (eds.). Concurrent Object-Oriented Programming and Petri Nets, Advances in Petri Nets, volume 2001 of Lecture Notes in Computer Science. Springer, 2001. doi:10.1007/3-540-45397-0.
• [17] Valk R. Object Petri Nets: Using the Nets-within-Nets Paradigm. In: Advances in Petri Nets, volume 3098 of Lecture Notes in Computer Science. Springer, 2003 pp. 819-848. URL https://doi.org/10.1007/978-3-540-27755-2_23.
• [18] Buchs D, Guelfi N. CO-OPN: a Concurrent Object Oriented Petri Net Approach. In: Proceedings of the 12th International Conference on Application and Theory of Petri Nets (ICATPN). 1991 pp. 432-454.
• [19] Sibertin-Blanc C. CoOperative Objects: Principles, Use and Implementation. In: Concurrent Object-Oriented Programming and Petri Nets, Advances in Petri Nets, volume 2001 of Lecture Notes in Computer Science. Springer, 2001 pp. 216-246. URL https://doi.org/10.1007/3-540-45397-0_7.
• [20] Lilius J. OB(PN)2: An Object Based Petri Net Programming Notation (Extended Abstract). In: Proceedings of the 2nd International Euro-Par Conference (Euro-Par), volume 1123 of Lecture Notes in Computer Science. Springer, 1996 pp. 660-663.
• [21] Giachino E, Laneve C. Analysis of Deadlocks in Object Groups. In: Proceedings of the International Conference on Formal Techniques for Distributed Systems (FMOODS/FORTE), volume 6722 of Lecture Notes in Computer Science. Springer, 2011 pp. 168-182. URL https://doi.org/10.1007/978-3-642-21461-5_11.
• [22] Giachino E, Laneve C, Lienhardt M. A framework for deadlock detection in core ABS. Software and System Modeling, 2016. 15(4):1013-1048. URL https://doi.org/10.1007/s10270-014-0444-y.
• [23] Giachino E, Laneve C, Lascu T. Deadlock and Livelock Analysis in Concurrent Objects with Futures. Technical report, University of Bologna, 2011. URL http://www.cs.unibo.it/laneve/publications.html.
• [24] Bravetti M, Gorrieri R. Deciding and axiomatizing weak ST bisimulation for a process algebra with recursion and action refinement. ACM Transactions on Computational Logic, 2002. 3(4):465-520. doi:10.1145/566385.566386.
• [25] Flores-Montoya A, Albert E, Genaim S. May-Happen-in-Parallel Based Deadlock Analysis for Concurrent Objects. In: Proceedings of the International Conference on Formal Techniques for Distributed Systems (FMOODS/FORTE), volume 7892 of Lecture Notes in Computer Science. Springer, 2013 pp. 273-288. URL https://doi.org/10.1007/978-3-642-38592-6_19.

Uwagi

Opracowanie rekordu w ramach umowy 509/P-DUN/2018 ze środków MNiSW przeznaczonych na działalność upowszechniającą naukę (2018).