Skip to content

Commit dc56844

Browse files
committed
Update SV-COMP performance testing tool to 2020/2021
- Use EC2 instead of CodeBuild to avoid Docker throttling. - Use a VPC for compatibility with current EC2 spot offerings. - Use capacity-optimized as spot allocation strategy. - Add profiling using Linux perf as gprof doesn't seem to be working anymore.
1 parent 0ea7f13 commit dc56844

File tree

6 files changed

+515
-346
lines changed

6 files changed

+515
-346
lines changed

scripts/perf-test/build.yaml

Lines changed: 184 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,184 @@
1+
---
2+
AWSTemplateFormatVersion: 2010-09-09
3+
4+
Parameters:
5+
Ami:
6+
Type: String
7+
8+
S3Bucket:
9+
Type: String
10+
11+
PerfTestId:
12+
Type: String
13+
14+
Repository:
15+
Type: String
16+
17+
CommitId:
18+
Type: String
19+
20+
UsePerf:
21+
Type: String
22+
23+
Resources:
24+
EC2Role:
25+
Type: "AWS::IAM::Role"
26+
Properties:
27+
AssumeRolePolicyDocument:
28+
Version: 2012-10-17
29+
Statement:
30+
Effect: Allow
31+
Principal:
32+
Service: ec2.amazonaws.com
33+
Action: "sts:AssumeRole"
34+
RoleName: !Sub "BR-${PerfTestId}"
35+
Policies:
36+
- PolicyName: !Sub "BP-${PerfTestId}"
37+
PolicyDocument:
38+
Version: 2012-10-17
39+
Statement:
40+
- Action:
41+
- "s3:PutObject"
42+
- "s3:GetObject"
43+
Effect: Allow
44+
Resource: !Join ["/", [!Sub "arn:aws:s3:::${S3Bucket}", "*"]]
45+
- Action:
46+
- "s3:ListBucket"
47+
Effect: Allow
48+
Resource: !Sub "arn:aws:s3:::${S3Bucket}"
49+
50+
EC2InstanceProfile:
51+
Type: "AWS::IAM::InstanceProfile"
52+
Properties:
53+
Roles:
54+
- !Ref EC2Role
55+
56+
ReleaseInstance:
57+
Type: "AWS::EC2::Instance"
58+
Properties:
59+
InstanceType: c5.2xlarge
60+
ImageId: !Ref Ami
61+
IamInstanceProfile: !Ref EC2InstanceProfile
62+
BlockDeviceMappings:
63+
- DeviceName: /dev/xvda
64+
Ebs:
65+
VolumeType: gp2
66+
VolumeSize: '30'
67+
DeleteOnTermination: 'true'
68+
UserData:
69+
Fn::Base64: !Sub |
70+
#!/bin/bash
71+
set -x -e
72+
73+
sed -i 's#/archive.ubuntu.com#/${AWS::Region}.ec2.archive.ubuntu.com#g' /etc/apt/sources.list
74+
export DEBIAN_FRONTEND=noninteractive
75+
apt-get update
76+
apt-get install -y awscli
77+
78+
# AWS Sig-v4 access
79+
aws configure set s3.signature_version s3v4
80+
81+
aws s3 cp s3://${S3Bucket}/ec2-terminate.sh /etc/init.d/ec2-terminate
82+
sed -i '25,31d' /etc/init.d/ec2-terminate
83+
sed -i 's/#S3BUCKET#/${S3Bucket}/g' /etc/init.d/ec2-terminate
84+
sed -i 's/#PERFTESTID#/${PerfTestId}/g' /etc/init.d/ec2-terminate
85+
chmod a+x /etc/init.d/ec2-terminate
86+
update-rc.d ec2-terminate defaults
87+
systemctl start ec2-terminate
88+
89+
trap poweroff EXIT
90+
91+
apt-get install -y build-essential flex bison git curl ccache zip
92+
93+
cd /root/
94+
aws s3 cp s3://${S3Bucket}/release-build-cache/ccache.zip ccache.zip || true
95+
unzip ccache.zip || true
96+
rm -f ccache.zip
97+
ccache -z --max-size=1G
98+
git clone --depth 3 --branch ${CommitId} ${Repository} cbmc.git
99+
cd cbmc.git
100+
echo ${Repository} > COMMIT_INFO
101+
git rev-parse --short HEAD >> COMMIT_INFO
102+
git log HEAD^..HEAD >> COMMIT_INFO
103+
make -C src minisat2-download glucose-download cadical-download
104+
export CCACHE_NOHASHDIR=1
105+
make -C src CXX="ccache g++" -j8
106+
ccache -s
107+
108+
aws s3 cp src/cbmc/cbmc s3://${S3Bucket}/${PerfTestId}/release/cbmc
109+
aws s3 cp src/goto-cc/goto-cc s3://${S3Bucket}/${PerfTestId}/release/goto-cc
110+
aws s3 cp COMMIT_INFO s3://${S3Bucket}/${PerfTestId}/release/COMMIT_INFO
111+
cd /root/
112+
zip -r ccache.zip .ccache
113+
aws s3 cp ccache.zip s3://${S3Bucket}/release-build-cache/ccache.zip
114+
115+
ProfilingInstance:
116+
Type: "AWS::EC2::Instance"
117+
Properties:
118+
InstanceType: c5.2xlarge
119+
ImageId: !Ref Ami
120+
IamInstanceProfile: !Ref EC2InstanceProfile
121+
BlockDeviceMappings:
122+
- DeviceName: /dev/xvda
123+
Ebs:
124+
VolumeType: gp2
125+
VolumeSize: '30'
126+
DeleteOnTermination: 'true'
127+
UserData:
128+
Fn::Base64: !Sub |
129+
#!/bin/bash
130+
set -x -e
131+
132+
sed -i 's#/archive.ubuntu.com#/${AWS::Region}.ec2.archive.ubuntu.com#g' /etc/apt/sources.list
133+
export DEBIAN_FRONTEND=noninteractive
134+
apt-get update
135+
apt-get install -y awscli
136+
137+
# AWS Sig-v4 access
138+
aws configure set s3.signature_version s3v4
139+
140+
aws s3 cp s3://${S3Bucket}/ec2-terminate.sh /etc/init.d/ec2-terminate
141+
sed -i '25,31d' /etc/init.d/ec2-terminate
142+
sed -i 's/#S3BUCKET#/${S3Bucket}/g' /etc/init.d/ec2-terminate
143+
sed -i 's/#PERFTESTID#/${PerfTestId}/g' /etc/init.d/ec2-terminate
144+
chmod a+x /etc/init.d/ec2-terminate
145+
update-rc.d ec2-terminate defaults
146+
systemctl start ec2-terminate
147+
148+
trap poweroff EXIT
149+
150+
apt-get install -y build-essential flex bison git curl ccache zip
151+
152+
cd /root/
153+
aws s3 cp s3://${S3Bucket}/profiling-build-cache/ccache.zip ccache.zip || true
154+
unzip ccache.zip || true
155+
rm -f ccache.zip
156+
ccache -z --max-size=1G
157+
git clone --depth 3 --branch ${CommitId} ${Repository} cbmc.git
158+
cd cbmc.git
159+
echo ${Repository} > COMMIT_INFO
160+
git rev-parse --short HEAD >> COMMIT_INFO
161+
git log HEAD^..HEAD >> COMMIT_INFO
162+
make -C src minisat2-download glucose-download cadical-download
163+
export CCACHE_NOHASHDIR=1
164+
if [ x${UsePerf} = xTrue ]
165+
then
166+
make -C src CXX="ccache g++" -j8 CXXFLAGS="-O2 -g -Wno-deprecated -fno-omit-frame-pointer"
167+
else
168+
make -C src CXX="ccache g++" -j8 CXXFLAGS="-O2 -pg -g -finline-limit=4 -Wno-deprecated" LINKFLAGS="-pg"
169+
fi
170+
ccache -s
171+
172+
aws s3 cp src/cbmc/cbmc s3://${S3Bucket}/${PerfTestId}/profiling/cbmc
173+
aws s3 cp src/goto-cc/goto-cc s3://${S3Bucket}/${PerfTestId}/profiling/goto-cc
174+
aws s3 cp COMMIT_INFO s3://${S3Bucket}/${PerfTestId}/profiling/COMMIT_INFO
175+
cd /root/
176+
df -h
177+
zip -r ccache.zip .ccache
178+
aws s3 cp ccache.zip s3://${S3Bucket}/profiling-build-cache/ccache.zip
179+
180+
Outputs:
181+
ReleaseInstanceId:
182+
Value: !Ref ReleaseInstance
183+
ProfilingInstanceId:
184+
Value: !Ref ProfilingInstance

scripts/perf-test/codebuild.yaml

Lines changed: 0 additions & 172 deletions
This file was deleted.

0 commit comments

Comments
 (0)