Sezgin,A.Gopalakrishnan,G.2024-09-102024-09-1020050780392272978-078039227-410.1109/MEMCOD.2005.14879152-s2.0-33745182538https://doi.org/10.1109/MEMCOD.2005.1487915We 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.eninfo:eu-repo/semantics/closedAccess[No Keyword Available]Conference Object20051881972