Correctness of concurrent programs
Correctness of concurrent programs
A concurrent program must satisfy two classes of property: safety and liveness.
Safety Properties : assert that nothing ‘bad’ will ever happen during an execution (that is, that the program will never enter a ‘bad’ state).
Liveness properties : assert that something ‘good’ will eventually happen during execution.
Liveness is concerned with making progress in a program. Situations which prevent progress are livelock and starvation.
Deadlock can be considered to impact both safety and liveness.
Liveness properties are in general more difficult to prove than safety properties since they are dependent on the scheduling properties being used and require reasoning about infinite sequences of actions.