Liveness property

A requirement of eventual progress, with no finite prefix ruling out its eventual satisfaction. For starvation freedom, a persistent requester must eventually enter its critical section. Establishing such a liveness property requires explicit scheduling and protocol assumptions in addition to mutual exclusion. Exhaustive finite thread interleaving checks alone do not establish eventual service for repeatedly competing software threads.^[ref]

For acquisition of a mutex, the guarantee that every persistent requester eventually succeeds, under specified scheduling assumptions and with owners eventually releasing. Some software threads repeatedly succeeding while another waits forever violates starvation freedom without violating mutual exclusion. A finite bound on the wait, and service in arrival order, are additional requirements.

With a LIFO stack of waiting requests, an old request may remain at the bottom while a new request arrives before each completion and is served next. Every service can finish in finite time while the old request waits forever. A FIFO queue prevents this overtaking within one priority class. Nonpreemptive strict-priority arbitration can separately starve a lower-priority class; using a LIFO stack adds potential starvation even among requests of equal priority.