Script to automate performance evaluation of CBMC on AWS

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