Come posso verificare gli algoritmi senza blocchi?
-
20-09-2019 - |
Domanda
In teoria, dovrebbe essere possibile forza bruta almeno una verifica di un algoritmo senza blocchi (ci sono solo tante combinazioni di chiamate di funzioni intersecano). Ci sono strumenti o processi di ragionamento formali a disposizione per dimostrare che in realtà un algoritmo senza blocchi è corretta (idealmente dovrebbe anche essere in grado di verificare la presenza di condizioni di gara e il problema ABA così)?
Nota: se si conosce un modo per provare un solo punto (ad esempio solo dimostrare che è sicuro dal problema ABA) o un problema che non ho menzionato poi inviare la soluzione in ogni caso. Nel peggiore dei casi, ogni metodo può essere fatto a turno per verificare appieno.
Soluzione
Si dovrebbe provare il modello Spin checker .
Si scrive un modello di programma come in un semplice linguaggio simile al C chiamato promela, che Spin internamente si traduce in una macchina a stati. Un modello può contenere più processi paralleli.
Cosa Spin poi fa è controllare ogni possibile interleaving delle istruzioni da ogni processo di qualunque condizione si desidera eseguire il test - tipicamente, l'assenza di condizioni di gara, la libertà da situazioni di stallo ecc La maggior parte di questi test possono essere facilmente scritti utilizzando le istruzioni assert()
. Se non v'è alcuna possibile sequenza di esecuzione che viola un'affermazione, la sequenza viene stampato, altrimenti si è dato il "via libera".
(Beh, in realtà si utilizza un algoritmo molto più elaborato e più veloce per raggiungere questo obiettivo, ma che è l'effetto. Per impostazione predefinita, tutti gli stati del programma raggiungibili vengono controllati.)
Questo è un incredibile , che ha vinto nel 2001 ACM System Software Award (altri vincitori includono Unix, Postscript, Apache, TeX). Ho iniziato ad usarlo molto rapidamente, e in un paio di giorni è stato in grado di implementare modelli di funzioni MPI_Isend()
MPI e MPI_Irecv()
in promela. Spin trovato un paio di difficile condizioni di gara in un segmento di codice parallelo ho convertito tutto per promela per il test.
Altri suggerimenti
Spin è davvero eccellente, ma prendere in considerazione anche Relacy Race Detector da Dmitriy V'jukov. È costruito appositamente per verificare algoritmi concorrenti tra cui non bloccante algoritmi (attendista / senza blocco). E 'open source e liberamente con licenza.
Relacy fornisce POSIX e Windows primitive di sincronizzazione (mutex, variabili di condizione, semafori, CriticalSections, eventi win32, Interlocked *, ecc), in modo da l'implementazione effettiva C ++ può essere alimentato a Relacy per la verifica. Non c'è bisogno di sviluppare un modello separato del vostro algoritmo con promela e Spin.
Relacy fornisce C ++ 0x std::atomic
(ordinamento memoria esplicita per la vittoria!) In modo da poter utilizzare pre-processore #defines
per scegliere tra l'attuazione del Relacy e la propria piattaforma specifica implementazione atomica ( TBB :: atomica , boost :: atomica, ecc).
La pianificazione è controllabile:. Casuale, legato al contesto, e la ricerca full (tutte le possibili interleavings) disponibili
Ecco un programma di Relacy esempio. Un paio di cose da notare:
- Il
$
è una macro Relacy che registra le informazioni di esecuzione. - bandiere
rl::var<T>
"normale" (non-atomico) le variabili che devono anche essere considerati come parte della verifica.
Il codice:
#include <relacy/relacy_std.hpp>
// template parameter '2' is number of threads
struct race_test : rl::test_suite<race_test, 2>
{
std::atomic<int> a;
rl::var<int> x;
// executed in single thread before main thread function
void before()
{
a($) = 0;
x($) = 0;
}
// main thread function
void thread(unsigned thread_index)
{
if (0 == thread_index)
{
x($) = 1;
a($).store(1, rl::memory_order_relaxed);
}
else
{
if (1 == a($).load(rl::memory_order_relaxed))
x($) = 2;
}
}
// executed in single thread after main thread function
void after()
{
}
// executed in single thread after every 'visible' action in main threads
// disallowed to modify any state
void invariant()
{
}
};
int main()
{
rl::simulate<race_test>();
}
Compila con il compilatore normale (Relacy è solo intestazione-) ed eseguire il file eseguibile:
struct race_test DATA RACE iteration: 8 execution history: [0] 0: atomic store, value=0, (prev value=0), order=seq_cst, in race_test::before, test.cpp(14) [1] 0: store, value=0, in race_test::before, test.cpp(15) [2] 0: store, value=1, in race_test::thread, test.cpp(23) [3] 0: atomic store, value=1, (prev value=0), order=relaxed, in race_test::thread, test.cpp(24) [4] 1: atomic load, value=1, order=relaxed, in race_test::thread, test.cpp(28) [5] 1: store, value=0, in race_test::thread, test.cpp(29) [6] 1: data race detected, in race_test::thread, test.cpp(29) thread 0: [0] 0: atomic store, value=0, (prev value=0), order=seq_cst, in race_test::before, test.cpp(14) [1] 0: store, value=0, in race_test::before, test.cpp(15) [2] 0: store, value=1, in race_test::thread, test.cpp(23) [3] 0: atomic store, value=1, (prev value=0), order=relaxed, in race_test::thread, test.cpp(24) thread 1: [4] 1: atomic load, value=1, order=relaxed, in race_test::thread, test.cpp(28) [5] 1: store, value=0, in race_test::thread, test.cpp(29) [6] 1: data race detected, in race_test::thread, test.cpp(29)
Le versioni recenti di Relacy forniscono anche modelli di memoria Java e CLI se siete in questo genere di cose.
rilevamento corsa dei dati è un problema difficile NP [Netzer & Miller 1990]
ho sentito parlare del Lockset strumenti, e DJit + (che insegnano nel corso CDP). Provate a leggere le diapositive, e googling cosa fanno riferimento a. Esso contiene alcune informazioni interessanti.
Non so quale piattaforma o linguaggio si sta utilizzando - ma sulla piattaforma .Net c'è un progetto di Microsoft Research chiamato Scacchi che sta cercando molto promettente ad aiutare quelli di noi facendo componenti multithreading - tra cui senza blocchi
.Non ho usato una quantità enorme, mente.
Funziona (spiegazione grezzo) da interleaving esplicitamente le discussioni nei più ristretti possibili modi per costringere effettivamente i bug fuori in libertà. Esso analizza anche il codice per trovare gli errori più comuni e modelli cattivi -. Simili a analisi del codice
In passato, ho anche costruito versioni speciali del codice in questione (attraverso blocchi #if ecc) che aggiungono informazioni-tracking dello stato in più; i conteggi, le versioni ecc che posso poi attingere all'interno di un test di unità.
Il problema di questo è che ci vuole molto più tempo per scrivere il codice, e non si può sempre aggiungere questo tipo di cose senza cambiare la struttura sottostante del codice che è già lì.
Se si desidera verificare veramente codice libero-lock (al contrario di testare in modo esauriente un piccolo esempio), è possibile utilizzare VCC ( http://vcc.codeplex.com ), un verificatore deduttivo codice C concorrente che è stato utilizzato per verificare alcuni algoritmi senza blocchi interessanti (es elenchi senza blocchi e hashtables ridimensionabili utilizzando puntatori di pericolo, transazione multiversion ottimistica elaborazione, virtualizzazione MMU, varie primitive di sincronizzazione, ecc). Fa verifica modulare, ed è stato utilizzato per verificare blocchi non banali di codice industriale (fino a circa 20KLOC).
Si noti, tuttavia, che VCC è un verificatore, non uno strumento di bug di caccia; si dovrà fare sostanziale annotazioni sul vostro codice per farlo verificare, e la curva di apprendimento può essere un po 'ripida. Si noti inoltre che assume consistenza sequenziale (come la maggior parte strumenti).
A proposito, peer review non è un buon modo per verificare un algoritmo concomitante (o anche uno sequenziale). C'è una lunga storia di personaggi famosi editoriali algoritmi concorrenti in riviste importanti, solo per avere i bug scoperti anni dopo.