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
Consider this program:
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