Correctness Proofs of Programs using Weak Memories

Report ID: 
1993-05
Authors: 
Manhoi Choy and Ambuj K. Singh
Date: 
1993-01-01 04:00:00

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.

Document

File 1993-05.ps