研究小组

并发计算

在过去的几十年里,并发编程得到了普及。每个语言和平台都提供了相应的基元,随着系统复杂度的增加,比如拥有多个NUMA节点,以及内存模型的放宽,这些基元越来越难以高效使用。由此在实践中产生了几个重要的问题。现在如何构建高效的并发算法?进度保证、效率和公平性之间的最佳权衡是什么?如何检查所有这些算法的正确性?如何对它们进行基准测试?虽然有些问题在学术界已经有了部分答案,但很多实际问题仍未解决。我们的主要关注点是通过提供实际合理的、有理论价值的解决方案以及高质量的工具来回答这些问题,以帮助并发领域的其他研究人员和开发人员。

我们感兴趣的话题包括:

  • 并发算法和数据结构
  • 非易失性存储器(NVM)
  • 测试和验证
  • 性能分析、调试和优化
  • 平行编程语言和模型
  • 记忆恢复

在此处查看完整的出版物列表。

主要项目:

用于 Kotlin 协同程序的同步和通信基元

传统的并发编程涉及到对共享的可变状态进行操作。这种编程风格的另一种选择是通信顺序进程(CSP)模型,它通过显式通信共享数据。Kotlin 协同程序是一个将这种模型引入 Kotlin 语言的库,在 Kotlin 语言中,进程通过协同程序来表示(它们是轻量级线程)。这样一来,协同程序之间的通信和同步就需要一些抽象,从众所周知的锁和信号量开始,到通道结束—特殊的生产者-消费者结构,在协同程序之间传输数据。本项目致力于开发高效的基元,并将其应用于 Kotlin 协同程序。.
https://github.com/Kotlin/kotlinx.coroutines

Lincheck:在 JVM 上测试并发性

Lincheck是一个实用的工具,用于测试基于 JVM 的语言中的并发算法,它同时支持压力测试和约束模型检查。相对于流行的测试工具(如 JCStress),Lincheck 的主要优势之一是它提供了一种声明式的编写并发测试的方法,通过指定所有要检查的操作、它们的正确性属性以及每个场景的调用次数。大致来说,Lincheck 会生成一系列并发场景,以压力测试或模型检查模式执行这些场景,并检查是否存在一些顺序执行,可以解释满足指定正确性属性的结果。除了上述功能外,Lincheck 还是第一个支持放宽数据结构语义的测试工具,支持生产者-消费者和协同程序实现中流行的双重数据结构设计,以及耐用的数据结构,专为 NVRAM 设计。
https://github.com/Kotlin/kotlinx-lincheck

并发图算法

并发图处理无论在理论上还是在实践上都是学术界的一个基础性和研究性很强的课题。然而,一些应用,如社交网络分析和编译器,需要这些算法在线,因此,需要并发。本项目旨在针对图处理的不同方面,建立切实有效的并发算法,包括使用多队列作为部分算法的优先级调度器,或者边缘插入和删除下的在线动态连接问题。现在,大多数硬件平台都有多个 NUMA 插座,因此,使所有这些算法支持 NUMA 是非常必要的。

实习生

我们全年都在招聘实习生。 理想的应聘者应该有很强的CS或数学背景,并对并发编程有一定的了解。请发电子邮件至nikita.koval@jetbrains.com,了解详情。

小组成员

Nikita Koval
Nikita Koval
研究实验室/小组负责人
Alexander Fedorov
Alexander Fedorov
研究员
Dmitry Khalanskiy
Dmitry Khalanskiy
研究员
Maria Sokolova
Maria Sokolova
研究员