Synchronization Schemas
Synchronization Schemas
复制标题
DOI：
10.1145/3452021.3458317
复制
发表时间：
2021-06
期刊：
影响因子：
--
通讯作者：
R. Alur;Phillip Hilliard;Z. Ives;Konstantinos Kallas;Konstantinos Mamouras;Filip Niksic;C. Stanford;V. Tannen;Anton Xue
中科院分区：
文献类型：
--
作者：
R. Alur;Phillip Hilliard;Z. Ives;Konstantinos Kallas;Konstantinos Mamouras;Filip Niksic;C. Stanford;V. Tannen;Anton Xue
我们提出了一个类型理论的框架，用于实时决策的数据流处理，其中所需的计算涉及顺序计算的混合，如平滑和检测的峰值和浪涌，自然并行计算，如关系运算，基于键的分区，和地图减少。我们的框架统一了顺序（有序）和关系（无序）数据模型。特别是，我们将同步模式定义为类型，并将串并行流（SPS）定义为这些类型的对象。同步模式在关系类型上强加了一个层次结构，该结构简洁地捕获不同类型的数据项之间的排序和同步需求。串并行流自然地对对象进行建模，例如关系、序列、关系序列、由键值索引的流集合、基于时间和基于事件的窗口以及通过嵌套这些而获得的更复杂的结构。我们引入串并行流转换器（SPST）作为一个特定于域的语言模块化规范的确定性转换在这样的流。SPST可证明只指定单调的转换，允许流，有一个模块化的结构，可以利用正确的并行实现，并且是可组合的，允许规范的复杂查询作为一个管道的转换。
We present a type-theoretic framework for data stream processing for real-time decision making, where the desired computation involves a mix of sequential computation, such as smoothing and detection of peaks and surges, and naturally parallel computation, such as relational operations, key-based partitioning, and map-reduce. Our framework unifies sequential (ordered) and relational (unordered) data models. In particular, we define synchronization schemas as types, and series-parallel streams (SPS) as objects of these types. A synchronization schema imposes a hierarchical structure over relational types that succinctly captures ordering and synchronization requirements among different kinds of data items. Series-parallel streams naturally model objects such as relations, sequences, sequences of relations, sets of streams indexed by key values, time-based and event-based windows, and more complex structures obtained by nesting of these. We introduce series-parallel stream transformers (SPST) as a domain-specific language for modular specification of deterministic transformations over such streams. SPSTs provably specify only monotonic transformations allowing streamability, have a modular structure that can be exploited for correct parallel implementation, and are composable allowing specification of complex queries as a pipeline of transformations.