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