Hard Drive Usage

[smo...@ualr.edu]

I have a several hundred line specification running on an 80 core HPC and after a day it is using 423GB of space. While I believe it is close to finished it is probably going to run out of space before it does. Is there a way to run TLC that uses less HDD space? I mean, there is 865GB of RAM in this machine. So I actually have more RAM available then HDD. It's currently only using 91 GB of RAM.

[Markus Alexander Kuppe]

Hi,

what OS do you run TLC on? What parameters do you pass to TLC and its
Java VM if any?

Thanks
Markus

[smo...@ualr.edu]

The OS is some version of centOS, and the command line I run is: java tlc2.TLC -workers 80 -deadlock -config config.cfg spec.tla

Thanks.

[Markus Alexander Kuppe]

On 14.02.2018 14:22, smo...@ualr.edu wrote:

The OS is some version of centOS, and the command line I run is: java tlc2.TLC -workers 80 -deadlock -config config.cfg spec.tla

Hi,

launch TLC with the "-gzip" parameter to on-the-fly compress the disk pages of the state queue. Compressing pages obviously comes at the expense of model checking time¹. If that doesn't cut it, I suggest to create a ramdisk with either ramfs or tmpfs and have TLC put its states/ folder in there (tmpfs swaps to disk).

If neither of the above solves your problem and you are adventurous, you can ping me off-line and I will share with you a TLC prototype that makes better use of memory.

Thanks
Markus

¹ For TLC's MongoRepl test spec [1] on an AWS x1.16xlarge [2] instance:
- gzip on: 2.8GB total state queue size and 40min model checking time
- gzip off: 33GB total state queue size and 25min model checking time

The actual state queue size at runtime is normally smaller because old pages are asynchronously garbage collected. For this measurement though I disabled the collector.

[1] https://github.com/tlaplus/tlaplus/tree/master/general/performance/MongoRepl
[2] https://aws.amazon.com/ec2/instance-types/#memory-optimized

[Sean Orme]

thanks. I'll give -gzip a go.

--
You received this message because you are subscribed to a topic in the Google Groups "tlaplus" group.
To unsubscribe from this topic, visit https://groups.google.com/d/topic/tlaplus/GDu_snWU_6w/unsubscribe.
To unsubscribe from this group and all its topics, send an email to tlaplus+unsubscribe@googlegroups.com.
To post to this group, send email to tla...@googlegroups.com.
Visit this group at https://groups.google.com/group/tlaplus.
For more options, visit https://groups.google.com/d/optout.

--

Sean Orme | Computer Science Instructor

University of Arkansas at Little Rock | EIT 576
501.569.8143 | smo...@ualr.edu | http://ualr.edu/computerscience/