利用验证提升的并行数据处理框架
Leveraging Parallel Data Processing Frameworks with Verified Lifting
摘要：
近年来，许多并行数据框架被提出，它们允许顺序程序访问并行处理。为了利用这些框架的优势，现有代码必须经常重写为每个框架支持的特定于域的语言。这种重写--单调乏味且容易出错--还要求开发人员在给定特定工作负载的情况下选择最优化性能的框架。本文介绍了Casper，一种新型的编译器，自动重定向顺序Java代码在Hadoop上执行，Hadoop是一个并行数据处理框架，实现了MapReduce范式。给定一个顺序代码片段，Casper使用验证提升来推断用我们的程序规约语言表达的高级摘要，然后编译该摘要以在Hadoop上执行。我们演示了Casper自动将Java基准转换为Hadoop。翻译结果的执行速度平均比顺序实现快3.3倍，并且可以更好地扩展到更大的数据集。
英文摘要：
Many parallel data frameworks have been proposed in recent years that let sequential programs access parallel processing. To capitalize on the benefits of such frameworks, existing code must often be rewritten to the domain-specific languages that each framework supports. This rewriting-tedious and error-prone-also requires developers to choose the framework that best optimizes performance given a specific workload. This paper describes Casper, a novel compiler that automatically retargets sequential Java code for execution on Hadoop, a parallel data processing framework that implements the MapReduce paradigm. Given a sequential code fragment, Casper uses verified lifting to infer a high-level summary expressed in our program specification language that is then compiled for execution on Hadoop. We demonstrate that Casper automatically translates Java benchmarks into Hadoop. The translated results execute on average 3.3x faster than the sequential implementations and scale better, as well, to larger datasets.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
