Применение алгоритмов проверки эквивалентности для оптимизации программ
https://doi.org/10.15514/ISPRAS-2015-27(4)-8
Аннотация
На примере двух моделей программ показано, что задача оптимизации размера программ может быть эффективно решена при помощи процедур проверки эквивалентности программ в рассматриваемых моделях. Основной результат работы - полиномиальные по времени алгоритмы минимизации конечных детерминированных автоматов-преобразователей над конечно порожденными разрешимыми группами и схем последовательных программ, семантика которых определяется конечно порожденными разрешимыми упорядоченными левосократимыми полугруппами. Предложенные алгоритмы можно использовать в качестве теоретической основы для построения эффективных процедур глобальной оптимизации императивных и реагирующих программ.
Об авторах
В. А. Захаров
ИСП РАН; МГУ имени М.В. Ломоносова, 2-й учебный корпус, факультет ВМК; Московский физико-технический институт (государственный университет); НИУ ВШЭ
Россия
Россия
В. В. Подымов
МГУ имени М.В. Ломоносова, 2-й учебный корпус, факультет ВМК; НИУ ВШЭ
Россия
Россия
Список литературы
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. Глушков В.М. К вопросу о минимизации микропрограмм и схем алгоритмов. Кибернетика. 1966, N 5, с. 1-3.
47. Глушков В.М., Летичевский А.А. Теория дискретных преобразователей. Избранные вопросы алгебры и логики: сб. статей. Новосибирск:Наука, 1973, с. 5-39.
48. Захаров В.А. Быстрые алгоритмы разрешения эквивалентности пропозициональных операторных программ на упорядоченных полугрупповых шкалах. Вестник Московского университета, сер. 15, Вычислительная математика и кибернетика. - 1999, N 3. с. 29-35.
49. Захаров В.А. Моделирование и анализ последовательных реагирующих программ. Труды Института системного программирования РАН, том 27, выпуск 2, 2015, стр. 221-250. DOI: 10.15514/ISPRAS-2015-27(2)-13
50. Касьянов В.Н. Оптимизирующие преобразования программ. М.: Наука, 1988. 336 с.
51. Котов В.Е., Сабельфельд В.К. Теория схем программ. М.:Наука, 1991. 348 с.
52. Ляпунов А.А. О логических схемах программ. Проблемы кибернетики, вып. 1, М.:Физматгиз, 1958, с. 46-74.
53. Подловченко Р.И. О минимизации схем программ с перестановочными блоками. Программирование, 2008, N 4, с. 72-77.
54. Подловченко Р.И. Полугрупповые модели программ. Программирование. 1981, N 4, с.3-13.
55. Подымов В.В., Захаров В.А. Полиномиальный алгоритм проверки эквивалентности в модели программ с перестановочными и подавляемыми операторами. Труды ИСП РАН, 2014, вып. 3, с. 145-166. DOI: 10.15514/ISPRAS-2014-26(3)-8
Рецензия
Для цитирования:
Захаров В.А., Подымов В.В. Применение алгоритмов проверки эквивалентности для оптимизации программ. Труды Института системного программирования РАН. 2015;27(4):145-174. https://doi.org/10.15514/ISPRAS-2015-27(4)-8
For citation:
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
Послать статью по эл. почте 