liu.seSearch for publications in DiVA
Endre søk
RefereraExporteraLink to record
Permanent link

Direct link
Referera
Referensformat
  • apa
  • ieee
  • modern-language-association-8th-edition
  • vancouver
  • oxford
  • Annet format
Fler format
Språk
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Annet språk
Fler språk
Utmatningsformat
  • html
  • text
  • asciidoc
  • rtf
Leveraging access mode declarations in a model for memory consistency in heterogeneous systems
Univ Claude Bernard Lyon 1, France; Univ Cote Azur, France.
Linköpings universitet, Institutionen för datavetenskap, Programvara och system. Linköpings universitet, Tekniska fakulteten.ORCID-id: 0000-0001-5241-0026
Linköpings universitet, Institutionen för datavetenskap, Programvara och system. Linköpings universitet, Tekniska fakulteten.ORCID-id: 0000-0001-8976-0484
2020 (engelsk)Inngår i: The Journal of logical and algebraic methods in programming, ISSN 2352-2208, E-ISSN 2352-2216, Vol. 110, artikkel-id UNSP 100498Artikkel i tidsskrift (Fagfellevurdert) Published
Abstract [en]

On a system that exposes disjoint memory spaces to the software, a program has to address memory consistency issues and perform data transfers so that it always accesses valid data. Several approaches exist to ensure the consistency of the memory accessed. Here we are interested 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. This article proves the correctness of the software cache-coherence mechanism used in VectorPU. Beyond the scope of VectorPU, this article provides a simple and effective formalization of memory consistency mechanisms based on the explicit declaration of the effect of each component on each memory space. The formalism we propose also takes into account arrays for which a single validity status is stored for the whole array; additional mechanisms for dealing with overlapping arrays are also studied. (C) 2019 Elsevier Inc. All rights reserved.

sted, utgiver, år, opplag, sider
ELSEVIER SCIENCE INC , 2020. Vol. 110, artikkel-id UNSP 100498
Emneord [en]
Memory consistency; CPU-GPU heterogeneous systems; Data transfer; Software caching; Cache coherence
HSV kategori
Identifikatorer
URN: urn:nbn:se:liu:diva-163369DOI: 10.1016/j.jlamp.2019.100498ISI: 000506718200002OAI: oai:DiVA.org:liu-163369DiVA, id: diva2:1391072
Merknad

Funding Agencies|EU H2020 project EXA2PRO [801015]

Tilgjengelig fra: 2020-02-03 Laget: 2020-02-03 Sist oppdatert: 2020-02-03

Open Access i DiVA

Fulltekst mangler i DiVA

Andre lenker

Forlagets fulltekst

Søk i DiVA

Av forfatter/redaktør
Kessler, ChristophLi, Lu
Av organisasjonen
I samme tidsskrift
The Journal of logical and algebraic methods in programming

Søk utenfor DiVA

GoogleGoogle Scholar

doi
urn-nbn

Altmetric

doi
urn-nbn
Totalt: 4 treff
RefereraExporteraLink to record
Permanent link

Direct link
Referera
Referensformat
  • apa
  • ieee
  • modern-language-association-8th-edition
  • vancouver
  • oxford
  • Annet format
Fler format
Språk
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Annet språk
Fler språk
Utmatningsformat
  • html
  • text
  • asciidoc
  • rtf