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 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 diff --git a/scripts/perf-test/ec2.yaml b/scripts/perf-test/ec2.yaml index 5933777f6e2..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 @@ -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" 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 diff --git a/scripts/perf-test/perf_test.py b/scripts/perf-test/perf_test.py index 0f4de36dc40..303bf25b712 100755 --- a/scripts/perf-test/perf_test.py +++ b/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()