Improvements to perf-test(.py)

scripts/perf-test/codebuild-glucose.yaml

@@ -0,0 +1,129 @@
+---
+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
+                                - sed -i 's/-Wno-error=misleading-indentation//' src/config.inc
+                                - 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
+                                - sed -i 's/-Wno-error=misleading-indentation//' src/config.inc
+                                - 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

@@ -28,7 +28,7 @@ Resources:
                 apt-get -y update
                 apt-get install git
                 cd /mnt
-                git clone --depth 1 --branch svcomp17 \
+                git clone --depth 1 --branch svcomp18 \
                         https://github.com/sosy-lab/sv-benchmarks.git
                 git clone --depth 1 \
                         https://github.com/sosy-lab/benchexec.git

scripts/perf-test/ec2.yaml

@@ -151,6 +151,7 @@ Resources:
                     # install packages
                     apt-get -y update
                     apt-get install -y git time wget binutils awscli make jq
+                    apt-get install -y zip unzip
                     apt-get install -y gcc libc6-dev-i386
 
                     # cgroup set up for benchexec
@@ -203,9 +204,14 @@ Resources:
                     update-rc.d ec2-terminate defaults
                     systemctl start ec2-terminate
 
+                    # update benchexec
+                    cd /mnt/benchexec
+                    git pull
+
                     # prepare for tool packaging
                     cd /mnt
                     cd cprover-sv-comp
+                    git pull
                     mkdir -p src/cbmc/
                     touch LICENSE
                     cd ..
@@ -290,10 +296,13 @@ Resources:
                         aws s3 cp s3://${S3Bucket}/${PerfTestId}/$cfg/cbmc \
                                 src/cbmc/cbmc
                         chmod a+x src/cbmc/cbmc
-                        make CBMC=. YEAR=N CBMC-sv-comp-N.tar.gz
+                        make CBMC=. cbmc.zip
                         cd ../run
-                        tar xzf ../cprover-sv-comp/CBMC-sv-comp-N.tar.gz
-                        rm ../cprover-sv-comp/CBMC-sv-comp-N.tar.gz
+                        unzip ../cprover-sv-comp/cbmc.zip
+                        mv cbmc cbmc-zip
+                        mv cbmc-zip/* .
+                        rmdir cbmc-zip
+                        rm ../cprover-sv-comp/cbmc.zip
 
                         date
                         echo "Task: $t"

scripts/perf-test/make-tables.sh

@@ -0,0 +1,72 @@
+#!/bin/bash
+
+set -e
+
+if [ -z "$BENCHEXEC" ]
+then
+  # default path to benchexec is set to a value that works for me(TM)
+  BENCHEXEC=~/Desktop/benchexec.git
+fi
+
+categories=""
+
+for d in "$@"
+do
+  c=$(echo $d/release/logs-* | tr ' ' '\n' | sed 's/.*logs-//')
+  categories=$(echo $categories $c | tr ' ' '\n' | sort | uniq)
+done
+
+official_logs="
+2017-01-11_1131.results.sv-comp17.ConcurrencySafety-Main.xml.bz2
+2017-01-11_1020.results.sv-comp17.MemSafety-Arrays.xml.bz2.merged.xml.bz2
+2017-01-11_1020.results.sv-comp17.MemSafety-Heap.xml.bz2.merged.xml.bz2
+2017-01-11_1020.results.sv-comp17.MemSafety-LinkedLists.xml.bz2.merged.xml.bz2
+2017-01-11_1020.results.sv-comp17.MemSafety-Other.xml.bz2.merged.xml.bz2
+2017-01-11_1354.results.sv-comp17.Overflows-BitVectors.xml.bz2.merged.xml.bz2
+2017-01-11_1354.results.sv-comp17.Overflows-Other.xml.bz2.merged.xml.bz2
+2017-01-10_1721.results.sv-comp17.ReachSafety-Arrays.xml.bz2.merged.xml.bz2
+2017-01-10_1721.results.sv-comp17.ReachSafety-BitVectors.xml.bz2.merged.xml.bz2
+2017-01-10_1721.results.sv-comp17.ReachSafety-ControlFlow.xml.bz2.merged.xml.bz2
+2017-01-10_1721.results.sv-comp17.ReachSafety-ECA.xml.bz2.merged.xml.bz2
+2017-01-10_1721.results.sv-comp17.ReachSafety-Floats.xml.bz2.merged.xml.bz2
+2017-01-10_1721.results.sv-comp17.ReachSafety-Heap.xml.bz2.merged.xml.bz2
+2017-01-10_1721.results.sv-comp17.ReachSafety-Loops.xml.bz2.merged.xml.bz2
+2017-01-10_1721.results.sv-comp17.ReachSafety-ProductLines.xml.bz2.merged.xml.bz2
+2017-01-10_1721.results.sv-comp17.ReachSafety-Recursive.xml.bz2.merged.xml.bz2
+2017-01-10_1721.results.sv-comp17.ReachSafety-Sequentialized.xml.bz2.merged.xml.bz2
+2017-01-11_1020.results.sv-comp17.Systems_BusyBox_MemSafety.xml.bz2.merged.xml.bz2
+2017-01-10_1721.results.sv-comp17.Systems_DeviceDriversLinux64_ReachSafety.xml.bz2.merged.xml.bz2
+"
+
+for c in $categories
+do
+  if [ ! -s official-sv-comp-17/*$c*.xml.bz2 ]
+  then
+    suffix=$(echo $official_logs | tr ' ' '\n' | grep "sv-comp17\.$c\.xml\.bz2" || true)
+    if [ -z "$suffix" ]
+    then
+      echo "No log known for $c"
+      srcs=""
+    else
+      wget \
+        http://sv-comp.sosy-lab.org/2017/results/results-verified/cbmc.$suffix \
+        -P official-sv-comp-17/
+      srcs="official-sv-comp-17/*$c*.xml.bz2"
+    fi
+  else
+    srcs="official-sv-comp-17/*$c*.xml.bz2"
+  fi
+
+  for d in "$@"
+  do
+    if [ -s $d/release/logs-$c/*.bz2 ]
+    then
+      srcs="$srcs $d/release/logs-$c/*.bz2"
+    fi
+  done
+
+  if [ -n "$srcs" ]
+  then
+    python3 $BENCHEXEC/bin/table-generator -n $c $srcs
+  fi
+done

scripts/perf-test/perf_test.py

@@ -66,14 +66,19 @@ def parse_args():
     parser.add_argument('-T', '--tasks', type=str,
                         default='quick',
                         help='Subset of tasks to run (quick, full; ' +
-                             'default: quick; or name of SV-COMP task)')
+                             'default: quick; or regex of SV-COMP task(s))')
+    parser.add_argument('-B', '--code-build', type=str,
+                        default=same_dir('codebuild.yaml'),
+                        help='Non-default CodeBuild template to use')
 
     args = parser.parse_args()
+
     assert(args.repository.startswith('https://github.com/') or
            args.repository.startswith('https://git-codecommit.'))
     assert(not args.ssh_key or args.ssh_key_name)
     if args.ssh_key:
         assert(os.path.isfile(args.ssh_key))
+    assert(os.path.isfile(args.code_build))
 
     return args
 
@@ -345,7 +350,8 @@ def prepare_ebs(session, region, az, ami):
     return snapshots['Snapshots'][0]['SnapshotId']
 
 
-def build(session, repository, commit_id, bucket_name, perf_test_id):
+def build(session, repository, commit_id, bucket_name, perf_test_id,
+        codebuild_file):
     # build the chosen commit in CodeBuild
     logger = logging.getLogger('perf_test')
 
@@ -356,7 +362,7 @@ def build(session, repository, commit_id, bucket_name, perf_test_id):
 
     cfn = session.resource('cloudformation', region_name='us-east-1')
     stack_name = 'perf-test-codebuild-' + perf_test_id
-    with open(same_dir('codebuild.yaml')) as f:
+    with open(codebuild_file) as f:
         CFN_codebuild = f.read()
     stack = cfn.create_stack(
             StackName=stack_name,
@@ -479,10 +485,8 @@ def seed_queue(session, region, queue, task_set):
     elif task_set == 'quick':
         tasks = ['ReachSafety-Loops', 'ReachSafety-BitVectors']
     else:
-        tasks = [task_set]
-
-    for t in tasks:
-        assert(t in set(all_tasks))
+        tasks = [t for t in all_tasks if re.match('^' + task_set + '$', t)]
+        assert(tasks)
 
     for t in tasks:
         response = queue.send_messages(
@@ -492,6 +496,9 @@ def seed_queue(session, region, queue, task_set):
                 ])
         assert(not response.get('Failed'))
 
+    logger.info(region + ': SQS queue seeded with {} jobs'.format(
+        len(tasks) * 2))
+
 
 def run_perf_test(
         session, mode, region, az, ami, instance_type, sqs_arn, sqs_url,
@@ -568,6 +575,7 @@ def run_perf_test(
             ],
             Capabilities=['CAPABILITY_NAMED_IAM'])
 
+    logger.info(region + ': Waiting for completition of ' + stack_name)
     waiter = cfn.meta.client.get_waiter('stack_create_complete')
     waiter.wait(StackName=stack_name)
     asg_name = stack.outputs[0]['OutputValue']
@@ -642,7 +650,7 @@ def main():
         session2 = boto3.session.Session()
         build_future = e.submit(
                 build, session2, args.repository, args.commit_id, bucket_name,
-                perf_test_id)
+                perf_test_id, args.code_build)
         session3 = boto3.session.Session()
         ebs_future = e.submit(prepare_ebs, session3, region, az, ami)
         session4 = boto3.session.Session()