Верификация многопоточных алгоритмов методом управляемого исполнения легковесных потоков

1. Введение 4
2. Постановка задачи 6
3. Обзор библиотек легковесных потоков 7
3.1. Kilim 7
3.2. Quasar 8
3.3. Jephyr 9
4. Требования к системе 10
5. Архитектура системы 11
6. Реализация 13
6.1. Преобразование байт-кода 14
6.2. Создание и управление потоками 18
6.3. Параллельный запуск легковесных потоков 20
6.4. Ограничения 21
7. Оценка производительности 22
8. Заключение 25
Список литературы 26
9. Приложение 27
Купить

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