Using TLA+ to Understand Xen Vchan • Hacker News Board

Re: Using TLA+ to Understand Xen Vchan

#11

Post by pron » Fri, Jan 04, 2019, 4:49 PM UTC

mjb wrote: post #10

pron wrote: post #9

Earlier quoted context omitted.

It may be worthwhile to allow declarations of the form VARIABLE x ∈ Nat but I haven't considered all the implications of doing that. May be worth a discussion on the mailing list or at the conference in September. As to "satisfying the type theory folks," I'm not sure what it means. Type theory studies the features of typed formalisms; it makes no claims as to when working in a typed formalism is preferable to workin…

I think it is worth a discussion. I simply meant that adding simple macros wouldn't make TLA+ typed, and so wouldn't make the people who think TLA+ should be typed any happier than they are today.

There are typed TLA formalisms[1], but they're not called TLA+. I don't know what it means to want TLA+ to be typed. It's like saying someone wants the untyped lambda calculus to be typed. I can understand someone who thinks Lamport was misguided in designing TLA+ as an untyped formalism, but so far it seems that he was right (for the reasons I detailed in my Reddit comment).

[1]: https://www.isa-afp.org/entries/TLA.html, https://drive.google.com/file/d/1rAn3N5hViv3xNe2E55lMzpFFym1...

Re: Using TLA+ to Understand Xen Vchan

#12

Post by im_down_w_otp » Sat, Jan 05, 2019, 3:13 AM UTC

pron wrote: post #6

im_down_w_otp wrote: post #5

Earlier quoted context omitted.

It seems like an odd comparison though. Considering that TLC is exercising a very, very coarse model and a fuzzer is usually exercising a real interface/implementation. The former is dealing with an idealized simplification and the latter is dealing with a shape of real domain coverage when searching for counter-examples. Making even moderately complex TLA+ models or minor iterations on a simple model's depth of repr…

> Considering that TLC is exercising a very, very coarse model and a fuzzer is usually exercising a real interface/implementation. The former is dealing with an idealized simplification and the latter is dealing with a shape of real domain coverage when searching for counter-examples. TLC checks the TLA+ specification, however detailed it is. In practice, it's true that it is usually much more useful to specify at a…

I'm aware of both of these things.

In either case the purpose and thus optimization of each kind of tool is fairly different, even if abstractly they're both "state space exploration", which made the comparison seem odd to me.

Re: Using TLA+ to Understand Xen Vchan

#13

Post by hwayne » Sat, Jan 05, 2019, 5:52 PM UTC

michaelmior wrote: post #4

Always love seeing more examples of TLA+ in action! > One really nice feature of TLC is that (unlike a fuzz tester) it does a breadth-first search and therefore finds minimal counter-examples for invariants. It's worth noting that many fuzzers go to great lengths to produce examples that are as small as possible, but it's true that this just comes naturally with TLC.

> It's worth noting that many fuzzers go to great lengths to produce examples that are as small as possible, but it's true that this just comes naturally with TLC.

While this is true for invariants, unfortunately it's not true for liveness properties. The currently implementation doesn't make any guarantees about the length of a minimum liveness counterexample, and in practice I find it's usually the _longest_ counterexample.

Still super useful, I'm just being a little pedantic here :)