liu.seSearch for publications in DiVA
Change search
CiteExportLink to record
Permanent link

Direct link
Cite
Citation style
  • apa
  • ieee
  • modern-language-association-8th-edition
  • vancouver
  • oxford
  • Other style
More styles
Language
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Other locale
More languages
Output format
  • 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öping University, Department of Computer and Information Science, Software and Systems. Linköping University, Faculty of Science & Engineering.ORCID iD: 0000-0001-5241-0026
Linköping University, Department of Computer and Information Science, Software and Systems. Linköping University, Faculty of Science & Engineering.ORCID iD: 0000-0001-8976-0484
2020 (English)In: The Journal of logical and algebraic methods in programming, ISSN 2352-2208, E-ISSN 2352-2216, Vol. 110, article id UNSP 100498Article in journal (Refereed) 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.

Place, publisher, year, edition, pages
ELSEVIER SCIENCE INC , 2020. Vol. 110, article id UNSP 100498
Keywords [en]
Memory consistency; CPU-GPU heterogeneous systems; Data transfer; Software caching; Cache coherence
National Category
Algebra and Logic
Identifiers
URN: urn:nbn:se:liu:diva-163369DOI: 10.1016/j.jlamp.2019.100498ISI: 000506718200002OAI: oai:DiVA.org:liu-163369DiVA, id: diva2:1391072
Note

Funding Agencies|EU H2020 project EXA2PRO [801015]

Available from: 2020-02-03 Created: 2020-02-03 Last updated: 2020-02-03

Open Access in DiVA

No full text in DiVA

Other links

Publisher's full text

Search in DiVA

By author/editor
Kessler, ChristophLi, Lu
By organisation
Software and SystemsFaculty of Science & Engineering
In the same journal
The Journal of logical and algebraic methods in programming
Algebra and Logic

Search outside of DiVA

GoogleGoogle Scholar

doi
urn-nbn

Altmetric score

doi
urn-nbn
Total: 2 hits
CiteExportLink to record
Permanent link

Direct link
Cite
Citation style
  • apa
  • ieee
  • modern-language-association-8th-edition
  • vancouver
  • oxford
  • Other style
More styles
Language
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Other locale
More languages
Output format
  • html
  • text
  • asciidoc
  • rtf