Исследовательская группа

Лаборатория параллельных вычислений

Основные проекты

Примитивы синхронизации и коммуникации для Kotlin Coroutines

В классическом многопоточном программировании потоки взаимодействуют друг с другом посредством изменения разделяемой памяти, что зачастую требует нетривиальной синхронизации и приводит к неожиданным ошибкам. Альтернативой такому подходу является Communicating Sequential Processes (CSP) программирование, где процессы обмениваются данными в явном виде, посылая и получая их при помощи специальных коммуникационных примитивов. Самый популярный пример этого подхода — корутины, которые появляются чуть ли не в каждом языке программирования, начиная с Go и заканчивая C++. Kotlin Coroutines — библиотека, которая позволяет применить CSP стиль в языке Kotlin. Однако, для взаимодействия корутин друг с другом необходимы эффективные абстракции, начиная с хорошо известных блокировок и семафоров и заканчивая каналами — специальной “трубой” для передачи данных. В рамках этого проекта мы разрабатываем эффективные алгоритмы для всех необходимых синхронизационных и коммуникационных примитивов в Kotlin Cotourines.
https://github.com/Kotlin/kotlinx.coroutines

Lincheck: тестирование многопоточности на JVM

Lincheck — это практический инструмент для тестирования многопоточных алгоритмов на языках, основанных на JVM. Он поддерживает как стресс-тестирование, так и bounded model checking. Одно из основных преимуществ Lincheck в сравнении с популярными инструментами для тестирования, такими как JCStress, в том, что он предоставляет возможность декларативного написания тестов. Пользователю нужно только объявить операции, которые необходимо проверить, их критерии корректности и число вызовов, которые будут использоваться для каждого из сценариев. Lincheck генерирует серию параллельных сценариев, выполняет их в режиме стресс-тестирования или model-checking и проверяет, существует ли какое-то последовательное исполнение, которое может объяснить результаты, удовлетворяющие заданному свойству корректности. В дополнение к перечисленному выше Lincheck –– это первый инструмент для тестирования, поддерживающий упрощенную семантику структур данных, конструкции двойной структуры данных, популярные в реализациях producer-consumer и корутин, а также надежные структуры данных, разработанные для NVRAM.
https://github.com/Kotlin/kotlinx-lincheck

Графовые алгоритмы Concurrent

Параллельная обработка графов — фундаментальная тема, хорошо изученная как в теоретическом, так и в практическом плане. Однако для некоторых приложений, таких как анализ социальных сетей и компиляторы, необходимо, чтобы эти алгоритмы были online, то есть чтобы они работали многопоточно. Этот проект направлен на создание эффективных многопоточных алгоритмов для различных аспектов обработки графов, включая использование многопоточных очередей в качестве планировщиков приоритетов для некоторых алгоритмов или проблем динамического подключения в режиме online при добавлении и удалении ребер. В настоящее время большинство аппаратных платформ имеют несколько сокетов NUMA, поэтому важно, чтобы все эти алгоритмы были дружественными к NUMA.