Grupo de investigación

Computación Simultánea

En las últimas décadas, la programación simultánea ha ido ganando popularidad. Cada lenguaje y plataforma proporciona sus correspondientes primitivos, que cada vez son más complicados de utilizar de forma eficiente debido a la cada vez mayor complejidad de los sistemas, como la presencia de nodos NUMA múltiples, así como a las relajaciones de los modelos de memoria. En la práctica, surgen una serie de preguntas importantes. ¿Cómo se pueden construir hoy en día algoritmos simultáneos eficientes? ¿Cuál es el mejor equilibrio entre las garantías de progreso, la eficiencia y la imparcialidad? ¿Cómo comprobar la exactitud de dichos algoritmos? ¿Cómo compararlos? Aunque la academia ha respondido parcialmente algunas de estas preguntas, todavía hay pendientes muchos problemas prácticos. Nuestro principal objetivo es responder estas preguntas con soluciones razonables en la práctica y valoradas teóricamente, así como con herramientas de alta calidad que puedan ayudar a otros investigadores y desarrolladores del campo de la simultaneidad.

Nuestros temas de interés:

  • Algoritmos simultáneos y estructuras de datos
  • Memoria no volátil (NVM)
  • Pruebas y verificaciones
  • Análisis del rendimiento, depuración y optimización
  • Lenguajes y modelos de programación paralela
  • Recuperación de memoria

La lista completa de publicaciones se puede consultar aquí.

Proyectos principales:

Primitivos de sincronización y comunicación para corrutinas de Kotlin

La programación simultánea tradicional incluye la manipulación de un estado mutable compartido. Una alternativa a este estilo de programación es el modelo de procesos secuenciales de comunicación (CSP), que comparte datos mediante comunicaciones explícitas. Las corrutinas de Kotlin son una biblioteca que trae este modelo al lenguaje Kotlin, donde los procesos se representan mediante corrutinas (son subprocesos atenuados). De esta forma, se necesitan varias abstracciones para la comunicación y la sincronización entre las corrutinas, empezando por los famosos bloqueos y semáforos, y terminando por los canales (una estructura especial productor-consumidor para transferir datos entre corrutinas). El objetivo de este proyecto es desarrollar primitivos eficientes y adoptarlos para las corrutinas de Kotlin.
https://github.com/Kotlin/kotlinx.coroutines

Lincheck: probar la simultaneidad en la JVM

Lincheck es una herramienta práctica para probar algoritmos simultáneos en lenguajes basados en JVM, compatible tanto con pruebas de estrés como con comprobación de modelos limitados. Una de las principales ventajas de Lincheck relacionada con las famosas herramientas de prueba, como JCStress, es que ofrece una forma declarativa de escribir pruebas simultáneas, especificando todas las operaciones que hay que examinar, la corrección de sus propiedades y la cantidad de invocaciones que hay que utilizar en cada escenario. Aproximadamente, Lincheck genera una serie de situaciones simultaneas, las ejecuta en modo prueba de estrés o comprobación de modelos, y comprueba si existe alguna ejecución secuencial que pueda explicar que los resultados cumplan con las propiedades de corrección especificadas. Además de las funcionalidades anteriores, Lincheck es la primera herramienta de testeo compatible con la semántica de la estructura de datos relajada, los diseños de estructura de datos duales populares entre productores-consumidores y las implementaciones de corrutinas, así como las estructuras de datos duraderas, diseñadas para NVRAM.
https://github.com/Kotlin/kotlinx-lincheck

Algoritmos gráficos TConcurrent

El procesamiento de gráficos paralelos es un tema fundamental y ampliamente estudiado por parte de la academia, tanto en su vertiente teórica como práctica. Sin embargo, algunas aplicaciones, como el análisis de redes sociales y los compiladores, requieren que dichos algoritmos estén en línea, es decir, sean simultáneos. El objetivo de este proyecto es construir algoritmos simultáneos eficientes en la práctica para diferentes aspectos de procesamiento de gráficos, entre los que se incluye el uso de colas múltiples como programadores de prioridad para algunos de los algoritmos, o problemas de conectividad dinámica en línea bajo la inserción y la eliminación de aristas. Actualmente, la mayoría de plataformas de hardware tienen varios sockets NUMA, de manera que es esencial que dichos algoritmos sean compatibles con NUMA.

Estudiantes becados

Contratamos becarios durante todo el año. El candidato ideal debería tener conocimientos sólidos de CS o matemáticas, y tener conocimientos básicos de programación simultánea. Para obtener más información, envíe un correo electrónico a Nikita Koval a la dirección nikita.koval@jetbrains.com.

Miembros del grupo

Nikita Koval
Nikita Koval
Responsable del laboratorio/grupo de investigación
Alexander Fedorov
Alexander Fedorov
Investigador
Dmitry Khalanskiy
Dmitry Khalanskiy
Investigador
Maria Sokolova
Maria Sokolova
Investigador