Annotation du comportement de verrouillage
Pour éviter des bogues d'accès concurrentiel dans votre programme multithread, suivez toujours une discipline appropriée de verrouillage et utilisez les annotations SAL.
Il est notoirement difficiles à se reproduire, diagnostiquer, et déboguer des bogues d'accès concurrentiel car ils ne sont pas déterministes.Les raisons relatives à l'de thread intercalés sont difficiles à mieux, et sont irréalistes lorsque vous concevez un corps du code qui a plus de quelques thread.Par conséquent, il est conseillé de suivre une discipline verrouillante dans vos programmes multithread.Par exemple, en obéissant un verrou passez commande tout en faisant glisser plusieurs verrous qui aide à éviter des interblocages, et en faisant glisser le verrou gardant approprié avant d'accéder à des aide à une ressource partagée empêché les conditions de concurrence critique.
Malheureusement, il peut être surpris être difficiles à suivre les règles de verrouillage apparemment simples dans la pratique.Une limitation fondamentale dans les langages de programmation et les compilateurs d'aujourd'hui est qu'ils ne prennent pas directement en charge la spécification et l'analyse des spécifications d'accès concurrentiel.Les programmeurs doivent dépendre des commentaires de code informels pour exprimer les intentions sur la manière dont ils utilisent des verrous.
Les annotations SAL d'accès concurrentiel sont conçues pour vous aider à spécifier des effets secondaires verrouillants, la responsabilité verrouillante, la tutelle de données, la hiérarchie de commande de verrouillage, et un autre comportement de verrouillage prévu.En effectuant des règles implicites explicites, les annotations d'accès concurrentiel SAL offrent un moyen cohérent pour que vous documentiez comment votre code utilise des règles de verrouillage.Les annotations d'accès concurrentiel améliorent également la possibilité de les outils d'analyse du code pour rechercher des conditions de concurrence critique, les interblocages, les opérations incompatibles de synchronisation, et d'autres petites erreurs d'accès concurrentiel.
Indications générales
En utilisant des annotations, vous pouvez déclarer les contrats qui sont impliquées par les définitions de fonction entre les implémentations (appelés) et les clients (appelants), word et les invariants et d'autres propriétés de programme qui peut davantage améliorer l'analyse.
SAL Le prend en charge différents types de verrouillage primitif- pour l'exemple, les sections critiques, les mutex, les verrous de rotation, et d'autres objets de ressource.De nombreuses annotations d'accès concurrentiel prennent une expression de verrou comme paramètre.Par convention, un verrouillage est illustré par l'expression du chemin d'accès de l'objet verrou sous-jacent.
Certains threads des règles de propriété de ne pas :
Les verrous de rotation sont des verrous uncounted qui ont la propriété claire de thread.
Mutex et sections critiques sont des verrous numérotés qui ont la propriété claire de thread.
Les sémaphores et les événements sont des verrous numérotés qui n'ont pas la propriété claire de thread.
Annotations de verrouillage
Le tableau suivant répertorie les annotations de verrouillage.
Annotation |
Description |
|---|---|
_Acquires_exclusive_lock_(expr) |
Annote une fonction et indique que dans l'état de publication les index de fonction par un nombre de verrou exclusif sur l'objet lock nommé par expr. |
_Acquires_lock_(expr) |
Annote une fonction et indique que dans l'état de publication que la fonction incrémente par une le nombre de verrous de l'objet lock nommé par expr. |
_Acquires_nonreentrant_lock_(expr) |
Le verrou nommé par expr est entré.Une erreur est signalée si le verrou est déjà maintenu. |
_Acquires_shared_lock_(expr) |
Annote une fonction et indique que dans l'état de publication les index de fonction par un nombre de verrous partagé de l'objet lock nommé par expr. |
_Create_lock_level_(name) |
Une instruction qui déclare le symbole name pour être un niveau de verrou afin qu'il puisse être utilisé dans les annotations _Has_Lock_level_ et _Lock_level_order_. |
_Has_lock_kind_(kind) |
Annote tout objet pour affiner les informations de type d'un objet de ressource.Quelquefois un type commun est utilisé pour différents types de ressources et le type surchargé n'est pas suffisant pour distinguer les spécifications sémantiques entre différentes ressources.Voici une liste de paramètres prédéfinis d' kind :
|
_Has_lock_level_(name) |
Annote un objet lock et lui affecte le verrou de niveau d' name. |
_Lock_level_order_(name1, name2) |
Une instruction qui donne le classement des verrous entre name1 et name2. |
_Post_same_lock_(expr1, expr2) |
Annote une fonction et indique que dans l'état de publication les deux verrous, expr1 et expr2, sont traités comme s'ils ont le même objet lock. |
_Releases_exclusive_lock_(expr) |
Annote une fonction et indique que dans l'état de publication que la fonction décrémente par une le nombre de verrou exclusif sur l'objet lock nommé par expr. |
_Releases_lock_(expr) |
Annote une fonction et indique que dans l'état de publication que la fonction décrémente par une le nombre de verrous de l'objet lock nommé par expr. |
_Releases_nonreentrant_lock_(expr) |
Le verrou nommé par expr est libéré.Une erreur est signalée si le verrou n'est pas actuellement maintenu. |
_Releases_shared_lock_(expr) |
Annote une fonction et indique que dans l'état de publication que la fonction décrémente par une le nombre de verrous partagé de l'objet lock nommé par expr. |
_Requires_lock_held_(expr) |
Annote une fonction et indique que l'état dans pre que le nombre de verrous de l'objet nommé par expr est au moins un. |
_Requires_lock_not_held_(expr) |
Annote une fonction et indique que l'état dans pre que le nombre de verrous de l'objet nommé par expr est zéro. |
_Requires_no_locks_held_ |
Annote une fonction et l'indique que le nombre de verrous de tous les verrous connus au vérificateur sont zéro. |
_Requires_shared_lock_held_(expr) |
Annote une fonction et indique que l'état dans pre que le nombre de verrous partagé de l'objet nommé par expr est au moins un. |
_Requires_exclusive_lock_held_(expr) |
Annote une fonction et indique que l'état dans pre que le nombre de verrou exclusif sur l'objet nommé par expr est au moins un. |
Intrinsèques SAL pour les objets verrouillants non exposés
Certains objets verrous ne sont pas exposés par l'implémentation des fonctions associées de verrouillage.Le tableau suivant répertorie les variables intrinsèques SAL qui activent des annotations sur les fonctions qui opèrent sur ces objets lock non exposés.
Annotation |
Description |
|---|---|
_Global_cancel_spin_lock_ |
Décrit le verrou rotation d'annulation. |
_Global_critical_region_ |
Décrit la zone critique. |
_Global_interlock_ |
Décrit un enclenché des opérations. |
_Global_priority_region_ |
Décrit la zone de priorité. |
Annotations d'Accès aux Données Partagées
Le tableau suivant répertorie les annotations pour l'accès aux données partagées.
Annotation |
Description |
|---|---|
_Guarded_by_(expr) |
Annote une variable et l'indique que toutes les fois que la variable est accessible, le nombre de verrous de l'objet lock nommé par expr est au moins un. |
_Interlocked_ |
Annote une variable et son équivalent à _Guarded_by_(_Global_interlock_). |
_Interlocked_operand_ |
Le paramètre de fonction annoté est l'opérande cible de l'une des différentes fonctions inter-verrouillées.Ces opérandes doivent avoir des propriétés supplémentaires spécifiques. |
_Write_guarded_by_(expr) |
Annote une variable et l'indique que toutes les fois que la variable est modifiée, le nombre de verrous de l'objet lock nommé par expr est au moins un. |
Voir aussi
Référence
Annotation de paramètres de fonction et valeurs de retour
Annotation du comportement d'une fonction
Structs et classes d'annotation
Spécification du moment où une annotation est applicable et dans quel cas
Meilleures pratiques et exemples (SAL)
Concepts
Autres ressources
Utilisation d'annotations SAL pour réduire les défauts du code C/C++