Safety and Liveness
Safety and Liveness
Safety vs. liveness
Safety: nothing “bad” will ever happen
Liveness: something “good” will happen eventually
(but we don’t know when)
Safety vs. liveness for sequential programs
Safety: the program will never produce a
wrong result
(“partial correctness”)
Liveness: the program will produce a result
(“termination”)
Safety vs. liveness for state-transition graphs
Safety:
those properties whose violation always
has a finite witness
(“if something bad happens on an infinite
run, then it happens already on some finite
prefix”)
For any run R, R satisfies P iff
every prefix of R satisfies P.
For any run R, R does not satisfy P iff
there exists a prefix of R that does not satisfy P.
Safety vs. liveness for state-transition graphs
Liveness:
those properties whose violation never
has a finite witness
(“no matter what happens along a finite run,
something good could still happen later”)
For any
finite
run R, there exists R1 such that
R1 is an extension of R, and R1 satisfies P.
Safety vs. liveness for state-transition graphs
Safety:
those properties whose violation always
has a finite witness
(“if something bad happens on an infinite
run, then it happens already on some finite
prefix”)
Liveness:
those properties whose violation never
has a finite witness
(“no matter what happens along a finite run,
something good could still happen later”)
Safety: the properties that can be
checked on finite executions
Liveness: the properties that cannot be
checked on finite executions
(they need to be checked on
infinite executions)
This is much easier.
Example: Mutual exclusion
It cannot happen that both threads are in their
critical sections simultaneously.
Safety
Example: Bounded overtaking
Whenever thread A wants to enter the critical
section, then thread B gets to enter at most
once before thread A gets to enter.
Safety
Example: Starvation freedom
Whenever thread A wants to enter the critical
section, provided thread B never stays in the
critical section forever, A gets to enter eventually.
Liveness
Example: Deadlock freedom
When only A wants to enter the critical section, it
gets to enter eventually.
Liveness
When both A and B want to enter the critical section,
one of them gets to enter eventually.
Safety and liveness are key concepts in program correctness evaluation. Safety ensures that nothing bad will happen, while liveness guarantees that something good will happen eventually. Safety focuses on correctness and preventing errors, while liveness emphasizes progress and termination. This article delves into the differences between safety and liveness in sequential programs and state-transition graphs, providing clarity on their importance in program analysis.
Download Presentation
Please find below an Image/Link to download the presentation.
The content on the website is provided AS IS for your information and personal use only. It may not be sold, licensed, or shared on other websites without obtaining consent from the author.If you encounter any issues during the download, it is possible that the publisher has removed the file from their server.
You are allowed to download the files provided on this website for personal or commercial use, subject to the condition that they are used lawfully. All files are the property of their respective owners.
The content on the website is provided AS IS for your information and personal use only. It may not be sold, licensed, or shared on other websites without obtaining consent from the author.
E N D
Presentation Transcript
Safety vs. liveness Safety: nothing bad will ever happen Liveness: something good will happen eventually (but we don t know when)
Safety vs. liveness for sequential programs Safety: the program will never produce a wrong result ( partial correctness ) Liveness: the program will produce a result ( termination )
Safety vs. liveness for state-transition graphs Safety: those properties whose violation always has a finite witness ( if something bad happens on an infinite run, then it happens already on some finite prefix ) For any run R, R does not satisfy P iff there exists a prefix of R that does not satisfy P. For any run R, R satisfies P iff every prefix of R satisfies P.
Safety vs. liveness for state-transition graphs Liveness: those properties whose violation never has a finite witness ( no matter what happens along a finite run, something good could still happen later ) For any finite run R, there exists R1 such that R1 is an extension of R, and R1 satisfies P.
Safety vs. liveness for state-transition graphs Safety: those properties whose violation always has a finite witness ( if something bad happens on an infinite run, then it happens already on some finite prefix ) Liveness: those properties whose violation never has a finite witness ( no matter what happens along a finite run, something good could still happen later )
This is much easier. Safety: the properties that can be checked on finite executions Liveness: the properties that cannot be checked on finite executions (they need to be checked on infinite executions)
Example: Mutual exclusion It cannot happen that both threads are in their critical sections simultaneously. Safety
Example: Bounded overtaking Whenever thread A wants to enter the critical section, then thread B gets to enter at most once before thread A gets to enter. Safety
Example: Starvation freedom Whenever thread A wants to enter the critical section, provided thread B never stays in the critical section forever, A gets to enter eventually. Liveness
Example: Deadlock freedom When only A wants to enter the critical section, it gets to enter eventually. When both A and B want to enter the critical section, one of them gets to enter eventually. Liveness
