UNIVERSITA’ DEGLI STUDI DI ROMA “La Sapienza”FACOLTÀ DI SCIENZE MATEMATICHE, FISICHE E NATURALI

CORSO DI LAUREA SPECIALISTICA IN INFORMATICA

FORMAL VERIFICATION OF PARALLEL COMPUTING:

ISP – IN-SITU MODEL CHECKER

Anno Accademico 2008/2009

RELATOREProf. Enrico TronciProf. Ganesh Gopalakrishnan

CANDIDATOSimone Atzeni

Introduzione

ISP – In-Situ Model Checker

Gestione delle MPI Collective Routine

Conclusioni

I n t r o d u z i o n e

Introduzione

ISP – In-Situ Model Checker

Gestione delle MPI Collective Routine

Conclusioni

I n t r o d u z i o n e

I n t r o d u z i o n e

MPI – Message Passing Interface• standard de-facto per programmi paralleli• impiego su cluster, supercomputer, etc.• API per C/C++/Fortran• semantica complessa delle funzioni

Model Checking• verifica di sistemi concorrenti a stati finiti• riduzione dello spazio degli stati• deadlock• assertion violation• resource leak

1/18

[ I S P – I n - S i t u M o d e l C h e c k e r ]

Introduzione

ISP – In-Situ Model Checker

Gestione delle MPI Collective Routine

Conclusioni

[ I S P – I n - S i t u M o d e l C h e c k e r ]

I S P- I n - S i t u M o d e l C h e c k e r -

Verifica di programmi MPI

Two-Sided Communication

Cattura 45 chiamate MPI

differenti

Individua deadlock,

resource leak, assertion violation

Esplora tutti e solo gli

interleavings rilevanti

2/18

[ I S P – I n - S i t u M o d e l C h e c k e r ]

I S P- I n - S i t u M o d e l C h e c k e r -

Verifica di programmi MPI

Two-Sided Communication

Cattura 45 chiamate MPI

differenti

Individua deadlock,

resource leak, assertion violation

Esplora tutti e solo gli

interleavings rilevanti

2/18

[ I S P – I n - S i t u M o d e l C h e c k e r ]

I S P- I n - S i t u M o d e l C h e c k e r -

Verifica di programmi MPI

Two-Sided Communication

Cattura 45 chiamate MPI

differenti

Individua deadlock,

resource leak, assertion violation

Esplora tutti e solo gli

interleavings rilevanti

2/18

[ I S P – I n - S i t u M o d e l C h e c k e r ]

Una fence è una funzione MPI bloccante, deve essere quindi completata prima che lo stesso processo effettui una qualsiasi altra chiamata MPI.Esempi di fence sono MPI_Barrier, MPI_Wait, MPI_Recv, ecc..

Fence

3/18

1° Passo - Profiler• intercetta le MPI_f fino al raggiungimento di una FENCE per ogni processo

2° Passo - Scheduler• esegue l’algoritmo POE

- se trova un match-set per ogni MPI_f intercettata riprende dal passo 1

P O E- Partial Order reduction avoiding Elusive interleavings -

- altrimenti termina l’esecuzione e segnala il DEADLOCK

Due passi di verifica

[ I S P – I n - S i t u M o d e l C h e c k e r ]

P O E a t w o r k

Process 0 Scheduler

Isend(1,req)

Process 1 Process 2

Barrier

Wait(req)

Irecv(*,req)

Barrier

Recv(2)

Wait(req)

Barrier

Isend(1,req)

Wait(req)

MPI Runtime

Isend(1,req)

sendNext

Barrier

NOFENCEFENCE

4/18

[ I S P – I n - S i t u M o d e l C h e c k e r ]

P O E a t w o r k

Process 0 Scheduler

Isend(1,req)

Process 1 Process 2

Barrier

Wait(req)

Irecv(*,req)

Barrier

Recv(2)

Wait(req)

Barrier

Isend(1,req)

Wait(req)

MPI Runtime

Irecv(*,req)

sendNext

NOFENCEFENCEBarrier

Isend(1,req)Barrier

5/18

[ I S P – I n - S i t u M o d e l C h e c k e r ]

P O E a t w o r k

Process 0 Scheduler

Isend(1,req)

Process 1 Process 2

Barrier

Wait(req)

Irecv(*,req)

Barrier

Recv(2)

Wait(req)

Barrier

Isend(1,req)

Wait(req)

MPI Runtime

Barrier FENCE

Irecv(*,req)Barrier

Isend(1,req)Barrier

6/18

[ I S P – I n - S i t u M o d e l C h e c k e r ]

P O E a t w o r k

Process 0 Scheduler

Isend(1,req)

Process 1 Process 2

Barrier

Wait(req)

Irecv(*,req)

Barrier

Recv(2)

Wait(req)

Barrier

Isend(1,req)

Wait(req)

MPI Runtime

Barrier

Isend(1,req)Barrier

Irecv(*,req)Barrier

MATCH-SET

7/18

[ I S P – I n - S i t u M o d e l C h e c k e r ]

P O E a t w o r k

Process 0 Scheduler

Isend(1,req)

Process 1 Process 2

Barrier

Wait(req)

Irecv(*,req)

Barrier

Recv(2)

Wait(req)

Barrier

Isend(1,req)

Wait(req)

MPI Runtime

sendNext

Barrier

Isend(1,req)Barrier

Irecv(*,req)Barrier

Wait(req)

Recv(2)

Isend(1,req)Wait(req)

FENCE

FENCE

NOFENCEFENCE

8/18

[ I S P – I n - S i t u M o d e l C h e c k e r ]

P O E a t w o r k

Process 0 Scheduler

Isend(1,req)

Process 1 Process 2

Barrier

Wait(req)

Irecv(*,req)

Barrier

Recv(2)

Wait(req)

Barrier

Isend(1,req)

Wait(req)

MPI Runtime

Barrier

Isend(1,req)Barrier

Irecv(*,req)Barrier

Wait(req)

Recv(2)

MATCH-SET

NOMATCH-

SETDEADLOCK

Isend(1,req)Wait(req)

9/18

G e s ti o n e d e l l e M P I C o l l e c ti v e R o u ti n e

Introduzione

ISP – In-Situ Model Checker

Gestione delle MPI Collective Routine

Conclusioni

G e s ti o n e d e l l e M P I C o l l e c ti v e R o u ti n e

C o l l e c ti v e R o u ti n e s B e h a v i o rUna Collective Communication è una comunicazione

che coinvolge tutti i processi in un comunicatore.

MPI Bcast MPI Reduce

MPI Scatter MPI Gather

MPI Barrier

L’MPI Standard definisce le Collective Routine come funzioni bloccanti.

10/18

MPI Bcast e MPI Reduce, sono bloccanti solo per il processo root.

• Risultati sperimentali

• MPI Forum

C o l l e c ti v e R o u ti n e s B e h a v i o r

ISP gestisce ogni Collective Routine come se fosse

bloccante per ogni processo

Modifica dell’algoritmo POE

• process ID == root

11/18

G e s ti o n e d e l l e M P I C o l l e c ti v e R o u ti n e

Problema

int MPI_Bcast(void* message, … , int root, …);

int MPI_Reduce(void* message, … , int root, …, MPI_Op operator, …);

MPI_f è bloccante

MPI_f è non-bloccante• process ID <> root

Non rileva alcuni DEADLOCK nei programmi che utilizzano

MPI Bcast e MPI Reduce

E s e m p i oP0: MPI_Recv(DATA1, from *, ...);

MPI_Reduce(..., ROOT = 0, ...); MPI_Recv(DATA2, from *, ...);printf(..., DATA1, DATA2);

P1: MPI_Send(DATA1 = 10, ..., to P0, ...);MPI_Reduce(..., ROOT = 0, ...);

P2: MPI_Reduce(..., ROOT = 0, ...);MPI_Send(DATA2 = 20, ..., to

P0, ...);

Librerie MPI

• Il programma termina correttamente stampando10 – 20

• Il programma termina correttamente stampando20 - 10

• Il programma non termina a causa di unDEADLOCK

Tre possibili INTERLEAVING

12/18

G e s ti o n e d e l l e M P I C o l l e c ti v e R o u ti n e

P r i m a d e l l a M o d i fi c a- ISP gestisce la Reduce come chiamata BLOCCANTE -

• Fence 1: match tra la prima Receive del Processo 0 e la Send del Processo 1.• Fence 2: match tra le Reduce dei tre processi.• Fence 3: match tra la seconda Receive del Processo 0 e la Send del Processo 2.

Il programma termina correttamente e stampa 10 - 20

13/18

G e s ti o n e d e l l e M P I C o l l e c ti v e R o u ti n e

ISP genera un solo INTERLEAVING

• Fence 1: match tra la prima Receive del Processo 0 e la Send del Processo 1.• Fence 2: match tra le Reduce dei tre processi.• Fence 3: match tra la seconda Receive del Processo 0 e la Send del Processo 2.

ROOT

14/18

G e s ti o n e d e l l e M P I C o l l e c ti v e R o u ti n e

D o p o l a M o d i fi c a- ISP gestisce la Reduce come chiamata non BLOCCANTE -

1° INTERLEAVING

Il programma termina correttamente e stampa 10 - 20

Esplora i 3 possibili interleaving del programma

• Fence 1: match tra la prima Receive del Processo 0 e la Send del Processo 2.• Fence 2: match tra le Reduce dei tre processi.• Fence 3: match tra la seconda Receive del Processo 0 e la Send del Processo 1.

15/18

G e s ti o n e d e l l e M P I C o l l e c ti v e R o u ti n e

Il programma termina correttamente e stampa 20 - 10

D o p o l a M o d i fi c a- ISP gestisce la Reduce come chiamata non BLOCCANTE -

ROOT

2° INTERLEAVING

• Fence 1: match tra la prima Receive del Processo 0 e la Send del Processo 2.• Fence 2: il Processo 2 termina, il Processo 0 è bloccato in attesa di un match con gli altri processi per la Reduce, il Processo 1 è bloccato in attesa di un match per la sua Send.

16/18

G e s ti o n e d e l l e M P I C o l l e c ti v e R o u ti n e

D o p o l a M o d i fi c a- ISP gestisce la Reduce come chiamata non BLOCCANTE -

Il programma non termina e ISP segnala il DEADLOCK

ROOT

3° INTERLEAVING

Introduzione

ISP – In-Situ Model Checker

Gestione delle MPI Collective Routine

Conclusioni

S v i l u p p i F u t u r i

C o n c l u s i o n i

Estendere il numero di chiamate MPI gestite

Sviluppo di ISP Plug-in (Visual Studio e Eclipse)

17/18

Verifica di programmi caratterizzati da un paradigma di comunicazione One-Sided

C o n c l u s i o n i

ISP rappresenta una realizzazione pratica dell’obiettivo dellaVerifica Formale nel contesto del calcolo parallelo

Garantisce Portabilità (Mac OS, Linux,

Windows)

Garantisce Correttezza (no falsi positivi)

Garantisce Completezza (non tralascia

interleaving rilevanti)

18/18

C o n c l u s i o n i

UNIVERSITA’ DEGLI STUDI DI ROMA “La Sapienza”FACOLTÀ DI SCIENZE MATEMATICHE, FISICHE E NATURALI

CORSO DI LAUREA SPECIALISTICA IN INFORMATICA

FORMAL VERIFICATION OF PARALLEL COMPUTING:

ISP – IN-SITU MODEL CHECKER

Anno Accademico 2008/2009

GRAZIE