4 ms·
Futexes in TLA+
- edvardas 2y agoSuccinct and rigorous. This article has a clear problem statement, explicitly calls out assumptions and expected properties, shows how to express them in TLA+/PlusCal, and even adds a sanity check by refining the mutex model. I wish I had seen this article when writing my BA thesis.