Concurrency




always:
nonexecutable dunk(P,T) if flush(T).

nonexecutable dunk(P,T) if dunk(P1,T), P <> P1.

nonexecutable dunk(P,T) if dunk(P,T1), T <> T1.