4 ms·

TLA+ doesn't prove anything to be "correct" or "flawless", I find it extremely worrisome that you claim as much. It failed to exhibit traces that violated your

by drdrey 6y ago

TLA+ doesn't prove anything to be "correct" or "flawless", I find it extremely worrisome that you claim as much. It failed to exhibit traces that violated your invariants, which says something completely different.

p0llard 6y ago
I've never actually used TLA+, but my understanding is that it does exhaustive model checking (presumably using some suitable simulation relation), so in this case failure to find a violating trace indicates that no such trace exists, and the invariants always hold. Correctness might well be defined solely by a set of invariants, so I don't quite understand your point here?
- hwayne 6y ago
  This is correct: the TLA+ model checker (TLC) will check all possible behaviors for the finite model. As the GP said, they were only working with a finite number of workers, but within those constraints it guarantees the spec always satisfies the invariants. (This is of course assuming that TLC doesn't have any bugs that would cause it to misreport. By contrast something like randomized testing doesn't guarantee the spec satisfies the invariants even if the tester is bug-free.)
  - sterlind 6y ago
    exactly. I've proven that in a scenario with a certain number of zones and workers, the invariants and temporal properties cannot be violated. With more work, I could prove the invariants for any number of workers and zones using TLAPS rather than TLC, though I couldn't prove the temporal properties in this way (since TLAPS doesn't support temporal logic, it can only prove invariants.)
- 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.
pron 6y ago
1. TLA+ doesn't "find" or not find anything. It is a mathematical language for describing systems and assertions about them. There is a proof assistant for TLA+ that checks your formal proofs of theorems that say that your assertions follow from the description, and model checkers that verify your theorems automatically. 2. If you use the model checker, it's not about it "failing to find" a counter example. A model checker result is a proof that no such example exists. True, it is usually a proof about some finite instance of your system description. 3. There is just no such thing as proving a system flawless. Software systems are physical systems exhibiting probabilistic behaviors. At best you can prove things about a mathematical description of a system, which mean that as long as the physical system behaves according to the description, the result follows. Of course, the first part at best holds with some probability.

by drdrey 6y ago

p0llard 6y ago

I've never actually used TLA+, but my understanding is that it does exhaustive model checking (presumably using some suitable simulation relation), so in this case failure to find a violating trace indicates that no such trace exists, and the invariants always hold. Correctness might well be defined solely by a set of invariants, so I don't quite understand your point here?

hwayne 6y ago
This is correct: the TLA+ model checker (TLC) will check all possible behaviors for the finite model. As the GP said, they were only working with a finite number of workers, but within those constraints it guarantees the spec always satisfies the invariants. (This is of course assuming that TLC doesn't have any bugs that would cause it to misreport. By contrast something like randomized testing doesn't guarantee the spec satisfies the invariants even if the tester is bug-free.)
- sterlind 6y ago
  exactly. I've proven that in a scenario with a certain number of zones and workers, the invariants and temporal properties cannot be violated. With more work, I could prove the invariants for any number of workers and zones using TLAPS rather than TLC, though I couldn't prove the temporal properties in this way (since TLAPS doesn't support temporal logic, it can only prove invariants.)
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.

pron 6y ago

1. TLA+ doesn't "find" or not find anything. It is a mathematical language for describing systems and assertions about them. There is a proof assistant for TLA+ that checks your formal proofs of theorems that say that your assertions follow from the description, and model checkers that verify your theorems automatically. 2. If you use the model checker, it's not about it "failing to find" a counter example. A model checker result is a proof that no such example exists. True, it is usually a proof about some finite instance of your system description. 3. There is just no such thing as proving a system flawless. Software systems are physical systems exhibiting probabilistic behaviors. At best you can prove things about a mathematical description of a system, which mean that as long as the physical system behaves according to the description, the result follows. Of course, the first part at best holds with some probability.