Sezgin, AGopalakrishnan, G2024-10-062024-10-062005780392272https://hdl.handle.net/20.500.14411/8752We 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.eninfo:eu-repo/semantics/closedAccess[No Keyword Available]Conference Object199208WOS:0002318766000221