A mutual exclusion test on peterson's algorithm

[zpzigi754]

I've used the loom to test peterson's algorithm.

Peterson's algorithm does not seem to provide mutual exclusion with the below memory ordering.

#[test]
fn peterson() {
    loom::model(|| {
        let turn = Arc::new(AtomicUsize::new(0));
        let flag0 = Arc::new(AtomicBool::new(false));
        let flag1 = Arc::new(AtomicBool::new(false));
        let data = Arc::new(AtomicUsize::new(0));

        let p0 = {
            let turn = turn.clone();
            let flag0 = flag0.clone();
            let flag1 = flag1.clone();
            let data = data.clone();
            let p0 = thread::spawn(move || {
                flag0.store(true, Release);
                println!("[P0] flag0 store: true");
                turn.store(1, Release);
                println!("[P0] turn store: 1");
                // Lock
                loop {
                    let flag1_curr = flag1.load(Acquire);
                    println!("[P0] flag1_curr : {}", flag1_curr);
                    let turn_curr = turn.load(Acquire);
                    println!("[P0] turn_curr : {}", turn_curr);
                    if !(flag1_curr == true && turn_curr == 1) {
                        println!("[P0] break");
                        break;
                    }
                }
                data.store(3, Release);
                assert_eq!(3, data.load(Acquire));

                // Unlock
                flag0.store(false, Release);
            });
            p0
        };

        let p1 = {
            let turn = turn.clone();
            let flag0 = flag0.clone();
            let flag1 = flag1.clone();
            let data = data.clone();
            let p1 = thread::spawn(move || {
                flag1.store(true, Release);
                println!("[P1] flag1 store: true");
                turn.store(0, Release);
                println!("[P1] turn store: 0");
                // Lock
                loop {
                    let flag0_curr = flag0.load(Acquire);
                    println!("[P1] flag0_curr : {}", flag0_curr);
                    let turn_curr = turn.load(Acquire);
                    println!("[P1] turn_curr : {}", turn_curr);
                    if !(flag0_curr == true && turn_curr == 0) {
                        println!("[P1] break");
                        break;
                    }
                }
                data.store(2, Release);
                println!("[P1] store");
                assert_eq!(2, data.load(Acquire));

                // Unlock
                flag1.store(false, Release);
            });
            p1
        };
        p0.join().expect("Unexpected panic");
        p1.join().expect("Unexpected panic");
    });
}

The below is the result.

---- peterson stdout ----
[P0] flag0 store: true
[P0] turn store: 1
[P0] flag1_curr : false
[P0] turn_curr : 1
[P0] break
[P0] store
[P1] flag1 store : true
[P1] turn store : 0
[P1] flag0_curr : false
[P1] turn_curr : 1
[P1] break
[P1] store
thread 'peterson' panicked at 'assertion failed: `(left == right)`
  left: `2`,
 right: `3`', src/lib.rs:71:17

How could I know in which order the code have been executed?
Does the ones printed with the above println! macro represent the exact order which have been executed?

How could the value of P1's flag0_curr contain false even after flag0 has been written as true by P0?
Does the result mean that only P0's turn has been correctly stored while other stores have not been reflected?

[tomtomjhj]

Correctness of Peterson's algorithm assumes that there is a total order among the instructions. This is not true in weak memory models such as C/C++/Rust's, because for example a load() can read from a "stale" store(). To make this work as expected, you will need to recover sequential consistency by passing SeqCst instead of Acquire and Release.

But unfortunately, due to technical limitations, Loom does not understand SeqCst in load(), store(), etc. methods of Atomic* types. However, Loom does support fence(SeqCst). See #180 for details.

For Peterson's algorithm, you can simply insert fence(SeqCst) between all the accesses.