Script to automate performance evaluation of CBMC on AWS

Evaluation is performed for a chosen GitHub or CodeCommit repository and
commit/branch/tag by running (a subset of) SV-COMP benchmarks. Runs are
done both in optimised as well as in profiling mode.

Execution should be as simple as

  ./perf_test.py \
        -r https://github.com/diffblue/cbmc -c develop \
        -e [email protected]

assuming that AWS access keys are set up (as required for AWS cli use) and boto3
is installed. Emails will then be sent as results become available.

The script sets up (and persists) an S3 bucket for storing results, SNS
queues for email updates on the process, as well as an EBS snapshot
containing the benmarking data.

For each benchmarking run, builds are set up and performed via
CodeBuild. Evaluation is then performed using AutoScalingGroups
synchronised via SQS.

The design premise for this work was:

"Compare multiple configurations for performance, correctness, capabilities."

This was broken down into:

Configuration: target platform, timeout, memory limit, benchmark set, tool
options, source version (=repository + revision).

Compare: log files, counterexamples, CPU profile, memory profile, verification
results.

Author: tautschnig

scripts/perf-test/codebuild.yaml

@@ -0,0 +1,127 @@
+---
+AWSTemplateFormatVersion: 2010-09-09
+
+Parameters:
+    S3Bucket:
+        Type: String
+
+    PerfTestId:
+        Type: String
+
+    RepoType:
+        Type: String
+
+    Repository:
+        Type: String
+
+Resources:
+    CodeBuildRole:
+        Type: "AWS::IAM::Role"
+        Properties:
+            AssumeRolePolicyDocument:
+                Version: 2012-10-17
+                Statement:
+                    Effect: Allow
+                    Principal:
+                        Service: codebuild.amazonaws.com
+                    Action: "sts:AssumeRole"
+            RoleName: !Sub "CR-${PerfTestId}"
+            Policies:
+                - PolicyName: !Sub "CP-${PerfTestId}"
+                  PolicyDocument:
+                    Version: 2012-10-17
+                    Statement:
+                        - Action:
+                            - "s3:PutObject"
+                          Effect: Allow
+                          Resource: !Join ["/", [!Sub "arn:aws:s3:::${S3Bucket}", "*"]]
+                        - Action:
+                            - "logs:CreateLogGroup"
+                            - "logs:CreateLogStream"
+                            - "logs:PutLogEvents"
+                          Effect: Allow
+                          Resource: !Sub 'arn:aws:logs:${AWS::Region}:${AWS::AccountId}:log-group:/aws/codebuild/*'
+
+    ReleaseBuild:
+        Type: "AWS::CodeBuild::Project"
+        Properties:
+            Artifacts:
+                Type: S3
+                Location: !Ref S3Bucket
+                Path: !Ref PerfTestId
+                Name: release
+            Environment:
+                ComputeType: BUILD_GENERAL1_LARGE
+                Image: aws/codebuild/ubuntu-base:14.04
+                Type: LINUX_CONTAINER
+            Name: !Sub "perf-test-release-build-${PerfTestId}"
+            ServiceRole: !Ref CodeBuildRole
+            Source:
+                BuildSpec: !Sub |
+                    version: 0.2
+                    phases:
+                        install:
+                            commands:
+                                - apt-get update -y
+                                - apt-get install -y software-properties-common
+                                - add-apt-repository ppa:ubuntu-toolchain-r/test
+                                - apt-get update -y
+                                - apt-get install -y libwww-perl g++-5 flex bison git
+                                - update-alternatives --install /usr/bin/gcc gcc /usr/bin/gcc-5 1
+                                - update-alternatives --install /usr/bin/g++ g++ /usr/bin/g++-5 1
+                        build:
+                            commands:
+                                - 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 -j8
+                    artifacts:
+                        files:
+                            - src/cbmc/cbmc
+                            - COMMIT_INFO
+                        discard-paths: yes
+                Type: !Ref RepoType
+                Location: !Ref Repository
+
+    ProfilingBuild:
+        Type: "AWS::CodeBuild::Project"
+        Properties:
+            Artifacts:
+                Type: S3
+                Location: !Ref S3Bucket
+                Path: !Ref PerfTestId
+                Name: profiling
+            Environment:
+                ComputeType: BUILD_GENERAL1_LARGE
+                Image: aws/codebuild/ubuntu-base:14.04
+                Type: LINUX_CONTAINER
+            Name: !Sub "perf-test-profiling-build-${PerfTestId}"
+            ServiceRole: !Ref CodeBuildRole
+            Source:
+                BuildSpec: !Sub |
+                    version: 0.2
+                    phases:
+                        install:
+                            commands:
+                                - apt-get update -y
+                                - apt-get install -y software-properties-common
+                                - add-apt-repository ppa:ubuntu-toolchain-r/test
+                                - apt-get update -y
+                                - apt-get install -y libwww-perl g++-5 flex bison git
+                                - update-alternatives --install /usr/bin/gcc gcc /usr/bin/gcc-5 1
+                                - update-alternatives --install /usr/bin/g++ g++ /usr/bin/g++-5 1
+                        build:
+                            commands:
+                                - 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 -j8 CXXFLAGS="-O2 -pg -g -finline-limit=4" LINKFLAGS="-pg"
+                    artifacts:
+                        files:
+                            - src/cbmc/cbmc
+                            - COMMIT_INFO
+                        discard-paths: yes
+                Type: !Ref RepoType
+                Location: !Ref Repository

scripts/perf-test/ebs.yaml

@@ -0,0 +1,53 @@
+---
+AWSTemplateFormatVersion: 2010-09-09
+
+Parameters:
+    Ami:
+        Type: String
+
+    AvailabilityZone:
+        Type: String
+
+Resources:
+    EC2Instance:
+        Type: "AWS::EC2::Instance"
+        Properties:
+            InstanceType: t2.micro
+            ImageId: !Ref Ami
+            AvailabilityZone: !Ref AvailabilityZone
+            Volumes:
+                - Device: "/dev/sdf"
+                  VolumeId: !Ref BaseVolume
+            UserData: !Base64 |
+                #!/bin/bash
+                set -e
+                # wait to make sure volume is available
+                sleep 10
+                mkfs.ext4 /dev/xvdf
+                mount /dev/xvdf /mnt
+                apt-get -y update
+                apt-get install git
+                cd /mnt
+                git clone --depth 1 --branch svcomp17 \
+                        https://github.com/sosy-lab/sv-benchmarks.git
+                git clone --depth 1 \
+                        https://github.com/sosy-lab/benchexec.git
+                git clone --depth 1 --branch trunk \
+                        https://github.com/sosy-lab/cpachecker.git
+                git clone --depth 1 \
+                        https://github.com/diffblue/cprover-sv-comp.git
+                halt
+
+    BaseVolume:
+        Type: "AWS::EC2::Volume"
+        DeletionPolicy: Snapshot
+        Properties:
+            AvailabilityZone: !Ref AvailabilityZone
+            Size: 8
+            Tags:
+                - Key: Name
+                  Value: perf-test-base
+
+Outputs:
+    InstanceId:
+       Value: !Ref EC2Instance