A class of synchronization systems that permit the use of large atomic blocks
Paolo A. G. Sivilotti · Conference of the Centre for Advanced Studies on Collaborative Research · 1998
This paper revisits the formal justification of a common practice used in formal and informal reasoning about distributed systems: considering certain sections of code to be implicitly atomic. This practice is extremely useful as it allows distributed and concurrent programs to be developed, tested, and verified with large atomic blocks, yet executed with a much finer granularity of parallelism for efficiency. We expose the elements on which this practice is based and characterize the synchronization systems for which this practice is valid. Unlike previous justifications for this practice, our approach is based on a weakest precondition semantics. Owing to the generality of our model of computation, the result is applicable to both distributed-memory and shared-memory systems.