ВЕРИФИКАЦИЯ КОРРЕКТНОСТИ ОПТИМИЗИРУЮЩИХ ПРЕОБРАЗОВАНИЙ ПРОГРАММЫ ОТНОСИТЕЛЬНО ТРЕБОВАНИЙ К СОГЛАСОВАННОСТИ ПАМЯТИ

Оптимизационные преобразования, выполняемые компилятором, могут нарушать требования по обеспечению согласованности доступа к общей памяти из различных потоков одной многопоточной программы — это приводит к ошибкам, в результате которых поведение программы будет отличаться от ожидаемого. Требования согласованности для того или иного языка программирования называются моделью памяти. Примером ошибки такого класса может быть некорректное изменение порядка выполнения инструкций, которое не влияет на поведение однопоточной программы, но приводит к непредсказуемым результатам в многопоточном случае. Такие ошибки часто трудно обнаружить, поскольку они проявляются редко и существенно зависят от аппаратуры и состояния вычислительной системы. Хотя существуют формальные методы проверки согласованности использования общей памяти, их масштабируемость для промышленного программного обеспечения остается серьезной проблемой. Для верификации многопоточных программ ранее был предложен инструмент MCC, использовавший простой вид статического анализа. В этой статье мы представляем модификацию инструмента MCC, в котором реализован метод проверки моделей для верификации корректности обеспечения согласованности доступа к памяти. Предложенный метод объединяет методы генерации тестовых программ и метод статического анализа программ. Для генерации тестовых программ используется инструмент ОТК, для статического анализа — модифицированная версия инструмента MCC, который проверяет все возможные варианты выполнения сгенерированной тестовой программы, не зависящие от специфики того или иного аппаратного обеспечения. Инструмент был опробован на промышленной виртуальной машине ARK и успешно выявил две реальные ошибки в оптимизации компилятора.

многопоточность, согласованность памяти, модель памяти, оптимизации компилятора, ошибки многопоточности