Reasoning behavior of a lock

[efenniht]

I'm wondering how I prove a given program is a correct lock. Informally, I believe that a lock must provide two main features:

1. Mutual exclusion: if thread A is holding a lock L, other threads cannot hold L.
2. Acquire-release of thread-wise views: whenever thread A unlocks L, view of A is released to L; another thread to hold L acquires its view.

However I'm still curious about writing proper proof in (1) midterm exam and (2) formal reasoning. How can I do?

[jeehoonkang]

• Actually, 2. implies 1.
• In the midterm exam, I'll not ask too difficult questions you cannot solve beyond the scope of the lectures.
• For formal reasoning of locks and other concurrent programs, see Iris: https://iris-project.org/

[efenniht]

Thanks for kind answer!