A Formal, Resource Consumption-Preserving Translation from Actors with Cooperative Scheduling to Haskell

• Autorzy: Albert Elvira , Bezirgiannis Nikolaos , de Boer Frank , Martin-Martin Enrique

Identyfikatory

DOI

10.3233/FI-2020-1988

• Języki publikacji: EN

Abstrakty

EN

We present a formal translation of a resource-aware extension of the Abstract Behavioral Specification (ABS) language to the functional language Haskell. ABS is an actor-based language tailored to the modeling of distributed systems. It combines asynchronous method calls with a suspend and resume mode of execution of the method invocations. To cater for the resulting cooperative scheduling of the method invocations of an actor, the translation exploits for the compilation of ABS methods Haskell functions with continuations. The main result of this article is a correctness proof of the translation by means of a simulation relation between a formal semantics of the source language and a high-level operational semantics of the target language, i.e., a subset of Haskell. We further prove that the resource consumption of an ABS program extended with a cost model is preserved over this translation, as we establish an equivalence of the cost of executing the ABS program and its corresponding Haskell-translation. Concretely, the resources consumed by the original ABS program and those consumed by the Haskell program are the same, considering a cost model. Consequently, the resource bounds automatically inferred for ABS programs extended with a cost model, using resource analysis tools, are sound resource bounds also for the translated Haskell programs. Our experimental evaluation confirms the resource preservation over a set of benchmarks featuring different asymptotic costs.

Słowa kluczowe

EN

actor model; futures; cooperative multitasking; coroutine; continuation; functional programming; operational semantics

• Wydawca: IOS Press
• Czasopismo: Fundamenta Informaticae
• Rocznik: 2020
• Tom: Vol. 177, nr 3/4
• Strony: 203--234
• Opis fizyczny: Bibliogr. 31 poz., wykr.

Twórcy

autor

Albert Elvira

• Universidad Complutense de Madrid, Madrid, Spain

autor

Bezirgiannis Nikolaos

• Centrum Wiskunde & Informatica (CWI), Amsterdam, Netherlands

autor

de Boer Frank

• Centrum Wiskunde & Informatica (CWI), Amsterdam, Netherlands

autor

Martin-Martin Enrique

• Universidad Complutense de Madrid, Madrid, Spain

Bibliografia

• [1] Lorincz K, Chen Br, Waterman J, Werner-Allen G, Welsh M. Resource Aware Programming in the Pixie OS. In: Proceedings of the 6th ACM Conference on Embedded Network Sensor Systems, SenSys ’08. ISBN 978-1-59593-990-6, 2008 pp. 211-224.
• [2] Johnsen EB, Hähnle R, Schäfer J, Schlatte R, Steffen M. ABS: A Core Language for Abstract Behavioral Specification. In: FMCO ’10, LNCS 6957. Springer, 2010 pp. 142-164.
• [3] Flanagan C, Felleisen M. The Semantics of Future and its Use in Program Optimization. In: Proc. POPL’95. ACM. ISBN 0-89791-692-1, 1995 pp. 209-220. doi:10.1145/199448.199484.
• [4] de Boer FS, Clarke D, Johnsen EB. A Complete Guide to the Future. In: Proc. ESOP ’07, LNCS 4421, pp. 316-330. Springer. ISBN 978-3-540-71314-2, 2007. doi:10.1007/978-3-540-71316-6_22.
• [5] Knuth DE. The Art of Computer Programming, Volume 1: Fundamental Algorithms, 2nd Edition. Addison-Wesley Professional, 1973.
• [6] Albert E, de Boer FS, Hähnle R, Johnsen EB, Schlatte R, Tapia Tarifa SL, Wong PYH. Formal modeling and analysis of resource management for cloud architectures: an industrial case study using Real-Time ABS. Service Oriented Computing and Applications, 2014. 8(4):323-339.
• [7] Albert E, Arenas P, Fernández JC, Genaim S, Gómez-Zamalloa M, Puebla G, Román-Díez G. Object-sensitive cost analysis for concurrent objects. Softw. Test., Verif. Reliab., 2015. 25(3):218-271.
• [8] Wong PY, Albert E, Muschevici R, Proena J, Schfer J, Schlatte R. The ABS Tool Suite: Modelling, Executing and Analysing Distributed Adaptable Object-Oriented Systems. STTT, 2012. 14(5):567-588.
• [9] Albert E, Arenas P, Flores-Montoya A, Genaim S, Gómez-Zamalloa M, Martin-Martin E, Puebla G, Román-Díez G. SACO: Static Analyzer for Concurrent Objects. In: Proc. TACAS ’14, LNCS 8413, pp. 562-567. Springer. ISBN 978-3-642-54861-1, 2014. doi:10.1007/978-3-642-54862-8_46.
• [10] Srinivasan S, Mycroft A. Kilim: Isolation-Typed Actors for Java. In: Proc. ECOOP ’08, LNCS 5142, pp. 104-128. Springer, 2008.
• [11] Bezirgiannis N, de Boer FS. ABS: A High-Level Modeling Language for Cloud-Aware Programming. In: Proc. SOFSEM’16, LNCS 9587, pp. 433-444. Springer, 2016.
• [12] Palacios A, Vidal G. Towards Modelling Actor-Based Concurrency in Term Rewriting. In: Proc. WPTE’15, volume 46 of OASICS. Dagstuhl Pub., 2015 pp. 19-29. doi:10.4230/OASIcs.WPTE.2015.19.
• [13] Vidal G. Towards Erlang Verification by Term Rewriting. In: Proc. LOPSTR ’13, LNCS 8901. Springer, 2013 pp. 109-126. doi:10.1007/978-3-319-14125-1_7.
• [14] Noll T. A Rewriting Logic Implementation of Erlang. ENTCS, 2001. 44(2):206-224. Proc. LDTA ’01.
• [15] Albert E, Arenas P, Gómez-Zamalloa M. Symbolic Execution of Concurrent Objects in CLP. In: Proc. PADL ’12, LNCS 7149. Springer, 2012 pp. 123-137. doi:10.1007/978-3-642-27694-1_10.
• [16] Nakata K, Saar A. Compiling Cooperative Task Management to Continuations. In: Proc. FSEN’13, LNCS 8161, pp. 95-110. Springer. ISBN 978-3-642-40212-8, 2013. doi:10.1007/978-3-642-40213-5_7.
• [17] Albert E, Bezirgiannis N, de Boer F, Martin-Martin E. A Formal, Resource Consumption-Preserving Translation of Actors to Haskell. In: Hermenegildo MV, Lopez-Garcia P (eds.), Proc. LOPSTR’16 (Revised Selected Papers), volume 10184 of LNCS 10184. Springer International Publishing. ISBN 978-3-319-63139-4, 2017 pp. 21-37. doi:10.1007/978-3-319-63139-4_2.
• [18] Schäfer J, Poetzsch-Heffter A. JCoBox: Generalizing Active Objects to Concurrent Components. In: ECOOP ’10, LNCS 6183, pp. 275-299. Springer, 2010.
• [19] Dean J, Ghemawat S. MapReduce: Simplified Data Processing on Large Clusters. Commun. ACM, 2008. 51(1):107-113. doi:10.1145/1327452.1327492.
• [20] Appel AW, Jim T. Continuation-passing, Closure-passing Style. In: Proceedings of the 16th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL ’89. ACM, New York, NY, USA. ISBN 0-89791-294-2, 1989 pp. 293-302. doi:10.1145/75277.75303. URL http://doi.acm.org/10.1145/75277.75303.
• [21] Danvy O, Filinski A. Representing Control: a Study of the CPS Transformation. Mathematical Structures in Computer Science, 1992. 2(4):361391. doi:10.1017/S0960129500001535.
• [22] Nipkow T, Wenzel M, Paulson LC. Isabelle/HOL: A Proof Assistant for Higher-order Logic. Springer-Verlag, 2002. ISBN 3-540-43376-7.
• [23] Paulin-Mohring C. Introduction to the Coq Proof-Assistant for Practical Software Verification, pp. 45-95. Springer Berlin Heidelberg, Berlin, Heidelberg. ISBN 978-3-642-35746-6, 2012. doi:10.1007/978-3-642-35746-6_3. URL https://doi.org/10.1007/978-3-642-35746-6_3.
• [24] Claessen K, Hughes J. QuickCheck: A Lightweight Tool for Random Testing of Haskell Programs. In: Proc. ICFP ’00. ACM. ISBN 1-58113-202-6, 2000 pp. 268-279. doi:10.1145/351240.351266.
• [25] Albert E, Arenas P, Correas J, Genaim S, Gómez-Zamalloa M, Puebla G, Román-Díez G. Object-Sensitive Cost Analysis for Concurrent Objects. Software Testing, Verification and Reliability, 2015. 25(3):218-271. doi:10.1002/stvr.1569.
• [26] Tarau P. Coordination and Concurrency in Multi-engine Prolog. In: Proc. COORDINATION ’11, LNCS 6721. Springer. ISBN 978-3-642-21463-9, 2011 pp. 157-171.
• [27] Meseguer J. Twenty years of rewriting logic. J. Log. Algebr. Program., 2012. 81(7-8):721-781.
• [28] Rosu G. K: A Semantic Framework for Programming Languages and Formal Analysis Tools. In: Dependable Software Systems Engineering, pp. 186-206. IOS Press, 2017. doi:10.3233/978-1-61499-810-5-186.
• [29] Nipkow T, Paulson LC, Wenzel M. Isabelle/HOL - A Proof Assistant for Higher-Order Logic, volume 2283 of Lecture Notes in Computer Science. Springer, 2002.
• [30] Bertot Y, Castéran P. Interactive Theorem Proving and Program Development - Coq’Art: The Calculus of Inductive Constructions. Texts in Theoretical Computer Science. An EATCS Series. Springer, 2004.
• [31] Leroy X. Formal verification of a realistic compiler. Commun. ACM, 2009. 52(7):107-115.

Uwagi

Opracowanie rekordu ze środków MNiSW, umowa Nr 461252 w ramach programu "Społeczna odpowiedzialność nauki" - moduł: Popularyzacja nauki i promocja sportu (2021).