[tlaplus] Performance of distributed TLC

[Ilya Shchepetkov <ilya.shchepetkov@xxxxxxxxx>]

Hello everybody,

Recently I've tried to run TLC in distributed mode (ad hoc), but was a bit disappointed with its performance. If I run server and worker on the same computer, then the performance (number of explored states per minute) is roughly twice as bad as when running TLC in its usual mode. When I add another worker, on a separate computer, the performance barely improves, if at all.

Is it an expected behavior? How many computers are typically required to see the benefits of distributed mode?

~ ilya shchepetkov

-- 
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 view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/cfa0cef9-affe-405f-8f4d-c14902bb03d1n%40googlegroups.com.