This talk argues that exposing inherent limitations of synchronization
can positively affect the design and verification of concurrent
programs. This is demonstrated with two examples:
The first result shows that, for a large class of objects,
any implementation must include specific, easy-to-detect patterns
of memory accesses. The second is a reduction theorem showing that many
locking protocols need only be verified in a sequential setting.
The talk is based on work that appeared in POPL 2010 and POPL 2011.