I (erroneously) took a course on checking parallel programs, and we still considered this method called the Ovitsky-Gris Method. Apparently, it is possible to prove various results about the program by comparing the statement with each statement and show that these statements are inductive and do not interfere with each other. One of our assignments includes the Lamports quick mutual exclusion algorithm, described in detail in this article :
The article provides proof of the Ovitsky-Gris style for mutual exclusion. He looks completely anti-intuitive. What I'm trying to understand is how to come up with these statements in the first place? When do you know that these statements are not too strong (so strong that they violate interference freedom) and not too weak (for example, something trivial, like a tautology with each statement)?
Greetings
source share