Instantly share code, notes, and snippets.

# durka/a.md

Forked from anonymous/a
Last active May 2, 2016 15:52

# 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 = ?;

// 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
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
// 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);

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);

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

similar to Arc

similar to Arc