Static analysis via abstract interpretation of multithreaded programs

L’obiettivo di questa tesi è di presentare un’analisi statica generica per programmi Java multithread. Un programma multithread esegue molteplici task, chiamati thread, in parallelo. I thread comunicano implicitamente attraverso una memoria condivisa, e si sincronizzano attraverso monitor, primitive wait-notify, etc... Le prime architetture dual-core sono apparse sul mercato a prezzi contenuti alcuni anni fa; oggi praticamente tutti i computer sono almeno dual-code. L’attuale trend di mercato è addirittura quello del many-core, ovvero di aumentare sempre di più il numero di core presenti su una CPU. Alcune nuove sfide sono state introdotte da questa rivoluzione multicore a livello di linguaggi di programmazione, dal momento che gli sviluppatori software devono implementare programmi multithread. Questo pattern di programmazione è supportato nativamente dalla maggior parte dei linguaggi di programmazione moderni come Java e C#. Lo scopo dell’analisi statica è di calcolare automaticamente e in maniera conservativa una serie di informazioni sul comportamento a tempo di esecuzione di un programma; una sua applicazione è lo sviluppo di strumenti che aiutino a trovare e correggere errori software. In questo campo svariati approcci sono stati proposti: nel corso della tesi verr`a seguita le teoria dell’interpretazione astratta, un approccio matematico che permette di definire e approssimare correttamente la semantica dei programmi. Questa metodologia è già stata utilizzata con successo per l’analisi di un vasto insieme di linguaggi di programmazione. Gli analizzatori generici possono essere instanziati con diversi domini numerici e applicati a svariate proprietà. Negli ultimi anni numerosi lavori sono stati centrati su questo approccio, e alcuni di essi sono stati utilizzati con successo in contesto industriale. Il loro punto di forza è il riutilizzo della maggior parte dell’analizzatore per verificare molteplici proprietà, e l’utilizzo di diversi domini numerici permette di ottenere analisi più veloci ma più approssimate, oppure più precise ma più lente. Nel corso di questa tesi presenteremo un analizzatore generico per programmi multithread. Definiremo innanzitutto il modello di memoria happens-before sotto forma di punto fisso e lo approssimeremo con una semantica che sia calcolabile. Un modello di memoria definisce quali comportamenti di un programma multithread sono consentiti durante la sua esecuzione. A partire da una definizione informale del modello di memoria happensbefore, introdurremo una semantica che costruisca tutte le esecuzioni finite che rispettino tale modello di memoria; in tale contesto un’esecuzione è rappresentata come una funzione che associa ciascun thread ad una traccia di stati che rappresenta la sua esecuzione. Introdurremo infine una semantica astratta che pu`o essere calcolata, provandone la correttezza formalmente. Definiremo e approssimeremo quindi una nuova proprietà focalizzata sui comportamenti non deterministici causati dall’esecuzione multithread (ad esempio dall’intercalarsi arbitrario durante l’esecuzione in parallelo di diversi thread). Prima di tutto, il non determinismo di un programma multithread è definito come di erenza tra esecuzioni. Un programma è non deterministico se due diverse esecuzioni espongono comportamenti di erenti a causa dei valori letti e scritti sulla memoria condivisa. Astrarremo quindi tale proprietà su due livelli: inizialmente tracceremo per ogni thread il valore astratto che potrebbe aver scritto sulla o letto dalla memoria condivisa. Al successivo passo di astrazione tracceremo un solo valore, che approssimerà tutti i possibili valori scritti in parallelo, e l’insieme dei thread che potrebbero aver fatto ciò. Sul primo livello di astrazione definiremo poi il concetto di determinismo debole. Proporremo quindi diverse modalità di rilassamento di tale proprietà, in particolare proiettandola su un sottoinsieme delle traccie di esecuzione e degli stati, definendo una gerarchia complessiva. Infine studieremo come la presenza di data race possa influenzare il determinismo di un programma. Tutto questo lavoro teorico verrà quindi applicato a programmi Java. In particolare definiremo una semantica concreta del linguaggio Java bytecode seguendo la sua specifica. Quindi lo approssimeremo in maniera da astrarre precisamente le informazioni richieste per poter analizzare un programma multithread. Il fulcro di ciò è l’approssimazione degli indirizzi di memoria per poter identificare i diversi thread, per controllare gli accessi alla memoria condivisa e per poter scoprire quando due thread sono sempre sincronizzati su uno stesso monitor e quindi quali parti di codice non possono essere eseguite in parallelo. L’analizzatore generico definito fin qui formalmente è stato implementato in heckmate, il primo analizzatore generico di programmi Java multithread. Riporteremo e studieremo approfonditamente i risultati sperimentali: in particolare verrà studiata la precisione dell’analisi quando utilizzata su alcuni pattern comuni di programmazione concorrente e alcuni casi di studio, e le sue prestazioni quando eseguita su un’applicazione incrementale e su un insieme di benchmark esterni. L’ultimo contributo della tesi sarà l’estensione di un analizzatore generico industriale esistente (Clousot) all’analisi degli accessi e ettuati tramite puntatori diretti alla memoria. In questa parte finale presenteremo l’applicazione di un analizzatore generico ad una proprietà di interesse pratico su codice industriale, mostrando quindi la forza di questo tipo di approccio allo scopo di costruire strumenti utili per sviluppare software.