From 3296e3a213fcd98d940e603c7acbc4d51841b3dc Mon Sep 17 00:00:00 2001 From: David Terry Date: Tue, 21 Apr 2020 11:40:59 +0200 Subject: [PATCH 1/4] prove-all: configurable memory headroom --- libexec/klab-prove-all | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/libexec/klab-prove-all b/libexec/klab-prove-all index 1d3249b9..7119e651 100755 --- a/libexec/klab-prove-all +++ b/libexec/klab-prove-all @@ -27,6 +27,7 @@ export RUNNING_DIR=$KLAB_OUT/meta/running export OBLIGATIONS=$KLAB_OUT/obligations.batch export BATCH_LIMIT=8 export THREADS=${THREADS:-2} +export MEMORY_HEADROOM=${MEMORY_HEADROOM:-2G} PNAME=$(jq -r '.name' < config.json) if [ "$PNAME" == "null" ]; then PNAME=""; fi export PNAME @@ -156,7 +157,7 @@ make_batch () { if [ -n "$KLAB_REPORT_PROJECT_DIR" ]; then cp -n "$KLAB_OUT"/specs/*.k "$KLAB_REPORT_NAME_DIR" fi; - parallel -u -P "$THREADS" do_proof {} < "$OBLIGATIONS" & parallel_id=$! + parallel -u --memfree $MEMORY_HEADROOM -P "$THREADS" do_proof {} < "$OBLIGATIONS" & parallel_id=$! trap 'echo "Trapped SIGTERM in klab-prove-all" && kill -s INT $parallel_id && exit 1' TERM trap 'echo "Trapped SIGINT in klab-prove-all" && kill -s INT $parallel_id && exit 1' INT wait $parallel_id From b8c1ad565dad4414d78553978728f710db6ae879 Mon Sep 17 00:00:00 2001 From: David Terry Date: Tue, 21 Apr 2020 15:25:18 +0200 Subject: [PATCH 2/4] libexec/klab-prove-all: quotes for MEMORY_HEADROOM Co-Authored-By: asymmetric --- libexec/klab-prove-all | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/libexec/klab-prove-all b/libexec/klab-prove-all index 7119e651..69adcfcc 100755 --- a/libexec/klab-prove-all +++ b/libexec/klab-prove-all @@ -157,7 +157,7 @@ make_batch () { if [ -n "$KLAB_REPORT_PROJECT_DIR" ]; then cp -n "$KLAB_OUT"/specs/*.k "$KLAB_REPORT_NAME_DIR" fi; - parallel -u --memfree $MEMORY_HEADROOM -P "$THREADS" do_proof {} < "$OBLIGATIONS" & parallel_id=$! + parallel -u --memfree "$MEMORY_HEADROOM" -P "$THREADS" do_proof {} < "$OBLIGATIONS" & parallel_id=$! trap 'echo "Trapped SIGTERM in klab-prove-all" && kill -s INT $parallel_id && exit 1' TERM trap 'echo "Trapped SIGINT in klab-prove-all" && kill -s INT $parallel_id && exit 1' INT wait $parallel_id From c0e8b68b02fab4c0929ea49900e7c7c352771383 Mon Sep 17 00:00:00 2001 From: David Terry Date: Tue, 21 Apr 2020 15:25:50 +0200 Subject: [PATCH 3/4] libexec/klab-prove-all: rm superflous export Co-Authored-By: asymmetric --- libexec/klab-prove-all | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/libexec/klab-prove-all b/libexec/klab-prove-all index 69adcfcc..0023e420 100755 --- a/libexec/klab-prove-all +++ b/libexec/klab-prove-all @@ -27,7 +27,7 @@ export RUNNING_DIR=$KLAB_OUT/meta/running export OBLIGATIONS=$KLAB_OUT/obligations.batch export BATCH_LIMIT=8 export THREADS=${THREADS:-2} -export MEMORY_HEADROOM=${MEMORY_HEADROOM:-2G} +MEMORY_HEADROOM=${MEMORY_HEADROOM:-2G} PNAME=$(jq -r '.name' < config.json) if [ "$PNAME" == "null" ]; then PNAME=""; fi export PNAME From 504eb74d9aaee68bc158e5f64adf28dcf718b274 Mon Sep 17 00:00:00 2001 From: David Terry Date: Tue, 21 Apr 2020 15:26:45 +0200 Subject: [PATCH 4/4] libexec/klab-prove-all: default MEMORY_HEADROOM to 4G --- libexec/klab-prove-all | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/libexec/klab-prove-all b/libexec/klab-prove-all index 0023e420..36b27aeb 100755 --- a/libexec/klab-prove-all +++ b/libexec/klab-prove-all @@ -27,7 +27,7 @@ export RUNNING_DIR=$KLAB_OUT/meta/running export OBLIGATIONS=$KLAB_OUT/obligations.batch export BATCH_LIMIT=8 export THREADS=${THREADS:-2} -MEMORY_HEADROOM=${MEMORY_HEADROOM:-2G} +MEMORY_HEADROOM=${MEMORY_HEADROOM:-4G} PNAME=$(jq -r '.name' < config.json) if [ "$PNAME" == "null" ]; then PNAME=""; fi export PNAME