2020

Equivalence of Dataflow Graphs via Rewrite Rules Using a Graph-to-Sequence Neural Model

Kommrusch, Steve, Barollet, Théo, Pouchet, Louis-Noël

Understand

In this work we target the problem of provably computing the equivalence between two programs represented as dataflow graphs.

To this end, we formalize the problem of equivalence between two programs as finding a set of semantics-preserving rewrite rules from one into the other, such that after the rewrite the two programs are structurally identical, and therefore trivially equivalent.
We then develop the first graph-to-sequence neural network system for program equivalence, trained to produce such rewrite sequences from a carefully crafted automatic example generation algorithm.
We extensively evaluate our system on a rich multi-type linear algebra expression language, using arbitrary combinations of 100+ graph-rewriting axioms of equivalence.

Built on

A Comprehensive Survey on Graph Neural Networks
Original
Zonghan Wu, Shirui Pan, Fengwen Chen, Guodong Long, Chengqi Zhang, and Philip S. Yu. 2019 · 1901
Earlier work this paper cites.
Regular expressions and the equivalence of programs
Donald M Kaplan. 1969 · 1969
Earlier work this paper cites.
Dynamic Construction of Finite Automata from examples using Hill-climbing. In Proceedings of the Fourth Annual Conference of the Cognitive Science Society . Ann Arbor, Michigan, 105–108
M. Tomita. 1982 · 1982
Earlier work this paper cites.
Rewriting techniques for program synthesis. In International Conference on Rewriting Techniques and Applications . Springer, 388–403
Uday S Reddy. 1989 · 1989
Earlier work this paper cites.
Data flow analysis as model checking. In International Symposium on Theoretical Aspects of Computer Software . Springer, 346–364
Bernhard Steffen. 1991 · 1991
Earlier work this paper cites.
Symbolic model checking: 1020 states and beyond
Jerry R Burch, Edmund M Clarke, Kenneth L McMillan, David L Dill, and Lain-Jinn Hwang. 1992 · 1992
Earlier work this paper cites.
Scheduling dynamic dataflow graphs with bounded memory using the token flow model. In 1993 IEEE international conference on acoustics, speech, and signal processing , Vol. 1. IEEE, 429–432
Joseph Tobin Buck and Edward A Lee. 1993 · 1993
Earlier work this paper cites.
Model checking and abstraction
Edmund M Clarke, Orna Grumberg, and David E Long. 1994 · 1994
Earlier work this paper cites.
Long short-term memory
Sepp Hochreiter and Jürgen Schmidhuber. 1997 · 1997
Earlier work this paper cites.
Syntactic program transformations for automatic abstraction. In International Conference on Computer Aided Verification . Springer, 435–449
Kedar S Namjoshi and Robert P Kurshan. 2000 · 2000
Earlier work this paper cites.
Translation validation for an optimizing compiler
George C Necula. 2000 · 2000
Earlier work this paper cites.
On the equivalence of two systems of affine recurrence equations
Denis Barthou, Paul Feautrier, and Xavier Redon. 2002 · 2002
Earlier work this paper cites.
Behavioral consistency of C and Verilog programs using bounded model checking. In Proceedings 2003. Design Automation Conference (IEEE Cat. No. 03CH37451) . IEEE, 368–371
Edmund Clarke, Daniel Kroening, and Karen Yorav. 2003 · 2003
Earlier work this paper cites.
Model checking programs
Willem Visser, Klaus Havelund, Guillaume Brat, SeungJoon Park, and Flavio Lerda. 2003 · 2003
Earlier work this paper cites.
On the recognition of algorithm templates
Christophe Alias and Denis Barthou. 2004 · 2004
Earlier work this paper cites.
Approximate probabilistic model checking. In International Workshop on Verification, Model Checking, and Abstract Interpretation . Springer, 73–84
Thomas Hérault, Richard Lassaigne, Frédéric Magniette, and Sylvain Peyronnet. 2004 · 2004
Earlier work this paper cites.
Program transformation with Stratego/XT
Eelco Visser. 2004 · 2004
Earlier work this paper cites.
On probabilistic program equivalence and refinement. In International Conference on Concurrency Theory . Springer, 156–170
Andrzej S Murawski and Joël Ouaknine. 2005 · 2005
Earlier work this paper cites.

Similar

Inference rules for proving the equivalence of recursive procedures
Benny Godlin and Ofer Strichman. 2008 · 2008
Cited alongside, same era.
High-performance implementation of the level-3 BLAS
Kazushige Goto and Robert Van De Geijn. 2008 · 2008
Cited alongside, same era.
Program transformations using temporal logic side conditions
Sara Kalvala, Richard Warburton, and David Lacey. 2009 · 2009
Cited alongside, same era.
Proving optimizations correct using parameterized program equivalence
Sudipta Kundu, Zachary Tatlock, and Sorin Lerner. 2009 · 2009
Cited alongside, same era.
The Graph Neural Network Model
Franco Scarselli, Marco Gori, Ah Chung Tsoi, Markus Hagenbuchner, and Gabriele Monfardini. 2009 · 2009
Cited alongside, same era.
Equivalence checking of static affine programs using widening to handle recurrences. In Computer aided verification . Springer, 599–613
Sven Verdoolaege, Gerda Janssens, and Maurice Bruynooghe. 2009 · 2009
Cited alongside, same era.
A framework for formal verification of compiler optimizations
William Mansky and Elsa Gunter. 2010 · 2010
Cited alongside, same era.
Probabilistic theorem proving
Original
Vibhav Gogate and Pedro Domingos. 2012 · 2012
Cited alongside, same era.
Well-structured program equivalence is highly undecidable
Robert Goldblatt and Marcel Jackson. 2012 · 2012
Cited alongside, same era.
Equivalence checking of static affine programs using widening to handle recurrences
Sven Verdoolaege, Gerda Janssens, and Maurice Bruynooghe. 2012 · 2012
Cited alongside, same era.
Interactive theorem proving and program development: Coq’Art: the calculus of inductive constructions
Yves Bertot and Pierre Castéran. 2013 · 2013
Cited alongside, same era.
Verification of loop and arithmetic transformations of array-intensive behaviors
Chandan Karfa, Kunal Banerjee, Dipankar Sarkar, and Chittaranjan Mandal. 2013 · 2013
Cited alongside, same era.

Then

Tensorflow: Large-scale machine learning on heterogeneous distributed systems
Original
Martín Abadi, Ashish Agarwal, Paul Barham, Eugene Brevdo, Zhifeng Chen, Craig Citro, Greg S Corrado, Andy Davis, Jeffrey Dean, Matthieu Devin, et al · 2016
Later among the works it cites.
Polycheck: Dynamic verification of iteration space transformations on affine programs. In ACM SIGPLAN Notices , Vol. 51. ACM, 539–554
Wenlei Bao, Sriram Krishnamoorthy, Louis-Noël Pouchet, Fabrice Rastello, and Ponnuswamy Sadayappan. 2016 · 2016
Later among the works it cites.
PHOG: Probabilistic Model for Code. In Proceedings of The 33rd International Conference on Machine Learning (Proceedings of Machine Learning Research) , Maria Florina Balcan and Kilian Q. Weinberger (Eds.), Vol. 48. PMLR, New York, New York, USA, 2933–2942
Pavol Bielik, Veselin Raychev, and Martin Vechev. 2016 · 2016
Later among the works it cites.
Gated Graph Sequence Neural Networks. In Proceedings of ICLR’16 (proceedings of iclr’16 ed.)
Yujia Li, Richard Zemel, Marc Brockschmidt, and Daniel Tarlow. 2016 · 2016
Later among the works it cites.
Context2Name: A Deep Learning-Based Approach to Infer Natural Variable Names from Usage Contexts
Rohan Bavishi, Michael Pradel, and Koushik Sen. 2017 · 2017
Later among the works it cites.
OpenNMT: Open-Source Toolkit for Neural Machine Translation. In Proc. ACL
Guillaume Klein, Yoon Kim, Yuntian Deng, Jean Senellart, and Alexander M. Rush. 2017 · 2017
Later among the works it cites.
Neural Network-based Graph Embedding for Cross-Platform Binary Code Similarity Detection. In Proceedings of the 2017 ACM SIGSAC Conference on Computer and Communications Security (CCS ’17) . ACM, New York, NY, USA, 363–376
Xiaojun Xu, Chang Liu, Qian Feng, Heng Yin, Le Song, and Dawn Song. 2017 · 2017
Later among the works it cites.
Compilation error repair: for the student programs, from the student programs. In Proceedings of the 40th International Conference on Software Engineering: Software Engineering Education and Training . ACM, 78–87
Umair Z Ahmed, Pawan Kumar, Amey Karkare, Purushottam Kar, and Sumit Gulwani. 2018 · 2018
Later among the works it cites.
A Survey of Machine Learning for Big Code and Naturalness
Miltiadis Allamanis, Earl T. Barr, Premkumar Devanbu, and Charles Sutton. 2018a · 2018
Later among the works it cites.
Learning to Represent Programs with Graphs. In 6th International Conference on Learning Representations, ICLR 2018, Vancouver, BC, Canada, April 30 - May 3, 2018, Conference Track Proceedings
Miltiadis Allamanis, Marc Brockschmidt, and Mahmoud Khademi. 2018b · 2018
Later among the works it cites.
Graph-to-Sequence Learning using Gated Graph Neural Networks. In Proceedings of the 56th Annual Meeting of the Association for Computational Linguistics (Volume 1: Long Papers) . Association for Computational Linguistics, 273–283
Daniel Beck, Gholamreza Haffari, and Trevor Cohn. 2018 · 2018
Later among the works it cites.
An Empirical Evaluation of Rule Extraction from Recurrent Neural Networks
Qinglong Wang, Kaixuan Zhang, Alexander G. Ororbia, II, Xinyu Xing, Xue Liu, and C. Lee Giles. 2018 · 2018
Later among the works it cites.
Code2Vec: Learning Distributed Representations of Code
Uri Alon, Meital Zilberstein, Omer Levy, and Eran Yahav. 2019 · 2019
Later among the works it cites.
SequenceR: Sequence-to-Sequence Learning for End-to-End Program Repair
Zimin Chen, Steve Kommrusch, Michele Tufano, Louis-Noël Pouchet, Denys Poshyvanyk, and Martin Monperrus. 2019 · 2019
Later among the works it cites.
DIRE: A Neural Approach to Decompiled Identifier Naming. In International Conference on Automated Software Engineering (ASE ’19)
Jeremy Lacomis, Pengcheng Yin, Edward J. Schwartz, Miltiadis Allamanis, Claire Le Goues, Graham Neubig, and Bogdan Vasilescu. 2019 · 2019
Later among the works it cites.
Graph2Seq: Fusion Embedding Learning for Knowledge Graph Completion
W. Li, X. Zhang, Y. Wang, Z. Yan, and R. Peng. 2019 · 2019
Later among the works it cites.
An Empirical Study on Learning Bug-Fixing Patches in the Wild via Neural Machine Translation
Michele Tufano, Cody Watson, Gabriele Bavota, Massimiliano Di Penta, Martin White, and Denys Poshyvanyk. 2019 · 2019
Later among the works it cites.

Beyond the bibliography

alphaXiv searches the wider corpus for related work and actual follow-ups.

Open on alphaXiv

alphaXiv is searching for related work…

Reading the bibliography…