Groupe de recherche

Informatique simultanée

La programmation concurrente a gagné en popularité au cours des dernières décennies. Chaque langage et chaque plateforme fournit des primitives correspondantes, qui deviennent de plus en plus difficiles à utiliser efficacement avec la complexité croissante des systèmes, comme le fait d'avoir plusieurs nœuds NUMA, ainsi qu'avec les assouplissements des modèles de mémoire. Dans la pratique, plusieurs questions importantes se posent à cet égard. Comment construire des algorithmes concurrents efficaces de nos jours ? Quel est le meilleur compromis entre garanties de progrès, efficacité et équité ? Comment vérifier l'exactitude de tous ces algorithmes ? Comment les comparer ? Si certaines de ces questions trouvent partiellement une réponse au niveau académique, de nombreux problèmes pratiques restent en suspens. Notre objectif premier est de répondre à ces questions en fournissant des solutions pratiquement raisonnables et théoriquement utiles ainsi que des outils de haute qualité qui peuvent aider les autres chercheurs et développeurs dans le domaine de la concurrence.

Voici quelques-uns de nos sujets d'intérêt :

  • Algorithmes et structures de données concurrents
  • Mémoire non-volatile (NVM)
  • Tests et vérifications
  • Analyse des performances, débogage et optimisation
  • Langages et modèles de programmation parallèle
  • Récupération de la mémoire

Consultez la liste complète des publications ici.

Principaux projets :

Primitives de synchronisation et de communication pour les coroutines Kotlin

La programmation concurrente traditionnelle implique la manipulation d'un état mutable partagé. Une alternative à ce style de programmation est le modèle des processus séquentiels communicants (CSP), qui partagent des données via une communication explicite. Kotlin Coroutines est une bibliothèque qui introduit ce modèle dans le langage Kotlin, où les processus sont représentés par des coroutines (ce sont des threads légers). De cette façon, plusieurs abstractions sont nécessaires pour la communication et la synchronisation entre les coroutines, en commençant par les célèbres verrous et sémaphores, et en terminant par les canaux — une structure spéciale producteur-consommateur pour transférer les données entre les coroutines. Ce projet est consacré au développement de primitives efficaces et à leur adoption pour Kotlin Coroutines.
https://github.com/Kotlin/kotlinx.coroutines

Lincheck : tester la concurrence sur la JVM

Lincheck est un outil pratique pour tester des algorithmes concurrents dans des langages JVM, qui prend en charge à la fois les tests de stress et la vérification de modèles délimités. L'un des principaux avantages de Lincheck par rapport aux outils de test populaires tels que JCStress est qu'il fournit une manière déclarative d'écrire des tests concurrents, en spécifiant toutes les opérations à examiner, leurs propriétés de justesse et le nombre d'invocations à utiliser pour chaque scénario. En gros, Lincheck génère une série de scénarios concurrents, les exécute en mode de test de stress ou de vérification de modèle, et vérifie s'il existe une exécution séquentielle qui peut expliquer les résultats satisfaisant la propriété de justesse spécifiée. En plus des fonctionnalités ci-dessus, Lincheck est le premier outil de test à prendre en charge la sémantique de structure de données assouplie, les conceptions de structure de données double populaires dans les implémentations producteur-consommateur et de coroutines, ainsi que les structures de données durables, conçues pour NVRAM.
https://github.com/Kotlin/kotlinx-lincheck

Algorithmes de graphiques TConcurrent

Le traitement parallèle des graphiques est un sujet fondamental et bien étudié dans le monde universitaire, tant dans ses aspects théoriques que pratiques. Cependant, certaines applications, telles que l'analyse des réseaux sociaux et les compilateurs, exigent que ces algorithmes soient en ligne, donc, qu'ils soient concurrents. Ce projet vise à construire des algorithmes concurrents pratiquement efficaces pour différents aspects du traitement des graphiques, notamment en utilisant des files d'attente multiples comme programmateurs de priorité pour certains des algorithmes, ou des problèmes de connectivité dynamique en ligne sous l'insertion et la suppression à la périphérie. De nos jours, la plupart des plateformes matérielles ont plusieurs sockets NUMA, il est donc essentiel de rendre tous ces algorithmes compatibles NUMA.

Stages pour étudiants

Nous recrutons des stagiaires tout au long de l'année. Le candidat idéal doit avoir une solide formation en informatique ou en mathématiques et avoir une certaine connaissance de la programmation concurrente. Veuillez envoyer un e-mail à Nikita Koval pour plus de détails à l'adresse nikita.koval@jetbrains.com.

Membres du groupe

Nikita Koval
Nikita Koval
Chef de laboratoire/groupe de recherche
Alexander Fedorov
Alexander Fedorov
Chercheur
Dmitry Khalanskiy
Dmitry Khalanskiy
Chercheur
Maria Sokolova
Maria Sokolova
Chercheur