Annotazione del comportamento di blocco
Per evitare i bug di concorrenza nel programma multithread, seguire sempre una disciplina appropriata del blocco e utilizzare le annotazioni SAL.
I bug di concorrenza sono notoriamente difficili da riprodurre e diagnosticare, il debug perché non sono deterministici.Ragionando su un'attenta interfoliazione del thread è difficile idealmente e diventa pratico quando si progetta un corpo del codice che ha più di un thread.Di conseguenza, è consigliabile seguire una disciplina di blocco nei programmi multithreading.Ad esempio, obbedendo a un blocco ordini e acquisiscono i blocchi che più consente di evitare deadlock e acquisendo il blocco corretto della custodia prima di accedere alle guide delle risorse condivise impedire race condition.
Sfortunatamente, le regole in apparenza semplici di blocco possono essere sorprendente difficili da utilizzare in pratica.Una limitazione elementare degli odierni linguaggi di programmazione e compilatori è che non supportano direttamente la specifica e l'analisi dei requisiti di concorrenza.I programmatori devono basarsi sui commenti del codice informali per esprimere le intenzioni su come utilizzare i blocchi.
Le annotazioni SAL di concorrenza sono progettate per specificare gli effetti collaterali del blocco, la responsabilità del blocco, la tutela di dati, la gerarchia dell'ordine di blocco e altro comportamento previsto di blocco.Creazione di regole implicite esplicite, le annotazioni di concorrenza di SAL forniscono un metodo coerente per documentino come il codice utilizza le regole di blocco.Le annotazioni di concorrenza agevolano inoltre la possibilità degli strumenti di analisi codice per trovare le race condition, deadlock, le operazioni di sincronizzazione non corrispondenti e altri errori difficili di concorrenza.
Indicazioni generali
Utilizzando le annotazioni, è possibile indicare i contratti coinvolti nelle definizioni di funzioni tra le implementazioni (chiamati) e i client (chiamanti) e word invarianti e altre proprietà programma che è possibile migliorare ulteriormente l'analisi.
Il SAL supporta vari tipi di blocco primitiva-, ad esempio le sezioni critiche, i mutex, gli spinlock e altri oggetti risorsa.Molte annotazioni di concorrenza utilizzano un'espressione di blocco come parametro.Per convenzione, un blocco è indicato dall'espressione del percorso dell'oggetto del blocco sottinteso.
Alcune proprietà del thread regole per ricordare:
Gli spinlock presenti blocchi innumerevoli con chiara proprietà del thread.
Mutex e le sezioni critiche vengono contati blocchi con chiara proprietà del thread.
I semafori e gli eventi vengono contati blocchi che non hanno chiara proprietà del thread.
Annotazioni di blocco
Nella tabella seguente sono elencate le annotazioni di blocco.
Annotazione |
Descrizione |
|---|---|
_Acquires_exclusive_lock_(expr) |
L'annotazione di una funzione e indica che nella postcondizione gli incrementi di funzione da uno il conteggio di blocco esclusivo dell'oggetto del blocco denominato da expr. |
_Acquires_lock_(expr) |
L'annotazione di una funzione e indica che nella postcondizione gli incrementi di funzione da uno il conteggio dei blocchi dell'oggetto del blocco denominato da expr. |
_Acquires_nonreentrant_lock_(expr) |
Il blocco denominato da expr viene acquisito.Viene restituito un errore se il blocco è già utilizzato. |
_Acquires_shared_lock_(expr) |
L'annotazione di una funzione e indica che nella postcondizione gli incrementi di funzione da uno il conteggio dei blocchi condiviso dell'oggetto del blocco denominato da expr. |
_Create_lock_level_(name) |
Un'istruzione che dichiara il simbolo name per essere un livello di blocco in modo da poter utilizzare le annotazioni _Has_Lock_level_ e _Lock_level_order_. |
_Has_lock_kind_(kind) |
L'annotazione di qualsiasi oggetto per migliorare le informazioni sul tipo di un oggetto risorsa.Talvolta un tipo comune viene utilizzato per diversi tipi di risorse e il tipo di overload non è sufficiente per distinguere i requisiti di semantica tra le varie risorse.Di seguito è riportato un elenco di parametri predefiniti di kind :
|
_Has_lock_level_(name) |
Annota un oggetto di blocco e gli fornisce il livello di blocco di name. |
_Lock_level_order_(name1, name2) |
Un'istruzione che fornisce l'ordine di blocco tra name1 e name2. |
_Post_same_lock_(expr1, expr2) |
L'annotazione di una funzione e indica che nella postcondizione i due blocchi, expr1 e expr2, viene considerato come se fossero lo stesso oggetto del blocco. |
_Releases_exclusive_lock_(expr) |
L'annotazione di una funzione e indica che nella postcondizione i decrementi di una funzione dal conteggio di blocco esclusivo dell'oggetto del blocco denominato da expr. |
_Releases_lock_(expr) |
L'annotazione di una funzione e indica che nella postcondizione i decrementi di una funzione dal conteggio dei blocchi dell'oggetto del blocco denominato da expr. |
_Releases_nonreentrant_lock_(expr) |
Il blocco denominato da expr viene rilasciato.Viene restituito un errore se il blocco non è attualmente utilizzato. |
_Releases_shared_lock_(expr) |
L'annotazione di una funzione e indica che nella postcondizione i decrementi di una funzione dal conteggio dei blocchi condiviso dell'oggetto del blocco denominato da expr. |
_Requires_lock_held_(expr) |
L'annotazione di una funzione e che indica che in pre presenta il conteggio dei blocchi dell'oggetto denominato da expr è almeno uno. |
_Requires_lock_not_held_(expr) |
L'annotazione di una funzione e che indica che in pre presenta il conteggio dei blocchi dell'oggetto denominato da expr è zero. |
_Requires_no_locks_held_ |
L'annotazione di una funzione e indica che i conteggi dei blocchi di tutti i blocchi che sono noti al verificatore sono zero. |
_Requires_shared_lock_held_(expr) |
L'annotazione di una funzione e che indica che in pre dichiara il conteggio dei blocchi condiviso dell'oggetto denominato da expr è almeno uno. |
_Requires_exclusive_lock_held_(expr) |
L'annotazione di una funzione e che indica che in pre indica il numero di blocco esclusivo dell'oggetto denominato da expr è almeno uno. |
Gli intrinseci di SAL per gli oggetti non esposti di blocco
Alcuni oggetti del blocco non vengono esposti dall'implementazione delle funzioni collegate di blocco.Nella tabella seguente sono elencate le variabili intrinseche di SAL che attivano le annotazioni sulle funzioni che operano sugli oggetti non esposti di blocco.
Annotazione |
Descrizione |
|---|---|
_Global_cancel_spin_lock_ |
Viene descritto lo spin lock di annullamento. |
_Global_critical_region_ |
Descrive l'area critica. |
_Global_interlock_ |
Vengono descritte le operazioni interlocked. |
_Global_priority_region_ |
Viene descritta la regione con. |
Annotazioni di accesso ai dati condivisi
Nella tabella seguente sono elencate le annotazioni per l'accesso ai dati condivisi.
Annotazione |
Descrizione |
|---|---|
_Guarded_by_(expr) |
L'annotazione di una variabile e indica che ogni volta che la variabile viene eseguito, il conteggio dei blocchi dell'oggetto del blocco denominato da expr è almeno uno. |
_Interlocked_ |
Annota una variabile ed è equivalente a _Guarded_by_(_Global_interlock_). |
_Interlocked_operand_ |
Il parametro di funzione annotato è l'operando di destinazione di una delle diverse funzioni collegate.Gli operandi devono presentare proprietà aggiuntive specifiche. |
_Write_guarded_by_(expr) |
L'annotazione di una variabile e indica che ogni volta che la variabile viene modificata, il conteggio dei blocchi dell'oggetto del blocco denominato da expr è almeno uno. |
Vedere anche
Riferimenti
Annotazione di parametri di funzione e valori restituiti
Annotazione del comportamento delle funzioni
Annotazioni di struct e classi
Specificare dove e quando applicare un'annotazione
Concetti
Altre risorse
Utilizzo delle annotazioni SAL per ridurre gli errori del codice C/C++