An Abstract State Machine Specification and Verification of the Location Consistency Memory Model and Cache Protocol
| dc.creator | Wallace,Charles | |
| dc.creator | Tremblay,Guy | |
| dc.creator | Amaral,Jose | |
| dc.date | 2001 | |
| dc.date.accessioned | 2024-02-06T12:51:25Z | |
| dc.date.available | 2024-02-06T12:51:25Z | |
| dc.description | 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. | |
| dc.format | text/html | |
| dc.identifier | https://doi.org/10.3217/jucs-007-11-1088 | |
| dc.identifier | https://lib.jucs.org/article/27838/ | |
| dc.identifier.uri | https://openrepository.mephi.ru/handle/123456789/8043 | |
| dc.language | en | |
| dc.publisher | Journal of Universal Computer Science | |
| dc.relation | info:eu-repo/semantics/altIdentifier/eissn/0948-6968 | |
| dc.relation | info:eu-repo/semantics/altIdentifier/pissn/0948-695X | |
| dc.rights | info:eu-repo/semantics/openAccess | |
| dc.rights | J.UCS License | |
| dc.source | JUCS - Journal of Universal Computer Science 7(11): 1088-1112 | |
| dc.subject | requirements/specifications | |
| dc.subject | multiprocessors | |
| dc.subject | shared memory | |
| dc.subject | cache memories | |
| dc.title | An Abstract State Machine Specification and Verification of the Location Consistency Memory Model and Cache Protocol | |
| dc.type | Research Article |