The essence of online data processing
The essence of online data processing
复制标题
DOI：
10.1145/3563320
复制
发表时间：
2022-10
影响因子：
--
通讯作者：
Philip Dexter;Yu David Liu;K. Chiu
中科院分区：
文献类型：
--
作者：
Philip Dexter;Yu David Liu;K. Chiu
数据处理系统是现代计算堆栈的基本组成部分。这些系统通常在线部署：它们不断接收数据处理操作的请求，并不断将结果返回给最终用户或客户端应用程序。在线数据处理系统具有超越传统数据处理的独特功能，为它们设计的优化是复杂的，特别是当数据本身是结构化和动态的时。本文介绍了DON演算，在线数据处理的第一个严格的基础。它捕获后端数据处理引擎和前端应用程序的基本行为，重点关注在线数据处理系统必不可少但独特的两个设计维度：增量操作处理（IOP）和时间局部性优化（TLO）。一个新颖的设计见解是，连续应用于数据的操作可以被定义为流经数据结构的操作流，这种抽象将IOP和TLO的不同设计统一在一个演算中。DON演算被赋予了一个机械化的元理论，该元理论围绕一个关键的可观察等价属性：尽管IOP和TLO引入了显著的非确定性执行，但DON演算数据处理的可观察结果与没有IOP和TLO的传统数据处理相同。从广义上讲，DON演算是积极追求为软件系统堆栈提供严格保证的一个新实例。DON演算的规范和机械化为未来数据处理系统的设计者提供了坚实的基础，帮助他们接受严格的语义工程，而无需从头开始开发。
Data processing systems are a fundamental component of the modern computing stack. These systems are routinely deployed online: they continuously receive the requests of data processing operations, and continuously return the results to end users or client applications. Online data processing systems have unique features beyond conventional data processing, and the optimizations designed for them are complex, especially when data themselves are structured and dynamic. This paper describes DON Calculus, the first rigorous foundation for online data processing. It captures the essential behavior of both the backend data processing engine and the frontend application, with the focus on two design dimensions essential yet unique to online data processing systems: incremental operation processing (IOP) and temporal locality optimization (TLO). A novel design insight is that the operations continuously applied to the data can be defined as an operation stream flowing through the data structure, and this abstraction unifies diverse designs of IOP and TLO in one calculus. DON Calculus is endowed with a mechanized metatheory centering around a key observable equivalence property: despite the significant non-deterministic executions introduced by IOP and TLO, the observable result of DON Calculus data processing is identical to that of conventional data processing without IOP and TLO. Broadly, DON Calculus is a novel instance in the active pursuit of providing rigorous guarantees to the software system stack. The specification and mechanization of DON Calculus provide a sound base for the designers of future data processing systems to build upon, helping them embrace rigorous semantic engineering without the need of developing from scratch.