a.md

Proofs of Send and Sync laws

T: Sync ⟺ &T: Send

Explanation

Consider a value a: T. Assume T: Sync. Then, to access a on multiple threads, it must be possible to send a reference to another thread, thus &T: Send. Therefore, T: Sync ⟹ &T: Send.

Assume &T: Send. Sending &a: &T to another thread means a can be accessed concurrently, thus T: Sync is required. Therefore, &T: Send ⟹ T: Sync.

T: Sync + Copy ⟹ T: Send

Proof

Assume T: Sync + Copy

let a: T = ?;

thread::spawn(move || {
	// T: Sync ∴ &T: Send
	let b: &T = &a;
	
	// T: Copy
	let c: T = *b;
});

∴ T: Send

T: Send ⟹ &mut T: Send

Explanation

A mutable reference &mut a (type &mut T) that is sent to another thread must then be the only way to access a (type T), since the type system ensures a mutable reference is an exclusive one.

T: Sync ⟹ &mut T: Sync

Explanation

The type system ensures that a mutable reference &mut a (type &mut T) must be the only way to access a (type T).

Note that T: Sync cannot be used to circumvent this restriction of the type system. Although &mut T: Sync ⟹ &&mut T: Send, a value of type &&mut T: Send cannot be dereferenced back to a value of type &mut T: Send.

T: Send ⟹ Unique<T>: Send

Explanation

A value b: Unique<T> wraps a value a: T, thus 'b' owns 'a'. Therefore, sending 'b' needs to be able to send a.

T: Sync ⟹ Unique<T>: Sync

Explanation

A value b: Unique<T> allows concurrent access to the wrapped value a: T, via the get and get_mut methods. Therefore, it must be safe to access a concurrently.

Shared<T>: !Send

Proof

Assume Shared<T>: Send and T aliases data (e.g. Rc<T>)

let mut a: T = ?;
let b = unsafe { Shared::new(&mut a) };

// Access a
thread::spawn(move || {
    let c = unsafe { *b };
    // *c == a
    // access c
});

∴ thread unsafety ∴ Shared<T>: !Send

Shared<T>: !Sync

Proof

Assume Shared<T>: Sync and T aliases data (for example, Rc<U>)

let mut a: T = ?;
let b = unsafe { Shared::new(&mut a) };

// access a
thread::spawn(move || {
	// T: Sync ∴ &T: Send
    let c = *(&b);
    // *c == a
    // access c
});

∴ thread unsafety ∴ Shared<T>: !Sync

Rc<T>: !Send

Assume Rc<T>: Send

let mut a: T = ?;
let b = Rc::new(a);

thread::spawn(move || {
    b.clone();
});

∴ thread unsafety, since changes to reference count of b are non-atomic and could be non-zero at end of block ∴ Rc<T>: !Send

Rc<T>: !Sync

Assume Rc<T>: Sync

let mut a: T = ?;
let b = Rc::new(a);

thread::spawn(move || {
	// T: Sync ⟹ &T: Send
    (&b).clone();
});

∴ thread unsafety, since changes to reference count of b are non-atomic and could be non-zero at end of block ∴ Rc<T>: !Sync

T: Send + Sync ⟹ Arc<T>: Send

Send bound -- because of try_unwrap Sync bound -- because of deref (sends an &T)

T: Send + Sync ⟹ Arc<T>: Sync

Send bound -- because of try_unwrap Sync bound -- because of deref (sends an &T)

T: Send ⟹ Mutex<T>: Send

Send bound -- because of lock & into_inner; also because Mutex wraps its value

T: Send ⟹ Mutex<T>: Sync

Send bound -- because of lock & into_inner

T: Send + Sync ⟹ RwLock<T>: Send

similar to Arc

T: Send + Sync ⟹ RwLock<T>: Sync

similar to Arc