Comment by edvardas

Succinct 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.