Weird failing assertions

[ZobyTwo]

The following code fails the assertion and I am not sure, why.

Whenever the mutex is held by the second thread, either the first did its update (a == b == false) or it didn't (a == b == true).
The second thread may have run the compare-exchange (or the swap) after the first thread changed both values, but if either of them is successful, the assertion isn't run. If the function continues, both a and b must still have their old value.
Strangely, this logic appears to hold with the compare-exchange, but not with the swap (which should have the same semantics because these values are just booleans?).

#[cfg(test)]
#[cfg(feature = "loom")]
mod test {
    use std::sync::Arc;
    use loom::{
        thread,
        sync::{
            Mutex,
            atomic::{AtomicBool, Ordering}
        }
    };

    #[test]
    fn failing_test() {
        pub struct Foo
        {
            a: Mutex<bool>,
            b: AtomicBool,
        }

        loom::model(|| {
            let foo = Arc::new(Foo{
                a: Mutex::new(true),
                b: AtomicBool::new(true),
            });

            let thread_1 = {
                let foo = Arc::clone(&foo);
                thread::spawn(move || {
                    let maybe_guard = (*foo).a.lock();
                    let mut a = maybe_guard.unwrap();
                    foo.b.store(false, Ordering::Relaxed); // Was Release before, but that should not matter.
                    *a = false;
                })
            };

            let thread_2 = {
                let foo = Arc::clone(&foo);
                thread::spawn(move || {
                    // Either those don't have an effect (so the values remain equal), 
                    // or I am exiting the function (not running the assertion):
                    {
                        // works:
                        // if foo.b.compare_exchange(false, true, Ordering::Relaxed, Ordering::Relaxed).is_ok() { return; }

                        // causes assertion:
                        if !foo.b.swap(true, Ordering::Relaxed) { return; }
                    }

                    {
                        let maybe_guard = (*foo).a.lock();
                        let a = maybe_guard.unwrap();
                        let b = (*foo).b.load(Ordering::Relaxed);
                        assert!(*a == b);
                    }
                })
            };

            thread_1.join().unwrap();
            thread_2.join().unwrap();
        })
    }
}

Edit: This also happens when we replace the mutex by a typical spinlock and only do try_lock instead of lock. It appears as though the AtomicBool::swap is not actually atomic, but does separate read and write operations, and thereby loses the value written by the first thread.

[mox692]

Looks like you're using std::sync::Arc instead of loom::sync::Arc, is that what you would like to do?

[ZobyTwo]

Looks like you're using std::sync::Arc instead of loom::sync::Arc, is that what you would like to do?

What gave you the idea this has anything to do with Arc?

This is specifically about loom running into an impossible execution and hitting the assert.

Edit: Verified that this also happens with loom's Arc.

[mox692]

Normally the Arc from std is not supposed to be used inside the loom::model, so I just wanted to check if this was an easy mistake. I haven't looked into deeply yet.

[ZobyTwo]

The documentation states:

Note that loom still works if some concurrent operations are hidden from it (for example, if you use std::sync::Arc instead of loom::sync::Arc). It just means that loom won’t be able to reason about the interaction between those operations and the other concurrent operations in your program, and thus certain executions that are possible in the real world won’t be modeled.

So at most loom should not explore valid executions, not invent invalid ones.

To reiterate the problem (or my wrong understanding):

• The swap on b either happens before the store, or after:
  • if it happens before, the store will write false again and the second thread should read false from a and b, due to the ordering from the mutex.
  • if it happens after, the swap will return false and the second thread will exit, not performing the assertion at all.

For the assertion to trigger, the swap has to happen after the store to b, but still return true, which is impossible.

[ZobyTwo]

I played some more with the code and basically minified it down to #254. I think they are the same problem.

[ZobyTwo]

I spent some time reading the paper and the code, and tried to debug this - I think that I now know what is happening. This is the minified version (don't mind the leak):

#[test]
fn swap_order() {
    loom::model(|| {
        // 1)
        let a = &*Box::leak(Box::new(AtomicBool::new(false)));

        let thread_1 = thread::spawn(move || { 
            // 3)
            a.store(true, Relaxed); }
        );
        
        // 2)
        let b1 = a.swap(false, Relaxed);
        
        thread_1.join().unwrap();

        // 4)
        let b2 = a.load(Relaxed);
        
        assert!(b2 != b1);
    })
}

The numbers annotate the order in which loom executes the effects of the atomic operations.
The core issue here is that the load in (4) selects (2) and (3) as possible loads (the read-from-set in the paper),
even though we are in an execution where (2) happened before (3), which we know by the value we observed in (2).
This is the resulting relation graph for that execution (hb = happens-before, rf = reads-from).

(1) a.init(false)
    .-hb+rf-'    '-----hb----.
    V                        V
(2) b1 = a.swap(false)  (3) a.store(true)
    '-hb+rf-.    .-----hb----'
            V    V
         (4) b2 = a.load()

The actual modification orders (the VersionVec= the clock of each thread when the statement was executed) are:

• (1): 0, 0
• (2): 2, 0
• (3): 0, 2
• (4): 3, 2

From these, it appears that the load from (2) at (4) is allowed. (A load is possible from a store if the store happens-before the load and there is no other store that comes in between in modification-order). This is the modification order graph, and this allows (4) to load from (2) and (3):

(1) -> (2) -> (4)
  '---> (3) ---^

The missing piece to the solution here is the "RMW Atomicity" constraint from the paper. It looks like this (mo = modification-order):

A: v.store(1)                           B: v.rmw()
   .-rf-'  '--mo--.            =>        '--mo--.
   V              V                             V
B: v.rmw()   C: v.store(2)             C: v.store(2)

If a store operation (C) overwrites a value that was previously read by an RMW operation (B), its modification
order is the pairwise max (joined) with the RMW operation (B). This makes sense as the store (C) cannot happen between
(A) and (B) as otherwise (B) would have read from (C), and it cannot happen between the load and the store parts
of (B), as (B) would not be an atomic RMW otherwise.
This applies to the issue at hand: (A) is (1), (B) is (2), (C) is (3). And thus, the mo-edge is missing from (2) to (3),
which would make reading from (2) impossible at (4).

I think the fix is to stick a last_rmw: VersionVec into State, join it with the current thread's causality in
State::rmw, and join it into the modification_order when in State::store. At least this fixes my original problem and the minified version.

I will prepare a PR later (though there is quite a backlog already in the repo) and see whether this also fixes the other, related issues.