Presburger Arithmetic in Memory Access Optimization for Data-Parallel Languages
Identifieur interne : 003C81 ( Hal/Curation ); précédent : 003C80; suivant : 003C82Presburger Arithmetic in Memory Access Optimization for Data-Parallel Languages
Auteurs : Ralf Karrenberg [Allemagne] ; Marek Kosta [France] ; Thomas Sturm [France]Source :
Abstract
Data-parallel languages like OpenCL and CUDA are an important means to exploit the computational power of today's computing devices. We consider the compilation of such languages for CPUs with SIMD instruction sets. To generate efficient code, one wants to statically decide whether or not certain memory operations access consecutive addresses. We formalize the notion of consecutivity and algorithmically reduce the static decision to satisfiability problems in Presburger Arithmetic. We introduce a preprocessing technique on these SMT problems, which makes it feasible to apply an off-the-shelf SMT solver. We show that a prototypical OpenCL CPU driver based on our approach generates more efficient code than any other state-of-the-art driver.
Url:
DOI: 10.1007/978-3-642-40885-4_5
Links toward previous steps (curation, corpus...)
- to stream Hal, to step Corpus: Pour aller vers cette notice dans l'étape Curation :003C81
Links to Exploration step
Hal:hal-00931954Le document en format XML
<record><TEI><teiHeader><fileDesc><titleStmt><title xml:lang="en">Presburger Arithmetic in Memory Access Optimization for Data-Parallel Languages</title><author><name sortKey="Karrenberg, Ralf" sort="Karrenberg, Ralf" uniqKey="Karrenberg R" first="Ralf" last="Karrenberg">Ralf Karrenberg</name><affiliation wicri:level="1"><hal:affiliation type="researchteam" xml:id="struct-397686" status="INCOMING"><orgName>Compiler Design Lab</orgName><desc><address><country key="DE"></country></address></desc><listRelation><relation active="#struct-49357" type="direct"></relation><relation active="#struct-365003" type="indirect"></relation></listRelation><tutelles><tutelle active="#struct-49357" type="direct"><org type="laboratory" xml:id="struct-49357" status="VALID"><orgName>Compiler Design Lab</orgName><desc><address><addrLine>FR 6.2 Informatik * Universität des Saarlandes * Campus E1 3 * Postfach 15 11 50 * 66041 Saarbrücken</addrLine><country key="DE"></country></address><ref type="url">http://rw4.cs.uni-saarland.de/</ref></desc><listRelation><relation active="#struct-365003" type="direct"></relation></listRelation></org></tutelle><tutelle active="#struct-365003" type="indirect"><org type="institution" xml:id="struct-365003" status="INCOMING"><orgName>SAARLAND UNIVERSITY</orgName><desc><address><country key="FR"></country></address></desc></org></tutelle></tutelles></hal:affiliation><country>Allemagne</country></affiliation></author><author><name sortKey="Kosta, Marek" sort="Kosta, Marek" uniqKey="Kosta M" first="Marek" last="Kosta">Marek Kosta</name><affiliation wicri:level="1"><hal:affiliation type="researchteam" xml:id="struct-107895" status="VALID"><idno type="RNSR">201020692C</idno><orgName>Modeling and Verification of Distributed Algorithms and Systems</orgName><orgName type="acronym">VERIDIS</orgName><desc><address><country key="FR"></country></address><ref type="url">http://www.inria.fr/equipes/veridis</ref></desc><listRelation><relation active="#struct-129671" type="direct"></relation><relation active="#struct-300009" type="indirect"></relation><relation active="#struct-423084" type="direct"></relation><relation active="#struct-206040" type="indirect"></relation><relation active="#struct-413289" type="indirect"></relation><relation name="UMR7503" active="#struct-441569" type="indirect"></relation></listRelation><tutelles><tutelle active="#struct-129671" type="direct"><org type="laboratory" xml:id="struct-129671" status="VALID"><idno type="RNSR">198618246Y</idno><orgName>INRIA Nancy - Grand Est</orgName><desc><address><addrLine>615 rue du Jardin Botanique 54600 Villers-lès-Nancy</addrLine><country key="FR"></country></address><ref type="url">http://www.inria.fr/nancy</ref></desc><listRelation><relation active="#struct-300009" type="direct"></relation></listRelation></org></tutelle><tutelle active="#struct-300009" type="indirect"><org type="institution" xml:id="struct-300009" status="VALID"><orgName>Institut National de Recherche en Informatique et en Automatique</orgName><orgName type="acronym">Inria</orgName><desc><address><addrLine>Domaine de VoluceauRocquencourt - BP 10578153 Le Chesnay Cedex</addrLine><country key="FR"></country></address><ref type="url">http://www.inria.fr/en/</ref></desc></org></tutelle><tutelle active="#struct-423084" type="direct"><org type="department" xml:id="struct-423084" status="VALID"><orgName>Department of Formal Methods </orgName><orgName type="acronym">LORIA - FM</orgName><desc><address><country key="FR"></country></address><ref type="url">http://www.loria.fr/la-recherche-en/departements/formal-methods</ref></desc><listRelation><relation active="#struct-206040" type="direct"></relation><relation active="#struct-300009" type="indirect"></relation><relation active="#struct-413289" type="indirect"></relation><relation name="UMR7503" active="#struct-441569" type="indirect"></relation></listRelation></org></tutelle><tutelle active="#struct-206040" type="indirect"><org type="laboratory" xml:id="struct-206040" status="VALID"><idno type="IdRef">067077927</idno><idno type="RNSR">198912571S</idno><idno type="IdUnivLorraine">[UL]RSI--</idno><orgName>Laboratoire Lorrain de Recherche en Informatique et ses Applications</orgName><orgName type="acronym">LORIA</orgName><date type="start">2012-01-01</date><desc><address><addrLine>Campus Scientifique BP 239 54506 Vandoeuvre-lès-Nancy Cedex</addrLine><country key="FR"></country></address><ref type="url">http://www.loria.fr</ref></desc><listRelation><relation active="#struct-300009" type="direct"></relation><relation active="#struct-413289" type="direct"></relation><relation name="UMR7503" active="#struct-441569" type="direct"></relation></listRelation></org></tutelle><tutelle active="#struct-413289" type="indirect"><org type="institution" xml:id="struct-413289" status="VALID"><idno type="IdRef">157040569</idno><idno type="IdUnivLorraine">[UL]100--</idno><orgName>Université de Lorraine</orgName><orgName type="acronym">UL</orgName><date type="start">2012-01-01</date><desc><address><addrLine>34 cours Léopold - CS 25233 - 54052 Nancy cedex</addrLine><country key="FR"></country></address><ref type="url">http://www.univ-lorraine.fr/</ref></desc></org></tutelle><tutelle name="UMR7503" active="#struct-441569" type="indirect"><org type="institution" xml:id="struct-441569" status="VALID"><idno type="ISNI">0000000122597504</idno><idno type="IdRef">02636817X</idno><orgName>Centre National de la Recherche Scientifique</orgName><orgName type="acronym">CNRS</orgName><date type="start">1939-10-19</date><desc><address><country key="FR"></country></address><ref type="url">http://www.cnrs.fr/</ref></desc></org></tutelle></tutelles></hal:affiliation><country>France</country><placeName><settlement type="city">Nancy</settlement><settlement type="city">Metz</settlement><region type="region" nuts="2">Grand Est</region><region type="old region" nuts="2">Lorraine (région)</region></placeName><orgName type="university">Université de Lorraine</orgName></affiliation></author><author><name sortKey="Sturm, Thomas" sort="Sturm, Thomas" uniqKey="Sturm T" first="Thomas" last="Sturm">Thomas Sturm</name><affiliation wicri:level="1"><hal:affiliation type="researchteam" xml:id="struct-107895" status="VALID"><idno type="RNSR">201020692C</idno><orgName>Modeling and Verification of Distributed Algorithms and Systems</orgName><orgName type="acronym">VERIDIS</orgName><desc><address><country key="FR"></country></address><ref type="url">http://www.inria.fr/equipes/veridis</ref></desc><listRelation><relation active="#struct-129671" type="direct"></relation><relation active="#struct-300009" type="indirect"></relation><relation active="#struct-423084" type="direct"></relation><relation active="#struct-206040" type="indirect"></relation><relation active="#struct-413289" type="indirect"></relation><relation name="UMR7503" active="#struct-441569" type="indirect"></relation></listRelation><tutelles><tutelle active="#struct-129671" type="direct"><org type="laboratory" xml:id="struct-129671" status="VALID"><idno type="RNSR">198618246Y</idno><orgName>INRIA Nancy - Grand Est</orgName><desc><address><addrLine>615 rue du Jardin Botanique 54600 Villers-lès-Nancy</addrLine><country key="FR"></country></address><ref type="url">http://www.inria.fr/nancy</ref></desc><listRelation><relation active="#struct-300009" type="direct"></relation></listRelation></org></tutelle><tutelle active="#struct-300009" type="indirect"><org type="institution" xml:id="struct-300009" status="VALID"><orgName>Institut National de Recherche en Informatique et en Automatique</orgName><orgName type="acronym">Inria</orgName><desc><address><addrLine>Domaine de VoluceauRocquencourt - BP 10578153 Le Chesnay Cedex</addrLine><country key="FR"></country></address><ref type="url">http://www.inria.fr/en/</ref></desc></org></tutelle><tutelle active="#struct-423084" type="direct"><org type="department" xml:id="struct-423084" status="VALID"><orgName>Department of Formal Methods </orgName><orgName type="acronym">LORIA - FM</orgName><desc><address><country key="FR"></country></address><ref type="url">http://www.loria.fr/la-recherche-en/departements/formal-methods</ref></desc><listRelation><relation active="#struct-206040" type="direct"></relation><relation active="#struct-300009" type="indirect"></relation><relation active="#struct-413289" type="indirect"></relation><relation name="UMR7503" active="#struct-441569" type="indirect"></relation></listRelation></org></tutelle><tutelle active="#struct-206040" type="indirect"><org type="laboratory" xml:id="struct-206040" status="VALID"><idno type="IdRef">067077927</idno><idno type="RNSR">198912571S</idno><idno type="IdUnivLorraine">[UL]RSI--</idno><orgName>Laboratoire Lorrain de Recherche en Informatique et ses Applications</orgName><orgName type="acronym">LORIA</orgName><date type="start">2012-01-01</date><desc><address><addrLine>Campus Scientifique BP 239 54506 Vandoeuvre-lès-Nancy Cedex</addrLine><country key="FR"></country></address><ref type="url">http://www.loria.fr</ref></desc><listRelation><relation active="#struct-300009" type="direct"></relation><relation active="#struct-413289" type="direct"></relation><relation name="UMR7503" active="#struct-441569" type="direct"></relation></listRelation></org></tutelle><tutelle active="#struct-413289" type="indirect"><org type="institution" xml:id="struct-413289" status="VALID"><idno type="IdRef">157040569</idno><idno type="IdUnivLorraine">[UL]100--</idno><orgName>Université de Lorraine</orgName><orgName type="acronym">UL</orgName><date type="start">2012-01-01</date><desc><address><addrLine>34 cours Léopold - CS 25233 - 54052 Nancy cedex</addrLine><country key="FR"></country></address><ref type="url">http://www.univ-lorraine.fr/</ref></desc></org></tutelle><tutelle name="UMR7503" active="#struct-441569" type="indirect"><org type="institution" xml:id="struct-441569" status="VALID"><idno type="ISNI">0000000122597504</idno><idno type="IdRef">02636817X</idno><orgName>Centre National de la Recherche Scientifique</orgName><orgName type="acronym">CNRS</orgName><date type="start">1939-10-19</date><desc><address><country key="FR"></country></address><ref type="url">http://www.cnrs.fr/</ref></desc></org></tutelle></tutelles></hal:affiliation><country>France</country><placeName><settlement type="city">Nancy</settlement><settlement type="city">Metz</settlement><region type="region" nuts="2">Grand Est</region><region type="old region" nuts="2">Lorraine (région)</region></placeName><orgName type="university">Université de Lorraine</orgName></affiliation></author></titleStmt><publicationStmt><idno type="wicri:source">HAL</idno><idno type="RBID">Hal:hal-00931954</idno><idno type="halId">hal-00931954</idno><idno type="halUri">https://hal.inria.fr/hal-00931954</idno><idno type="url">https://hal.inria.fr/hal-00931954</idno><idno type="doi">10.1007/978-3-642-40885-4_5</idno><date when="2013-09-18">2013-09-18</date><idno type="wicri:Area/Hal/Corpus">003C81</idno><idno type="wicri:Area/Hal/Curation">003C81</idno></publicationStmt><sourceDesc><biblStruct><analytic><title xml:lang="en">Presburger Arithmetic in Memory Access Optimization for Data-Parallel Languages</title><author><name sortKey="Karrenberg, Ralf" sort="Karrenberg, Ralf" uniqKey="Karrenberg R" first="Ralf" last="Karrenberg">Ralf Karrenberg</name><affiliation wicri:level="1"><hal:affiliation type="researchteam" xml:id="struct-397686" status="INCOMING"><orgName>Compiler Design Lab</orgName><desc><address><country key="DE"></country></address></desc><listRelation><relation active="#struct-49357" type="direct"></relation><relation active="#struct-365003" type="indirect"></relation></listRelation><tutelles><tutelle active="#struct-49357" type="direct"><org type="laboratory" xml:id="struct-49357" status="VALID"><orgName>Compiler Design Lab</orgName><desc><address><addrLine>FR 6.2 Informatik * Universität des Saarlandes * Campus E1 3 * Postfach 15 11 50 * 66041 Saarbrücken</addrLine><country key="DE"></country></address><ref type="url">http://rw4.cs.uni-saarland.de/</ref></desc><listRelation><relation active="#struct-365003" type="direct"></relation></listRelation></org></tutelle><tutelle active="#struct-365003" type="indirect"><org type="institution" xml:id="struct-365003" status="INCOMING"><orgName>SAARLAND UNIVERSITY</orgName><desc><address><country key="FR"></country></address></desc></org></tutelle></tutelles></hal:affiliation><country>Allemagne</country></affiliation></author><author><name sortKey="Kosta, Marek" sort="Kosta, Marek" uniqKey="Kosta M" first="Marek" last="Kosta">Marek Kosta</name><affiliation wicri:level="1"><hal:affiliation type="researchteam" xml:id="struct-107895" status="VALID"><idno type="RNSR">201020692C</idno><orgName>Modeling and Verification of Distributed Algorithms and Systems</orgName><orgName type="acronym">VERIDIS</orgName><desc><address><country key="FR"></country></address><ref type="url">http://www.inria.fr/equipes/veridis</ref></desc><listRelation><relation active="#struct-129671" type="direct"></relation><relation active="#struct-300009" type="indirect"></relation><relation active="#struct-423084" type="direct"></relation><relation active="#struct-206040" type="indirect"></relation><relation active="#struct-413289" type="indirect"></relation><relation name="UMR7503" active="#struct-441569" type="indirect"></relation></listRelation><tutelles><tutelle active="#struct-129671" type="direct"><org type="laboratory" xml:id="struct-129671" status="VALID"><idno type="RNSR">198618246Y</idno><orgName>INRIA Nancy - Grand Est</orgName><desc><address><addrLine>615 rue du Jardin Botanique 54600 Villers-lès-Nancy</addrLine><country key="FR"></country></address><ref type="url">http://www.inria.fr/nancy</ref></desc><listRelation><relation active="#struct-300009" type="direct"></relation></listRelation></org></tutelle><tutelle active="#struct-300009" type="indirect"><org type="institution" xml:id="struct-300009" status="VALID"><orgName>Institut National de Recherche en Informatique et en Automatique</orgName><orgName type="acronym">Inria</orgName><desc><address><addrLine>Domaine de VoluceauRocquencourt - BP 10578153 Le Chesnay Cedex</addrLine><country key="FR"></country></address><ref type="url">http://www.inria.fr/en/</ref></desc></org></tutelle><tutelle active="#struct-423084" type="direct"><org type="department" xml:id="struct-423084" status="VALID"><orgName>Department of Formal Methods </orgName><orgName type="acronym">LORIA - FM</orgName><desc><address><country key="FR"></country></address><ref type="url">http://www.loria.fr/la-recherche-en/departements/formal-methods</ref></desc><listRelation><relation active="#struct-206040" type="direct"></relation><relation active="#struct-300009" type="indirect"></relation><relation active="#struct-413289" type="indirect"></relation><relation name="UMR7503" active="#struct-441569" type="indirect"></relation></listRelation></org></tutelle><tutelle active="#struct-206040" type="indirect"><org type="laboratory" xml:id="struct-206040" status="VALID"><idno type="IdRef">067077927</idno><idno type="RNSR">198912571S</idno><idno type="IdUnivLorraine">[UL]RSI--</idno><orgName>Laboratoire Lorrain de Recherche en Informatique et ses Applications</orgName><orgName type="acronym">LORIA</orgName><date type="start">2012-01-01</date><desc><address><addrLine>Campus Scientifique BP 239 54506 Vandoeuvre-lès-Nancy Cedex</addrLine><country key="FR"></country></address><ref type="url">http://www.loria.fr</ref></desc><listRelation><relation active="#struct-300009" type="direct"></relation><relation active="#struct-413289" type="direct"></relation><relation name="UMR7503" active="#struct-441569" type="direct"></relation></listRelation></org></tutelle><tutelle active="#struct-413289" type="indirect"><org type="institution" xml:id="struct-413289" status="VALID"><idno type="IdRef">157040569</idno><idno type="IdUnivLorraine">[UL]100--</idno><orgName>Université de Lorraine</orgName><orgName type="acronym">UL</orgName><date type="start">2012-01-01</date><desc><address><addrLine>34 cours Léopold - CS 25233 - 54052 Nancy cedex</addrLine><country key="FR"></country></address><ref type="url">http://www.univ-lorraine.fr/</ref></desc></org></tutelle><tutelle name="UMR7503" active="#struct-441569" type="indirect"><org type="institution" xml:id="struct-441569" status="VALID"><idno type="ISNI">0000000122597504</idno><idno type="IdRef">02636817X</idno><orgName>Centre National de la Recherche Scientifique</orgName><orgName type="acronym">CNRS</orgName><date type="start">1939-10-19</date><desc><address><country key="FR"></country></address><ref type="url">http://www.cnrs.fr/</ref></desc></org></tutelle></tutelles></hal:affiliation><country>France</country><placeName><settlement type="city">Nancy</settlement><settlement type="city">Metz</settlement><region type="region" nuts="2">Grand Est</region><region type="old region" nuts="2">Lorraine (région)</region></placeName><orgName type="university">Université de Lorraine</orgName></affiliation></author><author><name sortKey="Sturm, Thomas" sort="Sturm, Thomas" uniqKey="Sturm T" first="Thomas" last="Sturm">Thomas Sturm</name><affiliation wicri:level="1"><hal:affiliation type="researchteam" xml:id="struct-107895" status="VALID"><idno type="RNSR">201020692C</idno><orgName>Modeling and Verification of Distributed Algorithms and Systems</orgName><orgName type="acronym">VERIDIS</orgName><desc><address><country key="FR"></country></address><ref type="url">http://www.inria.fr/equipes/veridis</ref></desc><listRelation><relation active="#struct-129671" type="direct"></relation><relation active="#struct-300009" type="indirect"></relation><relation active="#struct-423084" type="direct"></relation><relation active="#struct-206040" type="indirect"></relation><relation active="#struct-413289" type="indirect"></relation><relation name="UMR7503" active="#struct-441569" type="indirect"></relation></listRelation><tutelles><tutelle active="#struct-129671" type="direct"><org type="laboratory" xml:id="struct-129671" status="VALID"><idno type="RNSR">198618246Y</idno><orgName>INRIA Nancy - Grand Est</orgName><desc><address><addrLine>615 rue du Jardin Botanique 54600 Villers-lès-Nancy</addrLine><country key="FR"></country></address><ref type="url">http://www.inria.fr/nancy</ref></desc><listRelation><relation active="#struct-300009" type="direct"></relation></listRelation></org></tutelle><tutelle active="#struct-300009" type="indirect"><org type="institution" xml:id="struct-300009" status="VALID"><orgName>Institut National de Recherche en Informatique et en Automatique</orgName><orgName type="acronym">Inria</orgName><desc><address><addrLine>Domaine de VoluceauRocquencourt - BP 10578153 Le Chesnay Cedex</addrLine><country key="FR"></country></address><ref type="url">http://www.inria.fr/en/</ref></desc></org></tutelle><tutelle active="#struct-423084" type="direct"><org type="department" xml:id="struct-423084" status="VALID"><orgName>Department of Formal Methods </orgName><orgName type="acronym">LORIA - FM</orgName><desc><address><country key="FR"></country></address><ref type="url">http://www.loria.fr/la-recherche-en/departements/formal-methods</ref></desc><listRelation><relation active="#struct-206040" type="direct"></relation><relation active="#struct-300009" type="indirect"></relation><relation active="#struct-413289" type="indirect"></relation><relation name="UMR7503" active="#struct-441569" type="indirect"></relation></listRelation></org></tutelle><tutelle active="#struct-206040" type="indirect"><org type="laboratory" xml:id="struct-206040" status="VALID"><idno type="IdRef">067077927</idno><idno type="RNSR">198912571S</idno><idno type="IdUnivLorraine">[UL]RSI--</idno><orgName>Laboratoire Lorrain de Recherche en Informatique et ses Applications</orgName><orgName type="acronym">LORIA</orgName><date type="start">2012-01-01</date><desc><address><addrLine>Campus Scientifique BP 239 54506 Vandoeuvre-lès-Nancy Cedex</addrLine><country key="FR"></country></address><ref type="url">http://www.loria.fr</ref></desc><listRelation><relation active="#struct-300009" type="direct"></relation><relation active="#struct-413289" type="direct"></relation><relation name="UMR7503" active="#struct-441569" type="direct"></relation></listRelation></org></tutelle><tutelle active="#struct-413289" type="indirect"><org type="institution" xml:id="struct-413289" status="VALID"><idno type="IdRef">157040569</idno><idno type="IdUnivLorraine">[UL]100--</idno><orgName>Université de Lorraine</orgName><orgName type="acronym">UL</orgName><date type="start">2012-01-01</date><desc><address><addrLine>34 cours Léopold - CS 25233 - 54052 Nancy cedex</addrLine><country key="FR"></country></address><ref type="url">http://www.univ-lorraine.fr/</ref></desc></org></tutelle><tutelle name="UMR7503" active="#struct-441569" type="indirect"><org type="institution" xml:id="struct-441569" status="VALID"><idno type="ISNI">0000000122597504</idno><idno type="IdRef">02636817X</idno><orgName>Centre National de la Recherche Scientifique</orgName><orgName type="acronym">CNRS</orgName><date type="start">1939-10-19</date><desc><address><country key="FR"></country></address><ref type="url">http://www.cnrs.fr/</ref></desc></org></tutelle></tutelles></hal:affiliation><country>France</country><placeName><settlement type="city">Nancy</settlement><settlement type="city">Metz</settlement><region type="region" nuts="2">Grand Est</region><region type="old region" nuts="2">Lorraine (région)</region></placeName><orgName type="university">Université de Lorraine</orgName></affiliation></author></analytic><idno type="DOI">10.1007/978-3-642-40885-4_5</idno></biblStruct></sourceDesc></fileDesc><profileDesc><textClass></textClass></profileDesc></teiHeader><front><div type="abstract" xml:lang="en">Data-parallel languages like OpenCL and CUDA are an important means to exploit the computational power of today's computing devices. We consider the compilation of such languages for CPUs with SIMD instruction sets. To generate efficient code, one wants to statically decide whether or not certain memory operations access consecutive addresses. We formalize the notion of consecutivity and algorithmically reduce the static decision to satisfiability problems in Presburger Arithmetic. We introduce a preprocessing technique on these SMT problems, which makes it feasible to apply an off-the-shelf SMT solver. We show that a prototypical OpenCL CPU driver based on our approach generates more efficient code than any other state-of-the-art driver.</div></front></TEI><hal api="V3"><titleStmt><title xml:lang="en">Presburger Arithmetic in Memory Access Optimization for Data-Parallel Languages</title><author role="aut"><persName><forename type="first">Ralf</forename><surname>Karrenberg</surname></persName><email></email><idno type="halauthor">971397</idno><orgName ref="#struct-92733"></orgName><affiliation ref="#struct-397686"></affiliation></author><author role="aut"><persName><forename type="first">Marek</forename><surname>Kosta</surname></persName><email></email><idno type="halauthor">971398</idno><orgName ref="#struct-364443"></orgName><affiliation ref="#struct-107895"></affiliation><affiliation ref="#struct-397675"></affiliation></author><author role="aut"><persName><forename type="first">Thomas</forename><surname>Sturm</surname></persName><email></email><idno type="halauthor">971385</idno><orgName ref="#struct-364443"></orgName><affiliation ref="#struct-107895"></affiliation><affiliation ref="#struct-397684"></affiliation></author><editor role="depositor"><persName><forename>Stephan</forename><surname>Merz</surname></persName><email>Stephan.Merz@loria.fr</email></editor></titleStmt><editionStmt><edition n="v1" type="current"><date type="whenSubmitted">2014-01-16 10:19:06</date><date type="whenModified">2015-09-21 11:12:44</date><date type="whenReleased">2014-01-16 10:19:06</date><date type="whenProduced">2013-09-18</date></edition><respStmt><resp>contributor</resp><name key="104076"><persName><forename>Stephan</forename><surname>Merz</surname></persName><email>Stephan.Merz@loria.fr</email></name></respStmt></editionStmt><publicationStmt><distributor>CCSD</distributor><idno type="halId">hal-00931954</idno><idno type="halUri">https://hal.inria.fr/hal-00931954</idno><idno type="halBibtex">karrenberg:hal-00931954</idno><idno type="halRefHtml">Pascal Fontaine and Christophe Ringeissen and Renate A. Schmidt. 9th International Conference Frontiers of Combining Systems (FroCos 2013), Sep 2013, Nancy, France. Springer, 8152, pp.56-70, 2013, Frontiers of Combining Systems; Lecture Notes in Computer Science. <10.1007/978-3-642-40885-4_5></idno><idno type="halRef">Pascal Fontaine and Christophe Ringeissen and Renate A. Schmidt. 9th International Conference Frontiers of Combining Systems (FroCos 2013), Sep 2013, Nancy, France. Springer, 8152, pp.56-70, 2013, Frontiers of Combining Systems; Lecture Notes in Computer Science. <10.1007/978-3-642-40885-4_5></idno></publicationStmt><seriesStmt><idno type="stamp" n="CNRS">CNRS - Centre national de la recherche scientifique</idno><idno type="stamp" n="INRIA">INRIA - Institut National de Recherche en Informatique et en Automatique</idno><idno type="stamp" n="INRIA-LORRAINE">INRIA Nancy - Grand Est</idno><idno type="stamp" n="LORIA">LORIA - Laboratoire Lorrain de Recherche en Informatique et ses Applications</idno><idno type="stamp" n="LORIA2">Publications du LORIA</idno><idno type="stamp" n="INRIA-NANCY-GRAND-EST">INRIA Nancy - Grand Est</idno><idno type="stamp" n="INRIA_TEST">INRIA - Institut National de Recherche en Informatique et en Automatique</idno><idno type="stamp" n="UNIV-LORRAINE">Université de Lorraine</idno></seriesStmt><notesStmt><note type="audience" n="2">International</note><note type="invited" n="0">No</note><note type="popular" n="0">No</note><note type="peer" n="1">Yes</note><note type="proceedings" n="1">Yes</note></notesStmt><sourceDesc><biblStruct><analytic><title xml:lang="en">Presburger Arithmetic in Memory Access Optimization for Data-Parallel Languages</title><author role="aut"><persName><forename type="first">Ralf</forename><surname>Karrenberg</surname></persName><idno type="halAuthorId">971397</idno><orgName ref="#struct-92733"></orgName><affiliation ref="#struct-397686"></affiliation></author><author role="aut"><persName><forename type="first">Marek</forename><surname>Kosta</surname></persName><idno type="halAuthorId">971398</idno><orgName ref="#struct-364443"></orgName><affiliation ref="#struct-107895"></affiliation><affiliation ref="#struct-397675"></affiliation></author><author role="aut"><persName><forename type="first">Thomas</forename><surname>Sturm</surname></persName><idno type="halAuthorId">971385</idno><orgName ref="#struct-364443"></orgName><affiliation ref="#struct-107895"></affiliation><affiliation ref="#struct-397684"></affiliation></author></analytic><monogr><meeting><title>9th International Conference Frontiers of Combining Systems (FroCos 2013)</title><date type="start">2013-09-18</date><date type="end">2013-09-20</date><settlement>Nancy</settlement><country key="FR">France</country></meeting><editor>Pascal Fontaine and Christophe Ringeissen and Renate A. Schmidt</editor><imprint><publisher>Springer</publisher><biblScope unit="serie"></biblScope><biblScope unit="volume">8152</biblScope><biblScope unit="pp">56-70</biblScope><date type="datePub">2013</date></imprint></monogr><idno type="doi">10.1007/978-3-642-40885-4_5</idno></biblStruct></sourceDesc><profileDesc><langUsage><language ident="en">English</language></langUsage><textClass><classCode scheme="halDomain" n="info.info-lo">Computer Science [cs]/Logic in Computer Science [cs.LO]</classCode><classCode scheme="halTypology" n="COMM">Conference papers</classCode></textClass><abstract xml:lang="en">Data-parallel languages like OpenCL and CUDA are an important means to exploit the computational power of today's computing devices. We consider the compilation of such languages for CPUs with SIMD instruction sets. To generate efficient code, one wants to statically decide whether or not certain memory operations access consecutive addresses. We formalize the notion of consecutivity and algorithmically reduce the static decision to satisfiability problems in Presburger Arithmetic. We introduce a preprocessing technique on these SMT problems, which makes it feasible to apply an off-the-shelf SMT solver. We show that a prototypical OpenCL CPU driver based on our approach generates more efficient code than any other state-of-the-art driver.</abstract></profileDesc></hal></record>Pour manipuler ce document sous Unix (Dilib)
EXPLOR_STEP=$WICRI_ROOT/Wicri/Lorraine/explor/InforLorV4/Data/Hal/Curation
HfdSelect -h $EXPLOR_STEP/biblio.hfd -nk 003C81 | SxmlIndent | more
Ou
HfdSelect -h $EXPLOR_AREA/Data/Hal/Curation/biblio.hfd -nk 003C81 | SxmlIndent | more
Pour mettre un lien sur cette page dans le réseau Wicri
{{Explor lien
|wiki= Wicri/Lorraine
|area= InforLorV4
|flux= Hal
|étape= Curation
|type= RBID
|clé= Hal:hal-00931954
|texte= Presburger Arithmetic in Memory Access Optimization for Data-Parallel Languages
}}
| This area was generated with Dilib version V0.6.33. |  |