how to prove concurrent algorithms are correct

"An ounce of prevention equals a pound of cure"

预防为主，治疗为辅。

concurrent abstraction

programs are the execution of atomic statements

concurrent programs are interleavings of atomic statements from two or more threads

All possible interleavings of atomic statements must be shown to retain whatever property we are hoping to verify within a concurrent algorithm.

No thread's statements may be (unfairly) excluded from any arbitrary interleaving

we must show that the desirable property holds for all interleavings of atomic statements from two or more threads.



以互斥区的实现为例，需要hold的properties有以下两点：

1.The code enforces mutual exclusion. Threads are disallowed from entering the critical region when another thread is occupying the critical region. Plus, if there are multiple concurrent requests to enter the critical region and no other thread is currently executing within the region, only one requesting thread must be allowed to enter the critical region.

2.If a thread is not executing within the critical region, that thread cannot prevent another thread seeking entry from entering the region.