|
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.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 |