How to make a correct multiprocess program execute correctly on a multiprocessor

1 July 1997

journal article
Published by Institute of Electrical and Electronics Engineers (IEEE) in IEEE Transactions on Computers

Vol. 46 (7) , 779-782
https://doi.org/10.1109/12.599898

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

This publication has 15 references indexed in Scilit:

Memory consistency and event ordering in scalable shared-memory multiprocessors
Published by Institute of Electrical and Electronics Engineers (IEEE) ,2002
On Lamport's interprocessor communication model
ACM Transactions on Programming Languages and Systems, 1989
Atomic semantics of nonatomic programs
Information Processing Letters, 1988
The global time assumption and semantics for concurrent systems
Published by Association for Computing Machinery (ACM) ,1988
The mutual exclusion problem
Journal of the ACM, 1986
How to Make a Multiprocessor Computer That Correctly Executes Multiprocess Programs
IEEE Transactions on Computers, 1979
A New Approach to Proving the Correctness of Multiprocess Programs
ACM Transactions on Programming Languages and Systems, 1979
The temporal logic of programs
Published by Institute of Electrical and Electronics Engineers (IEEE) ,1977
Proving the Correctness of Multiprocess Programs
IEEE Transactions on Software Engineering, 1977
Proving assertions about parallel programs
Journal of Computer and System Sciences, 1975