Nondeterminism and the Correctness of Parallel Programs.
- 1 May 1977
- report
- Published by Defense Technical Information Center (DTIC)
Abstract
This paper presents the weakest preconditions which describe weak correctness, blocking, deadlock, and starvation for nondeterministic programs. A procedure for converting parallel programs to nondeterministic programs is described, and the correctness of various example parallel programs is treated in this manner. Among these are a busy-wait mutual exclusion scheme, and the problem of the Five Dining Philosophers.Keywords
This publication has 0 references indexed in Scilit: