Analisi automatica di programmi concorrenti e distribuiti

Gruppo di lavoro

• Prof. Salvatore La Torre (Università degli Studi di Salerno);
• Prof. Anna Lisa Ferrara (Università degli Studi del Molise);
• Prof. Marco Faella (Università degli Studi di Napoli Federico II);
• Prof. Bernd Fischer (Stellenbosch Universit);
• Dr. Peter Schrammel (University of Sussex);

Descrizione

Data la diffusione di processori contenenti diversi core, la programmazione concorrente sta diventando una tecnica consolidata di sviluppo del software. Tuttavia, sviluppare programmi concorrenti corretti, scalabili ed efficienti è un compito molto complesso, a causa del gran numero di possibili esecuzioni concorrenti che devono essere considerate. Di conseguenza, i programmi concorrenti spesso contengono bug che sono difficili da individuare, riprodurre e correggere. Sfortunatamente, anche progettare efficienti strumenti automatici di analisi e verifica per sistemi concorrenti è molto complesso in quanto si rende necessario esplorare un gran numero di stati dovuti alla natura non-deterministica di tali sistemi. Le soluzioni presenti in letteratura richiedono una grande quantità di memoria o sono tanto imprecise da esibire diversi falsi positivi. Tuttavia, se da un lato la concorrenza è un problema quando si ragiona riguardo la correttezza dei programmi, dall’altro dà la possibilità di progettare metodi scalabili che sfruttino la grande disponibilità di processori forniti da grandi cluster di computer o piattaforme di cloud. Le tecniche e gli strumenti di verifica formale attualmente disponibili non sono progettati né facilmente adattabili ad ambienti distribuiti. L’obiettivo di questa linea di ricerca è quello di ridurre questo gap tecnologico sviluppando e implementando algoritmi distribuiti per trovare bug in programmi concorrenti o per dimostrare la loro assenza.

Impatto

Il principale impatto accademico di questa linea di ricerca è quello di stabilire all’interno della comunità di verifica, l’idea che gli algoritmi distribuiti per la verifica dei sistemi possono essere un approccio fattibile per ridurre il tempo e il costo necessari per verificare e validare i sistemi. La nostra visione non è solo importante da un punto di vista fondazionale, ma può anche portare all’uso diretto di strumenti di verifica automatica off-the-shelf progettati per programmi concorrenti. Abbiamo quindi intenzione di costruire i nostri strumenti come plugin di verifica disponibile per eventuali altri gruppi di ricerca. Il nostro approccio può anche avere un impatto nell’area dell’IA. In generale, ci aspettiamo che le tecniche che svilupperemo possano essere applicate per la risoluzione di problemi legati al ragionamento automatico in diversi altri domini.

Pubblicazioni