Skip to content

Commit

Permalink
Reduce the number of object bits for refcell test (model-checking#3656)
Browse files Browse the repository at this point in the history
This is a mitigation for model-checking#3611 till we determine the reason for the high
memory consumption. Since this test frequently fails due to running out
of memory when running locally, reducing the number of object bits.

Without this change, memory usage is ~9 GB:
```
SUMMARY:
 ** 0 of 182 failed (1 unreachable)

VERIFICATION:- SUCCESSFUL
Verification Time: 30.51689s

Complete - 1 successfully verified harnesses, 0 failures, 1 total.
        Command being timed: "kani refcell.rs -Zfunction-contracts"
        User time (seconds): 25.17
        System time (seconds): 8.07
        Percent of CPU this job got: 100%
        Elapsed (wall clock) time (h:mm:ss or m:ss): 0:33.20
        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): 9196056
        Average resident set size (kbytes): 0
        Major (requiring I/O) page faults: 0
        Minor (reclaiming a frame) page faults: 3464218
        Voluntary context switches: 1834
        Involuntary context switches: 128
        Swaps: 0
        File system inputs: 0
        File system outputs: 5400
        Socket messages sent: 0
        Socket messages received: 0
        Signals delivered: 0
        Page size (bytes): 4096
        Exit status: 0
```
and with this change, it's about ~600MB:
```

VERIFICATION:- SUCCESSFUL
Verification Time: 2.0234118s

Complete - 1 successfully verified harnesses, 0 failures, 1 total.
        Command being timed: "kani refcell.rs -Zfunction-contracts --enable-unstable --cbmc-args --object-bits 12"
        User time (seconds): 3.82
        System time (seconds): 0.92
        Percent of CPU this job got: 100%
        Elapsed (wall clock) time (h:mm:ss or m:ss): 0:04.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): 613636
        Average resident set size (kbytes): 0
        Major (requiring I/O) page faults: 60
        Minor (reclaiming a frame) page faults: 289631
        Voluntary context switches: 1882
        Involuntary context switches: 16
        Swaps: 0
        File system inputs: 11832
        File system outputs: 5400
        Socket messages sent: 0
        Socket messages received: 0
        Signals delivered: 0
        Page size (bytes): 4096
        Exit status: 0
```

By submitting this pull request, I confirm that my contribution is made
under the terms of the Apache 2.0 and MIT licenses.
  • Loading branch information
zhassan-aws authored Oct 28, 2024
1 parent f03c65b commit b375b6b
Showing 1 changed file with 3 additions and 1 deletion.
Original file line number Diff line number Diff line change
@@ -1,6 +1,8 @@
// Copyright Kani Contributors
// SPDX-License-Identifier: Apache-2.0 OR MIT
// kani-flags: -Zfunction-contracts
// Temporarily reduce the number of object bits till
// https://github.com/model-checking/kani/issues/3611 is fixed
// kani-flags: -Zfunction-contracts --enable-unstable --cbmc-args --object-bits 12

/// The objective of this test is to check the modification of a RefCell used as interior mutability in an immutable struct
use std::cell::RefCell;
Expand Down

0 comments on commit b375b6b

Please sign in to comment.