(Omit source code)
while (owner != null) wait(); owner = phil;
if (phil == owner) owner = null; notify();