On the application of equivalence checking algorithms for program minimization
https://doi.org/10.15514/ISPRAS-2015-27(4)-8
Abstract
Equivalence checking algorithms found vast applications in system programming; they are used in software refactoring, security checking, malware detection, program integration, regression verification, compiler verification and validation. In this paper we show that equivalence checking procedures can be utilized for the development of global optimization transformation of programs. We consider minimization problem for two formal models of programs: deterministic finite state transducers over finitely generated decidable groups that are used as a model of sequential reactive programs, and deterministic program schemata that are used as a model of sequential imperative programs. Minimization problem for both models of programs can be solved following the same approach that is used for minimization of finite state automata by means of two basic optimizing transformations, namely, removing of useless states and joining equivalent states. The main results of the paper are Theorems 1 and 2.
About the Authors
V. A. Zakharov
ISP RAS; Lomonosov Moscow State University, 2nd Education Building, Faculty CMC, GSP-1; Moscow Institute of Physics and Technology; Higher School of Economics, National Research University
Russian Federation
Russian Federation
V. V. Podymov
Lomonosov Moscow State University, 2nd Education Building, Faculty CMC, GSP-1; Higher School of Economics, National Research University
Russian Federation
Russian Federation
References
1. Abel N.E., Bell J.R. Global optimization in compilers. Proceedings of the First USA-Japan Computer Conference. 1972.
2. Aho A.V., Sethi R., Ullman J.D. Compilers: principles, techniques, and tools. Addison-Wesley, Reading, MA, 1986.
3. Alias, C., Barthou, D. On the recognition of algorithm templates. Proceedings of the 2-nd International Workshop on Compiler Optimization Meets Compiler Verification, Electronic Notes in Theoretical Computer Science, 2004, v. 82, N 2, p. 395–409.
4. Alur R., Cerny P. Streaming transducers for algorithmic verification of single-pass list-processing programs. Proceedings of 38th ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages, 2011, p. 599-610.
5. Arons T., Elster E., Fix L., Mador-Haim S., Mishaeli M., Shalev J., Singerman E., Tiemeyer A., Vardi M. Y., Zuck L. D. Formal verification of backward compatibility of microcode. CAV, 2005, p. 185–198.
6. Allen F.E., Cocke J.L. A catalogue of optimizing transformations. Design and Optimization of Compilers, Prentice-Hall, Englewood Cliffs, N.J., 1972.
7. Barthe, G., D’Argenio, P.R., Rezk, T. Secure information flow by self-composition. Proceedings of the 17th IEEE Workshop on Computer Security Foundations, 2004, p. 100.
8. Benton, N. Simple relational correctness proofs for static analyses and program transformations. Proceedings of the 31st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 2004, ACM, New York.
9. Blattner M, Head T. The decidability of equivalence for deterministic finite transducers. Journal of Computer and System Sciences, 1979, v. 19, p. 45-49.
10. Busam V.A., England D.E. Optimization of expressions in Fortran. Communications of the Association for Computing Machinary. 1969, v. 12, N 12, p. 666-674.
11. Chaki, S., Gurfinkel, A., Strichman, O. Regression verification for multi-threaded programs. Proceedings of the 13th International Conference on Verification, Model Checking, and Abstract Interpretation, 2012, p. 119-135.
12. Christodorescu M., Jha S., Seshia S. A., Song D., Bryant R. E. Semantic-aware malware detection. Proceedings of the 2005 IEEE Symposium on Security and Privacy, Oakland, 2005.
13. Dissegna, S., Logozzo, F., Ranzato, F. Tracing compilation by abstract interpretation. Proceedings of the 41st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 2014, p. 47-59.
14. Ershov A.P. Alpha - an automatic programming system of high efficiency. Journal of the Association for Computing Machinary. 1966. v. 13, N 1. p. 17-24.
15. Feng X., Hu A. J. Cutpoints for formal equivalence verification of embedded software. Proceedings of the 5-th ACM International Conference on Embedded Software, 2005, p. 307–316.
16. Godlin, B., Strichman, O. Regression verification. Proceedings of the 46th Annual Design Automation Conference, 2009, IEEE Computer Society, Washington.
17. Goldberg, B., Zuck, L., Barrett, C. Into the loops: practical issues in translation validation for optimizing compilers. Theoretical Computer Science, 2005, v. 132, N 1, p. 53–71.
18. Guo, S.-Y., Palsberg, J. The essence of compiling with traces. Proceedings of the 38th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 2011, p. 563-574.
19. Kildall G. A unified approach to global program optimization. Conference Record of the Annual ACM SIGPLAN-SIGACT Simposium on Principles of Programming Languages, 1973, p. 194-206.
20. Kundu, S., Tatlock, Z., Lerner, S. Proving optimizations correct using parameterized program equivalence. Proceedings of the 2009 ACM SIGPLAN Conference on Programming Language Design and Implementation, 2009, p. 327-337.
21. Lahiri S. K., Hawblitzel C., Kawaguchi M., Rebelo H. SYMDIFF: A language-agnostic semantic diff tool for imperative programs. Proceedings of the 24th International Conference on Computer Aided Verification, 2012, p. 712–717.
22. Le V., Afshari, M., Su, Z. Compiler validation via equivalence modulo inputs. Proceedings of the 35th ACM SIGPLAN Conference on Programming Language Design and Implementation, 2014, ACM, New York.
23. Lopes N. P., · Monteiro J. Automatic equivalence checking of programs with uninterpreted functions and integer arithmetic. International Journal on Software Tools for Technology Transfer, 2015, N 1, p. 1-16.
24. Matsumoto, T., Saito, H., Fujita, M. Equivalence checking of C programs by locally performing symbolic simulation on dependence graphs. Proceedings of the 7-th International Symposiumon Quality Electronic Design, 2006, p. 370-375.
25. Mohri M. Finite state transducers in language and speech processing. Computer Linguistics, 1997, v. 23, N 2.
26. Mohri M. Minimization algorithms for sequential transducers. Theoretical Computer Science, 2000, v. 234, p. 177-201.
27. Namjoshi, K.S., Zuck, L.D. Witnessing program transformations. Proceedings of the 20th International Conference on Static Analysis, 2013, Springer, Berlin, Heidelberg.
28. Necula, G.C. Translation validation for an optimizing compiler. Proceedings of the ACM SIGPLAN 2000 Conference on Programming Language Design and Implementation. 2000, p. 83-94.
29. Nerode A., Kohn W. Models for hybrid systems: automata, topology, controllability, observability. Cornell University, Technical Report 93-28, 1993, MIT Press, Cambridge.
30. Pnueli, A., Siegel, M., Singerman, E. Translation validation. Proceedings of the 4th International Conference on Tools and Algorithms for Construction and Analysis of Systems, 1998, p. 151-166.
31. Ramos D. A., Engler D. R. Practical, low-effort equivalence verification of real code. CAV, 2011, p. 669–685.
32. Sharma R., Schkufza E., B/ Churchill, A. Aiken. Data-driven equivalence checking. Proceedings of the 2013 ACM SIGPLAN international conference on Object oriented programming systems languages & applications, 2013, p. 391-406.
33. Shashidhar, K.C., Bruynooghe,M., Catthoor, F., Janssens, G. Verification of source code transformations by program equivalence checking. Proceedings of the 14th International Conference on Compiler Construction. Springer, 2005, Berlin, Heidelberg.
34. de Souza R. On the decidability of the equivalence for k-valued transducers. Proceedings of 12th International Conference on Developments in Language Theory, 2008, p. 252-263.
35. Stepp, M., Tate, R., Lerner, S. Equality-based translation validator for LLVM. Proceedings of the 23rd International Conference on Computer Aided Verification, 2011, p. 737-742.
36. Terauchi, T.: Aiken, A. Secure information flow as a safety problem. Proceedings of the 12th International Conference on Static Analysis. 2005, p. 352-367.
37. Veanes M., Hooimeijer P., Livshits B., et al. Symbolic finite state transducers: algorithms and applications. Proceedings of the 39th ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages, 2012.
38. Verdoolaege, S., Janssens, G., Bruynooghe, M. Equivalence checking of static affine programs using widening to handle recurrences. Proceedings of the 21st International Conference on Computer Aided Verification, 2009, Springer, Berlin, Heidelberg.
39. Yang W., Horowitz S., Reps T. A program integration algorithm that accommodates semantics-preserving transformations. ACM Transactions of Software Engineering and Methodology, 1992, v. 1, N 3, p. 310–354.
40. Zakharov V.A. An efficient and unified approach to the decidability of equivalence of propositional program schemes. Lecture Notes in Computer Science. 1998, v. 1443, p. 247-258.
41. Zakharov V.A.. The equivalence problem for computational models: decidable and undecidable cases. Lecture Notes in Computer Science, 2001, v. 2055, p. 133-153.
42. Zakharov V.A., Kuzurin N.N., Podlovchenko R.I., Shcherbina V.V. Using algebraic models of programs for detecting metamorphic malwares. Труды Института Системного программирования, Том 12, 2007. c. 77-94.
43. Zaks, A., Pnueli, A. CoVaC: Compiler validation by program analysis of the cross-product. In: Proceedings of the 15th International Symposium on Formal Methods. Springer, 2008, Berlin, Heidelberg.
44. Zhao, J., Nagarakatte, S., Martin, M.M.K., Zdancewic, S. Formal verification of SSA-based optimizations for LLVM. Proceedings of the 34th ACM SIGPLAN Conference on Programming Language Design and Implementation, 2013, ACM, New York.
45. Zuck, L., Pnueli, A., Goldberg, B., Barrett, C., Fang, Y., Hu, Y. Translation and run-time validation of loop transformations. Formal Methods for System Design, 2005, v. 27, N 3, p. 335–360.
46. Glushkov V.M. K voprosu o minimizatcii microprogram i skhem algoritmov [On the minimization of microprograms and algorithm schemata]. Kibernetika [Cybernetics]. 1966, N 5, p. 1-3.
47. Glushkov V.M., Letichevskii A.A. Teoriya diskretnyh preobrazovateley [Theory of discrete transducers]. Izbranniye voprosy algebry i logiki [Selected issues in algebra and logics]. Nauka Publ., 1973, p. 5-39.
48. Zakharov V.A. Bystriye algoritmy razresheniya ekvivalentnosti propozicionalnyh operatornyh program na uporyadochennyh polugruppovyh shkalah [Fast equivalence checking algorithms for propositional sequential programs on the ordered semigroup frames]. Vestnik Moskovskogo Universiteta. Vychislitelnaya matematika i kibernetika [Moscow University Computational Mathematics and Cybernetics] . 1999, N 3. p. 29-35.
49. Zakharov V.A. Modelirovanije i analiz posledovatelnyh i reagirujuschih program [Modelling and analysis of sequential reactive programs]. Trudy ISP RАN [The Proceedings of ISP RAS], v. 27, issue 2, 2015, pp. 221-250. DOI: 10.15514/ISPRAS-2015-27(2)-13
50. Kasyanov V.N. Optimizirujuschije preobrazovanija program [Optimizing transformations of programs]. Nauka Publ., 1988. 336 p.
51. Kotov V.E., Sabelfeld V.K. Teorija shem program [Theory of program schemata]. Nauka Publ., 1991. 348 p.
52. Lyapunov A.A. O logicheskih shemah program [On logical program schemata]. Problemy kibernetiki [Problems of Cybernetics], 1958, v. 1, p. 46-74.
53. Podlovchenko R.I. Minimization problem for schemes of programs with commutative blocks. Programming and computer software, 2008, v. 34, N 4, с. 237-241.
54. Podlovchenko R.I. Polygruppovije modeli program [Semigroup models of programs]. Programmirovanije [Programming and computer software]1981, N 4, с.3-13.
55. Podymov V.V., Zakharov V.A. Polynomialnij algoritm proverki ekvivalentnosti program s perestanovochnimi I podavlyaemymi operatorami [A polynomial algorithm for checking the equivalence in models of programs with commutation and vast operators]. Trudy ISP RАN [The Proceedings of ISP RAS], v. 26, N 3, с. 145-166. DOI: 10.15514/ISPRAS-2014-26(3)-8
Review
For citations:
Zakharov V.A., Podymov V.V. On the application of equivalence checking algorithms for program minimization. Proceedings of the Institute for System Programming of the RAS (Proceedings of ISP RAS). 2015;27(4):145-174. (In Russ.) https://doi.org/10.15514/ISPRAS-2015-27(4)-8
Email this article 