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 | View the thread | More toots from pervognsen@mastodon.social
text/geminiThis content has been proxied by September (ba2dc).