Online streaming algorithms, tailored for continuous data processing, offer substantial benefits but are often more intricate to design than their offline counterparts. This paper introduces a novel approach for automatically synthesizing online streaming algorithms from their offline versions. In particular, we propose a novel methodology, based on the notion of relational function signature (RFS), for deriving an online algorithm given its offline version. Then, we propose a concrete synthesis algorithm that is an instantiation of the proposed methodology. Our algorithm uses the RFS to decompose the synthesis problem into a set of independent subtasks and uses a combination of symbolic reasoning and search to solve each subproblem. We implement the proposed technique in a new tool called Opera and evaluate it on over 50 tasks spanning two domains: statistical computations and online auctions. Our results show that Opera can automatically derive the online version of the original algorithm for 98% of the tasks. Our experiments also demonstrate that Opera significantly outperforms alternative approaches, including adaptations of SyGuS solvers to this problem as well as two of Opera's own ablations.

翻译：在线流式算法专为连续数据处理而设计，具有显著优势，但其设计往往比离线算法更为复杂。本文提出了一种新方法，能够从离线版本自动合成在线流式算法。具体而言，我们基于关系函数签名（RFS）的概念提出了一种新方法论，用于从给定离线算法推导出相应的在线算法。随后，我们给出了一种具体的合成算法，作为所提方法论的一个实例化。该算法利用RFS将合成问题分解为一组独立的子任务，并通过符号推理与搜索相结合的方式求解每个子问题。我们将所提出的技术实现为一个名为Opera的新工具，并在涵盖两个领域（统计计算与在线拍卖）的50余项任务上进行了评估。结果表明，Opera能够为98%的任务自动推导出原始算法的在线版本。实验还显示，Opera的性能显著优于替代方法，包括针对该问题适配的SyGuS求解器以及Opera自身的两种消融变体。