Okay, now I understand why you find auto-derivation of Sync to be frightening. I agree that auto-derivation of Sync for a type containing at least two Sync members may be unsound if Sync is interpreted as meaning "linearizable". Perhaps this auto-derivation rule could be restricted to types with only one Sync member as a conservative assumption until better rules are found, if that does not break too much existing code?
PS: Thanks for the links on atomics optimization! Very enlightening reads!
@vitalyd: I just opened a ticket on rustc's issue tracker in order to discuss this matter with core developers and see what they think about it.
Awesome, thanks! 
I think I know what the response will be, which is basically (1) it's about data race freedom and (2) they wanted anonymous/compiler-synthesized types to be Sync (i.e. closures); ensuring proper semantics are the author's responsibility. And, of course, the ship has sailed and now making any change is backwards incompatible. But, maybe I'm wrong and there's a different perspective these days.
The other aspect that I'd love to hear thoughts on are with respect to the right way to convey memory ordering affects of operations exposed by any Sync type. Should the community adopt a similar documentation practice that the, e.g., JDK developers use, which is to note memory effects in code docs (rustdoc for Rust)? I think this is a related, albeit slightly different, topic from the auto-derived aspects of Sync.
What I am sure about is that I would never get anyone to agree on that Sync should not be implemented for types with one internally mutable member, because it would likely break all wrappers of Sync types.
2+ internally mutable members, now... I would need to see how many libraries on crates.io correctly rely on that being automatically derived to be Sync. It may not be that big a breakage, especially considering how many threading beginner mistakes it would allow to be detected by the compiler.
As for memory orderings, the ideal situation would probably be to have a programmatic way to check if a function features an Acquire, Release, or SeqCst barrier, in order to avoid hand-written documentation that is likely to become obsolete as the implementation changes. But I'm likely dreaming