It's appropriate that this is appearing at the death of Niklaus_Wirth. He really was the first to get serious about formalizing concurrency. P and V, and all that.
This feels very retro. I used to work on this sort of thing, but that was back in the early 1980s. This reads like something from back then, when people were first figuring out how to think about concurrency.[1] That's how people thought about this back then.
There's been progress in the last four decades. There are completely different approaches, such as symbolic execution. The Microsoft Static Driver Verifier is an example. There's also a theory of eventually-consistent systems now, with conflict-free replicated data types. It's also more common today to think about concurrency in terms of messages rather than variable access, which is easier to reason about. There's also more of a handle on the tooling problem. Not enough of a handle, though. Proof of correctness software still hasn't really gone mainstream. (In IC design, though...)
There's a tendency in this area to fall in love with the notation and formalism, rather than viewing it as a means for making better software. In practice, most of the things you need to prove in program proving are trivial, and have to be mechanized or you never get anything done. Once in a while, a theoretically difficult problem shows up. You need some way to address those abstractly and feed the results back into the semi-automated system.
The main concurrent problem addressed in this paper is the Paxos algorithm. That's similar to the earlier arbiter problem.[2] The arbiter problem is also about resolving who wins access to a shared resource in a parallel system. It's down at the hardware level, where two processors talk to one memory, and has to be resolved in nanoseconds or less. There's no sound way to select a winner in one round. But, for each round, you can tell if the algorithm has settled and produced a winner. You have to iterate until it settles. There's no upper bound on how many rounds it takes, but it is statistically unlikely for it to take very many. Arbiters were the first hardware device to have that property, and it was very upsetting at the time. Multiprocessor computers were built before the arbiter problem was solved, and they did indeed have hardware race conditions on access to memory. I used to debug operating systems for those things, and we did get crashes from that.
Good to see someone is still plugging away on the classics.
[1] https://archive.org/details/manualzilla-id-5928072/mode/2up
[2] https://en.wikipedia.org/wiki/Arbiter_%28electronics%29