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]
Defining Liveness by Bowen Alpern and others. p. 182: every finite prefix can still be extended to satisfy a liveness property
New to topics? Read the docs here!