Ancestors

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

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

Toot

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

Descendants