Skip to content

Immovable synchronization primitives do not detect swapping #4670

@RalfJung

Description

@RalfJung

pthread synchronization primitives must not be moved. We currently do detect some cases of that, but if you just swap the contents of two synchronization primitives, that's a total NOP and the program will continue -- whereas a this is clearly UB in a real execution (and in some pthread implementations, e.g. on macOS). We should get better at detecting such things.

This also affects os_unfair_lock to some extent, which we currently implement as kind-of movable, though arguably we are being too permissive here.

We probably want to extend the before_memory_write hook to also do something with the synchronization primitive metadata at the affected bytes -- for futexes, that's completely fine, but all constructs that store data "in userspace" need to be marked as broken on such a write. Also, ifn we refactor this anyway it would be great to get rid of the LAZY_INIT_COOKIE scheme... that's such a hack.

Metadata

Metadata

Assignees

No one assigned

    Labels

    A-concurrencyArea: affects our concurrency (multi-thread) supportI-misses-UBImpact: makes Miri miss UB, i.e., a false negative (with default settings)

    Type

    No type

    Projects

    No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions