From 3269da7049664cb02a206593352ed1586a1a52a6 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Wed, 1 Nov 2017 15:23:43 +0000 Subject: [PATCH 1/7] Utility to generate HTML reports from perf-test experiments This is by and large in a works-for-me state and may need documentationa and generalisation. --- scripts/perf-test/make-tables.sh | 72 ++++++++++++++++++++++++++++++++ 1 file changed, 72 insertions(+) create mode 100755 scripts/perf-test/make-tables.sh diff --git a/scripts/perf-test/make-tables.sh b/scripts/perf-test/make-tables.sh new file mode 100755 index 00000000000..c159f8c91e5 --- /dev/null +++ b/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 From d3b29d233f9113706cfcf9d491443cbd9b7490af Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Wed, 1 Nov 2017 15:25:13 +0000 Subject: [PATCH 2/7] Update cprover-sv-comp, benchexec to latest version --- scripts/perf-test/ec2.yaml | 5 +++++ 1 file changed, 5 insertions(+) diff --git a/scripts/perf-test/ec2.yaml b/scripts/perf-test/ec2.yaml index 5933777f6e2..1a3559835f3 100644 --- a/scripts/perf-test/ec2.yaml +++ b/scripts/perf-test/ec2.yaml @@ -203,9 +203,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 .. From 6eeb672bec07f9f676142080d2d3b03ed4cf3582 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Wed, 1 Nov 2017 15:25:39 +0000 Subject: [PATCH 3/7] Permit selecting a regular-expression-defined set of tasks --- scripts/perf-test/perf_test.py | 11 ++++++----- 1 file changed, 6 insertions(+), 5 deletions(-) diff --git a/scripts/perf-test/perf_test.py b/scripts/perf-test/perf_test.py index 0f4de36dc40..a5fa709c101 100755 --- a/scripts/perf-test/perf_test.py +++ b/scripts/perf-test/perf_test.py @@ -66,7 +66,7 @@ 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))') args = parser.parse_args() assert(args.repository.startswith('https://github.com/') or @@ -479,10 +479,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 +490,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, From 1c0cf3224de0a6da01f14e9ae7213b890619f4d2 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Sun, 5 Nov 2017 22:49:14 +0000 Subject: [PATCH 4/7] Support custom CodeBuild templates --- scripts/perf-test/perf_test.py | 13 ++++++++++--- 1 file changed, 10 insertions(+), 3 deletions(-) diff --git a/scripts/perf-test/perf_test.py b/scripts/perf-test/perf_test.py index a5fa709c101..303bf25b712 100755 --- a/scripts/perf-test/perf_test.py +++ b/scripts/perf-test/perf_test.py @@ -67,13 +67,18 @@ def parse_args(): default='quick', help='Subset of tasks to run (quick, full; ' + '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, @@ -569,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'] @@ -643,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() From 98b9ae65be023a866e757ea90c14c713a6189cec Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Tue, 7 Nov 2017 10:26:14 +0000 Subject: [PATCH 5/7] SV-COMP now requires zip files --- scripts/perf-test/ec2.yaml | 10 +++++++--- 1 file changed, 7 insertions(+), 3 deletions(-) diff --git a/scripts/perf-test/ec2.yaml b/scripts/perf-test/ec2.yaml index 1a3559835f3..47b8e1628cc 100644 --- a/scripts/perf-test/ec2.yaml +++ b/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 @@ -295,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" From f659577ef283f2459b954b5c3d5489a343b282ba Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Fri, 1 Dec 2017 18:22:54 +0000 Subject: [PATCH 6/7] perf-test: build configuration using glucose Configuration can be used/enabled using -B codebuild-glucose.yaml --- scripts/perf-test/codebuild-glucose.yaml | 129 +++++++++++++++++++++++ 1 file changed, 129 insertions(+) create mode 100644 scripts/perf-test/codebuild-glucose.yaml diff --git a/scripts/perf-test/codebuild-glucose.yaml b/scripts/perf-test/codebuild-glucose.yaml new file mode 100644 index 00000000000..aaba1a51af1 --- /dev/null +++ b/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 From 03095d47d1f2ec1bd6c7290bb48a982604afb140 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Fri, 8 Dec 2017 14:51:14 +0000 Subject: [PATCH 7/7] Use svcomp18 as base --- scripts/perf-test/ebs.yaml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/scripts/perf-test/ebs.yaml b/scripts/perf-test/ebs.yaml index 609554c8f39..e76a7497880 100644 --- a/scripts/perf-test/ebs.yaml +++ b/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