Analisi automatica di programmi concorrenti e distribuiti

Referente: Prof. Parlato Gennaro

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

1 Omar Inverso, Ermenegildo Tomasco, Bernd Fischer, Salvatore La Torre, Gennaro Parlato: Bounded Verification of Multi-threaded Programs via Lazy Sequentialization. ACM Trans. Program. Lang. Syst. 44(1): 1:1-1:50 (2022)
2 Bernd Fischer, Salvatore La Torre, Gennaro Parlato, Peter Schrammel: CBMC-SSM: Bounded Model Checking of C Programs with Symbolic Shadow Memory. ASE 2022: 156:1-156:5
3 Bernd Fischer, Salvatore La Torre, Gennaro Parlato: VeriSmart 2.0: Swarm-Based Bug-Finding for Multi-threaded Programs with Lazy-CSeq. ASE 2019: 1150-1153
4 Truc L. Nguyen, Peter Schrammel, Bernd Fischer, Salvatore La Torre, Gennaro Parlato: Parallel bug-finding in concurrent programs via reduced interleaving instances. ASE 2017: 753-764
5 Truc L. Nguyen, Bernd Fischer, Salvatore La Torre, Gennaro Parlato: Concurrent Program Verification with Lazy Sequentialization and Interval Analysis. NETYS 2017: 255-271
6 Ermenegildo Tomasco, Truc Lam Nguyen, Bernd Fischer, Salvatore La Torre, Gennaro Parlato: Using Shared Memory Abstractions to Design Eager Sequentializations for Weak Memory Models. SEFM 2017: 185-202
7 Omar Inverso, Truc L. Nguyen, Bernd Fischer, Salvatore La Torre, Gennaro Parlato: Lazy-CSeq: A Context-Bounded Model Checking Tool for Multi-threaded C-Programs. ASE 2015: 807-812
8 Ermenegildo Tomasco, Omar Inverso, Bernd Fischer, Salvatore La Torre, Gennaro Parlato: Verifying Concurrent Programs by Memory Unwinding. TACAS 2015: 551-565
9 Omar Inverso, Ermenegildo Tomasco, Bernd Fischer, Salvatore La Torre, Gennaro Parlato: Bounded Model Checking of Multi-threaded C Programs via Lazy Sequentialization. CAV 2014: 585-602
10 Bernd Fischer, Omar Inverso, Gennaro Parlato: CSeq: A concurrency pre-processor for sequential C verification tools. ASE 2013: 710-713