Обнаружение гонок в Java-программах с применением синхронизационных контрактов

Состояние гонки (data race) возникает в многопоточной программе, когда несколько потоков одновременно обращаются к одному и тому же разделяемому участку памяти, где хотя бы одно обращение — запись. Состояния гонки трудновоспроизводимы и могут приводить к повреждению глобальных структур данных, поэтому исследования в области автоматического поиска гонок ведутся уже более 20 лет. В данной статье рассматривается вопрос повышения производительности динамического поиска гонок в Java-программах без существенной потери точности. Для решения этой задачи используются синхронизационные контракты — частичные спецификации поведения программных методов и классов в многопоточной среде. Применение контрактов позволяет исключать из анализа не интересные с точки зрения поиска гонок части целевого приложения (например, сторонние библиотеки). В статье рассматриваются преимущества и ограничения подхода, описывается язык спецификации контрактов и некоторые технические детали реализации.