Êtes-vous un étudiant de l'EPFL à la recherche d'un projet de semestre?
Travaillez avec nous sur des projets en science des données et en visualisation, et déployez votre projet sous forme d'application sur Graph Search.
En Informatique, les modèles de cohérence sont utilisés dans les systèmes répartis comme les systèmes de mémoire partagée distribuée (DSM) ou les magasins de données distribuées (tels que les système de fichiers, les bases de données, les systèmes de réplication optimiste ou la mise en cache web). On dit que le système supporte un modèle donné si les opérations sur la mémoire suivent des règles spécifiques. Le modèle de cohérence des données spécifie un contrat entre le programmeur et le système, dans lequel le système garantit que si le programmeur suit les règles, la mémoire sera cohérente et les résultats de la lecture, de l'écriture ou de la mise à jour de la mémoire seront prévisibles. Ceci est différent de la cohérence, qui se produit dans les systèmes avec ou sans cache, et qui est la cohérence des données par rapport à tous les processeurs. La cohérence consiste à maintenir un ordre global dans lequel les écritures dans un emplacement unique ou une variable unique sont vues par tous les processeurs. La cohérence concerne l'ordre des opérations sur plusieurs emplacements par rapport à tous les processeurs. Les langages de programmation de haut niveau, tels que C++ et Java, maintiennent partiellement le contrat en traduisant les opérations de mémoire en opérations de bas niveau de manière à préserver la sémantique de la mémoire. Pour respecter le contrat, les compilateurs peuvent réorganiser certaines instructions de mémoire, et les appels de bibliothèque tels que pthread_mutex_lock() encapsulent la synchronisation requise. La vérification de la cohérence séquentielle par vérification de modèles est indécidable en général, même pour les protocoles de cohérence de cache à état fini. Les modèles de cohérence définissent des règles pour l'ordre apparent et la visibilité des mises à jour, et se situent sur un continuum avec des compromis. Supposons que le cas suivant se produise : La ligne X est répliquée sur les nœuds M et N Le client A écrit la ligne X au nœud M Après une période de temps t, le client B lit la ligne X du nœud N Le modèle de cohérence doit déterminer si le client B voit l'écriture effectuée par le client A ou non.
Anastasia Ailamaki, Periklis Chrysogelos, Angelos Christos Anadiotis, Syed Mohammad Aunn Raza
Babak Falsafi, Mathias Josef Payer, Yuanlong Li, Siddharth Gupta, Yunho Oh, Qingxuan Kang, Abhishek Bhattacharjee
Davide Frey, Pierre-Louis Blaise Roman