Model checking double buffering

[Jeenu Viswambharan]

I'm modelling two audio channels playing back with double buffering. Each channel goes through a sequence of transitions on their own, but for the purpose of double buffering, each nudges the other's playback. In the beginning, one of the channels is given a head start, which then nudges the other, and the other does the same back, and so on. Together, they are you play back all the audio blobs.

I was able to get TLC to verify some of the properties. For others, I get temporal property violation, reporting stuttering. I wondered if I can use this example to clear some doubts:

Right now, I've to use -deadlock to get the checks successfully run (those that TLC can). From discussions here and elsewhere, having to use -deadlock stems from the fact that my model terminates. For example, a counter example given (without -deadlock) was this:

State 5: <Complete line 43, col 3 to line 45, col 28 of module AudioChannel>
/\ nextBlob = 2
/\ channels = << [blob |-> 1, state |-> "complete", id |-> 1],
[blob |-> 0, state |-> "idle", id |-> 2] >>

This situation arose because the first channel didn't nudge the second one, so no bootstrapping happened, and this is indeed a terminal state. But I did specify weak fairness on all steps. Given that, shouldn't TLC have definitely taken the nudge step?

(I had noticed a mention somewhere that liveness/fairness apply only to infinite behaviors. I could potentially run the model unconstrained, but then that never terminates!).

That brings me to my main question: I'm aware of the semantics of fairness formulae, but what exactly does fairness/liveness imply when model checking with TLC? In the presence of liveness/fairness, viz.:

• Does TLC seek out transitions eagerly that would satisfy the property?
• Or does TLC goes about its business as usual, and then check if the property is satisfied?
  

I ask because I had to specify weak fairness explicitly for one check to pass. Couple of others don't even pass--they report stuttering, as mentioned earlier. (I'll hazard that the way I've written them may be incorrect).

In general, though: why should fairness matter? Shouldn't fairness be the default as opposed to something explicitly picked out? I mean, one writes down steps with the intent that they're taken, so what additional meaning does fairness convey to the spec consumer? Like, "seriously, these steps are important, so do make sure you take them often enough"? Or, "this spec works only if you do these steps more as opposed to the rest"?

My interpretation (perhaps wrongly) has been that steps are to be taken automatically as soon as favorable conditions arise--more like an electronic circuit as opposed to an imperative program selectively checking conditional statements.

Apologies - this ended up being longer and chaotic than I originally thought. Any pointers are appreciated.

Thanks,

Jeenu

[Andrew Helwer]

Liveness checking won't work if your model is constrainted or bounded, unfortunately.

> Shouldn't fairness be the default as opposed to something explicitly picked out?

Not necessarily. Consider a system where you also specify possible errors that can occur. You usually wouldn't want to assert that an error step is weakly/strongly fair.

> My interpretation (perhaps wrongly) has been that steps are to be taken automatically as soon as favorable conditions arise

You can certainly write your spec so that it works this way, but this is a very strong assumption about your system. You generally want to make your assumptions as weak as possible, since that makes whatever invariants you can verify in that regime much more generally applicable. TLA+ is often useful for examining how your system works when all does not go to plan - processes die and then come alive again an arbitrary amount of time later, etc.

> But I did specify weak fairness on all steps. Given that, shouldn't TLC have definitely taken the nudge step?

Hard to say without really diving into your spec, but you may have needed strong fairness instead.

> what exactly does fairness/liveness imply when model checking with TLC?

It is adversarial. TLC will try to find a behavior serving as a counterexample to whatever property you're trying to show.

Andrew

[Stephan Merz]

It sounds like your spec has a deadlock (since you say that TLC found a terminal state). A fairness condition will not remove the deadlock: fairness conditions assert that actions that are "often enough" enabled will eventually be taken but in the deadlock state no action is enabled.

Glancing at your spec, the state found by TLC is indeed a deadlock, i.e. no action is enabled. In particular, Load(i) is disabled because nextBlob = channels[i].blob holds for no i, and Nudge(i) is disabled because channels[i].state \in {"ready", "playing"} holds for no i. Is this a state that you expect executions to reach? If not, inspect the trace that TLC displays for reaching that deadlock and see what goes wrong.

Also, it seems to me that you want to remove the conjunct

nextBlob <= MAX_BLOBS

from the definition of Load(i) since it looks that this condition is here only to bound the state space of the model. Such predicates should be added as state constraints for TLC (to be found under "Advanced Options"). The difference is that TLC will not consider the action to be disabled in a state that does not satisfy the predicate but will just ignore the successor states in model checking.

Hope this helps,

Stephan

--
You received this message because you are subscribed to the Google Groups "tlaplus" group.
To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+u...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/f1f9071d-c331-478c-a5a4-d7541d5d7e71n%40googlegroups.com.