On the Decidability of Shared Memory Consistency Verification

No Thumbnail Available

Date

2005

Journal Title

Journal ISSN

Volume Title

Publisher

IEEE Computer Society

Open Access Color

OpenAIRE Downloads

OpenAIRE Views

Research Projects

Organizational Units

Journal Issue

Events

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

Collections