Tag(sp22)
Last time we noticed that "every thread, whenever it becomes interested in the critical section, will eventually get access" is a different kind of property–-one that requires an infinite counterexample to disprove about the system. We called this sort of property a liveness property.
In a finite-state system, checking a liveness property amounts to looking for a bad cycle: some trace, starting from an initial state, that loops back on itself. Since these traces don't always loop back to the first state, we'll often call these lasso traces, named after a loop of rope.
Here's an example. Consider the (reachable states only) transition system we drew last time:
Can you find a lasso trace that violates our liveness property?
This lasso trace does just happen to loop back to its first state. It shows the second process executing forever, and the first process being forced to wait eternally.
How could we encode this sort of check in Forge? We wouldn't be able to use the inductive method–-at least, not without a lot of careful theoretical work! So let's use the finite-trace approach we used to generate games of Tic-Tac-Toe. But we can't just say that some state in a trace violates the property: we need to encode the search for a bad cycle.
We'll add the same finite-trace infrastructure as before. This time we're able to use full Forge, so we'll use the transpose (~
) operator to say that the initial state has no predecessors.
It's helpful to have a helper predicate that enforces the trace being found is a lasso.
Let's test this predicate to make sure it's satisfiable. And, because we're careful, let's make sure it's not satisfiable if we don't give the trace enough states to loop back on itself:
There is actually a hidden overconstraint bug in our lasso
predicate. It's not so extreme as to make the predicate unsatisfiable–-so the test above passes! What's the problem?
This is why thinking through vacuity testing is important. It's also a reason why, maybe, we'd like to avoid having to write all this temporal boilerplate (and potentially introduce bugs).
If we know that the trace is a lasso, we can write a predicate that identifies some process being starved. This isn't trivial, though. To see why, look at this initial attempt:
This test fails, which is what we'd expect. So what's wrong with it?
We might first wonder, as we usually should, whether the test allocates enough states to reasonably find a counterexample. We've got 8 reachable states, so maybe we'd need 8 (or 9?) states in the test. But there's something more subtle wrong here.
That sounds like a lot of work. More importantly, it sounds really easy to get wrong. Maybe there's a better way.
I wonder if we could add notions of "always" and "eventually" and so on to Forge?
Your class exercise today is to try out this survey.
In contrast to the last survey, we're not asking you whether some set of constraints should be satisfiable or unsatisfiable. Rather, we're asking whether a specific trace satisfies a constraint that uses the new operators.
Because of my illness last week and the snow day, we're around half a class behind versus the original plan. This means that this week's lab will be the first some of you see of Forge's temporal mode–-which introduces all the operators in the survey!
Here's a quick run-down:
Forge's temporal mode takes away the need for you to explicitly model traces. It forces the engine to only ever find lasso traces, and gives you some convenient syntax for working under that assumption. A field can be declared var
, meaning it may change over time. And so on.
I'll repeat the most important clause above: Forge's temporal mode forces the engine to only ever find lasso traces. It's very convenient if that's what you want, but don't use it if you don't!
Here's an example of what I mean. Suppose we're modeling a system with a single integer counter…
This is satisfiable, but only by exploiting integer overflow. If we weren't able to use overflow, this would be unsatisfiable: there wouldn't be enough integers available to form a lasso. And temporal mode only looks for lassos.