Atomics load with SeqCst ordering strange behaviour

[Mnwa]

Hey! I have two threads. First stores 1 to x and load y, second stores 1 to y and load x. But assert broke with message thread 'main' panicked at 'x = 0, y = 0', src/main.rs:23:9 Why it possible with the SeqCst ordering?

use loom::thread;
use loom::sync::atomic::{AtomicUsize, Ordering};
use loom::sync::Arc;

fn main() {
    loom::model(|| {
        let x = Arc::new(AtomicUsize::new(0));
        let y = Arc::new(AtomicUsize::new(0));
        let x1 = x.clone();
        let y1 = y.clone();
        let x2 = x.clone();
        let y2 = y.clone();
        let child_x = thread::spawn(move || {
            x1.store(1, Ordering::SeqCst);
            y1.load(Ordering::SeqCst)
        });
        let child_y = thread::spawn(move || {
            y2.store(1, Ordering::SeqCst);
            x2.load(Ordering::SeqCst)
        });
        let res_x = child_x.join().unwrap();
        let res_y = child_y.join().unwrap();
        assert!(!(res_x == 0 && res_y == 0), "x = {}, y = {}", res_x, res_y);
    })
}

[tomtomjhj]

https://github.com/tokio-rs/loom/blob/21db3cc153d480c84346267eaa692be5d7b66c65/src/rt/synchronize.rs#L31-L34 https://github.com/tokio-rs/loom/blob/21db3cc153d480c84346267eaa692be5d7b66c65/src/rt/thread.rs#L276-L280 It seems that loom is not handling SeqCst load yet.

[wvwwvwwv]

Hi all,

Thanks a lot for this incredible test framework. My colleagues and I use loom on a daily basis at work, and it has proved to be extremely useful when it comes to reasoning about release-acquire relationships.

However, it turns out that it does not implement the SeqCst semantics at all; it seems to me that the global order of SeqCst stores is not correctly preserved, thus allowing SeqCst loads to see different store order, causing trouble. For instance, in addition to the other examples in this post, the following simple (and famous) Peterson's lock cannot be reasoned about with loom.

use loom::sync::atomic::AtomicUsize;
use std::sync::atomic::Ordering::SeqCst;

let model = loom::model::Builder::new();
model.check(|| {
    let data: Arc<AtomicUsize> = Arc::new(AtomicUsize::default());
    let t1: Arc<AtomicUsize> = Arc::new(AtomicUsize::default());
    let t2: Arc<AtomicUsize> = Arc::new(AtomicUsize::default());
    let data_cloned = data.clone();
    let t1_cloned = t1.clone();
    let t2_cloned = t2.clone();
    let thread_handle = loom::thread::spawn(move || {
        t2_cloned.store(1, SeqCst);
        if t1_cloned.load(SeqCst) == 0 {
            data_cloned.fetch_add(1, SeqCst);
        }
    });
    t1.store(1, SeqCst);
    if t2.load(SeqCst) == 0 {
        data.fetch_add(1, SeqCst);
    }
    drop(thread_handle.join());
    assert!(data.load(SeqCst) < 2);
});

I guess, the lack of correct implementation of SeqCst has to be mentioned somewhere in the document until the SeqCst handling is rectified. What do you think of it?

[tomtomjhj]

I also agree that the docs should mention this issue or at least the unimplmeneted functions should panic.

Now towards supporting SeqCst in loom...

As background, I'd like to say what SeqCst offers in addition to what's already provided by release/acquire is the read-after-write (RAW, "later read sees the latests write") ordering. But it's unclear SeqCst accesses provides which RAW ordering. This topic is discussed in the "scfix" paper and WG21/P0668R5, but it seems (1) the semantic model is quite complex; and (2) the models are not agreed upon in the community. That being said, there is a model checker called GenMC that supports SeqCst accesses (and other memory models) and uses a more advanced algorithm than what loom is currently based on. But unfortunately, it's only support C and C++.

On the other hand, SeqCst fence (in the absence of SeqCst accesses) has well-understood and clear semantics, and can be used for enforcing RAW consistency. (For example, please see the "promising semantics" paper for the formal model.) For the Peterson's mutex example, you can use Relaxed for the accesses and insert fence(SeqCst) between the instructions. So I think it is better to use SeqCst fences when RAW consistency is necessary, at least for the time being.

Thanks to the simplicity of the SeqCst fences, I was able to support SeqCst fence for loom on my fork with minimal changes. It passes some basic tests and I have used it for grading homework for a course that I work as TA for. My plan was to upstream this and disallow SeqCst accesses (panic), but I've been busy working on other stuff. If you're interested in our fork, please let us know. Just FYI, I and my supervisor @jeehoonkang at KAIST Concurrency and Parallelism Laboratory are interested in improving loom and correctness checkers for Rust in general.

[wvwwvwwv]

@tomtomjhj

Thanks for the tip, we'll use a SeqCst fence instead when it's needed once your branch gets merged into the main branch.

Send my regards to @jeehoonkang as my company once had been affiliated with his group, and the mentioned paper helped us a lot.

[raspofabs]

Hi. I see this issue is still open, and wondered if I was missing something about the resolution. I don't know if Rust intends on having a different interpretation of sequential consistency, but when I refer to the Sequentially-consistent ordering section of https://en.cppreference.com/w/cpp/atomic/memory_order I see there is a code snippet which does a very similar sequence of changes to this bug report and it claims you only need to have the loads and stores ordered sequentially to avoid UB (and data-races). This seems inconsistent with the merged tests which appear to require the SeqCst store and load calls do not guarantee global sequencing.

[Darksonn]

I don't know whether this issue should have been closed with #220.

[raspofabs]

Well, it's still reproducible, so not closed as fixed either way. Possibly rejected if there is a different memory model being suggested. (again, only if I am understanding the promises of Sequential Consistency correctly)

[Darksonn]

Rust uses the C++ memory model.