> In Hoare's model, livelock and deadlock cannot be distinguished, This was true in the early days of CSP but the theory has evolved a fair bit since then. The current model explicitly includes failures and divergences as part of the semantics of a process (in addition to its traces); these were added in order to be able to reason rigorously about deadlock and livelock respectively.
During my ten or so years at the PRG, I never once heard either Tony Hoare or Carroll Morgan use the words "deadly embrace".
