Annotazione del comportamento di blocco

  • Articolo

Per evitare i bug di concorrenza in un programma multithread, seguire sempre un'appropriata disciplina di blocco e utilizzare le annotazioni SAL.

I bug di concorrenza sono notoriamente difficili da riprodurre, diagnosticare ed eseguire il debug perché non sono deterministici. Il ragionamento sull'interfoliazione dei thread è difficile al meglio e diventa poco pratico quando si progetta un corpo di codice con più di pochi thread. Pertanto, è consigliabile seguire una disciplina di blocco nei programmi multithread. Ad esempio, obbedendo a un ordine di blocco mentre si acquisiscono molteplici blocchi aiuta ad evitare deadlock e acquisendo correttamente la guardia del blocco prima di accedere ad una risorsa condivisa aiuta a impedire una race condition.

Sfortunatamente, queste regole di blocco in apparenza semplici sono sorprendentemente difficili da utilizzare nella pratica. Una limitazione fondamentale nei linguaggi di programmazione e nei compilatori odierni è che non supportano direttamente la specifica e l'analisi dei requisiti di concorrenza. I programmatori devono fare affidamento sui commenti informali del codice per esprime le intenzioni su come utilizzare i blocchi.

Le annotazioni di concorrenza SAL sono progettate per specificare gli effetti collaterali del blocco, la responsabilità del blocco, la tutela di dati, la gerarchia d'ordine e altri comportamenti previsti del blocco. Creando regole implicite esplicite, le annotazioni di concorrenza SAL forniscono un metodo coerente per documentare come il codice utilizza le regole di blocco. Le annotazioni di concorrenza migliorano anche la capacità degli strumenti di analisi del codice di trovare race condition, deadlock, operazioni di sincronizzazione non corrispondenti e altri difficili errori di concorrenza.

Linee guida generali

Usando le annotazioni, è possibile dichiarare i contratti impliciti nelle definizioni di funzione tra implementazioni (chiamate) e client (chiamanti). È anche possibile esprimere invarianti e altre proprietà del programma che possono migliorare ulteriormente l'analisi.

SAL supporta molti tipi diversi di primitive di blocco, come ad esempio le sezioni critiche, i mutex, gli spinlock e altri oggetti risorsa. Molte annotazioni di concorrenza accettano un'espressione di blocco come parametro. Per convenzione, un blocco viene indicato dall'espressione path dell'oggetto lock sottostante.

Alcune regole sulla proprietà dei thread da tenere in considerazione:

  • Gli spinlock sono blocchi non contati che dispongono della proprietà dei thread.

  • I mutex e le sezioni critiche sono blocchi contati che dispongono della proprietà dei thread.

  • I semafori e gli eventi sono blocchi contati che non hanno la proprietà del thread chiaro.

Annotazioni di blocco

Nella tabella seguente sono elencate le annotazioni di blocco.

Annotazione Descrizione
_Acquires_exclusive_lock_(expr) Annota una funzione e indica lo stato successivo della funzione incrementando di uno il conteggio dei blocchi esclusivi dell'oggetto di blocco denominato da expr.
_Acquires_lock_(expr) Annota una funzione e indica lo stato successivo della funzione incrementando di uno il conteggio dei blocchi dell'oggetto di 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) Annota una funzione e indica lo stato successivo della funzione incrementando di uno il conteggio dei blocchi condivisi dell'oggetto di blocco denominato da expr.
_Create_lock_level_(name) Un'istruzione che dichiara il simbolo name come un livello di blocco in modo che possa essere utilizzato nelle annotazioni _Has_Lock_level_ e _Lock_level_order_.
_Has_lock_kind_(kind) Annota qualsiasi oggetto per perfezionare le informazioni sul tipo di un oggetto risorsa. A volte un tipo comune viene usato per diversi tipi di risorse e il tipo di overload non è sufficiente per distinguere i requisiti semantici tra varie risorse. Ecco un elenco di parametri predefiniti kind :

_Lock_kind_mutex_
ID tipo di blocco per mutex.

_Lock_kind_event_
ID tipo di blocco per gli eventi.

_Lock_kind_semaphore_
ID tipo di blocco per semafori.

_Lock_kind_spin_lock_
ID tipo di blocco per i blocchi di selezione.

_Lock_kind_critical_section_
ID tipo di blocco per le sezioni critiche.
_Has_lock_level_(name) Annota un oggetto di blocco e lo fornisce al livello di blocco name.
_Lock_level_order_(name1, name2) Istruzione che fornisce l'ordinamento dei blocchi tra name1 e name2. I blocchi con livello name1 devono essere acquisiti prima dei blocchi con livello name2.
_Post_same_lock_(dst, src) Annota una funzione e indica che in post-state i due blocchi e dst src, vengono considerati come se fossero lo stesso oggetto lock, applicando le proprietà di blocco da src a dst.
_Releases_exclusive_lock_(expr) Annota una funzione e indica lo stato successivo della funzione riducendo di uno il conteggio dei blocchi esclusivi dell'oggetto di blocco denominato da expr.
_Releases_lock_(expr) Annota una funzione e indica lo stato successivo della funzione riducendo di uno il conteggio dei blocchi dell'oggetto di blocco denominato da expr.
_Releases_nonreentrant_lock_(expr) Il blocco denominato da expr viene rilasciato. Se il blocco non è attualmente mantenuto, viene segnalato un errore.
_Releases_shared_lock_(expr) Annota una funzione e indica lo stato successivo della funzione riducendo di uno il conteggio dei blocchi condivisi dell'oggetto di blocco denominato da expr.
_Requires_lock_held_(expr) Annota una funzione e indica che nello stato precedente il conteggio dei blocchi dell'oggetto denominato da expr è di almeno uno.
_Requires_lock_not_held_(expr) Annota una funzione e indica che nello stato precedente il conteggio del blocco dell'oggetto denominato da expr è zero.
_Requires_no_locks_held_ Annota una funzione e indica che il conteggio del blocco è zero in tutti i blocchi noti al controllore.
_Requires_shared_lock_held_(expr) Annota una funzione e indica che nello stato precedente il conteggio dei blocchi condivisi dell'oggetto denominato da expr è di almeno uno.
_Requires_exclusive_lock_held_(expr) Annota una funzione e indica che nello stato precedente il conteggio dei blocchi esclusivi dell'oggetto denominato da expr è di almeno uno.

Intrinseci SAL per oggetti di blocco non esposti

Alcuni oggetti lock non vengono esposti dall'implementazione delle funzioni di blocco associate. Nella tabella seguente sono elencate le variabili intrinseche SAL che abilitano le annotazioni sulle funzioni che operano sugli oggetti di blocco non esposti.

Annotazione Descrizione
_Global_cancel_spin_lock_ Viene descritto lo spin lock di annullamento.
_Global_critical_region_ Viene descritta l'area critica.
_Global_interlock_ Vengono descritte le operazioni con interlock.
_Global_priority_region_ Viene descritta la regione di prioritaria.

Annotazioni di accesso ai dati condivisi

Nella tabella seguente sono elencate le annotazioni per l'accesso ai dati condivisi.

Annotazione Descrizione
_Guarded_by_(expr) Annota una variabile e indica se la variabile è accessibile, il conteggio dei blocchi dell'oggetto di blocco denominato da expr è di almeno uno.
_Interlocked_ Annota una variabile ed è equivalente a _Guarded_by_(_Global_interlock_).
_Interlocked_operand_ Il parametro della funzione con annotazioni è l'operando di destinazione di una delle varie funzioni interlocked. Gli operandi devono avere altre proprietà specifiche.
_Write_guarded_by_(expr) Annota una variabile e indica se la variabile è modificata, il conteggio dei blocchi dell'oggetto di blocco denominato da expr è di almeno uno.

Annotazioni smart lock e RAII

I blocchi intelligenti in genere eseguono il wrapping dei blocchi nativi e gestiscono la loro durata. Nella tabella seguente sono elencate le annotazioni che possono essere usate con blocchi intelligenti e modelli di codifica RAII (Resource Acquisition Is Initialization) con supporto per move la semantica.

Annotazione Descrizione
_Analysis_assume_smart_lock_acquired_(lock) Indica all'analizzatore di presupporre che sia stato acquisito un blocco intelligente. Questa annotazione prevede un tipo di blocco di riferimento come parametro.
_Analysis_assume_smart_lock_released_(lock) Indica all'analizzatore di presupporre che sia stato rilasciato un blocco intelligente. Questa annotazione prevede un tipo di blocco di riferimento come parametro.
_Moves_lock_(target, source) Descrive un'operazione move constructor che trasferisce lo stato di blocco dall'oggetto source all'oggetto target. È target considerato un oggetto appena costruito, quindi qualsiasi stato che aveva prima viene perso e sostituito dallo source stato. viene source anche reimpostato su uno stato pulito senza conteggi di blocchi o destinazione di aliasing, ma gli alias che puntano a esso rimangono invariati.
_Replaces_lock_(target, source) Descrive la move assignment operator semantica in cui viene rilasciato il blocco di destinazione prima di trasferire lo stato dall'origine. È possibile considerarlo come una combinazione di _Moves_lock_(target, source) preceduta da un oggetto _Releases_lock_(target).
_Swaps_locks_(left, right) Descrive il comportamento standard swap , che presuppone che gli oggetti left e right lo scambio dello stato. Lo stato scambiato include il numero di blocchi e la destinazione di aliasing, se presente. Gli alias che puntano agli left oggetti e right rimangono invariati.
_Detaches_lock_(detached, lock) Descrive uno scenario in cui un tipo wrapper di blocco consente l'dissociazione con la risorsa contenuta. È simile a come std::unique_ptr funziona con il puntatore interno: consente ai programmatori di estrarre il puntatore e lasciare il contenitore puntatore intelligente in uno stato pulito. La logica simile è supportata da std::unique_lock e può essere implementata in wrapper di blocco personalizzati. Il blocco scollegato mantiene il proprio stato (numero di blocchi e destinazione di aliasing, se presente), mentre il wrapper viene reimpostato in modo da contenere zero numero di blocchi e nessuna destinazione di aliasing, mantenendone gli alias. Non esiste alcuna operazione sui conteggi dei blocchi (rilascio e acquisizione). Questa annotazione si comporta esattamente come _Moves_lock_ ad eccezione del fatto che l'argomento scollegato deve essere return anziché this.

Vedi anche