So it turns out I don't understand C11's memory model at all, after my colleague showed me this snippet:

fn main() {}

#[test]
fn foo() {
    use loom::{
        sync::{Arc, atomic::*},
        thread,
    };
    loom::model(|| {
        let v = Arc::new(AtomicU8::new(100));
        let reset = {
            let v = Arc::clone(&v);
            thread::spawn(move || {
                v.store(0, Ordering::Relaxed);
            })
        };
        let incre = {
            let v = Arc::clone(&v);
            thread::spawn(move || {
                v.fetch_add(1, Ordering::Relaxed);
            })
        };
        reset.join().unwrap();
        incre.join().unwrap();
        // fails, meaning it's possible to end up with 101
        assert_ne!(v.load(Ordering::Relaxed), 101);
    });
}

From what I understand, there's only two possible modification order for the shared atomic: (notations and graphs come from here)

  reset           v         incre
╭───────────╮   ┌─────┐   ╭───────────╮
│ store     ├─┐ │ 100 │ ┌─┤ fetch_add │
╰───────────╯ │ └─────┘ │ ╰───────────╯
              └─┬─────┐ │
                │ 0   │ │
                └─────┘ │
                ┌─────┬─┘
                │ 1   │
                └─────┘

  reset           v         incre
╭───────────╮   ┌─────┐   ╭───────────╮
│ store     ├─┐ │ 100 │ ┌─┤ fetch_add │
╰───────────╯ │ └─────┘ │ ╰───────────╯
              │ ┌─────┬─┘
              │ │ 101 │
              │ └─────┘
              └─┬─────┐
                │ 0   │
                └─────┘

IMHO these two graphs suffice to say that the only possible outcomes are either 0 or 1: 101 exists in MO of v only in the second scenario, and coherence means we should not see 101 since

following the reverse direction of arrows, then for each one of those, take a single step across every line that connects to the relevant memory location. It is not allowed for the access to read or write any value that appears above any one of these points."

The JoinHandle::join shall grant us required arrow (which I didn't draw): its return synchronizes-with all memory operations occurred in the spawned thread.

Am I missing something?

4 posts - 4 participants

Read full topic