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自身的两种消融变体。