An Assertional Proof of a Lock Synchronization Algorithm Using Fetch and Store Atomic Instruction. - Ting-Lu Huang; Jann-Hann Lin (ICPADS, 1994)