[Termtools] TcT StarExec problems

[David Keller]

Hello Jonas,

the problem could be something similar to the problems we have with 
AProVE and runsolver. The JVM reserves a predetermined amount of heap 
space and runsolver counts this completely as used memory. Especially 
when forking this is a problem. Then runsolver sometimes counts the 
memory twice (once for the original process and once for the forked 
process), even if none of the processes actually use that much memory 
and even though much of the actually used memory is shared memory in 
reality.

Since the job [2] is killed due to exceeding the memory limit by a 
factor of 2, I assume you might have a similar problem here. The 
workaround for AProVE is to give AProVE (or more precisely the JVM) a 
much tighter memory limit. We don't actually need more than a few GB in 
most cases, so we only give the JVM that much memory to work with.

BenchExec is much better at handling such cases, but unfortunately it 
does not work on StarExec. The corresponding issue [3] is still open.

Best regards,

David

[3]: https://github.com/StarExec/StarExec/issues/232


On 19.06.20 12:39, Johannes Waldmann wrote:
>> Does anybody know what the problem is?
> your program allocates too much? (or runsolver thinks so)
>
>> [2]: https://www.starexec.org/starexec/secure/details/pair.jsp?id=486124592
> 06/18/20 08:25:32 AM CDT: mem limit : 128873
>
> ./tct-trs ... +RTS -N4 -M128873M -K32M ...
>
> I am not sure about the exact semantics of -M  here.
> Could be off-by-one, could be Mega/Mebi confusion, could be  worse.
>
> perhaps try
> https://downloads.haskell.org/ghc/latest/docs/html/users_guide/runtime_control.html#rts-flag---disable-delayed-os-memory-return
>
> - J.W.
>
> _______________________________________________
> Termtools mailing list
> Termtools at lri.fr
> http://lists.lri.fr/cgi-bin/mailman/listinfo/termtools