Skip to content

Instantly share code, notes, and snippets.

@alexreg
Last active May 3, 2016 16:13
Show Gist options
  • Save alexreg/ae4cba905739370ee8c2020fb4ee1667 to your computer and use it in GitHub Desktop.
Save alexreg/ae4cba905739370ee8c2020fb4ee1667 to your computer and use it in GitHub Desktop.

Justification of Send and Sync rules

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.

Proof

Assume T: Sync

let a: T = ?;

// Can access `a` here

thread::scoped(|| {
	// Can access `a` concurrently, since `T: Sync`:
	let b: &T = &a;
});

&a: &T has effectively been sent to another thread ∴ &T: Send

Assume &T: Send

let a: T = ?;

// Can access `a` here

thread::scoped(|| {
	// Can send `&a` here, since `&T: Send`:
	let b: &T = &a;
	// Can access `a` concurrently here, by definition of `Send`
});

a: T has been accessed concurrently ∴ T: Sync

Note that these two proofs use the same code, just with different semantics.

T: Sync + Copy ⟹ T: Send

Proof

Assume T: Sync + Copy Hence &T: Send

let a: T = ?;

thread::scoped(|| {
	// Can send `&a` here, since `&T: Send`:
	let b: &T = &a;
	// Can copy `*b`, since `T: Copy`:
	let c: T = *b;
	// `c == a`
});

a: T has been sent to another thread ∴ T: Send

T: Send ⟹ &mut T: Send

Explanation

A mutable reference &mut a: &mut T that is sent to another thread must be (before and after) the only way to access a: T, since it is exclusive. Therefore, no thread unsafety can occur.

T: Sync ⟹ &mut T: Sync

Explanation

The type system ensures that a mutable reference &mut a: &mut T is the only way to access a: T, since it is exclusive. Therefore, no thread unsafety can occur.

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.

Proof

Assume T: Send

let mut a: Unique<T> = ?;

// Can dereference `*a` since `Unique<T>` owns value:
let b = unsafe { **a };

thread::scoped(|| {
	// Can send `b` here, since `b: Send`:
    let c: T = b;
    let d: Unique<T> = unsafe { Unique::new(&mut c) };
	// `d == a`
});

a: Unique<T> has effectively been sent to another thread ∴ Unique<T>: Send

T: Sync ⟹ Unique<T>: Sync

Explanation

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

Proof

Assume T: Sync Hence, &T: Send

let mut a: Unique<T> = ?;

// Access `a.get()`

thread::scoped(|| {
	// Can send `&a` here, since `&a: Send`:
    let b: T = &a;
    // Access `b.get()`
});

a is accessed concurrently in a safe manner ∴ Unique<T>: Sync

Shared<T>: !Send

Proof

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

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

// Access `a`

thread::scoped(|| {
	// Can send `b` here, since `Shared<T>: Send`:
    let c: *mut T = unsafe { *b };
    // `*c == a`
    // Access `c`
});

a is accessed concurrently in an unsafe manner ∴ Shared<T>: !Send

Shared<T>: !Sync

Proof

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

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

// Access `a`

thread::scoped(|| {
	// Can send `&b` here, since `&Shared<T>: Send`:
	let c: *mut T = *(&b);
	// `*c == a`
	// Access `c`
});

a is accessed ∴ Shared<T>: !Sync

Rc<T>: !Send

Assume Rc<T>: Send

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

thread::scoped(|| {
    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::scoped(|| {
	// Can send `b` here, since `&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

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment