I've been told by people at Intel and Amazon that model checking gave
them the confidence to make optimizations their systems that they
wouldn't have dared otherwise. That implies that they were able to
use large enough models to provide that confidence. The information
about Intel dates from perhaps a decade ago, so I expect they were
using computers less powerful than your Macbook. I believe they would
run their models for a couple of weeks.
I know of no easy way to tell in advance whether the system you're
building can be usefully modeled by a spec that can be checked with a
sufficiently large model to give you confidence in its correctness.
You will learn by experience how to reduce the number of reachable
states in your specs, broadening the range of systems for which model
checking will provide the confidence you want. When I first used the
model checker, I was surprised by how effective even tiny models were
at finding errors.
Renting time on a large machine from Amazon or Microsoft is not all
that expensive--certainly cheaper than building your own
supercomputer. If you're using TLA+ for serious system design, you
will probably at least want a second computer with as much memory as
you can afford so you can run TLC without tying up the computer you
use regularly.
Leslie
On Friday, February 8, 2019 at 7:16:23 AM UTC-8, 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.
Andy Dwelly