= 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>.<Defining Liveness by Bowen Alpern and others>[p. 182: every finite prefix can still be extended to satisfy a liveness property]{ref}
Back to article page
