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

dc.creatorWallace,Charles
dc.creatorTremblay,Guy
dc.creatorAmaral,Jose
dc.date2001
dc.date.accessioned2024-02-06T12:51:25Z
dc.date.available2024-02-06T12:51:25Z
dc.descriptionWe 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.
dc.formattext/html
dc.identifierhttps://doi.org/10.3217/jucs-007-11-1088
dc.identifierhttps://lib.jucs.org/article/27838/
dc.identifier.urihttps://openrepository.mephi.ru/handle/123456789/8043
dc.languageen
dc.publisherJournal of Universal Computer Science
dc.relationinfo:eu-repo/semantics/altIdentifier/eissn/0948-6968
dc.relationinfo:eu-repo/semantics/altIdentifier/pissn/0948-695X
dc.rightsinfo:eu-repo/semantics/openAccess
dc.rightsJ.UCS License
dc.sourceJUCS - Journal of Universal Computer Science 7(11): 1088-1112
dc.subjectrequirements/specifications
dc.subjectmultiprocessors
dc.subjectshared memory
dc.subjectcache memories
dc.titleAn Abstract State Machine Specification and Verification of the Location Consistency Memory Model and Cache Protocol
dc.typeResearch Article
Файлы
Коллекции