Paid Internship - GenMC integration (Lincheck)

Concurrent programming is notoriously complex and error-prone. Programming bugs can arise from various sources, such as operation re-reordering or an incomplete understanding of the memory model. With weaker-memory consistency architectures, such as ARM on the rise due to Apple efforts, ensuring that your concurrent algorithms are correct is as important as ever.

Some time ago, we presented Lincheck — a new practical tool for testing concurrent algorithms in JVM-based languages, such as Java, Kotlin, or Scala, that supports both stress testing and bounded model checking modes (GitHub). With such a tool, developing new algorithms becomes simpler and significantly more efficient. Please, read this blog post before going to the rest of the project description.

Since the main implementation language of Lincheck is Kotlin, which is multi-platform and interoperable with native languages like Swift or C/C++, one of our current main focuses is making it possible to write Lincheck tests for implementations in these languages. Currently, we have successfully supported the stress testing mode in Kotlin/Native, which automatically makes it possible to use Lincheck in C/C++.

With the ability to write tests in C/C++, it becomes intriguing to adopt the existing state-of-the-art model checkers to Lincheck. As mentioned in the beginning, it is vital to support weak memory models. Therefore, we consider two main model checkers: Nidhugg (GitHub) and GenMC (website, GitHub), both of which work on the level of LLVM bitcode.

During the internship, you will add a basic GenMC integration into Lincheck. It is also possible to discuss continuing the project in the lab after the summer internship.

• Strong knowledge of basic algorithms
• C/C++, and Kotlin or Java is expected