С ростом количества многопоточных алгоритмов растёт потребность в их тестировании и доказательстве корректности работы. Одним из базовых критериев корректности многопоточных алгоритмов является линеаризуемость [2] — свойство программы, при котором результат любого параллельного выполнения операций эквивалентен некоторому последовательному. Для проверки линеаризуемости существует несколько подходов [4]. Одним из них является поиск последовательности операций, при многопоточном исполнении которой результат выполнения не совпадает ни с одним результатом из множества последовательных выполнений. Если такая последовательность существует, то алгоритм нелинеаризуем. В противном случае, утверждать обратного нельзя.
Для поиска такого множества операций существует инструмент lin- check [11]. Он генерирует множества результатов последовательных исполнений. Затем составляет наборы операций и запускает их на нескольких потоках. Процесс тестирования является псевдослучайным, так как между операциями вставляются различные задержки. Это вызвано отсутствием необходимого для тестирования механизма синхронизации в проверяемых структурах. Данный фактор заставляет осуществлять многократный запуск одних и тех же тестовых данных и надеяться, что переключение потоков произойдёт в отличных от предыдущего запуска точках. Этого можно избежать в случае контролируемого переключения между потоками изнутри структуры.
Ход работы инструмента lin-check состоит из множества независимых друг от друга итераций. Данное утверждение позволяет выдвинуть гипотезу об увеличении скорости проверки структуры, если запускать каждую итерацию в своём потоке. Но такое улучшение вызовет значительное падение производительности при большом значении параметра запущенных одновременно исполнений. Это связано с особенностями модели работы стандартных JVM потоков.
На текущий момент виртуальная машина Java стандартно использует native модель для расспаралеливания потоков. Native-потоки — это потоки, за управление которыми отвечает операционная система. Создание большого их количества нагружает систему. Кроме того, стандартные средства Java не позволяют эффективно управлять их переключением [7, 8]. В целях решения этой проблемы были созданы легковесные потоки (Green Threads). Они эмулируют многопоточное исполнение, являясь по сути либо корутинами либо континуациями [9]. Кон- тинуации — это функции, чьё выполение может быть приостановлено и возобновлено. Корутины — механизм управления ходом выполнения программы, позволяющий приостанавливать выполняемую задачу, сохранять её состояние и выключать из потока. Проблема управления потоками заключается в том, что тестируемые структуры не обладают нужными точками переключений потоков. Устанавливать такие точки вручную внутри структур является сложной задачей, так как требует глубокого понимания логики работы многопоточного алгоритма.
В рамках данной работы были достигнуты следующие результаты.
• Проведён обзор библиотек Quasar и Kilim легковесных потоков для языка Java.
• Разработаны функциональные требования выделяющие фазы работы.
• Спроектирована новая архитектура инструмента Lin-Checker обладающая гибкостью для дальнейших усовершенствований.
• Выполнена реализация:
— Средства внедрения точек синхронизации путем трансформации кода на лету;
— Функциональности тестирования алгоритмов на легковесных потоках;
— Системы управления легковесными потоками.
• Проведена апробация для существующих структур данных и проведены замеры скорости работ.
