We report an error in a verification model in [4] and present a revised mod
el with verification result. Our result explains the reason why SPIN found
the race condition in the synchronization algorithm. We also show that the
suggested fix in [4] is incorrect.