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
.
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.
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
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.
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
.
A value b: Unique<T>
wraps a value a: T
, thus 'b' owns 'a'. Therefore, sending 'b' needs to be able to send a
.
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
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.
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
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
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
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
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
Send bound -- because of try_unwrap Sync bound -- because of deref (sends an &T)
Send bound -- because of try_unwrap Sync bound -- because of deref (sends an &T)
Send bound -- because of lock & into_inner; also because Mutex wraps its value
Send bound -- because of lock & into_inner
similar to Arc
similar to Arc