Skip to content

Commit

Permalink
Merge pull request #2014 from tautschnig/cadical-experiment
Browse files Browse the repository at this point in the history 
Performance test extensions and updates
  • Loading branch information
@tautschnig
tautschnig authored Jun 1, 2018
2 parents f50237b + a47941d commit 09b8cf7
Show file tree
Hide file tree
Showing 5 changed files with 107 additions and 162 deletions.
129 changes: 0 additions & 129 deletions scripts/perf-test/codebuild-glucose.yaml
View file

This file was deleted.

16 changes: 8 additions & 8 deletions scripts/perf-test/codebuild.yaml
View file
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
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
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

0 comments on commit 09b8cf7

Please sign in to comment.