liu.seSök publikationer i DiVA
Ändra sökning
RefereraExporteraLänk till posten
Permanent länk

Direktlänk
Referera
Referensformat
  • apa
  • ieee
  • modern-language-association-8th-edition
  • vancouver
  • oxford
  • Annat format
Fler format
Språk
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Annat 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 (Engelska)Ingår i: The Journal of logical and algebraic methods in programming, ISSN 2352-2208, E-ISSN 2352-2216, Vol. 110, artikel-id UNSP 100498Artikel i tidskrift (Refereegranskat) 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.

Ort, förlag, år, upplaga, sidor
ELSEVIER SCIENCE INC , 2020. Vol. 110, artikel-id UNSP 100498
Nyckelord [en]
Memory consistency; CPU-GPU heterogeneous systems; Data transfer; Software caching; Cache coherence
Nationell ämneskategori
Algebra och logik
Identifikatorer
URN: urn:nbn:se:liu:diva-163369DOI: 10.1016/j.jlamp.2019.100498ISI: 000506718200002OAI: oai:DiVA.org:liu-163369DiVA, id: diva2:1391072
Anmärkning

Funding Agencies|EU H2020 project EXA2PRO [801015]

Tillgänglig från: 2020-02-03 Skapad: 2020-02-03 Senast uppdaterad: 2020-02-03

Open Access i DiVA

Fulltext saknas i DiVA

Övriga länkar

Förlagets fulltext

Sök vidare i DiVA

Av författaren/redaktören
Kessler, ChristophLi, Lu
Av organisationen
Programvara och systemTekniska fakulteten
I samma tidskrift
The Journal of logical and algebraic methods in programming
Algebra och logik

Sök vidare utanför DiVA

GoogleGoogle Scholar

doi
urn-nbn

Altmetricpoäng

doi
urn-nbn
Totalt: 4 träffar
RefereraExporteraLänk till posten
Permanent länk

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