Skip to content

Commit 021fe8f

Browse files
author
Daniel Kroening
authored
Merge pull request diffblue#1492 from tautschnig/perf-test
Script to automate performance evaluation of CBMC on AWS
2 parents 0729e3d + c3e6726 commit 021fe8f

File tree

7 files changed

+1335
-0
lines changed

7 files changed

+1335
-0
lines changed

‎scripts/perf-test/codebuild.yaml

Lines changed: 127 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,127 @@
1+
---
2+
AWSTemplateFormatVersion: 2010-09-09
3+
4+
Parameters:
5+
S3Bucket:
6+
Type: String
7+
8+
PerfTestId:
9+
Type: String
10+
11+
RepoType:
12+
Type: String
13+
14+
Repository:
15+
Type: String
16+
17+
Resources:
18+
CodeBuildRole:
19+
Type: "AWS::IAM::Role"
20+
Properties:
21+
AssumeRolePolicyDocument:
22+
Version: 2012-10-17
23+
Statement:
24+
Effect: Allow
25+
Principal:
26+
Service: codebuild.amazonaws.com
27+
Action: "sts:AssumeRole"
28+
RoleName: !Sub "CR-${PerfTestId}"
29+
Policies:
30+
- PolicyName: !Sub "CP-${PerfTestId}"
31+
PolicyDocument:
32+
Version: 2012-10-17
33+
Statement:
34+
- Action:
35+
- "s3:PutObject"
36+
Effect: Allow
37+
Resource: !Join ["/", [!Sub "arn:aws:s3:::${S3Bucket}", "*"]]
38+
- Action:
39+
- "logs:CreateLogGroup"
40+
- "logs:CreateLogStream"
41+
- "logs:PutLogEvents"
42+
Effect: Allow
43+
Resource: !Sub 'arn:aws:logs:${AWS::Region}:${AWS::AccountId}:log-group:/aws/codebuild/*'
44+
45+
ReleaseBuild:
46+
Type: "AWS::CodeBuild::Project"
47+
Properties:
48+
Artifacts:
49+
Type: S3
50+
Location: !Ref S3Bucket
51+
Path: !Ref PerfTestId
52+
Name: release
53+
Environment:
54+
ComputeType: BUILD_GENERAL1_LARGE
55+
Image: aws/codebuild/ubuntu-base:14.04
56+
Type: LINUX_CONTAINER
57+
Name: !Sub "perf-test-release-build-${PerfTestId}"
58+
ServiceRole: !Ref CodeBuildRole
59+
Source:
60+
BuildSpec: !Sub |
61+
version: 0.2
62+
phases:
63+
install:
64+
commands:
65+
- apt-get update -y
66+
- apt-get install -y software-properties-common
67+
- add-apt-repository ppa:ubuntu-toolchain-r/test
68+
- apt-get update -y
69+
- apt-get install -y libwww-perl g++-5 flex bison git
70+
- update-alternatives --install /usr/bin/gcc gcc /usr/bin/gcc-5 1
71+
- update-alternatives --install /usr/bin/g++ g++ /usr/bin/g++-5 1
72+
build:
73+
commands:
74+
- echo ${Repository} > COMMIT_INFO
75+
- git rev-parse --short HEAD >> COMMIT_INFO
76+
- git log HEAD^..HEAD >> COMMIT_INFO
77+
- make -C src minisat2-download glucose-download
78+
- make -C src -j8
79+
artifacts:
80+
files:
81+
- src/cbmc/cbmc
82+
- COMMIT_INFO
83+
discard-paths: yes
84+
Type: !Ref RepoType
85+
Location: !Ref Repository
86+
87+
ProfilingBuild:
88+
Type: "AWS::CodeBuild::Project"
89+
Properties:
90+
Artifacts:
91+
Type: S3
92+
Location: !Ref S3Bucket
93+
Path: !Ref PerfTestId
94+
Name: profiling
95+
Environment:
96+
ComputeType: BUILD_GENERAL1_LARGE
97+
Image: aws/codebuild/ubuntu-base:14.04
98+
Type: LINUX_CONTAINER
99+
Name: !Sub "perf-test-profiling-build-${PerfTestId}"
100+
ServiceRole: !Ref CodeBuildRole
101+
Source:
102+
BuildSpec: !Sub |
103+
version: 0.2
104+
phases:
105+
install:
106+
commands:
107+
- apt-get update -y
108+
- apt-get install -y software-properties-common
109+
- add-apt-repository ppa:ubuntu-toolchain-r/test
110+
- apt-get update -y
111+
- apt-get install -y libwww-perl g++-5 flex bison git
112+
- update-alternatives --install /usr/bin/gcc gcc /usr/bin/gcc-5 1
113+
- update-alternatives --install /usr/bin/g++ g++ /usr/bin/g++-5 1
114+
build:
115+
commands:
116+
- echo ${Repository} > COMMIT_INFO
117+
- git rev-parse --short HEAD >> COMMIT_INFO
118+
- git log HEAD^..HEAD >> COMMIT_INFO
119+
- make -C src minisat2-download glucose-download
120+
- make -C src -j8 CXXFLAGS="-O2 -pg -g -finline-limit=4" LINKFLAGS="-pg"
121+
artifacts:
122+
files:
123+
- src/cbmc/cbmc
124+
- COMMIT_INFO
125+
discard-paths: yes
126+
Type: !Ref RepoType
127+
Location: !Ref Repository

‎scripts/perf-test/ebs.yaml

Lines changed: 53 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,53 @@
1+
---
2+
AWSTemplateFormatVersion: 2010-09-09
3+
4+
Parameters:
5+
Ami:
6+
Type: String
7+
8+
AvailabilityZone:
9+
Type: String
10+
11+
Resources:
12+
EC2Instance:
13+
Type: "AWS::EC2::Instance"
14+
Properties:
15+
InstanceType: t2.micro
16+
ImageId: !Ref Ami
17+
AvailabilityZone: !Ref AvailabilityZone
18+
Volumes:
19+
- Device: "/dev/sdf"
20+
VolumeId: !Ref BaseVolume
21+
UserData: !Base64 |
22+
#!/bin/bash
23+
set -e
24+
# wait to make sure volume is available
25+
sleep 10
26+
mkfs.ext4 /dev/xvdf
27+
mount /dev/xvdf /mnt
28+
apt-get -y update
29+
apt-get install git
30+
cd /mnt
31+
git clone --depth 1 --branch svcomp17 \
32+
https://github.com/sosy-lab/sv-benchmarks.git
33+
git clone --depth 1 \
34+
https://github.com/sosy-lab/benchexec.git
35+
git clone --depth 1 --branch trunk \
36+
https://github.com/sosy-lab/cpachecker.git
37+
git clone --depth 1 \
38+
https://github.com/diffblue/cprover-sv-comp.git
39+
halt
40+
41+
BaseVolume:
42+
Type: "AWS::EC2::Volume"
43+
DeletionPolicy: Snapshot
44+
Properties:
45+
AvailabilityZone: !Ref AvailabilityZone
46+
Size: 8
47+
Tags:
48+
- Key: Name
49+
Value: perf-test-base
50+
51+
Outputs:
52+
InstanceId:
53+
Value: !Ref EC2Instance

0 commit comments

Comments
 (0)