Модель памяти описывает требования консистентности памяти в многопоточной системе. Оптимизации компилятора могут нарушить требования консистентности из-за ошибок, и поведение программы будет отличаться от требуемого. Ошибки в оптимизациях компилятора, например, некорректную перестановку инструкций, очень сложно обнаружить, так как они могут возникать с очень небольшим шансом при реальном исполнении. Существуют различные подходы формальной верификации требований консистентности памяти, однако основная сложность состоит в том, что данные подходы не масшабируются на промышленное программное обеспечение. В данное работе представлен инструмент MCC, который был успешно апробирован на виртуальной машине ARK VM и обнаружил реальную ошибку в оптимизации компилятора. Инструмент MCC является статическим, что позволяет проверить все возможные выполнения конкретной тестовой программы, не полагаясь на реальной выполнение на определенной архитектуре. Подход также включает в себя генерацию тестов и спецификацию проверяемых свойств.
Проверка корректности модели памяти методами статического анализа
Проверка корректности модели памяти методами статического анализа
Язык статьиАнглийский
Аннотация
Ключевые слова
DOI10.31144/si.2307-6410.2023.n22.p1-10
УДК004
Номер
№ 22,
Страницы1-10
Файл
andrianovmutilin2023.pdf
(399.55 КБ)
Библиографическая ссылка
Андрианов П.С., Мутилин В.С. Проверка корректности модели памяти методами статического анализа // Системная информатика, 2023. – № 22. – С. 1-10. – DOI: https://doi.org/10.31144/si.2307-6410.2023.n22.p1-10.