[tlaplus] Model checking double buffering

[Jeenu Viswambharan <jeenuv@xxxxxxxxx>]

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

-- 
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+unsubscribe@xxxxxxxxxxxxxxxx.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/f1f9071d-c331-478c-a5a4-d7541d5d7e71n%40googlegroups.com.