Abstract
Correctness Proofs of Programs using Weak Memories
by: Manhoi Choy and Ambuj K. Singh
Abstract:
A method for reasoning with non-atomic memory is developed. A program usingnon-atomic memory is transformed into an equivalent one that uses atomicmemory. A number of non-atomic memories including pipelined RAM, causalmemory, and hybrid consistency are examined. The approach is illustrated withsome examples.
Keywords:
Concurrency, Program Correctness, Memory Consistency Conditions.
Date:
January 1993
Document: 1993-05
