109
Algorithm 3: proof of correctness
nMutual exclusion is preserved since:
uP0
and P1 are both in CS only if flag[0] = flag[1] = true and only if
turn = j for each Pi (impossible)
nWe now prove that the progress and bounded waiting
requirements are satisfied:
uPi
cannot enter CS only if stuck in while() with condition flag[j] = true and
turn = j.
uIf Pj is not ready to enter CS then flag[j] = false and Pi can then
enter its CS