fray

https://github.com/cmu-pasta/fray Is a concurrency testing framework for Java. It also does deterministic simulation.

My current thinking on model checking (still evolving): Modeling languages are useful to check the correctness of an algorithm during development. During development, a model can also serve as a specification for the actual implementation. This requires that your the modeling language is readable to a broad range of developers, which TLA+ is not. We have been experimenting with FizzBee (fizzbee.io) which looks promising in this regards. When you go to prod, you really want to test your actual implementation, not a model of it. For this you want something like https://github.com/awslabs/shuttle (for Rust), or https://github.com/cmu-pasta/fray (for Java). Or use something custom.

https://github.com/cmu-pasta/fray Fray is a controlled concurrency testing tool for the JVM that supports record and replay. It could be a perfect backend for codetracer. (I'm the author of Fray)

Using Fray does not require knowledge about "deterministic testing" or "controlled concurrency." This is one of its goals: developers write normal concurrency tests, and Fray controls the execution behind the scenes. In fact, when we evaluate Fray, we collect all existing concurrency tests from Lucene, Kafka, and Guava, and running them under different thread inter-leavings can already reveal so many bugs. [1] [1]: https://github.com/cmu-pasta/fray/blob/main/docs/bugs.md

I’m the author of Fray, a concurrency testing framework for the JVM, and I’m excited to finally share what I’ve been building over the past few years! Fray[1] is a concurrency testing tool for Java that can help you find and debug tricky race conditions that manifest as assertion violations, run-time exceptions, or deadlocks. I’d love to hear your thoughts—feel free to ask me anything! And if you’re curious, give Fray a try. [1]: https://github.com/cmu-pasta/fray

Hi HN, I’m excited to share Fray, a controlled concurrency testing framework for the JVM. Fray systematically explores different thread interleavings in your concurrency tests, helping to uncover tricky race conditions. It can also deterministically reproduce concurrency-related failures, making debugging significantly easier. For a deep dive into how Fray is designed, check out our technical report: https://arxiv.org/abs/2501.12618 The Lucene team recently wrote about how Fray helped them diagnose and fix a challenging concurrency bug: https://www.elastic.co/search-labs/blog/optimistic-concurren... Would love to hear your thoughts and feedback!