Check a concurrent algoithm using a large number of concurrent threads

[Elliot <elliot....@xxxxxxxxx>]

Hello,

I'm thinking of verifying a complex multi-threaded lockless tree data structure. Reading through the related papers I have found so far gave me the impression that most TLA+/+CAL checking for multi-threaded algorithms use only a small number of processes, like around 3 or 4. We will be using our tree structure with a higher degree of concurrency, like with 64 or even more threads (on real machines with 64 physical cores so the concurrency will be real). Is it possible to use TLA+ for our situation? Is using a gigantic cluster of computers to run lengthy simulations that involve 64 or more processes the only option? Or is there some sort of way to reduce the state space?

Any advice is welcome. I know there may be some related publications that I miss. So pointing me to the right paper would also be very helpful.

Thanks!

--
Elliot