Ricerca | Progetti Finanziati

VERIFICA DI SOFTWARE CONCORRENTE EMBEDDED E CON MODELLI DI MEMORIA RILASSATI

Si propone l'investigazione di risultati teorici e applicazioni nell'ambito della verifica dei programmi concorrenti attraverso le sequenzializzazioni. In particolare, il progetto si articola nei seguenti temi. (1) Programmi embedded con task periodici. I programmi embedded sono caratterizzati dall'esecuzione concorrente di task che sono innescati da interrupt e eventi, o schedulati periodicamente. Inoltre, la schedulazione avviene anche in base alle priorità dei task e l'eseguibilità di un task con maggiore priorità può causare o meno la preemption del task correntemente eseguito. Le sequenzializzazioni sono state pensate per singole applicazioni multithreaded assumendo una semantica per interleaving. Una maniera semplice per adattare le sequenzializzazioni esistenti ai programmi embedded è quella di implementare esplicitamente lo scheduler come una thread del programma e quindi procedere alla sequenzializzazione. Questo però comporta l'utilizzo di strutture dati (code, stack,etc.) che possono minare la scalabilità dell'approccio. Per i sistemi real-time un approccio standard è quello di modellare un clock discreto condiviso tra le thread. La modellazione esplicita del clock potrebbe ridurre l'efficienza del metodo e quando possibile implementazioni implicite del tempo sono da preferirsi. Si propone di investigare una maniera efficiente per combinare l'interleaving tra le thread, la gestione delle priorità e gli aspetti real-time della classe di programmi considerata. Infine, si osserva che un ulteriore aspetto critico è la numerosità dei task in applicazioni di livello industriale. (2) Modelli rilassati di memoria (weak memory models). I modelli rilassati della memoria possono essere catturati in termini del modello di consistenza sequenziale (dove ogni aggiornamento della memoria condivisa è immediatamente visibile in tutto il sistema) con l'opportuno utilizzo di struture dati quali ad esempio code e array. Una simulazione diretta dei modelli rilassati in genere impatta la scalabilità del metodo di verifica. Si propone di investigare opportune strutture dati per ottenere estensioni efficienti dei principali algoritmi di sequenzializzazione per catturare la semantica dei modelli rilassati di memoria quali TSO e PSO. In particolare, la ricerca si concentrerà sull'approccio lazy e quello basato sul memory unwinding (MU) implementati nel tool CSeq. Per una maggiore modularità e intercambiabilità degli approcci, si intende strutturare la soluzione in modo da avere una netta separazione tra l'algoritmo di sequenzializzazione e l'implementazione della memoria condivisa. Questo potrebbe essere ottenuto attraverso la definizione di un interfaccia (nel senso della programmazione object-oriented) che contenga tutte le primitive inerenti l'interazione con la memoria condivisa e le altre thread. Un'ulteriore direzione di ricerca riguarderà l'investigazione teorica delle proprietà dei modelli introdotti. (3) Correttezza dei programmi. La sequenzializzazione si è dimostrato in pratica un approccio molto effettivo per l'individuazione dei bug nei programmi concorrenti. Questo è particolarmente vero quando le sequenzializzazioni sono usate in combinazione con il bounded model-checking. In generale, tranne per alcune classi di sistemi (ad es. memoria asincrona, well-nested lock, scheduling deterministico), le sequenzializzazioni esistenti forniscono una sotto-approssimazione del programma concorrente (il programma sequenziale risultante cattura un sottoinsieme delle computazioni del programma originale) e quindi non possono essere utilizzate per dimostrare l'assenza di bug. Si propone l'investigazione di nuovi algoritmi di sequenzializzazione che possano funzionare bene anche per un'analisi unbounded, e che quindi consentano di catturare tutte le computazioni del programma di partenza. Gli algoritmi saranno poi implementati nel tool CSeq e eventualmente adattati al backend scelto per una migliore scalabilità.