More Web Proxy on the site http://driver.im/

research-article

Phased synthesis of divide and conquer programs

Authors:

Victor NicoletAuthors Info & Claims

PLDI 2021: Proceedings of the 42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation

Pages 974 - 986

https://doi.org/10.1145/3453483.3454089

Published: 18 June 2021 Publication History

Abstract

We propose a fully automated method that takes as input an iterative or recursive reference implementation and produces divide-and-conquer implementations that are functionally equivalent to the input. Three interdependent components have to be synthesized: a function that divides the original problem instance, a function that solves each sub-instance, and a function that combines the results of sub-computations. We propose a methodology that splits the synthesis problem into three successive phases, each with a substantially reduced state space compared to the original monolithic task, and therefore substantially more tractable. Our methodology is implemented as an addition to the existing synthesis tool Parsynt, and we demonstrate the efficacy of it by synthesizing highly nontrivial divide-and-conquer implementations of a set of benchmarks fully automatically.

Supplementary Material

Auxiliary Archive (pldi21main-p457-p-archive.zip)

This supplementary material provides detailed examples and proofs to accompany the paper on Phased Synthesis of Divide and Conquer Programs.

Download
627.77 KB

References

[1]

Maaz Bin Safeer Ahmad and Alvin Cheung. 2018. Automatically Leveraging MapReduce Frameworks for Data-Intensive Applications. In Proceedings of the 2018 International Conference on Management of Data. ACM, New York, NY, USA. 1205–1220. isbn:9781450347037 https://doi.org/10.1145/3183713.3196891

Digital Library

[2]

Aws Albarghouthi, Isil Dillig, and Arie Gurfinkel. 2016. Maximal Specification Synthesis. In Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. ACM, New York, NY, USA. 789–801. isbn:9781450335492 https://doi.org/10.1145/2914770.2837628

Digital Library

[3]

Rajeev Alur, Rastislav Bodík, Eric Dallal, Dana Fisman, Pranav Garg, Garvit Juniwal, Hadas Kress-Gazit, P. Madhusudan, Milo M. K. Martin, Mukund Raghothaman, Shambwaditya Saha, Sanjit A. Seshia, Rishabh Singh, Armando Solar-Lezama, Emina Torlak, and Abhishek Udupa. 2015. Syntax-Guided Synthesis. In Dependable Software Systems Engineering. 1–25. https://doi.org/10.1109/FMCAD.2013.6679385

[4]

Yosi Ben-Asher and Gadi Haber. 2001. Parallel Solutions of Simple Indexed Recurrence Equations. IEEE Trans. Parallel Distrib. Syst., 12, 1 (2001), Jan., 22–37. issn:1045-9219 https://doi.org/10.1109/71.899937

Digital Library

[5]

Jon Louis Bentley, Dorothea Haken, and James B Saxe. 1978. A General Method for Solving Divide-and-Conquer Recurrences. https://doi.org/10.1145/1008861.1008865

Digital Library

[6]

Leonardo De Moura and Nikolaj Bjørner. 2008. Z3: An efficient SMT solver. In International conference on Tools and Algorithms for the Construction and Analysis of Systems. 337–340. https://doi.org/10.1007/978-3-540-78800-3_24

[7]

Jeffrey Dean and Sanjay Ghemawat. 2008. MapReduce: Simplified Data Processing on Large Clusters. Commun. ACM, 51, 1 (2008), Jan., 107–113. issn:0001-0782 https://doi.org/10.1145/1327452.1327492

Digital Library

[8]

Azadeh Farzan and Victor Nicolet. 2017. Synthesis of Divide and Conquer Parallelism for Loops. In Proceedings of the 38th ACM SIGPLAN Conference on Programming Language Design and Implementation. ACM, 540–555. isbn:978-1-4503-4988-8 https://doi.org/10.1145/3140587.3062355

Digital Library

[9]

Azadeh Farzan and Victor Nicolet. 2019. Modular Divide-and-conquer Parallelization of Nested Loops. In Proceedings of the 40th ACM SIGPLAN Conference on Programming Language Design and Implementation. ACM, 610–624. isbn:978-1-4503-6712-7 https://doi.org/10.1145/3314221.3314612

Digital Library

[10]

Azadeh Farzan and Victor Nicolet. 2021. From Iterative Implementations to Single-pass Functions. http://www.cs.toronto.edu/~azadeh/resources/papers/functional_translation.pdf (manuscript).

[11]

Grigory Fedyukovich, Maaz Bin Safeer Ahmad, and Rastislav Bodik. 2017. Gradual Synthesis for Static Parallelization of Single-Pass Array-Processing Programs. In Proceedings of the 38th ACM SIGPLAN Conference on Programming Language Design and Implementation. Association for Computing Machinery, New York, NY, USA. 572–585. isbn:9781450349888 https://doi.org/10.1145/3140587.3062382

Digital Library

[12]

Allan L. Fisher and Anwar M. Ghuloum. 1994. Parallelizing Complex Scans and Reductions. In Proceedings of the ACM SIGPLAN 1994 Conference on Programming Language Design and Implementation. 135–146. https://doi.org/10.1145/773473.178255

Digital Library

[13]

Alfons Geser and Sergei Gorlatch. 1997. Parallelizing Functional Programs by Generalization. In Proceedings of the 6th International Joint Conference on Algebraic and Logic Programming. 46–60. isbn:3-540-63459-2 https://doi.org/10.1017/S0956796899003536

Digital Library

[14]

Sergei Gorlatch. 1996. Systematic Extraction and Implementation of Divide-and-Conquer Parallelism. In Proceedings of the 8th International Symposium on Programming Languages: Implementations, Logics, and Programs. 274–288. isbn:3-540-61756-6 https://doi.org/10.1007/3-540-61756-6_91

[15]

Shachar Itzhaky, Rohit Singh, Armando Solar-Lezama, Kuat Yessenov, Yongquan Lu, Charles Leiserson, and Rezaul Chowdhury. 2016. Deriving divide-and-conquer dynamic programming algorithms using solver-aided transformations. In ACM SIGPLAN Notices. 51, 145–164. https://doi.org/10.1145/3022671.2983993

Digital Library

[16]

Xavier Leroy, Damien Doligez, Alain Frisch, Jacques Garrigue, Didier Rémy, and Jérôme Vouillon. 2018. The OCaml system release 4.07: Documentation and user’s manual.

[17]

Zohar Manna and Richard Waldinger. 1979. Synthesis: dreams → programs. IEEE Transactions on Software Engineering, 294–328. https://doi.org/10.1109/TSE.1979.234198

Digital Library

[18]

Akimasa Morihata and Kiminori Matsuzaki. 2010. Automatic Parallelization of Recursive Functions Using Quantifier Elimination. In Functional and Logic Programming, 10th International Symposium, FLOPS 2010, Sendai, Japan, April 19-21, 2010. Proceedings. 321–336. https://doi.org/10.1007/978-3-642-12251-4_23

Digital Library

[19]

Kazutaka Morita, Akimasa Morihata, Kiminori Matsuzaki, Zhenjiang Hu, and Masato Takeichi. 2007. Automatic Inversion Generates Divide-and-conquer Parallel Programs. In Proceedings of the 28th ACM SIGPLAN Conference on Programming Language Design and Implementation. 146–155. https://doi.org/10.1145/1273442.1250752

Digital Library

[20]

Victor Nicolet. 2017. Parsynt. https://github.com/victornicolet/parsynt

[21]

Cosmin Radoi, Stephen J. Fink, Rodric Rabbah, and Manu Sridharan. 2014. Translating Imperative Code to MapReduce. In Proceedings of the 2014 ACM International Conference on Object Oriented Programming Systems Languages & Applications. 909–927. isbn:978-1-4503-2585-1 https://doi.org/10.1145/2660193.2660228

Digital Library

[22]

Veselin Raychev, Madanlal Musuvathi, and Todd Mytkowicz. 2015. Parallelizing User-defined Aggregations Using Symbolic Execution. In Proceedings of the 25th Symposium on Operating Systems Principles. 153–167. isbn:978-1-4503-3834-9 https://doi.org/10.1145/2815400.2815418

Digital Library

[23]

Calvin Smith and Aws Albarghouthi. 2016. MapReduce Program Synthesis. In Proceedings of the 37th ACM SIGPLAN Conference on Programming Language Design and Implementation. 51, 326–340. issn:0362-1340 https://doi.org/10.1145/2980983.2908102

Digital Library

[24]

Douglas R Smith. 1985. Top-down synthesis of divide-and-conquer algorithms. Artificial Intelligence, 27, 1 (1985), 43–96. https://doi.org/10.1016/0004-3702(85)90083-9

Digital Library

[25]

Emina Torlak and Rastislav Bodík. 2013. Growing solver-aided languages with rosette. In ACM Symposium on New Ideas in Programming and Reflections on Software, Onward! 2013, part of SPLASH ’13, Indianapolis, IN, USA, October 26-31, 2013. 135–152. https://doi.org/10.1145/2509578.2509586

Digital Library

Cited By

Zhang ZSun YJi RLi SPeng XHuang ZLi SZhu TXiong Yd'Amorim M(2024)ASAC: A Benchmark for Algorithm SynthesisCompanion Proceedings of the 32nd ACM International Conference on the Foundations of Software Engineering10.1145/3663529.3663802(577-581)Online publication date: 10-Jul-2024
https://dl.acm.org/doi/10.1145/3663529.3663802
Ji RZhao YPolikarpova NXiong YHu Z(2024)Superfusion: Eliminating Intermediate Data Structures via Inductive SynthesisProceedings of the ACM on Programming Languages10.1145/36564158:PLDI(939-964)Online publication date: 20-Jun-2024
https://dl.acm.org/doi/10.1145/3656415
Ji RZhao YXiong YWang DZhang LHu Z(2024)Decomposition-based Synthesis for Applying Divide-and-Conquer-like Algorithmic ParadigmsACM Transactions on Programming Languages and Systems10.1145/364844046:2(1-59)Online publication date: 17-Jun-2024
https://dl.acm.org/doi/10.1145/3648440
Show More Cited By

Index Terms

Phased synthesis of divide and conquer programs
1. Software and its engineering
  1. Software creation and management
    1. Software development techniques
      1. Automatic programming
2. Theory of computation

Recommendations

Can reactive synthesis and syntax-guided synthesis be friends?
SPLASH Companion 2021: Companion Proceedings of the 2021 ACM SIGPLAN International Conference on Systems, Programming, Languages, and Applications: Software for Humanity

While reactive synthesis and syntax-guided synthesis (SyGuS) have seen enormous progress in recent years, combining the two approaches has remained a challenge. In this work, we present the synthesis of reactive programs from Temporal Stream Logic ...
Optimizing synthesis with metasketches
POPL '16

Many advanced programming tools---for both end-users and expert developers---rely on program synthesis to automatically generate implementations from high-level specifications. These tools often need to employ tricky, custom-built synthesis algorithms ...
Can reactive synthesis and syntax-guided synthesis be friends?
PLDI 2022: Proceedings of the 43rd ACM SIGPLAN International Conference on Programming Language Design and Implementation

While reactive synthesis and syntax-guided synthesis (SyGuS) have seen enormous progress in recent years, combining the two approaches has remained a challenge. In this work, we present the synthesis of reactive programs from Temporal Stream Logic ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM Conferences

PLDI 2021: Proceedings of the 42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation

June 2021

1341 pages

ISBN:9781450383912

DOI:10.1145/3453483

General Chair:
Stephen N. Freund
Williams College, USA
,
Program Chair:
Eran Yahav
Technion, Israel

Copyright © 2021 ACM.

Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than ACM must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected]

Sponsors

SIGPLAN: ACM Special Interest Group on Programming Languages

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 18 June 2021

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Badges

Author Tags

Qualifiers

Research-article

Conference

PLDI '21

Sponsor:

SIGPLAN

PLDI '21: 42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation

June 20 - 25, 2021

Virtual, Canada

Acceptance Rates

Overall Acceptance Rate 406 of 2,067 submissions, 20%

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

7
Total Citations
View Citations
210
Total Downloads

Downloads (Last 12 months)35
Downloads (Last 6 weeks)2

Reflects downloads up to 09 Jan 2025

Other Metrics

View Author Metrics

Citations

Cited By

Zhang ZSun YJi RLi SPeng XHuang ZLi SZhu TXiong Yd'Amorim M(2024)ASAC: A Benchmark for Algorithm SynthesisCompanion Proceedings of the 32nd ACM International Conference on the Foundations of Software Engineering10.1145/3663529.3663802(577-581)Online publication date: 10-Jul-2024
https://dl.acm.org/doi/10.1145/3663529.3663802
Ji RZhao YPolikarpova NXiong YHu Z(2024)Superfusion: Eliminating Intermediate Data Structures via Inductive SynthesisProceedings of the ACM on Programming Languages10.1145/36564158:PLDI(939-964)Online publication date: 20-Jun-2024
https://dl.acm.org/doi/10.1145/3656415
Ji RZhao YXiong YWang DZhang LHu Z(2024)Decomposition-based Synthesis for Applying Divide-and-Conquer-like Algorithmic ParadigmsACM Transactions on Programming Languages and Systems10.1145/364844046:2(1-59)Online publication date: 17-Jun-2024
https://dl.acm.org/doi/10.1145/3648440
Hu JChong SSeltzer M(2024)Parallel Assembly SynthesisLogic-Based Program Synthesis and Transformation10.1007/978-3-031-71294-4_1(3-26)Online publication date: 7-Sep-2024
https://doi.org/10.1007/978-3-031-71294-4_1
Sun YPeng XXiong Y(2023)Synthesizing Efficient Memoization AlgorithmsProceedings of the ACM on Programming Languages10.1145/36228007:OOPSLA2(89-115)Online publication date: 16-Oct-2023
https://dl.acm.org/doi/10.1145/3622800
Levy BIshaq MSherman BKennard LMilanova AZikas VMeng WJensen CCremers CKirda E(2023)COMBINE: COMpilation and Backend-INdependent vEctorization for Multi-Party ComputationProceedings of the 2023 ACM SIGSAC Conference on Computer and Communications Security10.1145/3576915.3623181(2531-2545)Online publication date: 15-Nov-2023
https://dl.acm.org/doi/10.1145/3576915.3623181
Cambronero JGulwani SLe VPerelman DRadhakrishna ASimon CTiwari A(2023)FlashFill++: Scaling Programming by Example by Cutting to the ChaseProceedings of the ACM on Programming Languages10.1145/35712267:POPL(952-981)Online publication date: 11-Jan-2023
https://dl.acm.org/doi/10.1145/3571226

View Options

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Publication

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Media

Figures

Other

Tables

View Table of Contents