Skip to content
This repository was archived by the owner on Aug 20, 2021. It is now read-only.

prove-all: configurable memory headroom #409

Open
d-xo wants to merge 4 commits into
base: master
Choose a base branch
from
Open

prove-all: configurable memory headroom #409

Changes from all commits
Commits
Show all changes
4 commits
Select commit Hold shift + click to select a range
3296e3a
prove-all: configurable memory headroom
d-xo Apr 21, 2020
b8c1ad5
libexec/klab-prove-all: quotes for MEMORY_HEADROOM
xwvvvvwx Apr 21, 2020
c0e8b68
libexec/klab-prove-all: rm superflous export
xwvvvvwx Apr 21, 2020
504eb74
libexec/klab-prove-all: default MEMORY_HEADROOM to 4G
d-xo Apr 21, 2020
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
3 changes: 2 additions & 1 deletion libexec/klab-prove-all
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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}
MEMORY_HEADROOM=${MEMORY_HEADROOM:-4G}
PNAME=$(jq -r '.name' < config.json)
if [ "$PNAME" == "null" ]; then PNAME=""; fi
export PNAME
Expand Down Expand Up @@ -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
Expand Down