Utilisez la source Luc.
Toutes les notations sont des "clôtures" indiquant qu'une barrière primitive de l'unité centrale a empêché le type de danger de se produire. Ainsi, toutes les lectures/écritures antérieures seront engagées. vers le cache avant la "lecture/écriture" suivante. La "fonction" peut accepter n'importe quelle combinaison/permutation de ces valeurs.
cumul sont documentées dans la section 4.4.2 du document Chats de troupeaux... Il s'agit de clôtures "transitives" qui montrent que tous les threads/cores verront l'ordre.
En effet, comme Hasturkun l'a souligné, il existe huit annotations acceptées par l'Institut de recherche et de développement de l'Union européenne (IRU). CPROVER_fence() . Voir dangers de la wikipedia pour plus de détails, ainsi que d'autres documents cités.
- RRFence, pas un danger spécifique mais pourrait provoquer des événements en cascade
- RWFence, il s'agit d'une anti-dépendance qui pourrait être problématique pour les éléments dépendants.
- WRFence, un risque spécifique n'impliquant qu'une seule variable
- WWFence, un risque de sortie pourrait résulter d'une seule "variable".
- WWcumul
- RRcumul
- RWcumul
- WRcumul
Les versions "cumul" sont similaires aux "clôtures" normales, avec l'ajout que l'ordre est préservé pour tous les cœurs. Par exemple, sur l'unité centrale ARM, toutes les clôtures sont de type "cumul". La "clôture" droite ne concerne que les problèmes de désordre, tels que les tampons de pipeline et/ou d'écriture pour un seul cœur.
Toutes les notations sont des "clôtures" indiquant qu'une barrière primitive de l'unité centrale a empêché le type de danger de se produire. Ainsi, toutes les "lectures/écritures" antérieures seront validées avant les "lectures/écritures" suivantes. La "fonction" peut accepter n'importe quelle permutation de ces valeurs.
Certaines choses, comme un compteur, qui ne dépendent pas d'autres valeurs cohérentes, peuvent fonctionner avec seulement quelques clôtures. Toutefois, d'autres valeurs/tuples/structures sont à adresses multiples (non atomiques à charger/stocker) et peuvent nécessiter que plusieurs valeurs soient lues/écrites de manière cohérente. Une taxonomie des accès interdépendants Tableau III. Glossaire des noms des épreuves décisives de Chats de troupeaux... .
La page, Vérification des logiciels pour les mémoires faibles CProver est une pierre de Rosette pour ce sujet. Il se réfère principalement à l'outil "musketeer", mais une lecture plus approfondie montrera que de nombreux concepts sont incorporés dans l'outil CBMC. Même l'URL de la page contient 'wmm' qui se trouve également dans le répertoire 'goto-instrument' en tant que 'wmm' où cette fonctionnalité est implémentée.
Le répertoire cbmc-monnaie y ansi-c ont de nombreux exemples d'utilisation de la CPROVER_fence() et d'autres primitives de modélisation de la mémoire.
Exemple de code de démonstration en C à mettre en œuvre pthread_mutex_lock() pour l'analyse,
inline int pthread_mutex_lock(pthread_mutex_t *mutex)
{
__CPROVER_HIDE:;
#ifdef __CPROVER_CUSTOM_BITVECTOR_ANALYSIS
__CPROVER_assert(__CPROVER_get_must(mutex, "mutex-init"),
"mutex must be initialized");
__CPROVER_assert(!__CPROVER_get_may(mutex, "mutex-destroyed"),
"mutex must not be destroyed");
__CPROVER_assert(__CPROVER_get_must(mutex, "mutex-recursive") ||
!__CPROVER_get_may(mutex, "mutex-locked"),
"attempt to lock non-recurisive locked mutex");
__CPROVER_set_must(mutex, "mutex-locked");
__CPROVER_set_may(mutex, "mutex-locked");
__CPROVER_assert(*((__CPROVER_mutex_t *)mutex)!=-1,
"mutex not initialised or destroyed");
#else
__CPROVER_atomic_begin();
__CPROVER_assume(!*((__CPROVER_mutex_t *)mutex));
*((__CPROVER_mutex_t *)mutex)=1;
__CPROVER_atomic_end();
__CPROVER_fence("WWfence", "RRfence", "RWfence", "WRfence",
"WWcumul", "RRcumul", "RWcumul", "WRcumul");
#endif
return 0; // we never fail
}
J'ai cru comprendre qu'il s'agissait d'un contrôle,
- une seule serrure
- est initialisé avant l'appel
- le verrou n'est pas détruit lorsqu'il est maintenu
- le verrou n'est pas réinitialisé tant qu'il est maintenu
- tous les éléments de mémoire à ordre faible sont résolus (tous les caches sont vidés) après l'appel.
Intéressant, man pthread_mutex_lock() ne dit rien sur la synchronisation des CPU ou les clôtures. Nous avons l'inversion de priorité, le blocage, etc. avec la programmation des mutex/blocs, mais cela a aussi un prix sur la performance du pipeline. En effet, sur ARM/Linux/glibc, kuser_cmpxchg32_fixup appel smp_dmb arm pour satisfaire à cette exigence. Un test de régression similaire montre des échecs de pthread_create() où un tampon d'écriture pourrait laisser une valeur dans un état indéterminé au démarrage du thread initial, à moins qu'une barrière ne soit insérée en tant que pthread_create() n'a pas cette synchronisation.
Il semble que ces travaux soient assez récents (selon certains critères), avec des documents datant de 2013 et l'engagement de l'UCR Linux en 2016. Il est possible que les auteurs souhaitent que l'API reste fluide. Ils sont probablement plus concentrés sur la tâche plus agréable de prouver les prouveurs et n'ont pas eu le temps de documenter cette interface.
Nota: Les versions antérieures de la réponse supposaient que la synchronisation du cache avec les maîtres de bus non mis en cache était couverte par cette API. Ce n'est pas le cas. Les programmeurs système qui essaient d'utiliser cbmc de faire appel à d'autres mécaniciens, si cela vous préoccupe.
