3 ms·

Imagine the following scenario, you have encountered an actual bug in concurrent code, and you think it would be great to work on a model and invariants that le

by drdrey 6y ago

Imagine the following scenario, you have encountered an actual bug in concurrent code, and you think it would be great to work on a model and invariants that lets TLA+ find the bug (as an exercise). So you start writing a model, and a set of invariants, you run the tool and... it finds nothing. Does that mean you just proved the bug does not exist? No, you _know_ the bug exists, what it means is that you didn't write a correct model on your first try. So you iterate on it, add a few things you missed, put some extra labels, read the docs a bit more, maybe refine your invariants, make them stronger, work through a couple traces that don't actually make sense in practice (e.g. actors just never taking any action whatsoever). During all this time, you either found nothing or things that were not interesting. At no time have you ever proved anything correct, you just iterated on your model until you managed to capture a real life scenario. It takes some convincing to make the jump from "this model does not violate my invariants" to "I think this model and the invariants are close enough to what I care about that I think it's good enough"... I don't know how to go from there to things like "proven correct" and "flawless".

p0llard 6y ago
Ah sure. I interpreted "proven correct" to mean "proven correct wrt a set of invariants" in this context.
sterlind 6y ago
I mean, specific to my scenario, my invariant was "only one zone at a time" and the liveness property was "everyone who wants a zone eventually gets one", so respectively: 1. \A z \in Zones: Active(z) => ~\E o \in Zones: z # o /\ Active(o) 2. \A w \in Workers: \A z \in Zones: WorkerWantsZone(w, z) ~> WorkerHasZone(w, z) Unlike your scenario, I am checking the spec here. I know that code that properly implements the spec satisfies these two properties, therefore I've proven the spec correct. You can disagree on the importance of those two properties but I've mechanically checked that those properties are always preserved in my finite models, so I know the spec is correct, at least for the model size. You know, it's really not too hard to get started with this stuff. You can always nit-pick but why not try it out and see if it's useful for you?
- drdrey 6y ago
  I am using it, I just don't use it to make claims of correctness.

by drdrey 6y ago

p0llard 6y ago

Ah sure. I interpreted "proven correct" to mean "proven correct wrt a set of invariants" in this context.

sterlind 6y ago

I mean, specific to my scenario, my invariant was "only one zone at a time" and the liveness property was "everyone who wants a zone eventually gets one", so respectively: 1. \A z \in Zones: Active(z) => ~\E o \in Zones: z # o /\ Active(o) 2. \A w \in Workers: \A z \in Zones: WorkerWantsZone(w, z) ~> WorkerHasZone(w, z) Unlike your scenario, I am checking the spec here. I know that code that properly implements the spec satisfies these two properties, therefore I've proven the spec correct. You can disagree on the importance of those two properties but I've mechanically checked that those properties are always preserved in my finite models, so I know the spec is correct, at least for the model size. You know, it's really not too hard to get started with this stuff. You can always nit-pick but why not try it out and see if it's useful for you?

drdrey 6y ago
I am using it, I just don't use it to make claims of correctness.