MutexGuard<Cell<i32>> must not be Sync

[RalfJung]

Right now, MutexGuard<Cell<i32>> satisfies the Sync bound. That is rather bad, because it lets me write a program that has a data race:

use std::sync::Mutex;
use std::cell::Cell;

extern crate rayon;

fn main()
{
    let m = Mutex::new(Cell::new(0));
    let g = m.lock().unwrap();
    {
        rayon::join(
            || { g.set(g.get() + 1); println!("Thread 1: {:?}", g.get()) },
            || { g.set(g.get() + 1); println!("Thread 2: {:?}", g.get()) });
    }
}

The get and set calls in the two threads are unsynchronized (as usual for a Cell), and they are racing. This is a soundness bug.

The cause for this is that MutexGuard<T> implements Sync whenever T implements Send, which is plain wrong. The fix is to let MutexGuard<T> implement Sync whenever T implements Sync. I will submit a PR soon.

[RalfJung]

Btw, this bug was found while trying to prove soundnes of (an idealized version of) Mutex. Yay for formal methods :D

Also, this hints at a more general problem: OIBITS for types with custom invariants ("unsafe types") are dangerous.

[RalfJung]

Btw, this bug was found while trying to prove soundnes of (an idealized version of) Mutex. Yay for formal methods :D

Also, this hints at a more general problem: OIBITS for types with custom invariants ("unsafe types") are dangerous.

[RalfJung]

Also, this hints at a more general problem: OIBITS for types with custom invariants ("unsafe types") are dangerous.

To elaborate on this (from a formal proof perspective): To prove correctness of Send/Sync for an unsafe type (i.e., a type with its own invariant), I need to know exactly under which bounds the type is Send/Sync -- this defines the theorem I have to prove. However, if the type does not have an explicit impl for Send/Sync, I don't know how to even figure this out -- I would have to chase all types (including safe ones, and across all abstractions) of all fields recursively and then check when they are Send/Sync... that's way too error-prone. What I do instead is I try to compile small programs that only work e.g. if T: Send implies MutexGuard<T>: Sync. However, I may easily miss impls this way -- maybe we need T: Send+'static to get MutexGuard<T>: Sync? It is impossible to cover all possible constraints.

Also, even if there is an impl, there are still some subtleties: First of all, does giving a restrictive positive impl disable the more liberal automatic impl? (Tests indicate yes.) What if there is a restrictve negative impl? If I find impl<T: 'static> !Sync for MutexGuard<T>, does the automatic impl still apply for types that do not satisfy T:'static? (I haven't yet seen such a restrictive negative impl, so I don't know -- but this can happen accidentally with ?Sized if the type has T: ?Sized but the negative impl just has T.)

[RalfJung]

Also, this hints at a more general problem: OIBITS for types with custom invariants ("unsafe types") are dangerous.

To elaborate on this (from a formal proof perspective): To prove correctness of Send/Sync for an unsafe type (i.e., a type with its own invariant), I need to know exactly under which bounds the type is Send/Sync -- this defines the theorem I have to prove. However, if the type does not have an explicit impl for Send/Sync, I don't know how to even figure this out -- I would have to chase all types (including safe ones, and across all abstractions) of all fields recursively and then check when they are Send/Sync... that's way too error-prone. What I do instead is I try to compile small programs that only work e.g. if T: Send implies MutexGuard<T>: Sync. However, I may easily miss impls this way -- maybe we need T: Send+'static to get MutexGuard<T>: Sync? It is impossible to cover all possible constraints.

Also, even if there is an impl, there are still some subtleties: First of all, does giving a restrictive positive impl disable the more liberal automatic impl? (Tests indicate yes.) What if there is a restrictve negative impl? If I find impl<T: 'static> !Sync for MutexGuard<T>, does the automatic impl still apply for types that do not satisfy T:'static? (I haven't yet seen such a restrictive negative impl, so I don't know -- but this can happen accidentally with ?Sized if the type has T: ?Sized but the negative impl just has T.)