On the Decidability of Shared Memory Consistency Verification
No Thumbnail Available
Date
2005
Authors
Journal Title
Journal ISSN
Volume Title
Publisher
IEEE Computer Society
Open Access Color
OpenAIRE Downloads
OpenAIRE Views
Abstract
We view shared memories as structures which define relations over the set of programs and their executions. An implementation is modeled by a transducer, where the relation it realizes is its language. This approach allows us to cast shared memory verification as language inclusion. We show that a specification can be approximated by an infinite hierarchy of finite-state transducers, called the memory model machines. Also, checking whether an execution is generated by a sequentially consistent memory is approached through a constraint satisfaction formulation. It is proved that if a memory implementation generates a non interleaved sequential and unambiguous execution, it necessarily generates one such execution of bounded size. Our paper summarizes the key results from the first author's dissertation, and may help a practitioner understand with clarity what "sequential consistency checking is undecidable" means. © 2005 IEEE.
Description
Keywords
[No Keyword Available]
Turkish CoHE Thesis Center URL
Fields of Science
Citation
WoS Q
Scopus Q
Source
Proceedings - Third ACM and IEEE International Conference on Formal Methods and Models for Co-Design, MEMOCODE'05 -- 3rd ACM and IEEE International Conferenceon Formal Methods and Models for Co-Design, MEMOCODE'05 -- 11 July 2005 through 14 July 2005 -- Verona -- 67485
Volume
2005
Issue
Start Page
188
End Page
197