Need help understanding the Owicki-Gries method

Question

I've (mistakenly) picked up a course about verifying concurrent programs, and we've so far covered this method called "Owicki-Gries method". Apparently, one can prove various results about the program by associating an assertion with each statement, and show these assertions are inductive and don't interfere with each other. One of our assignments involves Lamports' Fast Mutual Exclusion algorithm, detailed in this paper:

In the paper, an Owicki-Gries style proof for mutual exclusion is given. It looks completely anti-intuitive. What I struggle to understand is how to come up with these assertions in the first place? When do you know these assertions are neither too strong (so strong that it breaks interference freedom) nor too weak(e.g. something trivial, like a tautology with each statement)?

Cheers

Medievalist

Answer 1

To start with, and to provide an understanding of the Owicki-Gries method, I'd strongly recommend checking out the two chapters on Owicki-Gries that can be found in this textbook.

(The full textbook can also be found in draft format here during mid 2021, or you could email Professor Morgan to request a copy)

When you write an assertion and then look to prove local correctness, to quote the textbook "each assertion ... is a postcondition for the fragment immediately before, and a precondition for the one (line of code) immediately after.

To answer your question, you ask about how to decide on the strength of an assertion. As an assertion is needed before and after each line of code, the assertion will range from extremely weak to moderately weak. As such, I'd suggest trying a moderately weak assertion initially.

As you're proving local correct, global invariants and global correctness, if you realise that the assertions are too strong, you can go back to the code and weaken them. Conversely, if the assertions are too weak you can try tweak them to be a little stronger.

You know they are the right strength when they support the running of your program while meeting the conditions of Owicki-Gries and satisfying the properties of safety and liveness.

Ca