Разработка промышленных систем требует создания высокопроиз-
водительных алгоритмов. Одним из способов увеличения производи-
тельности является многопоточность. Многопоточное программирова-
ние становится более популярным с распространением многоядерных
процессоров. Однако, многопоточное программирование ставит перед
программистом вопрос построения и тестирования потокобезопасных
компонент, чьи методы корректны в многопоточной среде без исполь-
зования неуместных барьеров и иных методов синхронизации.
Потокобезопасность компонент не является четко формализован-
ным термином. Более корректные условия корректности типов данных
включают отсутствие гонок [2], сериализуемость [8], линеаризуемость
[4]. Последнее время общепринятым стандартом потокобезопасности
является наличие линеаризуемости [3]. Говоря неформально, структура
данных является линеаризуемой, если результат любого многопоточ-
ного алгоритма над этой структурой данных эквивалентен результату
некоторого последовательного алгоритма. Иными словами многопоточ-
ное поведения можно рассматривать как набор последовательных операций.
Наиболее известными примерами линеаризуемых компонент явля-
ются типы данных, такие как очереди или множества, которые предо-
ставлены множеством различных библиотек, таких как Java Concurrency
[7] и PLINQ [9]. Классические подходы к тестированию [13] в целом
оказываются мало эффективны в многопоточном окружении, так как
программа может работать без ошибок почти всегда, кроме редких си-
туаций, когда ошибка проявит себя вследствие особой конфигурации
потоков и чередования операций в них. Это порождает необходимость
инструмента, который проверяет корректность реализации многопоточ-
ной структуры данных.
Объектно-ориентированная парадигма программирования подразу-
мевает взаимодействие структуры данных с внешним миром при помо-
щи некоторого конечного набора методов. Таким образом, любой алго-
ритм над структурой данных можно рассматривать как последователь-
ность методов этой структуры и набор входных данных.
Задача доказательства линеаризуемости является довольно трудо-
емкой и зачастую проводится вручную. Однако, на практике оказы-
вается довольно удобным альтернативный подход путем приведения
контрпримеров [14], то есть таких алгоритмов, которые могут работать
некорректно. Соответственно, при достаточно большом количестве рас-
смотренных алгоритмов можно дать вероятностную оценку линеаризу-
емости всей структуры данных в целом.
Одним из инструментов, предлагающих автоматизировать провер-
ку линеаризуемости, является lin-check [18] — библиотека, генериру-
ющая большой набор тестовых алгоритмов над структурой данных и
проверяющая их корректность путем многократного исполнения в мно-
гопоточной среде и проверки результатов на соответствие некоторому
последовательному исполнению. Однако, данная библиотека не учиты-
вает внутреннюю структуру функций тестируемых типов данных и не
имеет планировщика выполнения для управления ходом исполнения те-
стового алгоритма, что порождает множество ненужных запусков для
корректного (с точки зрения линеаризуемости) алгоритма, что в свою
очередь отрицательно влияет на производительность всей системы в целом.
В ходе работы были достигнуты следующие результаты:
• проведен обзор методологий проверки линеаризуемости многопоточных программ;
• разработана архитектура для создания стратегий управления ходом исполнения программы;
• формализованы операции виртуальной машины Java, влияющие на поведение алгоритма в многопоточной среде ;
• доработан существующий алгоритм управления порядком исполнения с учетом формализованых операций виртуальной машины Java;
• разработан алгоритм управления порядком исполнения многопоточных программ на языке Java;
• сравнение полученных алгоритмов с текущей реализацией выявило увеличение производительности разработанного алгоритма.
