Salvatore LA TORRE | Progetti

MODEL-CHECKING DI PROGRAMMI CONCORRENTI E PARAMETRICI: TECNICHE MULTICORE E COMPLESSITÀ COMPUTAZIONALE

Si propone di investigare risultati teorici e applicazioni nell'ambito della verifica dei programmi concorrenti e parametrici. In particolare, il progetto si articola nei seguenti temi.(1) Trasformazioni di codice finalizzate alla verifica dei programmi.La concorrenza pone una grande sfida per la verifica dei programmi ma offre anche un'opportunità per far scalare una metodologia. Gli algoritmi di verifica sono intrinsecamente sequenziali (esplorazioni di grafi) e i tentativi di migliorarli sfruttando la concorrenza si sono arenati di fronte alla necessità di continue sincronizzazioni tra le componenti. Un approccio di maggior successo ha invece sfruttato il parallelismo offerto dal multicore per eseguire sullo stesso input algoritmi sequenziali differenti e quindi interrompere l'analisi non appena una risposta viene fornita da uno dei processi (swarm approach). In questo progetto, si propone di esplorare un approccio differente in cui si vuole utilizzare uno stesso algoritmo ma su sottoistanze differenti dell'input. L'idea è di sviluppare una trasformazione a livello di codice sorgente che permetta di generare immediatamente un numero arbitrario di istanze di verifica indipendenti che siano significativamente più semplici dell'istanza di partenza e che nel loro complesso coprano tutte le sue computazioni.(2) Realizzazione di strumenti automatici per la verifica di programmi concorrenti. Realizzare tool di verifica robusti richiede risorse notevoli. Un approccio che consente la rapida ed efficace prototipazione di model-checkers per programmi concorrenti è la sequenzializzazione. Una sequenzializzazione è una trasformazione a livello di codice sorgente di un programma concorrente in un programma sequenziale equivalente (in termini della proprietà da verificare). Combinata con un metodo di verifica di programmi sequenziali, genera un metodo di verifica per i programmi concorrenti. Quindi, consente di riutilizzare completamente la tecnologia sviluppata per i programmi sequenziali e focalizzare l'attenzione soltanto sugli aspetti della concorrenza. Si propone di proseguire la ricerca nell'ambito delle sequenzializzazioni di programmi multi-threaded, e in particolare, di migliorare l'efficacia dell'approccio con nuove sequenzializzazioni e l'armonizzazione di quelle esistenti con l'approccio delineato al punto (1). Si procederà quindi ad implementare i nuovi moduli nell'ambito del framework CSeq, e a validare e a valutare sperimentalmente i prototipi di verifica risultanti. Si utlizzeranno i principali benchmark presenti nella letteratura e eventuali ulteriori benchmark ricavati da software reali.(3) Verifica di programmi parametrici.La creazione dinamica di thread nei programmi concorrenti e distribuiti aggiunge un fattore di complessità all’analisi di questi sistemi, in quanto il numero di thread attive in una computazione non è fissato a priori (sistema parametrico). La classe di programmi risultante è molto interessante in pratica (ad esempio, i device drivers che interagiscono con il kernel di un sistema operativo). Si propone di investigare il problema della verifica per questa classe di programmi. In particolare, si prenderanno in esame i modelli di automa pushdown multistack con creazione statica delle thread (un numero di thread arbitrario è creato all'inizio della computazione partendo da un insieme fissato di thread template) e con creazione dinamica delle thread (dynamic pushdown networks, le thread vengono istanziate attraverso transizioni specifiche). Si prenderanno in considerazione le restrizioni del bounded context-switching e scoped già introdotte in letteratura e si studierà la complessità computazionale della raggiungibilità. Oltre alla raggiungibilità, si investigheranno anche specifiche espresse nelle principali logiche temporali. L'obiettivo è quello di effettuare uno studio sistematico dei modelli citati e provare la decidibilità del problema della verifica rispetto a formalismi più espressivi.