Проверка корректности модели памяти методами статического анализа

Модель памяти описывает требования консистентности памяти в многопоточной системе. Оптимизации компилятора могут нарушить требования консистентности из-за ошибок, и поведение программы будет отличаться от требуемого. Ошибки в оптимизациях компилятора, например, некорректную перестановку инструкций, очень сложно обнаружить, так как они могут возникать с очень небольшим шансом при реальном исполнении. Существуют различные подходы формальной верификации требований консистентности памяти, однако основная сложность состоит в том, что данные подходы не масшабируются на промышленное программное обеспечение. В данное работе представлен инструмент MCC, который был успешно апробирован на виртуальной машине ARK VM и обнаружил реальную ошибку в оптимизации компилятора. Инструмент MCC является статическим, что позволяет проверить все возможные выполнения конкретной тестовой программы, не полагаясь на реальной выполнение на определенной архитектуре. Подход также включает в себя генерацию тестов и спецификацию проверяемых свойств.