[johnbender]

This is an important observation!

If the properties of concern for your thread or program are only safety properties (“never does a bad thing”) then the fact that the program may never do anything at all is just fine!

Then, if you want some liveness properties (“eventually does something good”) you’ll need to embed some assumption about fairness/scheduling/progress just as you’ve said!

This appears in early concurrency literature (TLA etc which I can’t be bothered to look for)