A shared memory algorithm and proof for the generalized alternative construct in CSP
Communicating sequential processes (CSP) is a paradigm for communication and synchronization among distributed processes. The alternative construct is a key feature of CSP that allows nondeterministic selection of one among several possible communicants. A generalized version of Hoare's original alternative construct that allows output commands to be included in guards has been proposed. Previous algorithms for this construct assume a message passing architecture and are not appropriate for multiprocessor systems that feature shared memory. This paper describes a distributed algorithm for the generalized alternative construct that exploits the capabilities of a parallel computer with shared memory. A correctness proof of the proposed algorithm is presented to show that the algorithm conforms to some safety and liveness criteria. Extensions to allow termination of processes and to ensure fairness in guard selection are also given.
- An Effective Implementation for the Generalized Input-Output Construct of CSP
- Comments on “Communicating Sequential Processes”
- Communicating sequential processes
- CSM: A Distributed Programming Language
- Guarded commands, nondeterminacy and formal derivation of programs
- scientific article; zbMATH DE number 4039251 (Why is no real title available?)
- Proving Failure-Free Properties of Concurrent Systems Using Temporal Logic
- Proving Liveness Properties of Concurrent Programs
- Transformations for communication fairness in CSP
This page was built for publication: A shared memory algorithm and proof for the generalized alternative construct in CSP
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q1100889)
