Ancestors

Toot

Written by Per Vognsen on 2024-12-30 at 02:18

Revisiting some material on model checking has made me realize that a lot of people (including myself) can be pretty sloppy when they call something a liveness property. In particular, deadlock freedom is definitely not a liveness property. It's a safety property but even more than that it's "just" an invariant property of a single system state. That's the very thing that makes deadlocks easy to dynamically detect (cycles in the waits-on graph).

=> More informations about this toot | More toots from pervognsen@mastodon.social

Descendants

Written by shachaf on 2024-12-30 at 02:20

@pervognsen Hmm, what's the meaning of "liveness" here that excludes deadlock-freedom?

=> More informations about this toot | More toots from shachaf@y.la

Written by Per Vognsen on 2024-12-30 at 02:21

@shachaf The actual formal definition of liveness property!

=> More informations about this toot | More toots from pervognsen@mastodon.social

Written by Per Vognsen on 2024-12-30 at 02:27

@shachaf E.g. https://en.wikipedia.org/wiki/Linear_time_property#Liveness_properties

=> More informations about this toot | More toots from pervognsen@mastodon.social

Written by shachaf on 2024-12-30 at 02:29

@pervognsen Ah, I thought you were saying that a deadlock wasn't a violation of liveness, but I guess you're saying "if your goal is to rule out deadlocks specifically, that's a safety property, since a deadlock is an invalid state".

=> More informations about this toot | More toots from shachaf@y.la

Written by Per Vognsen on 2024-12-30 at 02:31

@shachaf Right, I also think it's an example of why an intuitive slogan like Lamport's "a liveness property is when something good eventually happens" is insufficient because the essential distinction between safety and liveness properties is whether only looking at finite prefixes is always sufficient (regardless of the particular model).

=> More informations about this toot | More toots from pervognsen@mastodon.social

Written by Per Vognsen on 2024-12-30 at 03:01

@shachaf I find the terminology a bit confusing and I'm still not sure of the best way to square some of my intuitions with the formalism but FWIW this seems to be the standard definitions in model checking and related areas.

=> More informations about this toot | More toots from pervognsen@mastodon.social

Written by Per Vognsen on 2024-12-30 at 03:11

@shachaf I'm secretly hoping that an expert reads this and gets sufficiently annoyed to clear up my confusion. :)

=> More informations about this toot | More toots from pervognsen@mastodon.social

Written by Per Vognsen on 2024-12-30 at 03:28

@shachaf I think (part of) the source of my confusion is that the definition of a linear time property isn't made for a particular model, it's for all models with a given set of atomic propositions on states. It's not restricting the prefix extensions in the definition of liveness property to correspond to valid transitions for a particular transition system. If you want to constrain the stepwise property changes, you have to do that separately (with safety properties).

=> More informations about this toot | More toots from pervognsen@mastodon.social