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.

$\endgroup$
  • $\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 Sep 10 '15 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 '15 at 8:24
  • 1
    $\begingroup$ @hengxin That's a claim that he introduced the terms! Please post this as an answer. $\endgroup$ – Gilles Sep 13 '15 at 10:20
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.

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

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