genmc: Bug fixes

[michaliskok]

This PR bumps the GenMC version to 0.16.1:

• Fixes the incorrect treatment of atomic_fetch_{umax,umin} (GenMC correctness issues #4572)
• Fixes overflowing on large allocations (GenMC correctness issues #4572)
• Collects all wrappers around the GenMC API in a single file (Exploration.cpp)
• Performs minor cleanups
• Fixes a couple of... FIXMEs

r? @RalfJung
(Each commit includes a description and can be reviewed separately.)

[RalfJung]

Thanks!

The last commit mentions issues with memory allocation; what exactly are you referring to?

View changes since this review

[RalfJung]

Also, please run ./miri fmt to apply our standard formatting to the Rust code.
@rustbot author

[rustbot]

Reminder, once the PR becomes ready for a review, use @rustbot ready.

[RalfJung]

The last commit mentions issues with memory allocation; what exactly are you referring to?

Ah, the PR description mentions "Fixes overflowing on large allocations". Is this about a single large allocation, or many allocations accumulating to exhaust the 4GB per-thread limit? How large is "large"? Is it possible to test for that? What happens now when the per-thread 4GB memory region is exhausted?

[michaliskok]

The last commit mentions issues with memory allocation; what exactly are you referring to?

Ah, the PR description mentions "Fixes overflowing on large allocations". Is this about a single large allocation, or many allocations accumulating to exhaust the 4GB per-thread limit? How large is "large"? Is it possible to test for that? What happens now when the per-thread 4GB memory region is exhausted?

Each thread can allocate up to 4GB. If the limit is exceeded, the allocator would silently wrap around 0 and handle duplicate addresses. The new commit makes GenMC crash if the limit is exceeded, and doesn't overflow if a size/alignment >2^32 is passed to alloc_aligned.

[RalfJung]

The new commit makes GenMC crash if the limit is exceeded,

That may make it tricky to add a test then, depending on the exit status this will trigger.

[michaliskok]

The new commit makes GenMC crash if the limit is exceeded,

That may make it tricky to add a test then, depending on the exit status this will trigger.

The alternative would be to return an error code to Miri and let Miri crash.

[RalfJung]

I tried what happened when one thread allocates more than 4GB memory in total (but not at the same time, i.e. we allocate chunks of 512MB and free them again):

./miri run --features=genmc bench-cargo-miri/big-allocs/src/main.rs -Zmiri-genmc

With this PR, that leads to a panic:

thread 'rustc' (123993) panicked at src/concurrency/genmc/mod.rs:597:9:
assertion `left != right` failed: GenMC malloc returned nullptr.

EDIT: I get the same with an 8GB allocation, using this test:

fn main() {
    let _v = Vec::<u8>::with_capacity(8 * 1024 * 1024 * 1024);
}

So, I can't reproduce the GenMC crash.

[RalfJung]

The alternative would be to return an error code to Miri and let Miri crash.

The alternative would be to make Miri emit a nice error saying we ran out of memory for this thread. :)

We don't have to resolve that in this PR, but ideally we'd have some tests before we mark the item in #4572 as resolved.

[RalfJung]

Here's a little patch to give the user some more explanation for why they may run out of address space in genmc mode:

diff --git a/src/diagnostics.rs b/src/diagnostics.rs
index bb8ba1969..8e252d306 100644
--- a/src/diagnostics.rs
+++ b/src/diagnostics.rs
@@ -362,6 +362,10 @@ pub fn report_result<'tcx>(
                 vec![
                     note!("this is likely not a bug in the program; it indicates that the program performed an operation that Miri does not support"),
                 ],
+            ResourceExhaustion(ResourceExhaustionInfo::AddressSpaceFull) if ecx.machine.data_race.as_genmc_ref().is_some() =>
+                vec![
+                    note!("in GenMC mode, the address space is limited to 4GB per thread, and addresses cannot be reused")
+                ],
             UndefinedBehavior(AlignmentCheckFailed { .. })
                 if ecx.machine.check_alignment == AlignmentCheck::Symbolic
             =>

[michaliskok]

I tried what happened when one thread allocates more than 4GB memory in total (but not at the same time, i.e. we allocate chunks of 512MB and free them again):

./miri run --features=genmc bench-cargo-miri/big-allocs/src/main.rs -Zmiri-genmc

With this PR, that leads to a panic:

thread 'rustc' (123993) panicked at src/concurrency/genmc/mod.rs:597:9:
assertion `left != right` failed: GenMC malloc returned nullptr.

EDIT: I get the same with an 8GB allocation, using this test:

fn main() {
    let _v = Vec::<u8>::with_capacity(8 * 1024 * 1024 * 1024);
}

So, I can't reproduce the GenMC crash.

Indeed, sorry about that.

I thought I made GenMC panic in all cases, but that's not the case. For allocations taking place via handleMalloc, GenMC returns nullptr (and potentially an error trace, but error reporting is not hooked up yet anyway). I added a test ensuring that Miri produces an error report if addresses get depleted.

I also incorporated your other comments.

[michaliskok]

@rustbot ready

[RalfJung]

Looks great, thanks :)