文章基本信息

标题：An Abstract State Machine Specification and Verification of the Location Consistency Memory Model and Cache Protocol
本地全文：下载
作者：C. Wallace ; G. Tremblay ; J. N. Amaral 等
期刊名称：Journal of Universal Computer Science
印刷版ISSN：0948-6968
出版年度：2001
卷号：7
期号：11
DOI：10.3217/jucs-007-11-1088
出版社：Graz University of Technology and Know-Center
摘要：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
关键词：cache memories, multiprocessors, requirements/specifications, shared memory