Re: [tlaplus] Re: Scaling up model checking

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

On 16.11.19 06:02, william.schultz via tlaplus wrote:
> I see. Should I expect better scalability with distributed TLC? Your
> presentation here
> <https://www.youtube.com/watch?v=zGIK2p6csAo> indicates that distributed
> mode may be able to scale linearly in some cases. My goal is to try
> running multiple TLC worker processes on the same EC2 machine. Do you
> have reason to believe that will improve performance versus running all
> threads inside the same JVM process? I am also curious if using multiple
> fingerprint set servers is recommended for scaling to this level (i.e.
> 96 machine cores). I am just curious if it's worth throwing many
> cores/machines at the problem. If the improvements are only marginal, it
> may just be simpler for me to run non-distributed TLC with suitably many
> workers.
> 

Hi Will,

let's move this discussion to GitHub [1] because it is too specific for
the group's general scope.

Best
Markus

[1] https://github.com/tlaplus/tlaplus/issues/396

-- 
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/75f45a2c-8cd1-bec9-54ce-c1de52abd309%40lemmster.de.