Concurrent systems are often specified with two complementary kinds of correctness property.

A safety property says that something bad never happens. Mutual exclusion is a safety property: two tasks must never be inside the protected critical section at the same time. A corrupted state or duplicated supposedly unique allocation is another safety violation.

A liveness property says that something good eventually happens. A submitted task eventually completes, a waiting consumer eventually receives an available item, or a lock request eventually succeeds under the stated scheduling assumptions.

Deadlock violates liveness because all participants can wait forever. Livelock also violates progress even though participants keep executing: they repeatedly react to one another without completing useful work. Starvation occurs when some participant can be postponed indefinitely while others continue progressing.

Safety and liveness are independent. A program can preserve every invariant by never doing anything, making it safe but useless; it can also make continual progress while occasionally corrupting state.

Concurrent correctness therefore requires both: preserve required invariants under every allowed interleaving and establish the progress guarantees the application actually needs.