A fair calculus of communicating systems
We contrast a two level operational approach to fairness with a single level approach. The latter involves presenting a set of rules which generate all and only the fair execution sequences of a concurrent language. This we do for a subset of Milner's CCS.
Unable to display preview. Download preview PDF.
- [AO]K. Apt and E. Olderog. ‘Proof rules dealing with fairness'. Bericht Nr. 8104, Inst. für Informatik und Praktische Mathematik, Kiel University (1981).Google Scholar
- [CS1]G. Costa and C. Stirling. ‘A fair calculus of communicating systems'. To appear.Google Scholar
- [CS2]G. Costa and C. Stirling. ‘Fair rules for a concurrent guarded command language'. In preparation.Google Scholar
- [GPSS]D. Gabbay, A. Pnueli, S. Shelah and J. Stavi. ‘On the temporal analysis of fairness'. Proc. 7th ACM POPL, Las Vegas (1980).Google Scholar
- [H]M. Hennessy. ‘Axiomatising finite delay operators'. Technical Report CSR-124-82, Dept. of Computer Science, Edinburgh University (1982).Google Scholar
- [LPS]D. Lehmann, A. Pnueli and J. Stavi. ‘Impartiality, justice and fairness: the ethics of concurrent termination'. LNCS 115, pp. 264–77, Springer-Verlag (1981).Google Scholar
- [M1]R. Milner. ‘A Calculus of Communicating Systems'. LNCS 92, Springer-Verlag (1980).Google Scholar
- [M2]R. Milner. ‘A finite delay operator in synchronous CCS'. Technical Report CSR-116-82, Dept. of Computer Science, Edinburgh University (1982).Google Scholar
- [OL]S. Owicki and L. Lamport. ‘Proving liveness properties of concurrent programs'. Technical Report, SRI International (1980).Google Scholar
- [Pa]D. Park. ‘On the semantics of fair parallelism'. LNCS 86, pp. 504–26, Springer-Verlag (1980).Google Scholar
- [P]G. Plotkin. ‘A powerdomain for countable non-determinism'. LNCS 140, pp. 418–28, Springer-Verlag (1982).Google Scholar