You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
Reduce the number of object bits for refcell test (#3656)
This is a mitigation for #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.
0 commit comments