On 14.02.2018 14:22, smo...@xxxxxxxx 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.tlaHi,
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 --
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...@xxxxxxxxxxxxxxxx.
Visit this group at https://groups.google.com/group/tlaplus .
For more options, visit https://groups.google.com/d/optout .