[Termtools] TcT StarExec problems

[Jonas Schöpf]

Dear Johannes, David and Marcel!

First of all, thank you for your replies.

On 6/19/20 2:25 PM, Marcel Hark wrote:
> Dear Jonas,
> 
> as far as we know, the maintainers of star exec are debugging BenchExec
> right now, see [4]. However, this issue is also still open.
> 
> Best regards,
> 
> Marcel
> 
> [4] https://github.com/StarExec/StarExec/issues/258

On 6/19/20 2:00 PM, David Keller wrote:
> 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
> 

Most of the time I use runsolver, so I have no experience with
BenchExec, but if it works again it may be worth trying it :)

Normally (and it was also used in 2018, but maybe with BenchExec) we use
STAREXEC_MAX_MEM as memory limit and I already tried reducing it, but
maybe not enough. I started some test runs with even fewer memory.

On 6/19/20 12:39 PM, Johannes Waldmann wrote:
>> Does anybody know what the problem is?
> 
> your program allocates too much? (or runsolver thinks so)
Yes, I already tried yesterday reducing the memory limit, but it did not
work.
I think that it may be a similar problem as mentioned by David and Marcel.
> 
>> [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

This sounds promising. I will definitely try it today and hope that this
fixes my problem.

Thank you all!

Best regards,
Jonas

-- 
GPG fingerprint: 0BF3 B30B F1D5 6556 795E  F68F 8626 F794 FE62 BE1F