Edinburgh Research Explorer

Ensuring Memory Consistency in Heterogeneous Systems Based on Access Mode Declarations

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

  • Ludovic Henrio
  • C Kessler
  • Lu LI

Related Edinburgh Organisations

Open Access permissions

Open

Documents

https://ieeexplore.ieee.org/document/8514422
Original languageEnglish
Title of host publication5th International Symposium on Formal Approaches to Parallel and Distributed Systems, as part of The 16th International Conference on High Performance Computing Simulation (HPCS 2018)
Place of PublicationOrleans, France
PublisherInstitute of Electrical and Electronics Engineers (IEEE)
Pages716-723
Number of pages8
ISBN (Electronic)978-1-5386-7879-4
ISBN (Print)978-1-5386-7878-7
DOIs
Publication statusPublished - 1 Nov 2018
EventThe 5th International Symposium on Formal Approaches to Parallel and Distributed Systems (4PAD 2018) - Orléans, France
Duration: 16 Jul 201820 Jul 2018
http://hpcs2018.cisedu.info/2-conference/symposia---hpcs2018/symp05-4pad

Symposium

SymposiumThe 5th International Symposium on Formal Approaches to Parallel and Distributed Systems (4PAD 2018)
Abbreviated title4PAD 2018
CountryFrance
CityOrléans
Period16/07/1820/07/18
Internet address

Abstract

Running a program on disjoint memory spaces requires to address memory consistency issues and to perform transfers so that the program always accesses the right data. Several approaches exist to ensure the consistency of the memory accessed, we are interested here in the verification of a declarative approach where each component of a computation is annotated with an access mode declaring which part of the memory is read or written by the component. The programming framework uses the component annotations to guarantee the validity of the memory accesses. This is the mechanism used in VectorPU, a C++ library for programming CPU-GPU heterogeneous systems and this article proves the correctness of the software cache-coherence mechanism used in the library. Beyond the scope of VectorPU, this article can be considered as a simple and effective formalisation of memory consistency mechanisms based on the explicit declaration of the effect of each component on each memory space.

    Research areas

  • Index Terms-Memory consistency, CPU-GPU heterogeneous systems, data transfer, software caching, cache coherence

Download statistics

No data available

ID: 74745083