Salvatore LA TORRE | Progetti

MODELLI E TECNICHE DI VERIFICA DEL SOFTWARE

Si propone l'investigazione di risultati teorici e applicazioni nell'ambito della verifica e della sintesi dei sistemi. In particolare, il progetto si articola nei seguenti temi.(1) Complessità computazionale dei programmi concorrenti.In relazione alla verifica della correttezza dei programmi multithreaded, si prenderanno in considerazione modelli sia con un numero fissato che con un numero illimitato di thread. Entrambe le categorie di modelli sono significative per sistemi digitali reali. Ad esempio: per modellare accuratamente l'esecuzione di device drivers che interagiscono con il kernel di un sistema operativo occorre considerare un numero illimitato di thread; se la creazione di nuove thread non avviene in loop o chiamate di funzioni ricorsive, chiaramente il numero di massimo di thread di una computazione è limitato.Si analizzeranno le versioni con/senza creazione dinamica di thread e si investigheranno soluzioni esatte, dove possibile, oppure in alternativa di tipo bounded. Si prenderanno in considerazione modelli con memoria condivisa di tipo sincrono e asincrono, e "weak" come ad esempio TSO, e nei casi in cui questo dia dei vantaggi computazionali, modelli che limitano la memoria condivisa soltanto ai lock. Per quanto riguarda la modellazione delle singole thread si considereranno programmi con chiamate a funzione ricorsive e non, o altri sistemi di transizione con il problema della raggiungibilità decidibile come ad esempio alcune versioni delle reti di Petri o automi pushdown multistack o higher-order. (2) Implementazione di strumenti automatici per la verifica di programmi concorrenti.Si propone di proseguire la ricerca nell'ambito delle sequenzializzazioni di programmi a thread multiple (con stack e, a memoria condivisa o comunicazione asincrona) che ha come obiettivo il riutilizzo di tool per programmi sequenziali. In particolare, si propongono le seguenti investigazioni. - Per superare l'indecidibilità di fondo della raggiungibilità nei sistemi multithreaded a memoria condivisa (due stack sono sufficienti a simulare una macchina di Turing), sono state introdotte delle tecniche di approssimazione in cui si usano modelli che catturano un sottoinsieme delle computazioni (underapproximation). Le computazioni sono esplorate sulla base di un parametro che limita il numero di interazioni tra le thread. Il parametro più utilizzato è il numero di context-switch nell'interleaving delle singole thread. Si propone di investigare nuovi parametri e estenderli anche a programmi con thread comunicanti attraverso lo scambio di messaggi. - Uno degli aspetti più critici dell'analisi dei sistemi concorrenti è l'elevato numero di interleaving possibili tra le esecuzioni delle singole thread, anche se si opta per tecniche di tipo bounded. Saranno investigate nuove tecniche mirate da un lato a ridurre il numero di interleaving e dall'altro a scomporre la verifica in task separati che possono essere eseguiti in parallelo. L'obiettivo è quello di migliorare la scalabilità dei tool di sequenzializzazione esistenti. - Nelle architetture multicore, non è accurato in generale assumere la consistenza sequenziale della memoria condivisa. Si investigheranno e implementeranno nuovi algoritmi di sequenzializzazione per la verifica di programmi con modello di memoria TSO.(3) Sintesi automatica di programmi. Si propongono la sintesi di programmi sequenziali con chiamate ricorsive a partire da template di moduli indipendenti presi da una libreria. Ogni modulo può essere controllato localmente dando luogo ad una istanza della componente. Una soluzione è composta da un insieme di istanze di componenti che possono chiamarsi vicendevolmente attraverso il meccanismo standard di call-return tipico dei linguaggi di programmazione. Verranno considerate diverse classi di specifiche regolari e visibly pushdown. I programmi sintetizzati saranno corretti per definizione, in quanto saranno costruiti per soddisfare le specifiche date.