Leveraging Parallel Data Processing Frameworks with Verified Lifting

• Main Authors: Maaz Bin Safeer Ahmad, Alvin Cheung
• Format: Article
• Language: English
• Published: Open Publishing Association 2016-11-01
• Series: Electronic Proceedings in Theoretical Computer Science
• Online Access: http://arxiv.org/pdf/1611.07623v1

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.