[Solved]: Origin of the terms "safety" and "liveness" for concurrent algorithm properties?

Problem Detail: 

Properties of concurrent algorithms are usually divided into two categories:

1. Safety - something must not happen.

   Properties in this category are for example partial correctness and sometimes deadlock-freedom (the latter depending on the author).

2. Liveness - something that must happen eventually.

   Properties in this category are for example termination and starvation-freedom.

Which publication introduced these terms?

---

The oldest reference I was able to find is "Proving the Correctness of Multiprocess Programs" by Leslie Lamport, dated March 1977:

To prove the correctness of a program, one must prove two essentially different types of properties about it, which we call safety and liveness properties. [...]

It does, however, not claim to introduce these terms.

Asked By : dst

Answered By : hengxin

Lamport commented on his paper "Proving the Correctness of Multiprocess Programs" as follows:

This paper introduced the concepts of safety and liveness as the proper generalizations of partial correctness and termination to concurrent programs. It also introduced the terms "safety" and "liveness" for those classes of properties. I stole those terms from Petri nets, where they have similar but formally very different meanings. (Safety of a Petri net is a particular safety property; liveness of a Petri net is not a liveness property.)

This can be seen as a claim that he (Lamport) has introduced the terms.

Best Answer from StackOverflow

Question Source : http://cs.stackexchange.com/questions/47044

3.2K people like this

 Download Related Notes/Documents