Only those projects where I had a key role are mentioned. For each of the projects short descriptions and links to the related blog posts, publications, and talks are attached.

Buffered Channels

Improving data flow processing with new buffered channels in Kotlin Coroutines

Traditional concurrent programming involves manipulating shared mutable state. Alternatives to this programming style are communicating sequential processes (CSP) and actor models, which share data via explicit communication. These models have been known for almost half a century, and have recently had started to gain significant traction among modern programming languages. The common abstraction for communication between several processes is the channel. Although channels are similar to producer-consumer data structures, they have different semantics and support additional operations, such as the select expression. Despite their growing popularity, most known implementations of channels use lock-based data structures and can be rather inefficient. Under this project, I am working on efficient and scalable channel algorithms, which are far faster than the already existing ones. New related publications are coming soon.


Abstraction for fair synchronization and communication primitives

This project was started with a novel sempahore algorithm for Kotlin Coroutines (see the source code). After that, we decided to create a flexible abstraction for implementing synchronization and communication primitives. The one is called SegmentQueueSynchronizer and makes the development of such primitives much faster making them simpler and more efficient at the same time. Since we also support abortability of waiting requests (e.g., lock operation can be aborted by timeout) and these algorithm parts are usually the most complicated and error-prone ones, we decided to prove everything formally in the Iris framework for Coq. Now we are completing the proofs and working on experiments, and looking forward to a new paper soon!


Framework for testing concurrency on JVM

Lincheck is a practical tool for testing concurrent algorithms implemented in JVM-based languages, such as Java, Kotlin, or Scala. Roughly, lincheck takes the list of operations on the data structure to be tested, generates a series of concurrent scenarios, executes them in either stress testing or model checking mode, and checks whether there exists some sequential execution which can explain the results. I use this tool to test the concurrent algorithms in the Kotlin Coroutines library and to check a set of student assignments. In addition, it was used to find several known and unknown bugs in popular libraries, such as the race between removing and adding an element to the head of the Java’s ConcurrentLinkedDeque.


Tool for finding potential deadlocks via dynamic analysis

Dl-Check determines potential deadlock as a lock hierarchy violation and finds them via dynamic analysis in Java programs. This tool is implemented as Java agent and injects analysis code within class transformation during class loading, therefore it’s possible to use Dl-Check without any code change. The base algorithm for finding lock hierarchy violations is based on new cycles detection in the lock-order graph. For this purpose, an algorithm for incremental topological order maintenance is used.


Library for testing time-based functionality in Java programs

Time-test helps to test time-dependent functionality via time virtualization. It is implemented as a Java agent and replaces all time-dependent methods invocations with its own implementations on the fly. Unlike other implementations, it works not with System.currentTimeMillis() and System.nanoTime() methods only, but with Object.wait(..), Thread.sleep(..), and Unsafe.park(..) as well. In addition, time-test has a special waitUntilThreadsAreFrozen(timeout) method which waits until all threads have done their work.


Tool for finding code usages among Maven repositories

Usages tool finds code usages in the specified Maven repositories. It indexes repositories, downloads required artifacts, and scans .class files in them. The tool analyzes all kinds of dependencies: usages of fields and methods, extensions of classes and implementations of interfaces, usages of annotations, overrides of methods, and so on. The tool is separated into 2 parts: server application, which collects all information and analyzes classes, and a client one, which is implemented as an IntelliJ IDEA plugin.


Framework for simplifying java agents development