Properties of an execution of a computer program —particularly for concurrent and distributed systems— have long been formulated by giving ''safety properties'' ("bad things don't happen") and ''liveness properties'' ("good things do happen").
A simple example will illustrate safety and liveness. A program is
totally correct with respect to a precondition
and postcondition
if any execution started in a state satisfying
terminates in a state satisfying
. Total correctness is a conjunction of a safety property and a liveness property:
* The safety property prohibits these "bad things": executions that start in a state satisfying
and terminate in a final state that does not satisfy
. For a program
, this safety property is usually written using the
Hoare triple
Hoare logic (also known as Floyd–Hoare logic or Hoare rules) is a formal system with a set of logical rules for reasoning rigorously about the correctness of computer programs. It was proposed in 1969 by the British computer scientist and lo ...
.
* The liveness property, the "good thing", is that execution that starts in a state satisfying
terminates.
Note that a ''bad thing'' is discrete, since it happens at a particular place during execution.
A "good thing" need not be discrete, but the liveness property of termination is discrete.
Formal definitions that were ultimately proposed for safety properties and liveness properties
demonstrated that this decomposition is not only intuitively appealing but is also complete: all properties of an execution are a conjunction of safety and liveness properties.
Moreover, undertaking the decomposition can be helpful, because the formal definitions enable a proof that different methods must be used for verifying safety properties versus for verifying liveness properties.
Safety
A safety property proscribes discrete ''bad things'' from occurring during an execution.
A safety property thus characterizes what is permitted by stating what is prohibited. The requirement that the ''bad thing'' be discrete means that a ''bad thing'' occurring during execution necessarily occurs at some identifiable point.
Examples of a discrete ''bad thing'' that could be used to define a safety property include:
* An execution that starts in a state satisfying a given precondition terminates, but the final state does not satisfy the required postcondition;
* An execution of two concurrent processes, where the program counters for both designate statements within a critical section;
* An execution of two concurrent processes where each process is waiting for another to change state (known as
deadlock
In concurrent computing, deadlock is any situation in which no member of some group of entities can proceed because each waits for another member, including itself, to take action, such as sending a message or, more commonly, releasing a lo ...
).
An execution of a program can be described formally by giving the infinite sequence of program states that results as execution proceeds,
where the last state for a terminating program is repeated infinitely.
For a program of interest, let
denote the set of possible program states,
denote the set of finite sequences of program states,
and
denote the set of infinite sequences of program states. Relation
holds for sequences
and
iff
is a prefix of
or
equals
.
A property of a program is the set of allowed executions.
The essential characteristic of a safety property
is:
If some execution
does not satisfy
then the defining ''bad thing''
for that safety property occurs at some point in
. Notice that after such a ''bad thing'', if further execution results in an execution
, then
also does not satisfy
,
since the ''bad thing'' in
also occurs in
.
We take this inference about the irremediability of ''bad things'' to be the defining characteristic for
to be a safety property.
Formalizing this in predicate logic gives a formal definition for
being a safety property.
:
This formal definition for safety properties implies that if an execution
satisfies a safety property
then every prefix of
(with the last state repeated)
also satisfies
.
Liveness
A liveness property prescribes ''good things'' for every execution or, equivalently, describes something that must happen during an execution.
The ''good thing'' need not be discrete —it might involve an infinite number of steps. Examples of a ''good thing'' used to define a liveness property include:
* Termination of an execution that is started in a suitable state;
* Non-termination of an execution that is started in a suitable state;
* Guaranteed eventual entry to a critical section whenever entry is attempted;
* Fair access to a resource in the presence of contention.
The ''good thing'' in the first example is discrete but not in the others.
Producing an answer within a specified real-time bound is a safety property rather than a liveness property.
This is because a discrete ''bad thing'' is being proscribed: a partial execution that reaches a state where the answer still has not been produced and the value of the clock (a state variable) violates the bound. Deadlock freedom is a safety property: the "bad thing" is a
deadlock
In concurrent computing, deadlock is any situation in which no member of some group of entities can proceed because each waits for another member, including itself, to take action, such as sending a message or, more commonly, releasing a lo ...
(which is discrete).
Most of the time, knowing that a program eventually does some "good thing" is not satisfactory; we want to know that the program performs the "good thing" within some number of steps or before some deadline. A property that gives a specific bound to the "good thing" is a safety property (as noted above), whereas the weaker property that merely asserts the bound exists is a liveness property. Proving such a liveness property is likely to be easier than proving the tighter safety property because proving the liveness property doesn't require the kind of detailed accounting that is required for proving the safety property.
To differ from a safety property, a liveness property
cannot rule
out any finite prefix
of an execution (since such
an
would be a "bad thing" and, thus, would be defining a safety property).
That leads to defining a liveness property
to be a property that does not rule out any finite prefix.
:
This definition does not restrict a ''good thing'' to being discrete —the
''good thing'' can involve all of
, which is an infinite-length execution.
History
Lamport used the terms ''safety property'' and ''liveness property''
in his 1977 paper
on proving the correctness of
multiprocess (concurrent) programs.
He borrowed the terms from
Petri net theory
A Petri net, also known as a place/transition (PT) net, is one of several mathematical modeling languages for the description of distributed systems. It is a class of discrete event dynamic system. A Petri net is a directed bipartite graph that h ...
, which was using the terms
''liveness'' and ''boundedness'' for describing how the assignment of a Petri net's "tokens"
to its "places" could evolve; Petri net ''safety'' was a specific form of ''boundedness''.
Lamport subsequently developed a formal definition of safety for a
NATO short course on distributed systems in Munich.
It assumed that properties are invariant under stuttering.
The formal definition of safety given above appears in a paper by Alpern and
Schneider;
the connection between the two formalizations of safety properties
appears in a paper by Alpern, Demers, and Schneider.
Alpern and Schneider
gives the formal definition for liveness, accompanied by a proof that all properties can be constructed using safety properties and liveness properties. That proof was inspired by Gordon Plotkin's insight that safety properties correspond to closed sets and liveness properties correspond to dense sets in a natural topology. Subsequently, Alpern and Schneider
not only gave a
Büchi automaton
In computer science and automata theory, a deterministic Büchi automaton is a theoretical machine which either accepts or rejects infinite inputs. Such a machine has a set of states and a transition function, which determines which state the machi ...
characterization for the formal definitions of safety properties and liveness properties but used these automata-formulations to show that verification of safety properties would require an
invariant
Invariant and invariance may refer to:
Computer science
* Invariant (computer science), an expression whose value doesn't change during program execution
** Loop invariant, a property of a program loop that is true before (and after) each iteratio ...
and verification of liveness properties would require a
well-foundedness argument. The correspondence between the kind of property (safety vs liveness) with kind of proof (invariance vs well-foundeness) was a strong argument that the breakdown of properties into safety and liveness (as opposed to some other partitioning) was a
useful one –knowing the type of property to be proved dictated the type of proof that would be required.
References
{{reflist
Concurrent computing
Theoretical computer science
Model checking