a

# 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>

## `T: Send + Sync ⟹ RwLock<T>: Sync`
similar to Arc<T>