search

moves-rwth / storm

A Modern Probabilistic Model Checker
https://www.stormchecker.org
GNU General Public License v3.0
135 stars 74 forks source link

Sylvan: Better detection of thread count #495

Closed tquatmann closed 7 months ago

tquatmann commented 8 months ago

It seems that the automatic detection of the number of supported concurrent threads in Sylvan (or more specifically Lace) is not very accurate when it is restricted via, e.g., Docker or Slurm (more specifically, I think these are all using cgroups). This leads to slow execution of DD code and often requires to manually set the thread count using --sylvan:threads N.

When googling this, std::thread::hardware_concurency() pops up, but this also seems to yield the number of physical threads the hardware provides (and not the number of threads we can actually use). I haven't tested this, though.

incaseoftrouble commented 8 months ago

This should be possible by reading the file /sys/fs/cgroup/cpu.max (its contents are <cpu quota> <cpu period>. The period typically is 100000 (ms) and quota is how much cpu time per such a period the cgroup is allowed to get. So, <quota>/<period> should give the number of CPUs which are allowed to be used.

This can be checked by running docker run --cpus <n> -it debian cat /sys/fs/cgroup/cpu.max (--cpus is just a short-hand for setting period to 100000 and quota to n * 1000000)

NB: Without restrictions, <quota> can be max and it might be possible that the quota is set to more than the physical CPU count.