Representation and Implementation of CSP and VCR Traces

Brown, Neil C.C. and Smith, Marc L. (2008) Representation and Implementation of CSP and VCR Traces. In: Communicating Process Architectures 2008, Sep 07-10, 2008, York, England. (Full text available)

Download (212kB) Preview


Communicating Sequential Processes (CSP) was developed around a formal algebra of processes and a semantics based on traces (and failures and divergences). A trace is a record of the events engaged in by a process. Several programming languages use, or have libraries to use, CSP mechanisms to manage their concurrency. Most of these lack the facility to record the trace of a program. A standard trace is a flat list of events but structured trace models are possible that can provide more information such as the independent or concurrent engagement of the process in some of its events. One such trace model is View-Centric Reasoning (VCR), which offers an additional model of tracing, taking into account the multiple, possibly imperfect views of a concurrent computation. This paper also introduces ''structural'' traces, a new type of trace that reflects the nested parallelism in a CSP system. The paper describes the automated generation of these three trace types in the Communicating Haskell Processes (CHP) library, using techniques which could easily be applied in other libraries such as JCSP and C++CSP2. The ability to present such traces of a concurrent program assists in understanding the behaviour of real CHP programs and for debugging when the trace behaviours are wrong. These ideas and tools promote a deeper understanding of the association between practicalities of real systems software and the underlying CSP formalism.

Item Type: Conference or workshop item (Paper)
Uncontrolled keywords: csp vcr model-checking concurrency chp
Subjects: Q Science > QA Mathematics (inc Computing science) > QA 76 Software, computer programming,
Divisions: Faculties > Sciences > School of Computing > Systems Architecture Group
Depositing User: Neil Brown
Date Deposited: 29 Mar 2010 12:15 UTC
Last Modified: 18 Jul 2014 09:04 UTC
Resource URI: (The current URI for this page, for reference purposes)
  • Depositors only (login required):


Downloads per month over past year