Liveness means that a concurrent program continues to make progress instead of becoming permanently blocked or stalled. Progress may appear as advancing state counters, terminating a computation, or reaching a new configuration. section 20.7
Detecting progress in B9
In B9, update_thread and account_thread alternate through their critical sections, incrementing L->iteration and L->accounted. If user input does not intervene, L->iteration advances until a termination condition is met or the counter reaches SIZE_MAX. Because the visible cell configuration might otherwise repeat indefinitely, life_update detects a previously seen configuration and finishes the game. section 20.7
TAKEAWAY rules:
- Prove that relevant state changes advance toward termination or another demonstrable progress condition. section 20.7
- Treat repeated visible states as possible livelock unless hidden state or an explicit termination test guarantees progress. section 20.7
- Recognize that mutexes and condition variables can make liveness verification difficult in larger threaded programs. section 20.8
// thread A // thread B mtx_lock(&M);..........................mtx_lock(&N); mtx_lock(&N); /*waiting for B */ mtx_lock(&M); /*waiting for A */
A circular lock-acquisition pattern illustrates how threads can wait on one another instead of making progress. section 20.7
