Inherent limitations can facilitate design and verification of concurrent programs