Browsing by Author "Sezgin,A."

Filter results by typing the first few letters
Now showing 1 - 2 of 2
  • Thumbnail Image
    Conference Object
    Citation - Scopus: 2
    On the Decidability of Shared Memory Consistency Verification
    (IEEE Computer Society, 2005) Sezgin,A.; Gopalakrishnan,G.
    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.
  • Thumbnail Image
    Conference Object
    On the decidability of shared memory consistency verification
    (IEEE Computer Society, 2005) Sezgin,A.; Gopalakrishnan,G.
    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.