Re: [tlaplus] Check a concurrent algoithm using a large number of concurrent threads

[elliot....@xxxxxxxxx]

Thanks Stephen. Symmetry reduction will definitely be very useful in my verification. But deductive verification is beyond my capability for such a complex system; actually the reason I'm looking at TLA+ is that I can't deductively prove the system is correct.

So I'll begin with using a few threads, and run the model checking using more threads if time permits.

Thanks again for the input.

--
Elliot

On Wednesday, July 8, 2015 at 9:03:36 AM UTC-7, Stephan Merz wrote:
> Hello Elliot,
> 
> TLA+ is most useful for finding bugs in algorithms written at a relatively high level of abstraction. The model checker will typically run out of steam beyond a few threads, but this is usually enough to find concurrency errors, unless you expect that instances involving many more threads show significantly different types of errors. Quite obviously, a model with 4 processes will not give you any information on how scalable your algorithm is. It will however allow to catch possible race conditions between the participating processes, even if these are extreme outliers and do not show up in simulations. You can run TLC in distributed mode on a cluster to push the limit to some extent, but the state space intrinsically grows exponentially with the number of processes. 64 processes will certainly be out of reach.
> 
> Any reduction that you can think of will be useful. TLC offers symmetry reduction: for example, if your algorithm is independent of process IDs, it will come handy to declare processes as a symmetry set.
> 
> The basic technique that TLC uses for model checking is quite naive, based on an explicit enumeration of reachable states. There are many different model checking techniques that use symbolic representations (e.g., SAT or SMT encodings) and can be much more efficient for certain classes of algorithms. There is also the approach of statistical model checking, based on sampling executions and applying statistical tests in order to gain confidence on the probabilities of errors: these scale much further but by design cannot give you full guarantees. In principle, you could also attempt deductive system verification using theorem proving for establishing correctness for an arbitrary number of threads, but this will be much harder work.