Wolfgang Jeltsch (Dec 08 2022 at 14:44): Wolfgang Jeltsch (Dec 08 2022 at 14:44):When I run isabelle build on a non-trivial project, Isabelle tends to virtually take over my system, making other work difficult. It’s particularly bad when having a video call running concurrently. In this situation, the build typically takes much longer than usual and the video call effectively stops (basically no audio and video transmission anymore) and is finally dropped because of some timeout.
Initially, I thought that perhaps the scheduler assigns almost all CPU time to Isabelle’s threads, because Isabelle apparently wants to perform a lot of computation. However, this would be a bit stupid, and I find it hard to believe that Linux, which I’m using, can’t do a better scheduling job after 30 years of development. Recently, a colleague suggested that the problem I’m experiencing might have to do with RAM shortage instead.
In any case, are others here experiencing the same issue, and does someone know what the cause of this issue might be?
Jan van Brügge (Dec 09 2022 at 15:00):I would also guess RAM, Linux then has to start swapping to disk which is slow. You could try to use cgroups or containers (aka cgroups in disguise) to limit the RAM that isabelle has access to, e.g.:
cgcreate -g memory:isabelle
echo 500M > /sys/fs/cgroup/memory/isabelle/memory.limit_in_bytes
cgexec -g memory:isabelle isabelle build
(Adjust the 500M to a more suitable value ofc). Might need to install a package, on Ubuntu cgroup-tools
Jan van Brügge (Dec 09 2022 at 15:02):Otherwise systemd makes this a bit easier: systemd-run --scope -p MemoryMax=500M --user isabelle build
Wolfgang Jeltsch (Dec 09 2022 at 18:31):Thanks a lot. This seems to be helpful indeed.
Did I get this correctly that your solution boils down to letting Isabelle suffer from swapping more, while having other software, like the one for your video calls, suffer from swapping less or not at all?
Notification Bot (Dec 10 2022 at 00:28):Wolfgang Jeltsch has marked this topic as resolved.
Notification Bot (Dec 10 2022 at 00:28):Wolfgang Jeltsch has marked this topic as unresolved.
Jan van Brügge (Dec 10 2022 at 10:58):Theoretically yes, but in practice it should just run the garbage collection more often
Last updated: Apr 18 2024 at 20:16 UTC