Forschungsgruppe

Nebenläufiges Computing

Gleichzeitige Programmierung hat in den letzten Jahrzehnten an Popularität gewonnen. Jede Sprache und Plattform stellt entsprechende Primitive zur Verfügung, die mit zunehmender Systemkomplexität, z. B. mit mehreren NUMA-Knoten, sowie mit Auflockerungen der Speichermodelle immer schwieriger effizient zu nutzen sind. Daraus ergeben sich in der Praxis mehrere wichtige Fragen. Wie kann man heutzutage effiziente nebenläufige Algorithmen erstellen? Was ist der beste Kompromiss zwischen Fortschrittsgarantien, Effizienz und Fairness? Wie kann man all diese Algorithmen auf ihre Korrektheit überprüfen? Wie kann man Vergleichstests durchführen? Während einige dieser Fragen in der Wissenschaft bereits teilweise beantwortet sind, sind viele der praktischen Probleme noch offen. Unser Hauptfokus liegt auf der Beantwortung dieser Fragen, indem wir praktisch sinnvolle und theoretisch wertvolle Lösungen sowie hochwertige Tools bereitstellen, die anderen Forschenden und Entwickler*innen aus dem Bereich der gleichzeitigen Programmierung helfen können.

Unsere Interessensgebiete sind:

  • Gleichzeitige Algorithmen und Datenstrukturen
  • Nichtflüchtiger Speicher (NVM)
  • Testen und Verifizieren
  • Performance-Analyse, Fehlersuche und Optimierung
  • Parallele Programmiersprachen und -modelle
  • Arbeitsspeicherrückgewinnung

Sehen Sie die vollständige Liste der Publikationenhier an.

Hauptprojekte:

Synchronisations- und Kommunikationsprimitive für Kotlin Coroutines

Bei der traditionellen gleichzeitigen Programmierung wird ein gemeinsamer veränderbarer Zustand manipuliert. Eine Alternative zu diesem Programmierstil ist das Modell der kommunizierenden sequentiellen Prozesse (CSP), die Daten über explizite Kommunikation gemeinsam nutzen. Kotlin Coroutines ist eine Bibliothek, die dieses Modell in die Sprache Kotlin einbringt, wobei Prozesse durch Coroutines repräsentiert werden (sie sind leichtgewichtige Threads). Auf diese Weise gibt es mehrere Abstraktionen, die für die Kommunikation und Synchronisation zwischen den Coroutines benötigt werden, angefangen von den bekannten Locks und Semaphoren, bis hin zu Channels — spezielle Producer-Consumer-Strukturen, um die Daten zwischen den Coroutines zu übertragen. Dieses Projekt widmet sich der Entwicklung effizienter Primitive und deren Übernahme in Kotlin Coroutines.
https://github.com/Kotlin/kotlinx.coroutines

Lincheck: Testen von Gleichzeitigkeit auf der JVM

Lincheck ist ein praktisches Tool zum Testen nebenläufiger Algorithmen in JVM-basierten Sprachen, das sowohl Stresstests als auch Bounded-Model-Checking unterstützt. Einer der Hauptvorteile von Lincheck im Vergleich zu populären Testtools wie JCStress ist, dass es eine deklarative Methode zum Schreiben von nebenläufigen Tests bietet, indem es alle zu untersuchenden Operationen, ihre Korrektheitseigenschaften und die Anzahl der Aufrufe für jedes Szenario angibt. Grob gesagt, generiert Lincheck eine Reihe von nebenläufigen Szenarien, führt sie entweder im Stresstest- oder im Model-Checking-Modus aus und prüft, ob es eine sequenzielle Ausführung gibt, die die Ergebnisse erklären kann, die die angegebene Korrektheitseigenschaft erfüllen. Zusätzlich zu den oben genannten Funktionen ist Lincheck das erste Testtool, das eine entspannte Datenstruktursemantik, duale Datenstrukturdesigns, die in Producer-Consumer- und Coroutine-Implementierungen beliebt sind, sowie langlebige Datenstrukturen, die für NVRAM ausgelegt sind, unterstützt.
https://github.com/Kotlin/kotlinx-lincheck

Gleichzeitige Graphenalgorithmen

Parallele Graphenverarbeitung ist ein grundlegendes und gut untersuchtes Thema in der akademischen Welt, sowohl in theoretischer als auch in praktischer Hinsicht. Einige Anwendungen, wie z. B. die Analyse sozialer Netzwerke und Compiler, erfordern jedoch, dass diese Algorithmen online und damit nebenläufig sind. Dieses Projekt zielt darauf ab, praktisch effiziente nebenläufige Algorithmen für verschiedene Aspekte der Graphenverarbeitung zu entwickeln, einschließlich der Verwendung von Multi-Warteschlangen als Prioritäts-Scheduler für einige der Algorithmen, oder online dynamische Konnektivitätsprobleme unter Kanteneinfügung und -löschung. Heutzutage haben die meisten Hardware-Plattformen mehrere NUMA-Sockel, daher ist es wichtig, all diese Algorithmen NUMA-freundlich zu machen.

Studentenpraktika

Wir stellen das ganze Jahr über Praktikant*innen ein. Ideale Kandidat*innen haben einen starken Hintergrund in Informatik oder Mathematik und verfügen über einige Kenntnisse in der nebenläufigen Programmierung. Bitte senden Sie eine E-Mail an Nikita Koval für Details unter nikita.koval@jetbrains.com.

Gruppenmitglieder

Nikita Koval
Nikita Koval
Leiter*in Forschungslabor/-gruppe
Alexander Fedorov
Alexander Fedorov
Forscher*in
Dmitry Khalanskiy
Dmitry Khalanskiy
Forscher*in
Maria Sokolova
Maria Sokolova
Forscher*in