Skip to content

Performance test extensions and updates #2014

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
merged 5 commits into from
Jun 1, 2018
Merged

Performance test extensions and updates #2014

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
5 commits
Select commit Hold shift + click to select a range
f802d87
Support CaDiCaL in performance tests, remove redundant script
tautschnig Mar 31, 2018
afccaec
Provide goto-cc in performance tests
tautschnig Mar 31, 2018
1288ec7
perf-test: speed up builds just like e7bb127f0e3 did
tautschnig Mar 24, 2018
5b0395f
perf-test: Update Ubuntu AMI ids for latest version
tautschnig Apr 1, 2018
a47941d
perf-test: add -W/--witness-check to validate SV-COMP witness checking
tautschnig Apr 2, 2018
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
129 changes: 0 additions & 129 deletions scripts/perf-test/codebuild-glucose.yaml
View file
Open in desktop

This file was deleted.

16 changes: 8 additions & 8 deletions scripts/perf-test/codebuild.yaml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -62,9 +62,8 @@ Resources:
phases:
install:
commands:
- apt-get update -y
- apt-get install -y software-properties-common
- add-apt-repository ppa:ubuntu-toolchain-r/test
- echo "deb http://ppa.launchpad.net/ubuntu-toolchain-r/test/ubuntu trusty main" > /etc/apt/sources.list.d/toolchain.list
- apt-key adv --keyserver keyserver.ubuntu.com --recv-keys BA9EF27F
- apt-get update -y
- apt-get install -y libwww-perl g++-5 flex bison git openjdk-7-jdk
- update-alternatives --install /usr/bin/gcc gcc /usr/bin/gcc-5 1
Expand All @@ -74,11 +73,12 @@ Resources:
- echo ${Repository} > COMMIT_INFO
- git rev-parse --short HEAD >> COMMIT_INFO
- git log HEAD^..HEAD >> COMMIT_INFO
- make -C src minisat2-download glucose-download
- make -C src minisat2-download glucose-download cadical-download
- make -C src -j8
artifacts:
files:
- src/cbmc/cbmc
- src/goto-cc/goto-cc
- COMMIT_INFO
discard-paths: yes
Type: !Ref RepoType
Expand All @@ -104,9 +104,8 @@ Resources:
phases:
install:
commands:
- apt-get update -y
- apt-get install -y software-properties-common
- add-apt-repository ppa:ubuntu-toolchain-r/test
- echo "deb http://ppa.launchpad.net/ubuntu-toolchain-r/test/ubuntu trusty main" > /etc/apt/sources.list.d/toolchain.list
- apt-key adv --keyserver keyserver.ubuntu.com --recv-keys BA9EF27F
- apt-get update -y
- apt-get install -y libwww-perl g++-5 flex bison git openjdk-7-jdk
- update-alternatives --install /usr/bin/gcc gcc /usr/bin/gcc-5 1
Expand All @@ -116,11 +115,12 @@ Resources:
- echo ${Repository} > COMMIT_INFO
- git rev-parse --short HEAD >> COMMIT_INFO
- git log HEAD^..HEAD >> COMMIT_INFO
- make -C src minisat2-download glucose-download
- make -C src minisat2-download glucose-download cadical-download
- make -C src -j8 CXXFLAGS="-O2 -pg -g -finline-limit=4" LINKFLAGS="-pg"
artifacts:
files:
- src/cbmc/cbmc
- src/goto-cc/goto-cc
- COMMIT_INFO
discard-paths: yes
Type: !Ref RepoType
Expand Down
2 changes: 2 additions & 0 deletions scripts/perf-test/ebs.yaml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -36,6 +36,8 @@ Resources:
https://github.com/sosy-lab/cpachecker.git
git clone --depth 1 \
https://github.com/diffblue/cprover-sv-comp.git
git clone --depth 1 \
https://github.com/tautschnig/fshell-w2t.git
halt

BaseVolume:
Expand Down
81 changes: 73 additions & 8 deletions scripts/perf-test/ec2.yaml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -38,6 +38,9 @@ Parameters:
SSHKeyName:
Type: String

WitnessCheck:
Type: String

Conditions:
UseSpot: !Not [!Equals [!Ref MaxPrice, ""]]

Expand Down Expand Up @@ -153,6 +156,7 @@ Resources:
apt-get install -y git time wget binutils awscli make jq
apt-get install -y zip unzip
apt-get install -y gcc libc6-dev-i386
apt-get install -y ant python3-tempita python

# cgroup set up for benchexec
chmod o+wt '/sys/fs/cgroup/cpuset/'
Expand Down Expand Up @@ -212,7 +216,7 @@ Resources:
cd /mnt
cd cprover-sv-comp
git pull
mkdir -p src/cbmc/
mkdir -p src/cbmc src/goto-cc
touch LICENSE
cd ..
mkdir -p run
Expand All @@ -223,6 +227,27 @@ Resources:
mkdir -p tmp
export TMPDIR=/mnt/tmp

if [ x${WitnessCheck} = xTrue ]
then
cd cpachecker
ant

cd ../run
for def in \
cpa-seq-validate-correctness-witnesses \
cpa-seq-validate-violation-witnesses \
fshell-witness2test-validate-violation-witnesses
do
wget -O $def.xml https://raw.githubusercontent.com/sosy-lab/sv-comp/master/benchmark-defs/$def.xml
sed -i 's#[\./]*/results-verified/LOGDIR/sv-comp18.\${!inputfile_name}.files/witness.graphml#witnesses/sv-comp18.${!inputfile_name}-witness.graphml#' $def.xml
done

ln -s ../cpachecker/scripts/cpa.sh cpa.sh
ln -s ../cpachecker/config/ config

cp ../fshell-w2t/* .
fi

# reduce the likelihood of multiple hosts processing the
# same message (in addition to SQS's message hiding)
sleep $(expr $RANDOM % 30)
Expand Down Expand Up @@ -292,10 +317,12 @@ Resources:
--receipt-handle $msg

cd /mnt/cprover-sv-comp
rm -f src/cbmc/cbmc
rm -f src/cbmc/cbmc src/goto-cc/goto-cc
aws s3 cp s3://${S3Bucket}/${PerfTestId}/$cfg/cbmc \
src/cbmc/cbmc
chmod a+x src/cbmc/cbmc
aws s3 cp s3://${S3Bucket}/${PerfTestId}/$cfg/goto-cc \
src/goto-cc/goto-cc
chmod a+x src/cbmc/cbmc src/goto-cc/goto-cc
make CBMC=. cbmc.zip
cd ../run
unzip ../cprover-sv-comp/cbmc.zip
Expand Down Expand Up @@ -332,11 +359,26 @@ Resources:
tar czf witnesses.tar.gz cbmc.*.logfiles
rm -rf cbmc.*.logfiles
cd ..

if [ x${WitnessCheck} = xTrue ]
then
for wc in *-witnesses.xml
do
wcp=$(echo $wc | sed 's/-witnesses.xml$//')
mkdir witnesses
tar -C witnesses --strip-components=1 -xzf \
logs-$t/witnesses.tar.gz
../benchexec/bin/benchexec --no-container \
$wc --task $t -T 90s -M 15GB \
-o $wcp-logs-$t/ -N $max_par -c 1
rm -rf witnesses
done
fi
fi
if [ -f logs-$t/*.xml.bz2 ]
then
start_date="$(echo ${PerfTestId} | cut -f1-3 -d-) $(echo ${PerfTestId} | cut -f4-6 -d- | sed 's/-/:/g')"
cd logs-$t
start_date="$(echo ${PerfTestId} | cut -f1-3 -d-) $(echo ${PerfTestId} | cut -f4-6 -d- | sed 's/-/:/g')"
for l in *logs-$t/*.xml.bz2
do
cd $(dirname $l)
bunzip2 *.xml.bz2
perl -p -i -e \
"s/^(<result.*version=\"[^\"]*)/\$1:${PerfTestId}/" *.xml
Expand All @@ -346,22 +388,45 @@ Resources:
"s/^(<result.*date=)\"[^\"]*/\$1\"$start_date/" *.xml
bzip2 *.xml
cd ..
done

if [ x${WitnessCheck} = xTrue ]
then
../benchexec/bin/table-generator \
logs-$t/*xml.bz2 *-logs-$t/*.xml.bz2 -o logs-$t/
else
../benchexec/bin/table-generator \
logs-$t/*xml.bz2 -o logs-$t/
fi
aws s3 cp logs-$t \
s3://${S3Bucket}/${PerfTestId}/$cfg/logs-$t/ \
--recursive
for wc in *-witnesses.xml
do
[ -s $wc ] || break
wcp=$(echo $wc | sed 's/-witnesses.xml$//')
rm -rf $wcp-logs-$t/*.logfiles
aws s3 cp $wcp-logs-$t \
s3://${S3Bucket}/${PerfTestId}/$cfg/$wcp-logs-$t/ \
--recursive
done
else
rm -f gmon.sum gmon.out *.gmon.out.*
../benchexec/bin/benchexec cbmc.xml --no-container \
--task $t -T 600s -M 7GB -o logs-$t/ \
-N $max_par -c 1
if ls *.gmon.out.* >/dev/null 2>&1
then
gprof --sum ./cbmc-binary *.gmon.out.*
gprof --sum ./cbmc-binary cbmc*.gmon.out.*
gprof ./cbmc-binary gmon.sum > sum.profile-$t
rm -f gmon.sum
gprof --sum ./goto-cc goto-cc*.gmon.out.*
gprof ./goto-cc gmon.sum > sum.goto-cc-profile-$t
rm -f gmon.sum gmon.out *.gmon.out.*
aws s3 cp sum.profile-$t \
s3://${S3Bucket}/${PerfTestId}/$cfg/sum.profile-$t
aws s3 cp sum.goto-cc-profile-$t \
s3://${S3Bucket}/${PerfTestId}/$cfg/sum.goto-cc-profile-$t
fi
fi
rm -rf logs-$t sum.profile-$t
Expand Down
Loading