build.sh spawns too many jobs

snu-sf / promising-coq

The Coq development of A Promising Semantics for Relaxed-Memory Concurrency

https://sf.snu.ac.kr/promise-concurrency/

MIT License

32 stars 5 forks source link

build.sh spawns too many jobs #5

Open Janno opened 7 years ago

Janno commented 7 years ago

Currently, make is called with -j, which will spawn as many jobs as there are parallel targets at any given time. On systems with (only) 4 CPUs, this leads to unnecessary contention from the ~8 jobs running simultaneously. Additionally, the memory usage far exceeds my modest 8GB of RAM.

I don't quite know how to make an optional -jN parameter work well with your build.sh setup. In any case, I think it would be safer to not use -j by default.

jeehoonkang commented 7 years ago

It would be better for build.sh to accept the num_jobs parameter, e.g. ./build.sh 3 spawns three parallel jobs. It will not be super-hard, though I don't have domain knowledge on shell scripting.. In the mean time you can copy-and-paste build.sh into build-single.sh and then edit it ;)