Skip to content

Commit c62b957

Browse files
tautschnigtautschnig
authored
Merge pull request diffblue#1551 from tautschnig/perf-test-improvements
Improvements to perf-test(.py)
2 parents 1dfb5cd + 03095d4 commit c62b957

File tree

5 files changed

+230
-12
lines changed

5 files changed

+230
-12
lines changed

‎scripts/perf-test/codebuild-glucose.yaml

Lines changed: 129 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,129 @@
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+
- sed -i 's/-Wno-error=misleading-indentation//' src/config.inc
79+
- make -C src -j8
80+
artifacts:
81+
files:
82+
- src/cbmc/cbmc
83+
- COMMIT_INFO
84+
discard-paths: yes
85+
Type: !Ref RepoType
86+
Location: !Ref Repository
87+
88+
ProfilingBuild:
89+
Type: "AWS::CodeBuild::Project"
90+
Properties:
91+
Artifacts:
92+
Type: S3
93+
Location: !Ref S3Bucket
94+
Path: !Ref PerfTestId
95+
Name: profiling
96+
Environment:
97+
ComputeType: BUILD_GENERAL1_LARGE
98+
Image: aws/codebuild/ubuntu-base:14.04
99+
Type: LINUX_CONTAINER
100+
Name: !Sub "perf-test-profiling-build-${PerfTestId}"
101+
ServiceRole: !Ref CodeBuildRole
102+
Source:
103+
BuildSpec: !Sub |
104+
version: 0.2
105+
phases:
106+
install:
107+
commands:
108+
- apt-get update -y
109+
- apt-get install -y software-properties-common
110+
- add-apt-repository ppa:ubuntu-toolchain-r/test
111+
- apt-get update -y
112+
- apt-get install -y libwww-perl g++-5 flex bison git
113+
- update-alternatives --install /usr/bin/gcc gcc /usr/bin/gcc-5 1
114+
- update-alternatives --install /usr/bin/g++ g++ /usr/bin/g++-5 1
115+
build:
116+
commands:
117+
- echo ${Repository} > COMMIT_INFO
118+
- git rev-parse --short HEAD >> COMMIT_INFO
119+
- git log HEAD^..HEAD >> COMMIT_INFO
120+
- make -C src minisat2-download glucose-download
121+
- sed -i 's/-Wno-error=misleading-indentation//' src/config.inc
122+
- make -C src -j8 CXXFLAGS="-O2 -pg -g -finline-limit=4" LINKFLAGS="-pg"
123+
artifacts:
124+
files:
125+
- src/cbmc/cbmc
126+
- COMMIT_INFO
127+
discard-paths: yes
128+
Type: !Ref RepoType
129+
Location: !Ref Repository

‎scripts/perf-test/ebs.yaml

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -28,7 +28,7 @@ Resources:
2828
apt-get -y update
2929
apt-get install git
3030
cd /mnt
31-
git clone --depth 1 --branch svcomp17 \
31+
git clone --depth 1 --branch svcomp18 \
3232
https://github.com/sosy-lab/sv-benchmarks.git
3333
git clone --depth 1 \
3434
https://github.com/sosy-lab/benchexec.git

‎scripts/perf-test/ec2.yaml

Lines changed: 12 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -151,6 +151,7 @@ Resources:
151151
# install packages
152152
apt-get -y update
153153
apt-get install -y git time wget binutils awscli make jq
154+
apt-get install -y zip unzip
154155
apt-get install -y gcc libc6-dev-i386
155156

156157
# cgroup set up for benchexec
@@ -203,9 +204,14 @@ Resources:
203204
update-rc.d ec2-terminate defaults
204205
systemctl start ec2-terminate
205206

207+
# update benchexec
208+
cd /mnt/benchexec
209+
git pull
210+
206211
# prepare for tool packaging
207212
cd /mnt
208213
cd cprover-sv-comp
214+
git pull
209215
mkdir -p src/cbmc/
210216
touch LICENSE
211217
cd ..
@@ -290,10 +296,13 @@ Resources:
290296
aws s3 cp s3://${S3Bucket}/${PerfTestId}/$cfg/cbmc \
291297
src/cbmc/cbmc
292298
chmod a+x src/cbmc/cbmc
293-
make CBMC=. YEAR=N CBMC-sv-comp-N.tar.gz
299+
make CBMC=. cbmc.zip
294300
cd ../run
295-
tar xzf ../cprover-sv-comp/CBMC-sv-comp-N.tar.gz
296-
rm ../cprover-sv-comp/CBMC-sv-comp-N.tar.gz
301+
unzip ../cprover-sv-comp/cbmc.zip
302+
mv cbmc cbmc-zip
303+
mv cbmc-zip/* .
304+
rmdir cbmc-zip
305+
rm ../cprover-sv-comp/cbmc.zip
297306

298307
date
299308
echo "Task: $t"

‎scripts/perf-test/make-tables.sh

Lines changed: 72 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,72 @@
1+
#!/bin/bash
2+
3+
set -e
4+
5+
if [ -z "$BENCHEXEC" ]
6+
then
7+
# default path to benchexec is set to a value that works for me(TM)
8+
BENCHEXEC=~/Desktop/benchexec.git
9+
fi
10+
11+
categories=""
12+
13+
for d in "$@"
14+
do
15+
c=$(echo $d/release/logs-* | tr ' ' '\n' | sed 's/.*logs-//')
16+
categories=$(echo $categories $c | tr ' ' '\n' | sort | uniq)
17+
done
18+
19+
official_logs="
20+
2017-01-11_1131.results.sv-comp17.ConcurrencySafety-Main.xml.bz2
21+
2017-01-11_1020.results.sv-comp17.MemSafety-Arrays.xml.bz2.merged.xml.bz2
22+
2017-01-11_1020.results.sv-comp17.MemSafety-Heap.xml.bz2.merged.xml.bz2
23+
2017-01-11_1020.results.sv-comp17.MemSafety-LinkedLists.xml.bz2.merged.xml.bz2
24+
2017-01-11_1020.results.sv-comp17.MemSafety-Other.xml.bz2.merged.xml.bz2
25+
2017-01-11_1354.results.sv-comp17.Overflows-BitVectors.xml.bz2.merged.xml.bz2
26+
2017-01-11_1354.results.sv-comp17.Overflows-Other.xml.bz2.merged.xml.bz2
27+
2017-01-10_1721.results.sv-comp17.ReachSafety-Arrays.xml.bz2.merged.xml.bz2
28+
2017-01-10_1721.results.sv-comp17.ReachSafety-BitVectors.xml.bz2.merged.xml.bz2
29+
2017-01-10_1721.results.sv-comp17.ReachSafety-ControlFlow.xml.bz2.merged.xml.bz2
30+
2017-01-10_1721.results.sv-comp17.ReachSafety-ECA.xml.bz2.merged.xml.bz2
31+
2017-01-10_1721.results.sv-comp17.ReachSafety-Floats.xml.bz2.merged.xml.bz2
32+
2017-01-10_1721.results.sv-comp17.ReachSafety-Heap.xml.bz2.merged.xml.bz2
33+
2017-01-10_1721.results.sv-comp17.ReachSafety-Loops.xml.bz2.merged.xml.bz2
34+
2017-01-10_1721.results.sv-comp17.ReachSafety-ProductLines.xml.bz2.merged.xml.bz2
35+
2017-01-10_1721.results.sv-comp17.ReachSafety-Recursive.xml.bz2.merged.xml.bz2
36+
2017-01-10_1721.results.sv-comp17.ReachSafety-Sequentialized.xml.bz2.merged.xml.bz2
37+
2017-01-11_1020.results.sv-comp17.Systems_BusyBox_MemSafety.xml.bz2.merged.xml.bz2
38+
2017-01-10_1721.results.sv-comp17.Systems_DeviceDriversLinux64_ReachSafety.xml.bz2.merged.xml.bz2
39+
"
40+
41+
for c in $categories
42+
do
43+
if [ ! -s official-sv-comp-17/*$c*.xml.bz2 ]
44+
then
45+
suffix=$(echo $official_logs | tr ' ' '\n' | grep "sv-comp17\.$c\.xml\.bz2" || true)
46+
if [ -z "$suffix" ]
47+
then
48+
echo "No log known for $c"
49+
srcs=""
50+
else
51+
wget \
52+
http://sv-comp.sosy-lab.org/2017/results/results-verified/cbmc.$suffix \
53+
-P official-sv-comp-17/
54+
srcs="official-sv-comp-17/*$c*.xml.bz2"
55+
fi
56+
else
57+
srcs="official-sv-comp-17/*$c*.xml.bz2"
58+
fi
59+
60+
for d in "$@"
61+
do
62+
if [ -s $d/release/logs-$c/*.bz2 ]
63+
then
64+
srcs="$srcs $d/release/logs-$c/*.bz2"
65+
fi
66+
done
67+
68+
if [ -n "$srcs" ]
69+
then
70+
python3 $BENCHEXEC/bin/table-generator -n $c $srcs
71+
fi
72+
done

‎scripts/perf-test/perf_test.py

Lines changed: 16 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -66,14 +66,19 @@ def parse_args():
6666
parser.add_argument('-T', '--tasks', type=str,
6767
default='quick',
6868
help='Subset of tasks to run (quick, full; ' +
69-
'default: quick; or name of SV-COMP task)')
69+
'default: quick; or regex of SV-COMP task(s))')
70+
parser.add_argument('-B', '--code-build', type=str,
71+
default=same_dir('codebuild.yaml'),
72+
help='Non-default CodeBuild template to use')
7073

7174
args = parser.parse_args()
75+
7276
assert(args.repository.startswith('https://github.com/') or
7377
args.repository.startswith('https://git-codecommit.'))
7478
assert(not args.ssh_key or args.ssh_key_name)
7579
if args.ssh_key:
7680
assert(os.path.isfile(args.ssh_key))
81+
assert(os.path.isfile(args.code_build))
7782

7883
return args
7984

@@ -345,7 +350,8 @@ def prepare_ebs(session, region, az, ami):
345350
return snapshots['Snapshots'][0]['SnapshotId']
346351

347352

348-
def build(session, repository, commit_id, bucket_name, perf_test_id):
353+
def build(session, repository, commit_id, bucket_name, perf_test_id,
354+
codebuild_file):
349355
# build the chosen commit in CodeBuild
350356
logger = logging.getLogger('perf_test')
351357

@@ -356,7 +362,7 @@ def build(session, repository, commit_id, bucket_name, perf_test_id):
356362

357363
cfn = session.resource('cloudformation', region_name='us-east-1')
358364
stack_name = 'perf-test-codebuild-' + perf_test_id
359-
with open(same_dir('codebuild.yaml')) as f:
365+
with open(codebuild_file) as f:
360366
CFN_codebuild = f.read()
361367
stack = cfn.create_stack(
362368
StackName=stack_name,
@@ -479,10 +485,8 @@ def seed_queue(session, region, queue, task_set):
479485
elif task_set == 'quick':
480486
tasks = ['ReachSafety-Loops', 'ReachSafety-BitVectors']
481487
else:
482-
tasks = [task_set]
483-
484-
for t in tasks:
485-
assert(t in set(all_tasks))
488+
tasks = [t for t in all_tasks if re.match('^' + task_set + '$', t)]
489+
assert(tasks)
486490

487491
for t in tasks:
488492
response = queue.send_messages(
@@ -492,6 +496,9 @@ def seed_queue(session, region, queue, task_set):
492496
])
493497
assert(not response.get('Failed'))
494498

499+
logger.info(region + ': SQS queue seeded with {} jobs'.format(
500+
len(tasks) * 2))
501+
495502

496503
def run_perf_test(
497504
session, mode, region, az, ami, instance_type, sqs_arn, sqs_url,
@@ -568,6 +575,7 @@ def run_perf_test(
568575
],
569576
Capabilities=['CAPABILITY_NAMED_IAM'])
570577

578+
logger.info(region + ': Waiting for completition of ' + stack_name)
571579
waiter = cfn.meta.client.get_waiter('stack_create_complete')
572580
waiter.wait(StackName=stack_name)
573581
asg_name = stack.outputs[0]['OutputValue']
@@ -642,7 +650,7 @@ def main():
642650
session2 = boto3.session.Session()
643651
build_future = e.submit(
644652
build, session2, args.repository, args.commit_id, bucket_name,
645-
perf_test_id)
653+
perf_test_id, args.code_build)
646654
session3 = boto3.session.Session()
647655
ebs_future = e.submit(prepare_ebs, session3, region, az, ami)
648656
session4 = boto3.session.Session()

0 commit comments

Comments
 (0)