Skip to content

Miri can't track pointer through atomic bit-flip, which happens as usize #1993

Closed
@jonhoo

Description

@jonhoo

In haphazard, I maintain a concurrent linked list of things that can be "locked" through a bit flip in the next pointer. The relevant code is here:

https://github.com/jonhoo/haphazard/blob/ba8ffcceba6f0a0b117c0e35d2ab05a6c1bb5233/src/domain.rs#L259-L281

It basically looks like this:

let head_available = AtomicUsize::new(0);

// ...

let avail = hazptrs.head_available.load(Ordering::Acquire);
if avail == core::ptr::null::<HazPtrRecord>() as usize {
    return core::ptr::null_mut();
}
if (avail & LOCK_BIT) == 0 {
    let avail: *const HazPtrRecord = avail as _;

    // The available list is not currently locked.
    // Take the lock by flipping the bit.
    if head_available.compare_exchange_weak(
        avail as usize,
        avail as usize | LOCK_BIT,
        Ordering::AcqRel,
        Ordering::Relaxed,
    ).is_ok() {
        // ...

I would love to run this code through Miri with -Zmiri-tag-raw-pointers (it runs fine without), but then I (as expected) run into "parent tag " due to the int-to-ptr conversion, which matches the README's note saying " You can recognize false positives by <untagged> occurring in the message -- this indicates a pointer that was cast from an integer, so Miri was unable to track this pointer." You can replicate the issue using:

$ env "MIRIFLAGS=-Zmiri-tag-raw-pointers" cargo +nightly miri test --test lib feels_good
    Finished test [unoptimized + debuginfo] target(s) in 0.03s
     Running tests/lib.rs (/home/jon/.cargo-target/miri/x86_64-unknown-linux-gnu/debug/deps/lib-c166183ccbed9275)

running 1 test
test feels_good ... error: Undefined Behavior: trying to reborrow for SharedReadWrite at alloc65366, but parent tag <untagged> does not have an appropriate item in the borrow stack
   --> /home/jon/dev/streams/haphazard/src/domain.rs:310:33
    |
310 |         let mut next = unsafe { &*tail }.available_next.load(Ordering::Relaxed);
    |                                 ^^^^^^ trying to reborrow for SharedReadWrite at alloc65366, but parent tag <untagged> does not have an appropriate item in the borrow stack
    |
    = help: this indicates a potential bug in the program: it performed an invalid operation, but the rules it violated are still experimental
    = help: see https://github.com/rust-lang/unsafe-code-guidelines/blob/master/wip/stacked-borrows.md for further information

    = note: inside `haphazard::Domain::<haphazard::Global>::try_acquire_available_locked::<1_usize>` at /home/jon/dev/streams/haphazard/src/domain.rs:310:33
    = note: inside `haphazard::Domain::<haphazard::Global>::try_acquire_available::<1_usize>` at /home/jon/dev/streams/haphazard/src/domain.rs:284:45
    = note: inside `haphazard::Domain::<haphazard::Global>::acquire_many::<1_usize>` at /home/jon/dev/streams/haphazard/src/domain.rs:217:29
    = note: inside `haphazard::Domain::<haphazard::Global>::acquire` at /home/jon/dev/streams/haphazard/src/domain.rs:211:9
    = note: inside `haphazard::HazardPointer::new_in_domain` at /home/jon/dev/streams/haphazard/src/hazard.rs:54:21
    = note: inside `haphazard::HazardPointer::<'static>::new` at /home/jon/dev/streams/haphazard/src/hazard.rs:41:9
note: inside `feels_good` at tests/lib.rs:106:17
   --> tests/lib.rs:106:17
    |
106 |     let mut h = HazardPointer::new();
    |                 ^^^^^^^^^^^^^^^^^^^^
note: inside closure at tests/lib.rs:77:1
   --> tests/lib.rs:77:1
    |
76  |   #[test]
    |   ------- in this procedural macro expansion
77  | / fn feels_good() {
78  | |     let drops_42 = Arc::new(AtomicUsize::new(0));
79  | |
80  | |     let x = AtomicPtr::new(Box::into_raw(Box::new((
...   |
160 | |     assert_eq!(drops_9001.load(Ordering::SeqCst), 1);
161 | | }
    | |_^
    = note: this error originates in the attribute macro `test` (in Nightly builds, run with -Z macro-backtrace for more info)

Is there any way for me to "help" Miri realize what's going on here? For reference, the pointer stores happen here:

https://github.com/jonhoo/haphazard/blob/ba8ffcceba6f0a0b117c0e35d2ab05a6c1bb5233/src/domain.rs#L320-L322

and here

https://github.com/jonhoo/haphazard/blob/ba8ffcceba6f0a0b117c0e35d2ab05a6c1bb5233/src/domain.rs#L337-L350

Metadata

Metadata

Assignees

No one assigned

    Labels

    A-intptrcastArea: affects int2ptr and ptr2int castsC-enhancementCategory: a PR with an enhancement or an issue tracking an accepted enhancement

    Type

    No type

    Projects

    No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions