×

zbMATH — the first resource for mathematics

Leveraging access mode declarations in a model for memory consistency in heterogeneous systems. (English) Zbl 07161318
Summary: 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.

MSC:
68 Computer science
Software:
SkePU; StarPU
PDF BibTeX XML Cite
Full Text: DOI
References:
[1] Dastgeer, U.; Kessler, C., Smart containers and skeleton programming for GPU-based systems, Int. J. Parallel Program., 44, 3, 506-530 (2016)
[2] Augonnet, C.; Thibault, S.; Namyst, R.; Wacrenier, P.-A., StarPU: A unified platform for task scheduling on heterogeneous multicore architectures, Concurr. Comput., 23, 187-198 (2011)
[3] Enmyren, J.; Kessler, C. W., SkePU: A multi-backend skeleton programming library for multi-GPU systems, (Proc. 4th Int. Workshop on High-Level Parallel Programming and Applications. Proc. 4th Int. Workshop on High-Level Parallel Programming and Applications, HLPP-2010 (2010), ACM: ACM Baltimore, Maryland, USA), 5-14
[4] Li, L.; Kessler, C., VectorPU: A generic and efficient data-container and component model for transparent data transfer on GPU-based heterogeneous systems, (Proc. PARMA-DITAM’17 (2017), ACM), 7-12
[5] Henrio, L.; Kessler, C.; Li, L., Ensuring memory consistency in heterogeneous systems based on access mode declarations, (Loulergue, F.; Couvreur, J.-M., 5th International Symposium on Formal Approaches to Parallel and Distributed Systems, as part of The 16th International Conference on High Performance Computing & Simulation. 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 (2018), IEEE)
[6] Nielson, F.; Nielson, H. R.; Hankin, C., Type and Effect Systems, 283-363 (1999), Springer: Springer Berlin-Heidelberg
[7] de Berg, M.; van Kreveld, M.; Overmars, M.; Schwarzkopf, O., Computational Geometry (2000), Springer · Zbl 0939.68134
[8] Pong, F.; Dubois, M., Verification techniques for cache coherence protocols, ACM Comput. Surv., 29, 1, 82-126 (1997)
[9] Gerth, R., Sequential consistency and the lazy caching algorithm, Distrib. Comput., 12, 2, 57-59 (1999)
[10] Ladkin, P.; Lamport, L.; Olivier, B.; Roegel, D., Lazy caching in TLA, Distrib. Comput., 12, 2, 151-174 (1999)
[11] Barrio-Solórzano, M.; Encarnación Beato, M.; Cuesta, C. E.; de la Fuente, P., Formal verification of coherence for a shared memory multiprocessor model, (Malyshkin, V., Parallel Computing Technologies (2001), Springer: Springer Berlin-Heidelberg), 17-26 · Zbl 0997.68597
[12] Crary, K.; Sullivan, M. J., A calculus for relaxed memory, (Proceedings of the 42nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. Proceedings of the 42nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL ’15 (2015), ACM: ACM New York, NY, USA), 623-636 · Zbl 1346.68048
[13] Bijo, S.; Johnsen, E. B.; Pun, K. I.; Tarifa, S. L.T., An operational semantics of cache coherent multicore architectures, (Proceedings of the 31st Annual ACM Symposium on Applied Computing. Proceedings of the 31st Annual ACM Symposium on Applied Computing, SAC ’16 (2016), ACM: ACM New York, NY, USA), 1219-1224
[14] Bijo, S.; Johnsen, E. B.; Pun, K. I.; Tapia Tarifa, S. L., A maude framework for cache coherent multicore architectures, (Lucanu, D., Rewriting Logic and Its Applications (2016), Springer International Publishing: Springer International Publishing Cham)
[15] Bijo, S.; Johnsen, E. B.; Pun, K. I.; Tapia Tarifa, S. L., A formal model of parallel execution on multicore architectures with multilevel caches, (Proença, J.; Lumpe, M., Formal Aspects of Component Software (2017), Springer International Publishing: Springer International Publishing Cham), 58-77
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.