Go home now Header Background Image
Search
Submission Procedure
share: |
 
Follow us
 
 
 
 
Volume 7 / Issue 11

available in:   PDF (245 kB) PS (191 kB)
 
get:  
Similar Docs BibTeX   Write a comment
  
get:  
Links into Future
 
DOI:   10.3217/jucs-007-11-1088

 

An Abstract State Machine Specification and Verification of the Location Consistency Memory Model and Cache Protocol

Charles Wallace (Computer Science Dept., Michigan Technological University, USA)

Guy Tremblay (Dept. d'informatique, Université du Québec à Montréal, Canada)

Jose N. Amaral (Computing Science Dept., University of Alberta, Canada)

Abstract:

We use the Abstract State Machine methodology to give formal operational semantics for the Location Consistency memory model and cache protocol. With these formal models, we prove that the cache protocol satisfies the memory model, but in a way that is strictly stronger than necessary, disallowing certain behavior allowed by the memory model.

Keywords: cache memories, multiprocessors, requirements/specifications, shared memory

Categories: B.3.2, C.1.2, D.2.1