Skip to content

The data race detector does not understand TCP-socket-based synchronization, leading to incorrect data race reports #5199

Description

@RalfJung

Consider this program:

fn test_race() {
    static mut VAL: u8 = 0;

    let (server_sockfd, addr) = net::make_listener_ipv4().unwrap();
    let client_sockfd =
        unsafe { errno_result(libc::socket(libc::AF_INET, libc::SOCK_STREAM, 0)).unwrap() };

    let thread1 = thread::spawn(move || {
        let (peerfd, _) = net::accept_ipv4(server_sockfd).unwrap();
        // write() from the main thread will occur before the read() here
        // because preemption is disabled and the main thread yields after write().
        let buf = read_exact_array::<1>(peerfd).unwrap();
        assert_eq!(&buf, b"a");
        // The read above establishes a happens-before so it is now safe to access this global variable.
        unsafe { assert_eq!(VAL, 1) };
    });
    net::connect_ipv4(client_sockfd, addr).unwrap();

    unsafe { VAL = 1 };
    write_all(client_sockfd, b"a").unwrap();
    thread1.join().unwrap();
}

This program is correct. However, Miri reports a data race, because it does not see the happens-before relationship that is established by the main thread writing to the socket and the child thread later reading from the peer socket.

This is kind of tricky to deal with since we don't actually know whether any two sockets in Miri are talking to each other.
Cc @WhySoBad

Metadata

Metadata

Assignees

No one assigned

    Labels

    A-data-raceArea: data race detectorA-shimsArea: This affects the external function/static shimsC-bugCategory: This is a bug.I-false-UBImpact: makes Miri falsely report UB, i.e., a false positive (with default settings)

    Type

    No type

    Projects

    No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions