publication . Article . Preprint . 2020

Leveraging access mode declarations in a model for memory consistency in heterogeneous systems

Henrio, Ludovic; Kessler, Christoph; Li, Lu;
Open Access
  • Published: 01 Jan 2020
  • Country: France
Abstract
Abstract 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 heterog...
Subjects
free text keywords: software caching, data transfer, Memory consistency, CPU-GPU heterogeneous systems, cache coherence, [INFO.INFO-DC]Computer Science [cs]/Distributed, Parallel, and Cluster Computing [cs.DC], Computer Science - Distributed, Parallel, and Cluster Computing, Political Science and International Relations, Cultural Studies, Sociology and Political Science, Declaration, Correctness, Mathematics, Software, business.industry, business, Software framework, computer.software_genre, computer, Disjoint sets, Theoretical computer science, Formalism (philosophy), Computation
Funded by
EC| EXA2PRO
Project
EXA2PRO
Enhancing Programmability and boosting Performance Portability for Exascale Computing Systems
  • Funder: European Commission (EC)
  • Project Code: 801015
  • Funding stream: H2020 | RIA
Communities
FET H2020FET HPC: Transition to Exascale Computing
FET H2020FET HPC: Enhancing Programmability and boosting Performance Portability for Exascale Computing Systems

[1] U. Dastgeer, C. Kessler, Smart containers and skeleton programming for GPU-based systems, Int. J. of Par. Progr. 44 (3) (2016) 506{530. doi: 10.1007/s10766-015-0357-6.

[2] C. Augonnet, S. Thibault, R. Namyst, P.-A. Wacrenier, StarPU: A unied platform for task scheduling on heterogeneous multicore architectures, Concurrency and Computation: Practice and Experience 23 (2011) 187{ 198. doi:10.1002/cpe.1631. URL http://hal.inria.fr/inria-00550877

[3] J. Enmyren, C. W. Kessler, SkePU: A multi-backend skeleton programming library for multi-GPU systems, in: Proc. 4th Int. Workshop on High-Level Parallel Programming and Applications (HLPP-2010), Baltimore, Maryland, USA, ACM, 2010, pp. 5{14, doi: 10.1145/1863482.1863487. [OpenAIRE]

[4] L. Li, C. Kessler, VectorPU: A generic and e cient data-container and component model for transparent data transfer on GPU-based heterogeneous systems, in: Proc. PARMA-DITAM'17, ACM., ACM, 2017, pp. 7{12. doi:10.1145/3029580.3029582.

[5] L. Henrio, C. Kessler, L. Li, Ensuring memory consistency in heterogeneous systems based on access mode declarations, in: F. Loulergue, J.-M. Couvreur (Eds.), 5th International Symposium on Formal Approaches to Parallel and Distributed Systems, as part of The 16th International Conference on High Performance Computing & Simulation (HPCS 2018), IEEE, 2018. [OpenAIRE]

[6] F. Nielson, H. R. Nielson, C. Hankin, Type and E ect Systems, Springer Berlin Heidelberg, 1999, pp. 283{363. doi:10.1007/978-3-662-03811-6\ _5.

[7] M. de Berg, M. van Kreveld, M. Overmars, O. Schwarzkopf, Computational Geometry, Second Revised Edition, Springer, 2000.

[8] F. Pong, M. Dubois, Veri cation techniques for cache coherence protocols, ACM Computing Surveys (CSUR) 29 (1) (1997) 82{126. [OpenAIRE]

[9] R. Gerth, Sequential consistency and the lazy caching algorithm, Distributed Computing 12 (2) (1999) 57{59. doi:10.1007/s004460050057. [OpenAIRE]

[10] P. Ladkin, L. Lamport, B. Olivier, D. Roegel, Lazy caching in TLA, Distributed Computing 12 (2) (1999) 151{174. doi:10.1007/s004460050063.

[11] M. Barrio-Solorzano, M. Encarnacion Beato, C. E. Cuesta, P. de la Fuente, Formal veri cation of coherence for a shared memory multiprocessor model, in: V. Malyshkin (Ed.), Parallel Computing Technologies, Springer Berlin Heidelberg, 2001, pp. 17{26. [OpenAIRE]

[12] K. Crary, M. J. Sullivan, A calculus for relaxed memory, in: Proceedings of the 42nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL '15, ACM, New York, NY, USA, 2015, pp. 623{636. doi:10.1145/2676726.2676984. [OpenAIRE]

[13] S. Bijo, E. B. Johnsen, K. I. Pun, S. L. T. Tarifa, An operational semantics of cache coherent multicore architectures, in: Proceedings of the 31st Annual ACM Symposium on Applied Computing, SAC '16, ACM, New York, NY, USA, 2016, pp. 1219{1224. doi:10.1145/2851613.2851718. [OpenAIRE]

[14] S. Bijo, E. B. Johnsen, K. I. Pun, S. L. Tapia Tarifa, A maude framework for cache coherent multicore architectures, in: D. Lucanu (Ed.), Rewriting Logic and Its Applications, Springer International Publishing, Cham, 2016. [OpenAIRE]

[15] S. Bijo, E. B. Johnsen, K. I. Pun, S. L. Tapia Tarifa, A formal model of parallel execution on multicore architectures with multilevel caches, in: J. Proenca, M. Lumpe (Eds.), Formal Aspects of Component Software, Springer International Publishing, Cham, 2017, pp. 58{77.

Abstract
Abstract 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 heterog...
Subjects
free text keywords: software caching, data transfer, Memory consistency, CPU-GPU heterogeneous systems, cache coherence, [INFO.INFO-DC]Computer Science [cs]/Distributed, Parallel, and Cluster Computing [cs.DC], Computer Science - Distributed, Parallel, and Cluster Computing, Political Science and International Relations, Cultural Studies, Sociology and Political Science, Declaration, Correctness, Mathematics, Software, business.industry, business, Software framework, computer.software_genre, computer, Disjoint sets, Theoretical computer science, Formalism (philosophy), Computation
Funded by
EC| EXA2PRO
Project
EXA2PRO
Enhancing Programmability and boosting Performance Portability for Exascale Computing Systems
  • Funder: European Commission (EC)
  • Project Code: 801015
  • Funding stream: H2020 | RIA
Communities
FET H2020FET HPC: Transition to Exascale Computing
FET H2020FET HPC: Enhancing Programmability and boosting Performance Portability for Exascale Computing Systems

[1] U. Dastgeer, C. Kessler, Smart containers and skeleton programming for GPU-based systems, Int. J. of Par. Progr. 44 (3) (2016) 506{530. doi: 10.1007/s10766-015-0357-6.

[2] C. Augonnet, S. Thibault, R. Namyst, P.-A. Wacrenier, StarPU: A unied platform for task scheduling on heterogeneous multicore architectures, Concurrency and Computation: Practice and Experience 23 (2011) 187{ 198. doi:10.1002/cpe.1631. URL http://hal.inria.fr/inria-00550877

[3] J. Enmyren, C. W. Kessler, SkePU: A multi-backend skeleton programming library for multi-GPU systems, in: Proc. 4th Int. Workshop on High-Level Parallel Programming and Applications (HLPP-2010), Baltimore, Maryland, USA, ACM, 2010, pp. 5{14, doi: 10.1145/1863482.1863487. [OpenAIRE]

[4] L. Li, C. Kessler, VectorPU: A generic and e cient data-container and component model for transparent data transfer on GPU-based heterogeneous systems, in: Proc. PARMA-DITAM'17, ACM., ACM, 2017, pp. 7{12. doi:10.1145/3029580.3029582.

[5] L. Henrio, C. Kessler, L. Li, Ensuring memory consistency in heterogeneous systems based on access mode declarations, in: F. Loulergue, J.-M. Couvreur (Eds.), 5th International Symposium on Formal Approaches to Parallel and Distributed Systems, as part of The 16th International Conference on High Performance Computing & Simulation (HPCS 2018), IEEE, 2018. [OpenAIRE]

[6] F. Nielson, H. R. Nielson, C. Hankin, Type and E ect Systems, Springer Berlin Heidelberg, 1999, pp. 283{363. doi:10.1007/978-3-662-03811-6\ _5.

[7] M. de Berg, M. van Kreveld, M. Overmars, O. Schwarzkopf, Computational Geometry, Second Revised Edition, Springer, 2000.

[8] F. Pong, M. Dubois, Veri cation techniques for cache coherence protocols, ACM Computing Surveys (CSUR) 29 (1) (1997) 82{126. [OpenAIRE]

[9] R. Gerth, Sequential consistency and the lazy caching algorithm, Distributed Computing 12 (2) (1999) 57{59. doi:10.1007/s004460050057. [OpenAIRE]

[10] P. Ladkin, L. Lamport, B. Olivier, D. Roegel, Lazy caching in TLA, Distributed Computing 12 (2) (1999) 151{174. doi:10.1007/s004460050063.

[11] M. Barrio-Solorzano, M. Encarnacion Beato, C. E. Cuesta, P. de la Fuente, Formal veri cation of coherence for a shared memory multiprocessor model, in: V. Malyshkin (Ed.), Parallel Computing Technologies, Springer Berlin Heidelberg, 2001, pp. 17{26. [OpenAIRE]

[12] K. Crary, M. J. Sullivan, A calculus for relaxed memory, in: Proceedings of the 42nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL '15, ACM, New York, NY, USA, 2015, pp. 623{636. doi:10.1145/2676726.2676984. [OpenAIRE]

[13] S. Bijo, E. B. Johnsen, K. I. Pun, S. L. T. Tarifa, An operational semantics of cache coherent multicore architectures, in: Proceedings of the 31st Annual ACM Symposium on Applied Computing, SAC '16, ACM, New York, NY, USA, 2016, pp. 1219{1224. doi:10.1145/2851613.2851718. [OpenAIRE]

[14] S. Bijo, E. B. Johnsen, K. I. Pun, S. L. Tapia Tarifa, A maude framework for cache coherent multicore architectures, in: D. Lucanu (Ed.), Rewriting Logic and Its Applications, Springer International Publishing, Cham, 2016. [OpenAIRE]

[15] S. Bijo, E. B. Johnsen, K. I. Pun, S. L. Tapia Tarifa, A formal model of parallel execution on multicore architectures with multilevel caches, in: J. Proenca, M. Lumpe (Eds.), Formal Aspects of Component Software, Springer International Publishing, Cham, 2017, pp. 58{77.

Powered by OpenAIRE Open Research Graph
Any information missing or wrong?Report an Issue
publication . Article . Preprint . 2020

Leveraging access mode declarations in a model for memory consistency in heterogeneous systems

Henrio, Ludovic; Kessler, Christoph; Li, Lu;