Memory consistency models using constraints

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Abstract

Memory consistency models (MCMs) are at the heart of concurrent programming. They represent the behaviour of concurrent programs at the chip level. To test these models small program snippets called litmus test are generated, which show allowed or forbidden behaviour of different MCMs. This paper is showcasing the use of constraint programming to automate the generation and testing of litmus tests for memory consistency models. We produce a few exemplary case studies for two MCMs, namely Sequential Consistency and Total Store Order. These studies demonstrate the flexibility of constrains programming in this context and lay foundation to the direct verification of MCMs against the software facing cache coherence protocols.
Original languageEnglish
Title of host publicationThe Seventeenth Workshop on Constraint Modelling and Reformulation (ModRef 2018), Proceedings
Number of pages16
Publication statusPublished - 27 Aug 2018
Event24th International Conference on Principles and Practice of Constraint Programming (CP 2018) - Euratechnologies, Lille, France
Duration: 27 Aug 201831 Aug 2018
Conference number: 24
http://cp2018.a4cp.org/

Conference

Conference24th International Conference on Principles and Practice of Constraint Programming (CP 2018)
Abbreviated titleCP 2018
Country/TerritoryFrance
CityLille
Period27/08/1831/08/18
Internet address

Keywords

  • Memory consistency
  • Concurrent programming
  • Litmus tests
  • Constraints programming
  • Modelling

Fingerprint

Dive into the research topics of 'Memory consistency models using constraints'. Together they form a unique fingerprint.

Cite this