Static Analysis of Shape in TensorFlow Programs

Authors Sifis Lagouvardos, Julian Dolby, Neville Grech, Anastasios Antoniadis, Yannis Smaragdakis



PDF
Thumbnail PDF

File

LIPIcs.ECOOP.2020.15.pdf
  • Filesize: 0.61 MB
  • 29 pages

Document Identifiers

Author Details

Sifis Lagouvardos
  • University of Athens, Greece
Julian Dolby
  • IBM Research, Yorktown Heights, NY, USA
Neville Grech
  • University of Athens, Greece
Anastasios Antoniadis
  • University of Athens, Greece
Yannis Smaragdakis
  • University of Athens, Greece

Cite As Get BibTex

Sifis Lagouvardos, Julian Dolby, Neville Grech, Anastasios Antoniadis, and Yannis Smaragdakis. Static Analysis of Shape in TensorFlow Programs. In 34th European Conference on Object-Oriented Programming (ECOOP 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 166, pp. 15:1-15:29, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020) https://doi.org/10.4230/LIPIcs.ECOOP.2020.15

Abstract

Machine learning has been widely adopted in diverse science and engineering domains, aided by reusable libraries and quick development patterns. The TensorFlow library is probably the best-known representative of this trend and most users employ the Python API to its powerful back-end. TensorFlow programs are susceptible to several systematic errors, especially in the dynamic typing setting of Python. We present Pythia, a static analysis that tracks the shapes of tensors across Python library calls and warns of several possible mismatches. The key technical aspects are a close modeling of library semantics with respect to tensor shape, and an identification of violations and error-prone patterns. Pythia is powerful enough to statically detect (with 84.62% precision) 11 of the 14 shape-related TensorFlow bugs in the recent Zhang et al. empirical study - an independent slice of real-world bugs.

Subject Classification

ACM Subject Classification
  • Theory of computation → Program analysis
  • Software and its engineering → Compilers
  • Software and its engineering → General programming languages
Keywords
  • Python
  • TensorFlow
  • static analysis
  • Doop
  • Wala

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads

References

  1. Martín Abadi, Ashish Agarwal, Paul Barham, Eugene Brevdo, Zhifeng Chen, Craig Citro, Greg S. Corrado, Andy Davis, Jeffrey Dean, Matthieu Devin, Sanjay Ghemawat, Ian Goodfellow, Andrew Harp, Geoffrey Irving, Michael Isard, Yangqing Jia, Rafal Jozefowicz, Lukasz Kaiser, Manjunath Kudlur, Josh Levenberg, Dandelion Mané, Rajat Monga, Sherry Moore, Derek Murray, Chris Olah, Mike Schuster, Jonathon Shlens, Benoit Steiner, Ilya Sutskever, Kunal Talwar, Paul Tucker, Vincent Vanhoucke, Vijay Vasudevan, Fernanda Viégas, Oriol Vinyals, Pete Warden, Martin Wattenberg, Martin Wicke, Yuan Yu, and Xiaoqiang Zheng. TensorFlow: Large-scale machine learning on heterogeneous systems, 2015. Software available from tensorflow.org. URL: https://www.tensorflow.org/.
  2. Rami Al-Rfou, Guillaume Alain, Amjad Almahairi, Christof Angermueller, Dzmitry Bahdanau, Nicolas Ballas, Frederic Bastien, Justin Bayer, Anatoly Belikov, and others . Theano: A python framework for fast computation of mathematical expressions. arXiv preprint, January 2016. URL: http://arxiv.org/abs/1605.02688.
  3. Miltiadis Allamanis, Earl Barr, Premkumar Devanbu, and Charles Sutton. A survey of machine learning for big code and naturalness. ACM Computing Surveys, 51, September 2017. URL: https://doi.org/10.1145/3212695.
  4. Jong-hoon An, Avik Chaudhuri, and Jeffrey S. Foster. Static Typing for Ruby on Rails. In Proceedings of ASE, pages 590-594, November 2009. URL: https://doi.org/10.1109/ASE.2009.80.
  5. Davide Ancona, Massimo Ancona, Antonio Cuni, and Nicholas D. Matsakis. Rpython: A step towards reconciling dynamically and statically typed oo languages. In Proceedings of the 2007 Symposium on Dynamic Languages, DLS '07, pages 53-64, New York, NY, USA, 2007. ACM. URL: https://doi.org/10.1145/1297081.1297091.
  6. Ed Anderson, Zhaojun Bai, Jack Dongarra, A. Greenbaum, A. McKenney, Jeremy Du Croz, Sven Hammarling, James Demmel, Christian Bischof, and Danny C. Sorensen. Lapack: A portable linear algebra library for high-performance computers. In Proceedings of the 1990 ACM/IEEE Conference on Supercomputing, Supercomputing ’90, pages 2-11, Washington, DC, USA, 1990. IEEE Computer Society Press. Google Scholar
  7. bandit. https://github.com/openstack/bandit. Accessed: 2020-01-06.
  8. Martin Bravenboer and Yannis Smaragdakis. Exception analysis and points-to analysis: Better together. In Proc. of the 18th International Symp. on Software Testing and Analysis, ISSTA '09, pages 1-12, New York, NY, USA, 2009. ACM. URL: https://doi.org/10.1145/1572272.1572274.
  9. Martin Bravenboer and Yannis Smaragdakis. Strictly declarative specification of sophisticated points-to analyses. In Proc. of the 24th Annual ACM SIGPLAN Conf. on Object Oriented Programming, Systems, Languages, and Applications, OOPSLA '09, New York, NY, USA, 2009. ACM. Google Scholar
  10. Satish Chandra, Colin S. Gordon, Jean-Baptiste Jeannin, Cole Schlesinger, Manu Sridharan, Frank Tip, and Youngil Choi. Type inference for static compilation of JavaScript. SIGPLAN Not., 51(10):410-429, October 2016. URL: https://doi.org/10.1145/3022671.2984017.
  11. Wontae Choi, Satish Chandra, George C. Necula, and Koushik Sen. Sjs: A type system for JavaScript with fixed object layout. In Sandrine Blazy and Thomas Jensen, editors, SAS, volume 9291 of Lecture Notes in Computer Science, pages 181-198. Springer, 2015. URL: http://dblp.uni-trier.de/db/conf/sas/sas2015.html#ChoiCNS15.
  12. Julian Dolby, Avraham Shinnar, Allison Allain, and Jenna Reinen. Ariadne: Analysis for machine learning programs. In Proceedings of the 2Nd ACM SIGPLAN International Workshop on Machine Learning and Programming Languages, MAPL 2018, pages 1-10, New York, NY, USA, 2018. ACM. URL: https://doi.org/10.1145/3211346.3211349.
  13. Flake8. https://github.com/PyCQA/flake8. Accessed: 2020-01-06.
  14. Michael Furr, Jong-hoon (David) An, and Jeffrey S. Foster. Profile-guided static typing for dynamic scripting languages. In Proceedings of OOPSLA, pages 283-300, 2009. URL: https://doi.org/10.1145/1639949.1640110.
  15. Michael Gorbovitski, Yanhong A. Liu, Scott D. Stoller, Tom Rothamel, and Tuncay K. Tekle. Alias analysis for optimization of dynamic languages. In Proceedings of the 6th Symposium on Dynamic Languages, DLS '10, pages 27-42, New York, NY, USA, 2010. ACM. URL: https://doi.org/10.1145/1869631.1869635.
  16. Neville Grech, Bernd Fischer, and Julian Rathke. Preemptive type checking. Journal of Logical and Algebraic Methods in Programming, 101:151-181, 2018. URL: https://doi.org/10.1016/j.jlamp.2018.08.003.
  17. Clemens Grelck and Sven-Bodo Scholz. SAC - a functional array language for efficient multi-threaded execution. International Journal of Parallel Programming, 34(4):383-427, August 2006. URL: https://doi.org/10.1007/s10766-006-0018-x.
  18. Salvatore Guarnieri and Benjamin Livshits. GateKeeper: mostly static enforcement of security and reliability policies for Javascript code. In Proc. of the 18th USENIX Security Symposium, SSYM' 09, pages 151-168, Berkeley, CA, USA, 2009. USENIX Association. URL: http://dl.acm.org/citation.cfm?id=1855768.1855778.
  19. Brian Hackett and Shu-yu Guo. Fast and precise hybrid type inference for JavaScript. In Proceedings of the 33rd ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI '12, pages 239-250, New York, NY, USA, 2012. ACM. URL: https://doi.org/10.1145/2254064.2254094.
  20. Elnar Hajiyev, Mathieu Verbaere, and Oege de Moor. CodeQuest: Scalable source code queries with Datalog. In Proc. of the 20th European Conf. on Object-Oriented Programming, ECOOP '06, pages 2-27. Springer, 2006. Google Scholar
  21. jedi. https://github.com/davidhalter/jedi. Accessed: 2020-01-06.
  22. Simon Holm Jensen, Anders Møller, and Peter Thiemann. Type analysis for JavaScript. In Proceedings of the 16th International Symposium on Static Analysis, SAS '09, pages 238-255, Berlin, Heidelberg, 2009. Springer-Verlag. URL: https://doi.org/10.1007/978-3-642-03237-0_17.
  23. Melvin Johnson, Mike Schuster, Quoc V. Le, Maxim Krikun, Yonghui Wu, Zhifeng Chen, Nikhil Thorat, Fernanda Viégas, Martin Wattenberg, Greg Corrado, Macduff Hughes, and Jeffrey Dean. Google’s multilingual neural machine translation system: Enabling zero-shot translation. Transactions of the Association for Computational Linguistics, 5:339-351, 2017. URL: https://transacl.org/ojs/index.php/tacl/article/view/1081.
  24. Herbert Jordan, Bernhard Scholz, and Pavle Subotić. Soufflé: On synthesis of program analyzers. In Swarat Chaudhuri and Azadeh Farzan, editors, Computer Aided Verification, pages 422-430, Cham, 2016. Springer International Publishing. Google Scholar
  25. George Kastrinis and Yannis Smaragdakis. Hybrid context-sensitivity for points-to analysis. In Proc. of the 2013 ACM SIGPLAN Conf. on Programming Language Design and Implementation, PLDI '13, New York, NY, USA, 2013. ACM. Google Scholar
  26. Sanjay Krishnan and Eugene Wu. Palm: Machine learning explanations for iterative debugging. In Proceedings of the 2Nd Workshop on Human-In-the-Loop Data Analytics, HILDA'17, pages 4:1-4:6, New York, NY, USA, 2017. ACM. URL: https://doi.org/10.1145/3077257.3077271.
  27. Monica S. Lam, John Whaley, V. Benjamin Livshits, Michael C. Martin, Dzintars Avots, Michael Carbin, and Christopher Unkel. Context-sensitive program analysis as database queries. In Proc. of the 24th Symp. on Principles of Database Systems, PODS '05, pages 1-12, New York, NY, USA, 2005. ACM. URL: https://doi.org/10.1145/1065167.1065169.
  28. Benjamin S. Lerner, Liam Elberty, Jincheng Li, and Shriram Krishnamurthi. Combining form and function: Static types for jquery programs. In Proceedings of the 27th European Conference on Object-Oriented Programming, ECOOP'13, pages 79-103, Berlin, Heidelberg, 2013. Springer-Verlag. URL: https://doi.org/10.1007/978-3-642-39038-8_4.
  29. Benjamin S. Lerner, Joe Gibbs Politz, Arjun Guha, and Shriram Krishnamurthi. Tejas: Retrofitting type systems for JavaScript. SIGPLAN Not., 49(2):1-16, October 2013. URL: https://doi.org/10.1145/2578856.2508170.
  30. Percy Liang and Mayur Naik. Scaling abstraction refinement via pruning. In Proc. of the 2011 ACM SIGPLAN Conf. on Programming Language Design and Implementation, PLDI '11, pages 590-601, New York, NY, USA, 2011. ACM. URL: https://doi.org/10.1145/1993498.1993567.
  31. Shiqing Ma, Yousra Aafer, Zhaogui Xu, Wen-Chuan Lee, Juan Zhai, Yingqi Liu, and Xiangyu Zhang. Lamp: Data provenance for graph based machine learning algorithms through derivative computation. In Proceedings of the 2017 11th Joint Meeting on Foundations of Software Engineering, ESEC/FSE 2017, pages 786-797, New York, NY, USA, 2017. ACM. URL: https://doi.org/10.1145/3106237.3106291.
  32. Shiqing Ma, Yingqi Liu, Wen-Chuan Lee, Xiangyu Zhang, and Ananth Grama. Mode: Automated neural network model debugging via state differential analysis and input selection. In Proceedings of the 2018 26th ACM Joint Meeting on European Software Engineering Conference and Symposium on the Foundations of Software Engineering, ESEC/FSE 2018, pages 175-186, New York, NY, USA, 2018. ACM. URL: https://doi.org/10.1145/3236024.3236082.
  33. Magnus Madsen, Benjamin Livshits, and Michael Fanning. Practical static analysis of JavaScript applications in the presence of frameworks and libraries. In Proc. of the ACM SIGSOFT International Symp. on the Foundations of Software Engineering, FSE '13, pages 499-509. ACM, 2013. URL: https://doi.org/10.1145/2491411.2491417.
  34. Simon Marlow and Philip Wadler. A practical subtyping system for Erlang. In Proceedings of ICFP, pages 136-149, August 1997. URL: https://doi.org/10.1145/258949.258962.
  35. mccabe. https://pypi.python.org/pypi/mccabe. Accessed: 2020-01-06.
  36. Mayur Naik, Alex Aiken, and John Whaley. Effective static race detection for java. In Proc. of the 2006 ACM SIGPLAN Conf. on Programming Language Design and Implementation, PLDI '06, pages 308-319, New York, NY, USA, 2006. ACM. URL: https://doi.org/10.1145/1133981.1134018.
  37. Adam Paszke, Sam Gross, Soumith Chintala, Gregory Chanan, Edward Yang, Zachary DeVito, Zeming Lin, Alban Desmaison, Luca Antiga, and Adam Lerer. Automatic differentiation in pytorch. In NIPS-W, 2017. Google Scholar
  38. Kexin Pei, Yinzhi Cao, Junfeng Yang, and Suman Jana. Deepxplore: Automated whitebox testing of deep learning systems. In Proceedings of the 26th Symposium on Operating Systems Principles, SOSP '17, pages 1-18, New York, NY, USA, 2017. ACM. URL: https://doi.org/10.1145/3132747.3132785.
  39. Simon J. D. Prince. Computer Vision: Models, Learning, and Inference. Cambridge University Press, New York, NY, USA, 1st edition, 2012. Google Scholar
  40. Prospector. https://prospector.readthedocs.io/en/master/. Accessed: 2020-01-06.
  41. pycodestyle. http://pep8.readthedocs.org/en/latest/. Accessed: 2020-01-06.
  42. pydocstyle. https://github.com/PyCQA/pydocstyle. Accessed: 2020-01-06.
  43. pyflakes. https://launchpad.net/pyflakes. Accessed: 2020-01-06.
  44. Pylint. http://www.pylint.org/. Accessed: 2020-01-06.
  45. Python Taint. https://github.com/python-security/pyt. Accessed: 2020-01-06.
  46. Thomas W. Reps. Demand interprocedural program analysis using logic databases. In R. Ramakrishnan, editor, Applications of Logic Databases, pages 163-196. Kluwer Academic Publishers, 1994. Google Scholar
  47. Micha Sharir and Amir Pnueli. Two approaches to interprocedural data flow analysis. In Steven S. Muchnick and Neil D. Jones, editors, Program flow analysis: theory and applications, chapter 7, pages 189-233. Prentice-Hall, Inc., Englewood Cliffs, NJ, 1981. Google Scholar
  48. Olin Shivers. Control-Flow Analysis of Higher-Order Languages. PhD thesis, Carnegie Mellon University, may 1991. Google Scholar
  49. Yannis Smaragdakis and George Balatsouras. Pointer analysis. Foundations and Trends in Programming Languages, 2(1):1-69, 2015. URL: https://doi.org/10.1561/2500000014.
  50. Manu Sridharan, Satish Chandra, Julian Dolby, Stephen J. Fink, and Eran Yahav. Alias analysis for object-oriented programs. In Dave Clarke, James Noble, and Tobias Wrigstad, editors, Aliasing in Object-Oriented Programming. Types, Analysis and Verification, volume 7850 of Lecture Notes in Computer Science, pages 196-232. Springer Berlin Heidelberg, 2013. URL: https://doi.org/10.1007/978-3-642-36946-9_8.
  51. Yuchi Tian, Kexin Pei, Suman Jana, and Baishakhi Ray. Deeptest: Automated testing of deep-neural-network-driven autonomous cars. In Proceedings of the 40th International Conference on Software Engineering, ICSE '18, pages 303-314, New York, NY, USA, 2018. ACM. URL: https://doi.org/10.1145/3180155.3180220.
  52. Raja Vallée-Rai, Phong Co, Etienne Gagnon, Laurie J. Hendren, Patrick Lam, and Vijay Sundaresan. Soot - a Java bytecode optimization framework. In Proc. of the 1999 Conf. of the Centre for Advanced Studies on Collaborative research, CASCON '99, pages 125-135. IBM Press, 1999. URL: http://dl.acm.org/citation.cfm?id=781995.782008.
  53. John Whaley, Dzintars Avots, Michael Carbin, and Monica S. Lam. Using Datalog with binary decision diagrams for program analysis. In Proc. of the 3rd Asian Symp. on Programming Languages and Systems, pages 97-118. Springer, 2005. URL: https://doi.org/10.1007/11575467_8.
  54. John Whaley and Monica S. Lam. Cloning-based context-sensitive pointer alias analysis using binary decision diagrams. In Proc. of the 2004 ACM SIGPLAN Conf. on Programming Language Design and Implementation, PLDI '04, pages 131-144, New York, NY, USA, 2004. ACM. URL: https://doi.org/10.1145/996841.996859.
  55. Xiaoyuan Xie, Joshua W. K. Ho, Christian Murphy, Gail Kaiser, Baowen Xu, and Tsong Yueh Chen. Testing and validating machine learning classifiers by metamorphic testing. J. Syst. Softw., 84(4):544-558, April 2011. URL: https://doi.org/10.1016/j.jss.2010.11.920.
  56. Zhaogui Xu, Peng Liu, Xiangyu Zhang, and Baowen Xu. Python predictive analysis for bug detection. In Proceedings of the 2016 24th ACM SIGSOFT International Symposium on Foundations of Software Engineering, FSE 2016, pages 121-132, New York, NY, USA, 2016. ACM. URL: https://doi.org/10.1145/2950290.2950357.
  57. Xin Zhang, Ravi Mangal, Radu Grigore, Mayur Naik, and Hongseok Yang. On abstraction refinement for program analyses in Datalog. In Proc. of the 2014 ACM SIGPLAN Conf. on Programming Language Design and Implementation, PLDI '14, pages 239-248, New York, NY, USA, 2014. ACM. URL: https://doi.org/10.1145/2594291.2594327.
  58. Yuhao Zhang, Yifan Chen, Shing-Chi Cheung, Yingfei Xiong, and Lu Zhang. An empirical study on tensorflow program bugs. In Proceedings of the 27th ACM SIGSOFT International Symposium on Software Testing and Analysis, ISSTA 2018, pages 129-140, New York, NY, USA, 2018. ACM. URL: https://doi.org/10.1145/3213846.3213866.
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail