[Termtools] TcT StarExec problems

[Marcel Hark]

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

Am 19.06.20 um 14:00 schrieb 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
> _______________________________________________
> Termtools mailing list
> Termtools at lri.fr
> http://lists.lri.fr/cgi-bin/mailman/listinfo/termtools
-- 

Marcel Hark
Research Group Computer Science 2
RWTH Aachen University
52056 Aachen
Germany

E-Mail: marcel.hark at cs.rwth-aachen.de"
Phone: +49-241/80-21214
Fax: +49-241/80-22217
Room: 4208, Ahornstr. 55

-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.lri.fr/pipermail/termtools/attachments/20200619/4408bcfc/attachment-0001.htm>