[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

Re: [tlaplus] Multi-threaded TLC Simulation Mode

On 24.02.2018 18:03, William Schultz wrote:

I am trying to check a model with TLC using the following parameters (the specific spec isn't really important):

java tlc2.TLC -simulate -depth 20 -cleanup -gzip -workers 12 -metadir /hdd/tlc_states_1 -config MC.cfg MC.tla

When I actually run TLC the CPU utilization looks suspiciously low (my machine has 12 cores). Here is a a snapshot from htop while TLC was running:

Does simulation mode not run in a multi-threaded mode by default? One alternative I imagine is to just run multiple TLC processes in simulation mode, each with a different random seed, which would probably achieve the same result. Just wondering if this is a known/expected behavior.

Hi William,

the Simulator is indeed single-threaded. Running multiple instances of TLC in simulation mode (with different seeds) is currently the only approach to scale simulation. In the future we might want to build multi-threaded simulator though to avoid the overhead of running multiple Java VMs. Can you open a Github issue for this feature?

In the short term TLC.java could be changed to reject command line parameters that do not apply to the selected mode. For example, -gzip is also meaningless in simulation mode.