I’m a fan and long-term user of the Isabelle/HOL proof assistant. More recently I have been studying Lamport’s TLA+ system which is a popular choice for writing specifications of systems. This post is a slightly tidied-up version of some notes about my early experiences of playing with the implementation of TLA within Isabelle/HOL, to record a handful of obstacles I hit and some techniques I found useful.
Project Loom (JEP 425) is probably amongst the most awaited feature additions to Java ever;
its implementation of virtual threads (or "green threads") promises developers the ability to create highly concurrent applications,
for instance with hundreds of thousands of open HTTP connections,
sticking to the well-known thread-per-request programming model,
without having to resort to less familiar and often more complex to use reactive approaches.
Having been in the workings for several years, Loom got merged into the mainline of OpenJDK just recently and is available as a preview feature in the latest Java 19 early access builds.
I.e. it’s the perfect time to get your hands onto virtual threads and explore the new feature.
In this post I’m going to share an interesting aspect I learned about thread scheduling fairness for CPU-bound workloads running on Loom.
Project Loom introduces lightweight and efficient virtual threads called fibers, massively increasing resource efficiency while preserving the same simple thread abstraction for developers.