Title :
How to make a correct multiprocess program execute correctly on a multiprocessor
Author_Institution :
Syst. Res. Center, Digital Equipment Corp., Palo Alto, CA, USA
fDate :
7/1/1997 12:00:00 AM
Abstract :
A multiprocess program executing on a modern multiprocessor must issue explicit commands to synchronize memory accesses. A method is proposed for deriving the necessary commands from a correctness proof of the underlying algorithm in a formalism based on temporal relations among operation executions
Keywords :
concurrency control; processor scheduling; program verification; synchronisation; correctness proof; memory accesses; multiprocess program; multiprocessor; operation executions; temporal relations; Computer architecture; Data mining; Hardware; High level languages; Memory architecture; Notice of Violation; Programming profession; Safety;
Journal_Title :
Computers, IEEE Transactions on
