Dear Florian,
thanks for all your work.
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.
Excerpts from emails 29 Mar 2019:
DH -> Akihisa Yamada and Jera Hensel: "[...] thanks a lot, also to Johannes, for your hints and suggestions to overcome the memory/core dump problem - but without success. The current workaround (start with 20G instead of 128G as last year) will most certainly result in losing proofs [...]"
Answer by Jera Hensel: "AProVE is also affected. We run it with only 4G, which reduces the memouts significantly but does not solve the problem completely. We think that for most categories, at least it does not affect the ranking. But for example in „C Integer“, we lost the first place due to some memouts. However, we do not want to use even less than 4G since this might also lead to a loss of solved problems. Therefore, we just gave up on this."
Best Dieter
On Thu, 2024-06-13 at 15:06 +0200, Florian Frohn wrote:
Dear all,
I was just informed that the benchmarking framework that we used in the past (BenchExec) is no longer available on StarExec. Hence, we'll have to work with "runsolver" instead. 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.
--
Dieter Hofbauer dieter_hofbauer@web.de Mühlengasse 16, D-34125 Kassel, Germany phone (+49) 561 739 29 54