| A CSP approach to sequential consistency (2007) | |||||||||||||||
Abstract | |||||||||||||||
| In this paper, we show how the process notation of Communicating Sequential Processes (CSP) may be used to describe a lazy caching protocol. We then show that the traces model for CSP can be used to specify the property of sequential consistency. The model-based approach of CSP allows us to demonstrate that the protocol description satisfies the specification, thus verifying that the lazy caching protocol is sequentially consistent. 1 Introduction In shared-memory multiprocessor systems, the time taken to perform memory access operations is critical. In most designs, this is reduced by equipping each processor with a cache: a local image of the shared store. If each cache contains a copy of the locations that the corresponding processor is most likely to access, then any delay due to shared memory access will be minimised. However, if a system contains multiple copies of the same datum, care must be exercised if the system is to behave in a predictable and satisfactory fashion. Whene... | |||||||||||||||
Publication details | |||||||||||||||
| |||||||||||||||