[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
Re: [tlaplus] TLC throughput decreases by 3 orders of magnitude over time
On 28.11.20 13:10, Arnaud Bos wrote:
I'm running TLC via the Toolbox and I'm observing an impressive decrease
of throughput over time.
Here's an abridged summary of the state space progression with
additional details below:
From start to 01:26:50 the rate was around 14 million states per minute.
From 01:26:50 to 03:36:09 it slowly decreased from 14 to about 10
million states per minute.
At 03:36:09, it suddenly decreased from 10 to around 4 or 5 million
states per minute and stayed there until 04:17:03.
Between 04:17:03 and 04:34:03 there was nothing. The metric jumps from
17 minutes and only 976,955 more states.
Same thing between 04:34:03 and 04:40:01, it jumps by 6 minutes and
Then, from 04:40:01 to 15:24:42 the metrics logging restarts every
minute at a rate of only about 10K states per minutes,
until I went back to my laptop and cancelled the task.
It's running on my 2018 MacBook Pro:
* 2.6 GHz 6-Core Intel Core i7
* 32 GB 2400 MHz DDR4
When I checked the same spec on a smaller number of initial states (with
the same parameters, see below) the day before, my fan went all crazy
and I witnessed almost 100% usage of all my cores. TLC stopped after
around an hour at 190 million states and diameter 100-something if I
remember correctly (here the diameter never got past 7).
In this instance, CPU usage did not exceed 25% from what I could see
between two "doing my weekend business".
The first time I ran this model it took up 300Gb of disk space which was
more than was left on my SSD, so it stopped.
The state space progression above is from the next run I did, replacing
the storage unit with a 1Tb HDD I had at home (I don't know much about
its characteristics other than storage capacity).
So disk I/O does not seem to be the problem, I guess.
Here are the relevant (I think) settings I have used. Basically turning
some knobs up regarding my hardware but not sure what I was doing.
Are my settings the reason why increasing the number of initial states
leads to lower CPU usage? Or is it something with the way the spec is
And what could explain this decreasing throughput behavior?
your description matches the case when TLC's fingerprint set (contains
hashes of all explored states) no longer fits into memory and is
extended to disk. From this point on, for newly generated states, TLC
has to lookup fingerprints on the disk. I suggest running TLC on a
machine with more memory. If your problems remain, please share your
spec and model privately.
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/9823b0b0-45af-068f-8288-f7a74c39acff%40lemmster.de.