Dear all,

finally, BenchExec is working again!

Note that the current post-processors (plain.ari..., ceta.ari...) don't work with BenchExec. I'll upload new post-processors.

Best
Florian

On 6/20/24 09:28, Florian Frohn wrote:

Dear all,

BenchExec is available again on StarExec. However, it doesn't work yet in my tests (all pairs fail with 'run script errors'). I'll let you know as soon as it is fixed.

Best
Florian

On 6/14/24 08:49, Florian Frohn wrote:

Dear all,

I got new from the StarExec team. In the best case, BenchExec will be back at the beginning of next week.

If they don't manage to get it running, we'll ditch the memory limit completely (by setting it to an unrealistically huge value), and we'll only run one benchmark per node at a time. If a solver exhausts the memory of its node, it will start swapping, slow down, and time out, eventually.

I think both options are acceptable for us, even though the latter will double the time that's needed to run the competition, as we can only run one instead of two benchmarks per node. So in this case, we'll have to think about countermeasures (e.g., a smaller timeout).

Best
Florian



-------- Forwarded Message --------
Subject: Re: [Termtools] Re: BenchExec no longer available
Date: Thu, 13 Jun 2024 18:15:14 +0200
From: Florian Frohn <florian.frohn@informatik.rwth-aachen.de>
To: termtools@lists.rwth-aachen.de


Dear Dieter, 

If I remember correctly, we used runsolver at some point, but then
we switched to BenchExec due to issues with the measurement of the
runtime. If you remember any details / your tool was affected by
these problems, please let me know.

Wasn't runsolver this piece of software that couldn't handle memory
management properly, especially for Java applications like Aprove and
MnM? We had lively discussions on this topic in 2019, but without
helpful results. Only replacing runsolver by benchexec finally solved
the issue. I definitely don't want to experience this disaster again.
In 2019, I seriously considered removing MnM from TermComp for that
reason.

You're right, it was about memory, not runtime. I made clear that this is a serious issue for us, and asked whether they can revive benchexec.

Best
Florian


_______________________________________________
Termtools mailing list -- termtools@lists.rwth-aachen.de
To unsubscribe send an email to termtools-leave@lists.rwth-aachen.de


_______________________________________________
Termtools mailing list -- termtools@lists.rwth-aachen.de
To unsubscribe send an email to termtools-leave@lists.rwth-aachen.de