Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

test(s2n-quic-core): enable kani on a few harnesses #1644

Merged
merged 1 commit into from
Feb 28, 2023

Conversation

zhassan-aws
Copy link
Contributor

Resolved issues:

N/A

Description of changes:

Enable Kani on a few Bolero harnesses (ct, ipv4, ipv6, and rtt_estimator). This brings up the number of harnesses run by Kani from 16 to 30.

The runtime goes up by about 4 minutes. Current:

Complete - 16 successfully verified harnesses, 0 failures, 16 total.
        Command being timed: "cargo kani --tests"
        User time (seconds): 412.77
        System time (seconds): 22.20
        Percent of CPU this job got: 107%
        Elapsed (wall clock) time (h:mm:ss or m:ss): 6:43.56
        Average shared text size (kbytes): 0
        Average unshared data size (kbytes): 0
        Average stack size (kbytes): 0
        Average total size (kbytes): 0
        Maximum resident set size (kbytes): 3067656
        Average resident set size (kbytes): 0
        Major (requiring I/O) page faults: 527
        Minor (reclaiming a frame) page faults: 9324258
        Voluntary context switches: 132921
        Involuntary context switches: 3566
        Swaps: 0
        File system inputs: 280
        File system outputs: 10068744
        Socket messages sent: 0
        Socket messages received: 0
        Signals delivered: 0
        Page size (bytes): 4096
        Exit status: 0

After:

Complete - 30 successfully verified harnesses, 0 failures, 30 total.
        Command being timed: "cargo kani --tests"
        User time (seconds): 634.79
        System time (seconds): 30.46
        Percent of CPU this job got: 106%
        Elapsed (wall clock) time (h:mm:ss or m:ss): 10:26.72
        Average shared text size (kbytes): 0
        Average unshared data size (kbytes): 0
        Average stack size (kbytes): 0
        Average total size (kbytes): 0
        Maximum resident set size (kbytes): 3096388
        Average resident set size (kbytes): 0
        Major (requiring I/O) page faults: 569
        Minor (reclaiming a frame) page faults: 13935868
        Voluntary context switches: 179314
        Involuntary context switches: 4479
        Swaps: 0
        File system inputs: 296
        File system outputs: 11680040
        Socket messages sent: 0
        Socket messages received: 0
        Signals delivered: 0
        Page size (bytes): 4096
        Exit status: 0

Call-outs:

Testing:

No

By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 license.

@zhassan-aws zhassan-aws changed the title tests(s2n-quic-core): enable kani on a few harnesses test(s2n-quic-core): enable kani on a few harnesses Feb 28, 2023
Copy link
Contributor

@camshaft camshaft left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Very cool!

@camshaft camshaft merged commit 618f579 into aws:main Feb 28, 2023
@zhassan-aws zhassan-aws deleted the more-kani branch February 28, 2023 23:01
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

2 participants