Re: [tlaplus] Do I need a supercomputer

[Markus Kuppe <tlaplus-google-group@xxxxxxxxxxx>]

On 08.02.19 07:16, Andy Dwelly wrote:
> I'm working my way through the Video lectures, and today towards the end
> of Video 7 - Paxos commit, I was struck by the comment that extending
> Ballot from {0, 1} to {0, 1, 2} takes 1.5 hours to check on a 128 core
> machine.
> 
> I've got 6 cores on my newish Macbook, so I guess it would take me
> around 32 hours, perhaps a little less given recent clock speeds.
> 
> So I'm wondering if, in general I'll need either special hardware or
> tolerance of a big AWS bill in order to run practical models. I
> appreciate that a lot can be done with a small model but I'm curious how
> this pans out in practice.
> 
> That said, I quite like the idea of having a good excuse for building my
> own supercomputer.


Hi Andy,

you might be interested in two more advanced Toolbox/TLC features:

One is Cloud TLC [1] which - I assume - is comparably simple to use in
contrast to deploying and maintaining a supercomputer (the cloud also
does not outdate as quickly as supercomputers).  The upcoming 1.5.8
Toolbox adds Packet.Net in addition to the already supported Azure and
AWS clouds.

Secondly, the TLC profiler [2] - still under active development but
already quiet usable - will enable you to analyze your specifications
from a cost perspective.  While it won't cure the curse of state space
explosion, it should help you optimize your spec and reduce model
checking time.

Lastly, you might also want to watch my talk on large scale model
checking [3] and Igor Konnov's talk on an SMT based model checker for TLA+.

Thanks
Markus

[1] https://tla.msr-inria.inria.fr/tlatoolbox/doc/cloudtlc/
[2] https://twitter.com/lemmster/status/1082819438036963329
[3] https://www.youtube.com/watch?v=zGIK2p6csAo
[4] https://www.youtube.com/watch?v=Xl1--arESl8

-- 
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 post to this group, send email to tlaplus@xxxxxxxxxxxxxxxx.
Visit this group at https://groups.google.com/group/tlaplus.
For more options, visit https://groups.google.com/d/optout.