zbMATH — the first resource for mathematics

A reduction semantics for direct-style asynchronous observables. (English) Zbl 1423.68097
Summary: Asynchronous programming has gained in importance, not only due to hardware developments like multi-core processors, but also due to pervasive asynchronicity in client-side Web programming and large-scale Web applications. However, asynchronous programming is challenging. For example, control-flow management and error handling are much more complex in an asynchronous than a synchronous context. Programming with asynchronous event streams is especially difficult: expressing asynchronous stream producers and consumers requires explicit state machines in continuation-passing style when using widely-used languages like Java.
In order to address this challenge, recent language designs like Google’s Dart introduce asynchronous generators which allow expressing complex asynchronous programs in a familiar blocking style while using efficient non-blocking concurrency control under the hood. However, several issues remain unresolved, including the integration of analogous constructs into statically-typed languages, and the formalization and proof of important correctness properties.
This paper presents a design for asynchronous stream generators for Scala, thereby extending previous facilities for asynchronous programming in Scala from tasks/futures to asynchronous streams. We present a complete formalization of the programming model based on a reduction semantics and a static type system. Building on the formal model, we contribute a complete type soundness proof, as well as the proof of a subject reduction theorem which establishes that the programming model enforces an important state transition protocol for asynchronous streams.
68N30 Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.)
68Q55 Semantics in the theory of computing
Full Text: DOI
[1] Agha, Gul A., ACTORS: A Model of Concurrent Computation in Distributed Systems, Artif. Intell., (1986), The MIT Press: The MIT Press Cambridge, Massachusetts
[2] Agha, Gul A.; Mason, Ian A.; Smith, Scott F.; Talcott, Carolyn L., A foundation for actor computation, J. Funct. Program., 7, 1, 1-72, (January 1997)
[3] Armstrong, J., Erlang — a survey of the language and its industrial applications, (INAP’96 — The 9th Exhibitions and Symposium on Industrial Applications of Prolog. INAP’96 — The 9th Exhibitions and Symposium on Industrial Applications of Prolog, Hino, Tokyo, Japan, (October 1996)), 16-18
[4] Armstrong, Joe; Virding, Robert; Wikström, Claes; Williams, Mike, Concurrent Programming in Erlang, (1996), Prentice Hall · Zbl 0869.68026
[5] Bierhoff, Kevin; Beckman, Nels E.; Aldrich, Jonathan, Practical API protocol checking with access permissions, (Drossopoulou, Sophia, ECOOP. ECOOP, Lect. Notes Comput. Sci., vol. 5653, (2009), Springer), 195-219
[6] Bierman, Gavin; Parkinson, Matthew; Pitts, Andrew, MJ: An Imperative Core Calculus for Java and Java with Effects, (April 2003), University of Cambridge, Computer Laboratory, Technical Report UCAM-CL-TR-563
[7] Bierman, Gavin M.; Russo, Claudio V.; Mainland, Geoffrey; Meijer, Erik; Torgersen, Mads, Pause ’n’ play: formalizing asynchronous C#, (ECOOP, (2012), Springer), 233-257
[8] Bracha, Gilad, The Dart Programming Language, (2015), Addison-Wesley: Addison-Wesley Boston, Massachusetts
[9] Burmako, Eugene, Scala macros: let our powers combine!, (Proceedings of the 4th Workshop on Scala, (2013), ACM), 3:1-3:10
[10] de Boer, Frank S.; Clarke, Dave; Johnsen, Einar Broch, A complete guide to the future, (De Nicola, Rocco, ESOP. ESOP, Lect. Notes Comput. Sci., vol. 4421, (2007), Springer), 316-330
[11] DeLine, Robert; Fähndrich, Manuel, Typestates for objects, (Odersky, Martin, ECOOP. ECOOP, Lect. Notes Comput. Sci., vol. 3086, (2004), Springer), 465-490
[12] Ekman, Torbjörn; Hedin, Görel, Pluggable checking and inferencing of nonnull types for Java, J. Object Technol., 6, 9, 455-475, (2007)
[13] Eriksen, Marius, Your server as a function, Oper. Syst. Rev., 48, 1, 51-57, (2014)
[14] Lea, Doug, JSR166: concurrency utilities
[15] Eugster, Patrick Th.; Felber, Pascal; Guerraoui, Rachid; Kermarrec, Anne-Marie, The many faces of publish/subscribe, ACM Comput. Surv., 35, 2, 114-131, (2003)
[16] Fähndrich, Manuel; Leino, K. Rustan M., Declaring and checking non-null types in an object-oriented language, (Crocker, Ron; Steele, Guy L., OOPSLA, (2003), ACM), 302-312
[17] Flatt, Matthew; Krishnamurthi, Shriram; Felleisen, Matthias, A programmer’s reduction semantics for classes and mixins, (Alves-Foss, Jim, Formal Syntax and Semantics of Java. Formal Syntax and Semantics of Java, Lect. Notes Comput. Sci., vol. 1523, (1999), Springer), 241-269
[18] Forkmann, Steffen; Petricek, Tomas; Riley, Ryan; Scheffer, Mauricio; Fox, Jack, The FSharp.Control.AsyncSeq library
[19] Fournet, Cédric; Le Fessant, Fabrice; Maranget, Luc; Schmitt, Alan, JoCaml: a language for concurrent distributed and mobile programming, (Jeuring, Johan; Jones, Simon L. Peyton, Advanced Functional Programming. Advanced Functional Programming, Lect. Notes Comput. Sci., vol. 2638, (2002), Springer), 129-158
[20] Fournet, Cédric; Gonthier, Georges, The reflexive CHAM and the join-calculus, (Boehm, Hans-Juergen; Steele, Guy L., POPL, (1996), ACM), 372-385
[21] (April 2015), Reactive Streams Working Group. Reactive Streams 1.0
[22] Haller, Philipp, On the integration of the actor model in mainstream technologies: the Scala perspective, (Agha, Gul A.; Bordini, Rafael H.; Marron, Assaf; Ricci, Alessandro, AGERE!@SPLASH, (2012), ACM), 1-6
[23] Haller, Philipp; Van Cutsem, Tom, Implementing joins using extensible pattern matching, (COORDINATION, (2008), Springer), 135-152
[24] Haller, Philipp; Odersky, Martin, Scala actors: unifying thread-based and event-based programming, Theor. Comput. Sci., 410, 2-3, 202-220, (2009) · Zbl 1162.68396
[25] Haller, Philipp; Prokopec, Aleksandar; Miller, Heather; Klang, Viktor; Kuhn, Roland; Jovanovic, Vojin, SIP-14: futures and promises, (2012)
[26] Haller, Philipp; Zaugg, Jason, SIP-22: Async, (2013)
[27] (Hejlsberg, Anders; Togersen, Mads; Wiltamuth, Scott; Golde, Peter, The C# Programming Language, (2011), Addison-Wesley)
[28] Carl, Hewitt, Viewing control structures as patterns of passing messages, Artif. Intell., 8, 3, 323-364, (1977)
[29] Hoare, C. A.R., Communicating Sequential Processes, (1985), Prentice Hall · Zbl 0637.68007
[30] Honda, Kohei; Tokoro, Mario, An object calculus for asynchronous communication, (America, Pierre, ECOOP. ECOOP, Lect. Notes Comput. Sci., vol. 512, (1991), Springer), 133-147
[31] Honda, Kohei; Yoshida, Nobuko; Carbone, Marco, Multiparty asynchronous session types, J. ACM, 63, 1, 9:1-9:67, (2016) · Zbl 1426.68047
[32] Igarashi, Atsushi; Pierce, Benjamin C.; Wadler, Philip, Featherweight Java: a minimal core calculus for Java and GJ, ACM Trans. Program. Lang. Syst., 23, 3, 396-450, (2001)
[33] International, Ecma, Dart Programming Language Specification, (2015), 4th edition (ECMA-408)
[34] Jim, Trevor; Morrisett, J. Gregory; Grossman, Dan; Hicks, Michael W.; Cheney, James; Wang, Yanling, Cyclone: a safe dialect of C, (Ellis, Carla Schlatter, USENIX Annual Technical Conference, General Track, (2002), USENIX), 275-288
[35] Johnsen, Einar Broch; Hähnle, Reiner; Schäfer, Jan; Schlatte, Rudolf; Steffen, Martin, ABS: a core language for abstract behavioral specification, (FMCO, (2010), Springer), 142-164
[36] Johnsen, Einar Broch; Owe, Olaf, An asynchronous communication model for distributed concurrent objects, Softw. Syst. Model., 6, 1, 39-58, (2007)
[37] Johnson, R. E.; Foote, B., Designing reusable classes, J. Object-Oriented Program., 1, 2, 22-35, (1988)
[38] Halstead, Robert H., Multilisp: a language for concurrent symbolic computation, ACM Trans. Program. Lang. Syst., 7, 4, 501-538, (1985) · Zbl 0581.68037
[39] Karmani, Rajesh K.; Shali, Amin; Agha, Gul, Actor frameworks for the JVM platform: a comparative analysis, (Stephenson, Ben; Probst, Christian W., PPPJ, (2009), ACM), 11-20
[40] Liskov, Barbara; Shrira, Liuba, Promises: linguistic support for efficient asynchronous procedure calls in distributed systems, (Wexelblat, Richard L., PLDI, (1988), ACM), 260-267
[41] Meijer, Erik, Your mouse is a database, Commun. ACM, 55, 5, 66-73, (2012)
[42] Meijer, Erik; Millikin, Kevin; Bracha, Gilad, Spicing up Dart with side effects, ACM Queue, 13, 3, 40, (2015)
[43] Miller, Heather; Haller, Philipp; Odersky, Martin, Spores: a type-based foundation for closures in the age of concurrency and distribution, (Jones, Richard, ECOOP. ECOOP, Lect. Notes Comput. Sci., vol. 8586, (2014), Springer), 308-333
[44] Milner, Robin, Communicating and Mobile Systems - The Pi-Calculus, (1999), Cambridge University Press · Zbl 0942.68002
[45] Morrisett, J. Gregory; Walker, David; Crary, Karl; Glew, Neal, From system F to typed assembly language, ACM Trans. Program. Lang. Syst., 21, 3, 527-568, (1999)
[46] Odersky, Martin; Spoon, Lex; Venners, Bill, Programming in Scala, (2010), Artima
[47] Okur, Semih; Erdogan, Cansu; Dig, Danny, Converting parallel code from low-level abstractions to higher-level abstractions, (Jones, Richard, ECOOP. ECOOP, Lect. Notes Comput. Sci., vol. 8586, (2014), Springer), 515-540
[48] Östlund, Johan; Wrigstad, Tobias, Welterweight Java, (TOOLS (48), (2010), Springer), 97-116
[49] Ousterhout, John K.; Agrawal, Parag; Erickson, David; Kozyrakis, Christos; Leverich, Jacob; Mazières, David; Mitra, Subhasish; Narayanan, Aravind; Ongaro, Diego; Parulkar, Guru M.; Rosenblum, Mendel; Rumble, Stephen M.; Stratmann, Eric; Stutsman, Ryan, The case for RAMCloud, Commun. ACM, 54, 7, 121-130, (2011)
[50] Petricek, Tomas; Syme, Don, The F# computation expression zoo, (Flatt, Matthew; Guo, Hai-Feng, PADL. PADL, Lect. Notes Comput. Sci., vol. 8324, (2014), Springer), 33-48
[51] Pierce, Benjamin C., Types and Programming Languages, (2002), MIT Press · Zbl 0995.68018
[52] Schäfer, Jan; Poetzsch-Heffter, Arnd, JCobox: generalizing active objects to concurrent components, (D’Hondt, Theo, ECOOP. ECOOP, Lect. Notes Comput. Sci., vol. 6183, (2010), Springer), 275-299
[53] Stoy, Joseph E., Denotational Semantics: The Scott-Strachey Approach to Programming Language Theory, (1977), MIT Press: MIT Press Cambridge, MA · Zbl 0503.68059
[54] Syme, Don; Petricek, Tomas; Lomov, Dmitry, The F# asynchronous programming model, (Rocha, Ricardo; Launchbury, John, PADL, (2011), Springer), 175-189
[55] von Behren, J. Robert; Condit, Jeremy; Brewer, Eric A., Why events are a bad idea (for high-concurrency servers), (Jones, Michael B., HotOS, (2003), USENIX), 19-24
[56] Wright, Andrew K.; Felleisen, Matthias, A syntactic approach to type soundness, Inf. Comput., 115, 1, 38-94, (November 1994)
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.