Maria Sokolova est une des développeuses de l’équipe des coroutines de Kotlin et de Lincheck et elle va nous présenter Lincheck, une librairie permettant de valider les algorithmes concurrents.

On prend comme exemple une bounded queue basée sur ConcurrentLinkedList dont l’implémentation a été faite par ChatGTP en Kotlin.

L’implémentation proposée par ChatGTP semble correcte à première vue, mais comment la tester ?

Stress Test ? Non car c’est non déterministe.

L’équipe de Kotlin a créé Lincheck pour ça : tester des structures de données dans une utilisation concurrente.

Avec Lincheck, on définit plusieurs opérations qui sont des méthodes annotée par @Operation puis on lance de manière concurrente les différentes opérations dans une méthode de test annoté par @Test grâce une des classes de test fournie ; par exemple StressOptions().check(this::class).

La difficulté c’est d’exprimer ce qui est correcte dans un monde concurrent, ce qui est simple dans un monde séquentiel.

Une execution concurrente correcte se base sur le principe de « linerazibility » : s’il existe une exécution séquentielle possible entre les différents threads, alors l’exécution concurrente est correcte.

Si on reprend l’exemple généré par ChatGPT, celui-ci n’est pas valide car la méthode add n’est pas atomic et deux threads peuvent s’entrelacer (interleave).

Comment marche Lincheck:

1. Génère des scénarii concurrents (à la fuzzer)
2. Examine les scénarii via stress test ou model testing
3. Vérifie automatiquement les résultats

Lincheck injecte du code de vérification avant chaque lecture / écriture d’un champ (bytecode enhancement qui utilise invokedynamic).

Lincheck peut aussi détecter si il y a des threads bloqués (obstruction freedom) par un algorithme ce qui aide à développer des algorithmes lock-free / wait-free.