P ROGETTO DI I NFORMATICA PER LA MULTIMEDIALITÀ LA CASA FANTASMA di LIA CAPORIN e CLAUDIA SCHIAVOI.
UNIVERSITA DEGLI STUDI DI ROMA La Sapienza F ACOLTÀ DI S CIENZE M ATEMATICHE, F ISICHE E N ATURALI...
-
Upload
edmondo-sole -
Category
Documents
-
view
213 -
download
0
Transcript of UNIVERSITA DEGLI STUDI DI ROMA La Sapienza F ACOLTÀ DI S CIENZE M ATEMATICHE, F ISICHE E N ATURALI...
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