Abstract
We propose a denotational semantic framework for deterministic dataflow and stream processing that encompasses a variety of existing streaming models. Our proposal is based on the idea that data streams, stream transformations, and stream-processing programs should be classified using types. The type of a data stream is captured formally by a monoid, an algebraic structure with a distinguished binary operation and a unit. The elements of a monoid model the finite fragments of a stream, the binary operation represents the concatenation of stream fragments, and the unit is the empty fragment. Stream transformations are modeled using monotone functions on streams, which we call stream transductions. These functions can be implemented using abstract machines with a potentially infinite state space, which we call stream transducers. This abstract typed framework of stream transductions and transducers can be used to (1) verify the correctness of streaming computations, that is, that an implementation adheres to the desired behavior, (2) prove the soundness of optimizing transformations, e.g. for parallelization and distribution, and (3) inform the design of programming models and query languages for stream processing. In particular, we show that several useful combinators can be supported by the full class of stream transductions and transducers: serial composition, parallel composition, and feedback composition.
Chapter PDF
Similar content being viewed by others
References
Abadi, D.J., Ahmad, Y., Balazinska, M., Cetintemel, U., Cherniack, M., Hwang, J.H., Lindner, W., Maskey, A., Rasin, A., Ryvkina, E., Tatbul, N., Xing, Y., Zdonik, S.: The design of the Borealis stream processing engine. In: Proceedings of the 2nd Biennial Conference on Innovative Data Systems Research (CIDR ’05). pp. 277–289 (2005), http://cidrdb.org/cidr2005/papers/P23.pdf
Abadi, D.J., Carney, D., Cetintemel, U., Cherniack, M., Convey, C., Lee, S., Stonebraker, M., Tatbul, N., Zdonik, S.: Aurora: A new model and architecture for data stream management. The VLDB Journal 12(2), 120–139 (2003). https://doi.org/10.1007/s00778-003-0095-z
Abbas, H., Alur, R., Mamouras, K., Mangharam, R., Rodionova, A.: Real-time decision policies with predictable performance. Proceedings of the IEEE, Special Issue on Design Automation for Cyber-Physical Systems 106(9), 1593–1615 (2018). https://doi.org/10.1109/JPROC.2018.2853608
Abbas, H., Rodionova, A., Mamouras, K., Bartocci, E., Smolka, S.A., Grosu, R.: Quantitative regular expressions for arrhythmia detection. IEEE/ACM Transactions on Computational Biology and Bioinformatics 16(5), 1586–1597 (2019). https://doi.org/10.1109/TCBB.2018.2885274
Affetti, L., Tommasini, R., Margara, A., Cugola, G., Della Valle, E.: Defining the execution semantics of stream processing engines. Journal of Big Data 4(1) (2017). https://doi.org/10.1186/s40537-017-0072-9
Akidau, T., Balikov, A., Bekiroğlu, K., Chernyak, S., Haberman, J., Lax, R., McVeety, S., Mills, D., Nordstrom, P., Whittle, S.: MillWheel: Fault-tolerant stream processing at Internet scale. Proceedings of the VLDB Endowment 6(11), 1033–1044 (2013). https://doi.org/10.14778/2536222.2536229
Akidau, T., Bradshaw, R., Chambers, C., Chernyak, S., Fernández-Moctezuma, R.J., Lax, R., McVeety, S., Mills, D., Perry, F., Schmidt, E., Whittle, S.: The dataflow model: A practical approach to balancing correctness, latency, and cost in massive-scale, unbounded, out-of-order data processing. Proceedings of the VLDB Endowment 8(12), 1792–1803 (2015). https://doi.org/10.14778/2824032.2824076
Alur, R., Černý, P.: Streaming transducers for algorithmic verification of single-pass list-processing programs. In: Proceedings of the 38th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. pp. 599–610. POPL ’11, ACM, New York, NY, USA (2011). https://doi.org/10.1145/1926385.1926454
Alur, R., Fisman, D., Mamouras, K., Raghothaman, M., Stanford, C.: Streamable regular transductions. Theoretical Computer Science 807, 15–41 (2020). https://doi.org/10.1016/j.tcs.2019.11.018
Alur, R., Mamouras, K.: An introduction to the StreamQRE language. Dependable Software Systems Engineering 50, 1–24 (2017). https://doi.org/10.3233/978-1-61499-810-5-1
Alur, R., Mamouras, K., Stanford, C.: Automata-based stream processing. In: Chatzigiannakis, I., Indyk, P., Kuhn, F., Muscholl, A. (eds.) Proceedings of the 44th International Colloquium on Automata, Languages, and Programming (ICALP ’17). Leibniz International Proceedings in Informatics (LIPIcs), vol. 80, pp. 112:1–112:15. Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik, Dagstuhl, Germany (2017). https://doi.org/10.4230/LIPIcs.ICALP.2017.112
Alur, R., Mamouras, K., Stanford, C.: Modular quantitative monitoring. Proceedings of the ACM on Programming Languages 3(POPL), 50:1–50:31 (2019). https://doi.org/10.1145/3290363
Alur, R., Mamouras, K., Stanford, C., Tannen, V.: Interfaces for stream processing systems. In: Lohstroh, M., Derler, P., Sirjani, M. (eds.) Principles of Modeling: Essays Dedicated to Edward A. Lee on the Occasion of His 60th Birthday, Lecture Notes in Computer Science, vol. 10760, pp. 38–60. Springer, Cham (2018). https://doi.org/10.1007/978-3-319-95246-8_3
Alur, R., Mamouras, K., Ulus, D.: Derivatives of quantitative regular expressions. In: Aceto, L., Bacci, G., Bacci, G., Ingólfsdóttir, A., Legay, A., Mardare, R. (eds.) Models, Algorithms, Logics and Tools: Essays Dedicated to Kim Guldstrand Larsen on the Occasion of His 60th Birthday, Lecture Notes in Computer Science, vol. 10460, pp. 75–95. Springer, Cham (2017). https://doi.org/10.1007/978-3-319-63121-9_4
Arasu, A., Babcock, B., Babu, S., Cieslewicz, J., Datar, M., Ito, K., Motwani, R., Srivastava, U., Widom, J.: STREAM: The Stanford data stream management system. Tech. Rep. 2004–20, Stanford InfoLab (2004), http://ilpubs.stanford.edu:8090/641/
Arasu, A., Babu, S., Widom, J.: The CQL continuous query language: Semantic foundations and query execution. The VLDB Journal 15(2), 121–142 (2006). https://doi.org/10.1007/s00778-004-0147-z
Arasu, A., Widom, J.: A denotational semantics for continuous queries over streams and relations. SIGMOD Record 33(3), 6–11 (2004). https://doi.org/10.1145/1031570.1031572
Babcock, B., Babu, S., Datar, M., Motwani, R., Widom, J.: Models and issues in data stream systems. In: Proceedings of the Twenty-first ACM SIGMOD-SIGACT-SIGART Symposium on Principles of Database Systems. pp. 1–16. PODS ’02, ACM, New York, NY, USA (2002). https://doi.org/10.1145/543613.543615
Bai, Y., Thakkar, H., Wang, H., Luo, C., Zaniolo, C.: A data stream language and system designed for power and extensibility. In: Proceedings of the 15th ACM International Conference on Information and Knowledge Management. pp. 337–346. CIKM ’06, ACM, New York, NY, USA (2006). https://doi.org/10.1145/1183614.1183664
Benveniste, A., Caspi, P., Edwards, S.A., Halbwachs, N., Guernic, P.L., de Simone, R.: The synchronous languages 12 years later. Proceedings of the IEEE 91(1), 64–83 (2003). https://doi.org/10.1109/JPROC.2002.805826
Benveniste, A., Guernic, P.L., Jacquemot, C.: Synchronous programming with events and relations: The SIGNAL language and its semantics. Science of Computer Programming 16(2), 103–149 (1991). https://doi.org/10.1016/0167-6423(91)90001-E
Berry, G., Gonthier, G.: The Esterel synchronous programming language: Design, semantics, implementation. Science of Computer Programming 19(2), 87–152 (1992). https://doi.org/10.1016/0167-6423(92)90005-V
Bertot, Y., Castéran, P.: Interactive Theorem Proving and Program Development. Springer (2013). https://doi.org/10.1007/978-3-662-07964-5
Bilsen, G., Engels, M., Lauwereins, R., Peperstraete, J.: Cyclo-static dataflow. IEEE Transactions on Signal Processing 44(2), 397–408 (1996). https://doi.org/10.1109/78.485935
Botan, I., Derakhshan, R., Dindar, N., Haas, L., Miller, R.J., Tatbul, N.: SECRET: A model for analysis of the execution semantics of stream processing systems. Proceedings of the VLDB Endowment 3(1–2), 232–243 (2010). https://doi.org/10.14778/1920841.1920874
Bouillet, E., Kothari, R., Kumar, V., Mignet, L., Nathan, S., Ranganathan, A., Turaga, D.S., Udrea, O., Verscheure, O.: Processing 6 billion CDRs/day: From research to production (experience report). In: Proceedings of the 6th ACM International Conference on Distributed Event-Based Systems. pp. 264–267. DEBS ’12, ACM, New York, NY, USA (2012). https://doi.org/10.1145/2335484.2335513
Bourke, T., Pouzet, M.: Zélus: A synchronous language with ODEs. In: Proceedings of the 16th International Conference on Hybrid Systems: Computation and Control. pp. 113–118. HSCC ’13, ACM, New York, NY, USA (2013). https://doi.org/10.1145/2461328.2461348
Boussinot, F., de Simone, R.: The ESTEREL language. Proceedings of the IEEE 79(9), 1293–1304 (1991). https://doi.org/10.1109/5.97299
Brenna, L., Demers, A., Gehrke, J., Hong, M., Ossher, J., Panda, B., Riedewald, M., Thatte, M., White, W.: Cayuga: A high-performance event processing engine. In: Proceedings of the 2007 ACM SIGMOD International Conference on Management of Data. pp. 1100–1102. SIGMOD ’07, ACM, New York, NY, USA (2007). https://doi.org/10.1145/1247480.1247620
Brock, J.D., Ackerman, W.B.: Scenarios: A model of non-determinate computation. In: DÃaz, J., Ramos, I. (eds.) Proceedings of the International Colloquium on the Formalization of Programming Concepts (ICFPC ’81). Lecture Notes in Computer Science, vol. 107, pp. 252–259. Springer, Berlin, Heidelberg (1981). https://doi.org/10.1007/3-540-10699-5_102
Caspi, P., Pilaud, D., Halbwachs, N., Plaice, J.A.: LUSTRE: A declarative language for real-time programming. In: Proceedings of the 14th ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages. pp. 178–188. POPL ’87, ACM, New York, NY, USA (1987). https://doi.org/10.1145/41625.41641
Chandrasekaran, S., Cooper, O., Deshpande, A., Franklin, M.J., Hellerstein, J.M., Hong, W., Krishnamurthy, S., Madden, S., Raman, V., Reiss, F., Shah, M.: TelegraphCQ: Continuous dataflow processing for an uncertain world. In: Proceedings of the First Biennial Conference on Innovative Data Systems Research (CIDR ’03) (2003), http://cidrdb.org/cidr2003/program/p24.pdf
Chen, C.M., Agrawal, H., Cochinwala, M., Rosenbluth, D.: Stream query processing for healthcare bio-sensor applications. In: Proceedings of the 20th International Conference on Data Engineering. pp. 791–794. ICDE ’04, IEEE (2004). https://doi.org/10.1109/ICDE.2004.1320048
Cooper, G.H., Krishnamurthi, S.: Embedding dynamic dataflow in a call-by-value language. In: Sestoft, P. (ed.) Proceedings of the 15th European Symposium on Programming (ESOP ’06). Lecture Notes in Computer Science, vol. 3924, pp. 294–308. Springer, Berlin, Heidelberg (2006). https://doi.org/10.1007/11693024_20
Coquand, T., Huet, G.: The calculus of constructions. Information and Computation 76(2), 95–120 (1988). https://doi.org/10.1016/0890-5401(88)90005-3
Courtney, A.: Frappé: Functional reactive programming in Java. In: Ramakrishnan, I.V. (ed.) Proceedings of the 3rd International Symposium on Practical Aspects of Declarative Languages (PADL ’01). Lecture Notes in Computer Science, vol. 1990, pp. 29–44. Springer, Berlin, Heidelberg (2001). https://doi.org/10.1007/3-540-45241-9_3
Cranor, C., Johnson, T., Spataschek, O., Shkapenyuk, V.: Gigascope: A stream database for network applications. In: Proceedings of the 2003 ACM SIGMOD International Conference on Management of Data. pp. 647–651. SIGMOD ’03, ACM, New York, NY, USA (2003). https://doi.org/10.1145/872757.872838
Czaplicki, E., Chong, S.: Asynchronous functional reactive programming for GUIs. In: Proceedings of the 34th ACM SIGPLAN Conference on Programming Language Design and Implementation. pp. 411–422. PLDI ’13, ACM, New York, NY, USA (2013). https://doi.org/10.1145/2491956.2462161
D’Angelo, B., Sankaranarayanan, S., Sanchez, C., Robinson, W., Finkbeiner, B., Sipma, H.B., Mehrotra, S., Manna, Z.: LOLA: Runtime monitoring of synchronous systems. In: Proceedings of the 12th International Symposium on Temporal Representation and Reasoning (TIME ’05). pp. 166–174. IEEE (2005). https://doi.org/10.1109/TIME.2005.26
Demers, A., Gehrke, J., Hong, M., Riedewald, M., White, W.: Towards expressive publish/subscribe systems. In: Ioannidis, Y., Scholl, M.H., Schmidt, J.W., Matthes, F., Hatzopoulos, M., Boehm, K., Kemper, A., Grust, T., Boehm, C. (eds.) Proceedings of the 10th International Conference on Extending Database Technology (EDBT ’06). Lecture Notes in Computer Science, vol. 3896, pp. 627–644. Springer, Berlin, Heidelberg (2006). https://doi.org/10.1007/11687238_38
Demers, A., Gehrke, J., Panda, B., Riedewald, M., Sharma, V., White, W.: Cayuga: A general purpose event monitoring system. In: Proceedings of the 3rd Biennial Conference on Innovative Data Systems Research (CIDR ’07). pp. 412–422 (2007), http://cidrdb.org/cidr2007/papers/cidr07p47.pdf
Dennis, J.B.: First version of a data flow procedure language. In: Robinet, B. (ed.) Programming Symposium. Lecture Notes in Computer Science, vol. 19, pp. 362–376. Springer, Berlin, Heidelberg (1974). https://doi.org/10.1007/3-540-06859-7_145
Deshmukh, J.V., Donzé, A., Ghosh, S., Jin, X., Juniwal, G., Seshia, S.A.: Robust online monitoring of signal temporal logic. Formal Methods in System Design 51(1), 5–30 (2017). https://doi.org/10.1007/s10703-017-0286-7
Dindar, N., Tatbul, N., Miller, R.J., Haas, L.M., Botan, I.: Modeling the execution semantics of stream processing engines with SECRET. The VLDB Journal 22(4), 421–446 (2013). https://doi.org/10.1007/s00778-012-0297-3
Elgot, C.C., Mezei, J.E.: On relations defined by generalized finite automata. IBM Journal of Research and Development 9(1), 47–68 (1965). https://doi.org/10.1147/rd.91.0047
Elliott, C., Hudak, P.: Functional reactive animation. In: Proceedings of the Second ACM SIGPLAN International Conference on Functional Programming. pp. 263–273. ICFP ’97, ACM, New York, NY, USA (1997). https://doi.org/10.1145/258948.258973
Elliott, C.M.: Push-pull functional reactive programming. In: Proceedings of the 2nd ACM SIGPLAN Symposium on Haskell. pp. 25–36. Haskell ’09, ACM, New York, NY, USA (2009). https://doi.org/10.1145/1596638.1596643
Ginsburg, S., Rose, G.F.: A characterization of machine mappings. Canadian Journal of Mathematics 18, 381–388 (1966). https://doi.org/10.4153/CJM-1966-040-3
Grathwohl, N.B.B., Kozen, D., Mamouras, K.: KAT + B! In: Proceedings of the Joint Meeting of the Twenty-Third EACSL Annual Conference on Computer Science Logic (CSL) and the Twenty-Ninth Annual ACM/IEEE Symposium on Logic in Computer Science (LICS). pp. 44:1–44:10. CSL-LICS ’14, ACM, New York, NY, USA (2014). https://doi.org/10.1145/2603088.2603095
Gyllstrom, D., Wu, E., Chae, H.J., Diao, Y., Stahlberg, P., Anderson, G.: SASE: Complex event processing over streams. In: Proceedings of the 3rd Biennial Conference on Innovative Data Systems Research (CIDR ’07). pp. 407–411 (2007), http://cidrdb.org/cidr2007/papers/cidr07p46.pdf
Halbwachs, N., Caspi, P., Raymond, P., Pilaud, D.: The synchronous data flow programming language LUSTRE. Proceedings of the IEEE 79(9), 1305–1320 (1991). https://doi.org/10.1109/5.97300
Havelund, K., Roşu, G.: Efficient monitoring of safety properties. International Journal on Software Tools for Technology Transfer 6(2), 158–173 (2004). https://doi.org/10.1007/s10009-003-0117-6
Hirzel, M.: Partition and compose: Parallel complex event processing. In: Proceedings of the 6th ACM International Conference on Distributed Event-Based Systems. pp. 191–200. DEBS ’12, ACM, New York, NY, USA (2012). https://doi.org/10.1145/2335484.2335506
Hirzel, M., Soulé, R., Schneider, S., Gedik, B., Grimm, R.: A catalog of stream processing optimizations. ACM Computing Surveys (CSUR) 46(4), 46:1–46:34 (2014). https://doi.org/10.1145/2528412
Hudak, P., Courtney, A., Nilsson, H., Peterson, J.: Arrows, robots, and functional reactive programming. In: Jeuring, J., Jones, S.L.P. (eds.) Revised Lectures of the 4th International School on Advanced Functional Programming: AFP 2002, Oxford, UK, August 19–24, 2002, Lecture Notes in Computer Science, vol. 2638, pp. 159–187. Springer, Berlin, Heidelberg (2003). https://doi.org/10.1007/978-3-540-44833-4_6
Hughes, J.: Generalising monads to arrows. Science of Computer Programming 37(1), 67–111 (2000). https://doi.org/10.1016/S0167-6423(99)00023-4
Jain, N., Mishra, S., Srinivasan, A., Gehrke, J., Widom, J., Balakrishnan, H., Çetintemel, U., Cherniack, M., Tibbetts, R., Zdonik, S.: Towards a streaming SQL standard. Proceedings of the VLDB Endowment 1(2), 1379–1390 (2008). https://doi.org/10.14778/1454159.1454179
Joyal, A., Street, R., Verity, D.: Traced monoidal categories. Mathematical Proceedings of the Cambridge Philosophical Society 119(3), 447–468 (1996). https://doi.org/10.1017/S0305004100074338
Kahn, G.: The semantics of a simple language for parallel programming. Information Processing 74, 471–475 (1974)
Kahn, G., MacQueen, D.B.: Coroutines and networks of parallel processes. Information Processing 77, 993–998 (1977)
Karp, R.M., Miller, R.E.: Properties of a model for parallel computations: Determinacy, termination, queueing. SIAM Journal on Applied Mathematics 14(6), 1390–1411 (1966). https://doi.org/10.1137/0114108
Kozen, D.: A completeness theorem for Kleene algebras and the algebra of regular events. Information and Computation 110(2), 366–390 (1994). https://doi.org/10.1006/inco.1994.1037
Kozen, D.: Kleene algebra with tests. ACM Transactions on Programming Languages and Systems (TOPLAS) 19(3), 427–443 (1997). https://doi.org/10.1145/256167.256195
Kozen, D., Mamouras, K.: Kleene algebra with equations. In: Esparza, J., Fraigniaud, P., Husfeldt, T., Koutsoupias, E. (eds.) Proceedings of the 41st International Colloquium on Automata, Languages and Programming (ICALP ’14). Lecture Notes in Computer Science, vol. 8573, pp. 280–292. Springer, Berlin, Heidelberg (2014). https://doi.org/10.1007/978-3-662-43951-7_24
Kozen, D., Parikh, R.: An elementary proof of the completeness of PDL. Theoretical Computer Science 14(1), 113–118 (1981). https://doi.org/10.1016/0304-3975(81)90019-0
Kozen, D., Tiuryn, J.: On the completeness of propositional Hoare logic. Information Sciences 139(3–4), 187–195 (2001). https://doi.org/10.1016/S0020-0255(01)00164-5
Krämer, J., Seeger, B.: Semantics and implementation of continuous sliding window queries over data streams. ACM Transactions on Database Systems (TODS) 34(1), 4:1–4:49 (2009). https://doi.org/10.1145/1508857.1508861
Krishnaswami, N.R.: Higher-order functional reactive programming without spacetime leaks. In: Proceedings of the 18th ACM SIGPLAN International Conference on Functional Programming. pp. 221–232. ICFP ’13, ACM, New York, NY, USA (2013). https://doi.org/10.1145/2500365.2500588
Krishnaswami, N.R., Benton, N.: Ultrametric semantics of reactive programs. In: Proceedings of the 26th Annual IEEE Symposium on Logic in Computer Science (LICS ’11). pp. 257–266. IEEE (2011). https://doi.org/10.1109/LICS.2011.38
Kulkarni, S., Bhagat, N., Fu, M., Kedigehalli, V., Kellogg, C., Mittal, S., Patel, J.M., Ramasamy, K., Taneja, S.: Twitter Heron: Stream processing at scale. In: Proceedings of the 2015 ACM SIGMOD International Conference on Management of Data. pp. 239–250. SIGMOD ’15, ACM, New York, NY, USA (2015). https://doi.org/10.1145/2723372.2742788
Law, Y.N., Wang, H., Zaniolo, C.: Relational languages and data models for continuous queries on sequences and data streams. ACM Transactions on Database Systems (TODS) 36(2), 8:1–8:32 (2011). https://doi.org/10.1145/1966385.1966386
Le Guernic, P., Benveniste, A., Bournai, P., Gautier, T.: SIGNAL-a data flow-oriented language for signal processing. IEEE Transactions on Acoustics, Speech, and Signal Processing 34(2), 362–374 (1986). https://doi.org/10.1109/TASSP.1986.1164809
Lee, E.A., Messerschmitt, D.G.: Synchronous data flow. Proceedings of the IEEE 75(9), 1235–1245 (1987). https://doi.org/10.1109/PROC.1987.13876
Leucker, M., Schallhart, C.: A brief account of runtime verification. The Journal of Logic and Algebraic Programming 78(5), 293–303 (2009). https://doi.org/10.1016/j.jlap.2008.08.004
Li, J., Maier, D., Tufte, K., Papadimos, V., Tucker, P.A.: Semantics and evaluation techniques for window aggregates in data streams. In: Proceedings of the 2005 ACM SIGMOD International Conference on Management of Data. pp. 311–322. SIGMOD ’05, ACM, New York, NY, USA (2005). https://doi.org/10.1145/1066157.1066193
Maier, D., Li, J., Tucker, P., Tufte, K., Papadimos, V.: Semantics of data streams and operators. In: Eiter, T., Libkin, L. (eds.) Proceedings of the 10th International Conference on Database Theory (ICDT ’05). Lecture Notes in Computer Science, vol. 3363, pp. 37–52. Springer, Berlin, Heidelberg (2005). https://doi.org/10.1007/978-3-540-30570-5_3
Maier, I., Odersky, M.: Higher-order reactive programming with incremental lists. In: Castagna, G. (ed.) Proceedings of the 27th European Conference on Object-Oriented Programming (ECOOP ’13). Lecture Notes in Computer Science, vol. 7920, pp. 707–731. Springer, Berlin, Heidelberg (2013). https://doi.org/10.1007/978-3-642-39038-8_29
Mamouras, K.: On the Hoare theory of monadic recursion schemes. In: Proceedings of the Joint Meeting of the 23rd EACSL Annual Conference on Computer Science Logic (CSL) and the 29th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS). pp. 69:1–69:10. CSL-LICS ’14, ACM, New York, NY, USA (2014). https://doi.org/10.1145/2603088.2603157
Mamouras, K.: Extensions of Kleene Algebra for Program Verification. Ph.D. thesis, Cornell University, Ithaca, NY (August 2015), http://hdl.handle.net/1813/40960
Mamouras, K.: Synthesis of strategies and the Hoare logic of angelic nondeterminism. In: Pitts, A. (ed.) Proceedings of the 18th International Conference on Foundations of Software Science and Computation Structures (FoSSaCS ’15). Lecture Notes in Computer Science, vol. 9034, pp. 25–40. Springer, Berlin, Heidelberg (2015). https://doi.org/10.1007/978-3-662-46678-0_2
Mamouras, K.: The Hoare logic of deterministic and nondeterministic monadic recursion schemes. ACM Transactions on Computational Logic (TOCL) 17(2), 13:1–13:30 (2016). https://doi.org/10.1145/2835491
Mamouras, K.: Synthesis of strategies using the Hoare logic of angelic and demonic nondeterminism. Logical Methods in Computer Science 12(3) (2016). https://doi.org/10.2168/LMCS-12(3:6)2016
Mamouras, K.: Equational theories of abnormal termination based on Kleene algebra. In: Esparza, J., Murawski, A.S. (eds.) Proceedings of the 20th International Conference on Foundations of Software Science and Computation Structures (FoSSaCS ’17). Lecture Notes in Computer Science, vol. 10203, pp. 88–105. Springer, Berlin, Heidelberg (2017). https://doi.org/10.1007/978-3-662-54458-7_6
Mamouras, K., Raghothaman, M., Alur, R., Ives, Z.G., Khanna, S.: StreamQRE: Modular specification and efficient evaluation of quantitative queries over streaming data. In: Proceedings of the 38th ACM SIGPLAN Conference on Programming Language Design and Implementation. pp. 693–708. PLDI ’17, ACM, New York, NY, USA (2017). https://doi.org/10.1145/3062341.3062369
Mamouras, K., Stanford, C., Alur, R., Ives, Z.G., Tannen, V.: Data-trace types for distributed stream processing systems. In: Proceedings of the 40th ACM SIGPLAN Conference on Programming Language Design and Implementation. pp. 670–685. PLDI ’19, ACM, New York, NY, USA (2019). https://doi.org/10.1145/3314221.3314580
McSherry, F., Murray, D.G., Isaacs, R., Isard, M.: Differential dataflow. In: Proceedings of the 6th Biennial Conference on Innovative Data Systems Research (CIDR ’13) (2013), http://cidrdb.org/cidr2013/Papers/CIDR13_Paper111.pdf
Mealy, G.H.: A method for synthesizing sequential circuits. The Bell System Technical Journal 34(5), 1045–1079 (1955). https://doi.org/10.1002/j.1538-7305.1955.tb03788.x
Mei, Y., Madden, S.: ZStream: A cost-based query processor for adaptively detecting composite events. In: Proceedings of the 2009 ACM SIGMOD International Conference on Management of Data. pp. 193–206. SIGMOD ’09, ACM, New York, NY, USA (2009). https://doi.org/10.1145/1559845.1559867
Meyerovich, L.A., Guha, A., Baskin, J., Cooper, G.H., Greenberg, M., Bromfield, A., Krishnamurthi, S.: Flapjax: A programming language for Ajax applications. In: Proceedings of the 24th ACM SIGPLAN Conference on Object Oriented Programming Systems Languages and Applications. pp. 1–20. OOPSLA ’09, ACM, New York, NY, USA (2009). https://doi.org/10.1145/1640089.1640091
Moore, E.F.: Gedanken-Experiments on Sequential Machines, Annals of Mathematics Studies, vol. 34, pp. 129–153. Princeton University Press (1956)
Motwani, R., Widom, J., Arasu, A., Babcock, B., Babu, S., Datar, M., Manku, G.S., Olston, C., Rosenstein, J., Varma, R.: Query processing, approximation, and resource management in a data stream management system. In: Proceedings of the First Biennial Conference on Innovative Data Systems Research (CIDR ’03) (2003), http://cidrdb.org/cidr2003/program/p22.pdf
Murray, D.G., McSherry, F., Isaacs, R., Isard, M., Barham, P., Abadi, M.: Naiad: A timely dataflow system. In: Proceedings of the Twenty-Fourth ACM Symposium on Operating Systems Principles. pp. 439–455. SOSP ’13, ACM, New York, NY, USA (2013). https://doi.org/10.1145/2517349.2522738
Nilsson, H., Courtney, A., Peterson, J.: Functional reactive programming, continued. In: Proceedings of the 2002 ACM SIGPLAN Workshop on Haskell. pp. 51–64. Haskell ’02, ACM, New York, NY, USA (2002). https://doi.org/10.1145/581690.581695
Noghabi, S.A., Paramasivam, K., Pan, Y., Ramesh, N., Bringhurst, J., Gupta, I., Campbell, R.H.: Samza: Stateful scalable stream processing at LinkedIn. Proceedings of the VLDB Endowment 10(12), 1634–1645 (2017). https://doi.org/10.14778/3137765.3137770
Raney, G.N.: Sequential functions. Journal of the ACM 5(2), 177–180 (1958). https://doi.org/10.1145/320924.320930
Rutten, J.J.M.M.: Automata and coinduction (an exercise in coalgebra). In: Sangiorgi, D., de Simone, R. (eds.) Proceedings of the 9th International Conference on Concurrency Theory (CONCUR ’98). Lecture Notes in Computer Science, vol. 1466, pp. 194–218. Springer, Berlin, Heidelberg (1998). https://doi.org/10.1007/BFb0055624
Rutten, J.J.M.M.: Universal coalgebra: A theory of systems. Theoretical Computer Science 249(1), 3–80 (2000). https://doi.org/10.1016/S0304-3975(00)00056-6
Rutten, J.J.M.M.: A coinductive calculus of streams. Mathematical Structures in Computer Science 15(1), 93–147 (2005). https://doi.org/10.1017/S0960129504004517
Sadri, R., Zaniolo, C., Zarkesh, A., Adibi, J.: Expressing and optimizing sequence queries in database systems. ACM Transactions on Database Systems 29(2), 282–318 (2004). https://doi.org/10.1145/1005566.1005568
Sakarovitch, J.: Elements of Automata Theory. Cambridge University Press (2009)
Schneider, S., Hirzel, M., Gedik, B., Wu, K.L.: Safe data parallelism for general streaming. IEEE Transactions on Computers 64(2), 504–517 (2015). https://doi.org/10.1109/TC.2013.221
Schützenberger, M.P.: Sur une variante des fonctions séquentielles. Theoretical Computer Science 4(1), 47–57 (1977). https://doi.org/10.1016/0304-3975(77)90055-X
Sculthorpe, N., Nilsson, H.: Safe functional reactive programming through dependent types. In: Proceedings of the 14th ACM SIGPLAN International Conference on Functional Programming. pp. 23–34. ICFP ’09, ACM, New York, NY, USA (2009). https://doi.org/10.1145/1596550.1596558
Shivers, O., Might, M.: Continuations and transducer composition. In: Proceedings of the 27th ACM SIGPLAN Conference on Programming Language Design and Implementation. pp. 295–307. PLDI ’06, ACM, New York, NY, USA (2006). https://doi.org/10.1145/1133981.1134016
Thati, P., Roşu, G.: Monitoring algorithms for metric temporal logic specifications. Electronic Notes in Theoretical Computer Science 113, 145–162 (2005). https://doi.org/10.1016/j.entcs.2004.01.029
The Coq development team: The Coq proof assistant. https://coq.inria.fr (2020), [Online; accessed February 22, 2020]
Thies, W., Karczmarek, M., Amarasinghe, S.: StreamIt: A language for streaming applications. In: Horspool, R.N. (ed.) Proceedings of the 11th International Conference on Compiler Construction (CC ’02). Lecture Notes in Computer Science, vol. 2304, pp. 179–196. Springer, Berlin, Heidelberg (2002). https://doi.org/10.1007/3-540-45937-5_14
Toshniwal, A., Taneja, S., Shukla, A., Ramasamy, K., Patel, J.M., Kulkarni, S., Jackson, J., Gade, K., Fu, M., Donham, J., Bhagat, N., Mittal, S., Ryaboy, D.: Storm @ Twitter. In: Proceedings of the 2014 ACM SIGMOD International Conference on Management of Data. pp. 147–156. SIGMOD ’14, ACM, New York, NY, USA (2014). https://doi.org/10.1145/2588555.2595641
Tucker, P.A., Maier, D., Sheard, T., Fegaras, L.: Exploiting punctuation semantics in continuous data streams. IEEE Transactions on Knowledge and Data Engineering 15(3), 555–568 (2003). https://doi.org/10.1109/TKDE.2003.1198390
Veanes, M., Hooimeijer, P., Livshits, B., Molnar, D., Bjorner, N.: Symbolic finite state transducers: Algorithms and applications. In: Proceedings of the 39th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. pp. 137–150. POPL ’12, ACM, New York, NY, USA (2012). https://doi.org/10.1145/2103656.2103674
Wu, E., Diao, Y., Rizvi, S.: High-performance complex event processing over streams. In: Proceedings of the 2006 ACM SIGMOD International Conference on Management of Data. pp. 407–418. SIGMOD ’06, ACM, New York, NY, USA (2006). https://doi.org/10.1145/1142473.1142520
Zaharia, M., Das, T., Li, H., Hunter, T., Shenker, S., Stoica, I.: Discretized streams: Fault-tolerant streaming computation at scale. In: Proceedings of the Twenty-Fourth ACM Symposium on Operating Systems Principles. pp. 423–438. SOSP ’13, ACM, New York, NY, USA (2013). https://doi.org/10.1145/2517349.2522737
Zaharia, M., Xin, R.S., Wendell, P., Das, T., Armbrust, M., Dave, A., Meng, X., Rosen, J., Venkataraman, S., Franklin, M.J., Ghodsi, A., Gonzalez, J., Shenker, S., Stoica, I.: Apache Spark: A unified engine for big data processing. Communications of the ACM 59(11), 56–65 (2016). https://doi.org/10.1145/2934664
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Open Access This chapter is licensed under the terms of the Creative Commons Attribution 4.0 International License (http://creativecommons.org/licenses/by/4.0/), which permits use, sharing, adaptation, distribution and reproduction in any medium or format, as long as you give appropriate credit to the original author(s) and the source, provide a link to the Creative Commons license and indicate if changes were made.
The images or other third party material in this chapter are included in the chapter's Creative Commons license, unless indicated otherwise in a credit line to the material. If material is not included in the chapter's Creative Commons license and your intended use is not permitted by statutory regulation or exceeds the permitted use, you will need to obtain permission directly from the copyright holder.
Copyright information
© 2020 The Author(s)
About this paper
Cite this paper
Mamouras, K. (2020). Semantic Foundations for Deterministic Dataflow and Stream Processing. In: Müller, P. (eds) Programming Languages and Systems. ESOP 2020. Lecture Notes in Computer Science(), vol 12075. Springer, Cham. https://doi.org/10.1007/978-3-030-44914-8_15
Download citation
DOI: https://doi.org/10.1007/978-3-030-44914-8_15
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-030-44913-1
Online ISBN: 978-3-030-44914-8
eBook Packages: Computer ScienceComputer Science (R0)