Concurrent algorithms classically relied on locks to guarantee the absence of interference when accessing shared resources. The massive use of distributed systems and of new multi-core architectures makes this approach unfeasible, and novel techniques are needed. Lock-Free algorithms have thus gained momentum. We define a core imperative calculus, equipped with concurrency and low level lock-free synchronization primitives, based on the Load-Link/Store-Conditional model. We propose a Hoare-Separation-style system to prove correct lock-free algorithms implemented in this language. Judgements distinguish local from global state, transfering knowledge between the worlds in the rules for loading and copying variables. We present a simple yet illustrative example of a proof for a concurrent data structure.
A simple proof system for lock-free concurrency
