2
$\begingroup$

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.

Improve this question
$\endgroup$
3
  • $\begingroup$ I don't know who introduced these terms into concurrent algorithms, but they were already used with similar meanings in Petri nets before 1977. $\endgroup$
    – Gilles 'SO- stop being evil'
    Sep 10, 2015 at 16:46
  • $\begingroup$ @Gilles Lamport has commented that "This paper (of 1977) 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.) " $\endgroup$
    – hengxin
    Sep 13, 2015 at 8:24
  • 1
    $\begingroup$ @hengxin That's a claim that he introduced the terms! Please post this as an answer. $\endgroup$
    – Gilles 'SO- stop being evil'
    Sep 13, 2015 at 10:20

1 Answer 1

Reset to default
4
$\begingroup$

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.

Improve this answer
$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge that you have read and understand our privacy policy and code of conduct.

Not the answer you're looking for? Browse other questions tagged or ask your own question.