CSP has proven to be a highly influential language design. An enormous body of research has grown up dealing with variants and derivatives of CSP, concerning logics, semantic models, and specification and verification of program properties by automated techniques. We have re-examined some language design alternatives from the original paper. We have shown that it is possible to build a simple and flexible semantic framework based on asynchronous communication and fair parallelism, simultaneously suitable for interpreting shared-variable programs and communicating processes. Despite being based "only" on a form of traces, our semantics provides a proper account of deadlock and divergence. In certain respects our framework has advantages: a natural account of fairness, and a unification of paradigms belied by the disparate collection of semantic models that evolved historically. This reaffirmation of the common roots of these paradigms, along with the simplicity and generality of our framework, are surely resonant of Tony Hoare's philosophy. Our semantics may be recast into a relationally parametric setting. This permits an elegant generalization of the principle of representation independence, yielding a link to another important early paper of Hoare, on proving the correctness of data representations. The traditional CSP models were developed within the established bounds of Scott-Strachey denotational semantics: program constructs were taken to denote continuous functions on a semantic domain, and recursive definitions were interpreted as least fixed-points. Relying implicitly on the finitistic nature of the failures model, Hoare's book showed how to reason algebraically about processes, taking advantage of the fact that (in the failures semantics) any guarded recursive definition has a unique solution. We cannot immediately adopt such an approach in our idealized setting, since our incorporation of fairness means that our model is no longer finitistic, and guarded equations may have more than one solution. Despite these complications one can develop a straightforward style of reasoning about fair recursive processes, as outlined in. The key is to use a form of fair expansion for recursive processes that meshes properly with fair parallel composition.
展开▼
