Případová studie akcelerace pomocí GPGPU: enumerativní ověřování modelu Jiří Barnat Gfjg ParaDiSe z: == Parallel & Distributed .JI_I Systems Laboratory Technologie CUDA • Levná a dostupná HW akcelerace • Masově rozšířená • Vyžaduje specifický způsob paralelizace algoritmů PV197 2/48 Anotace této případové studie Enumerativní ověřování modelu • Formální verifikace asynchronních paralelních systémů • Výpočetně a prostorově náročná aplikace • Nevyžaduje aritmetiku s pohyblivou desetinnou čárkou • P-úplné algoritmy (nelze snadno efektivně paralelizovat) CBB ParaDiSe _____________,_________________,_______________ _ Sm™:™ • Prostředí s distribuovanou pamětí (výpočetní klastry) • Prostředí se sdílenou pamětí (vícejaderné výpočetní servery) Otázka • Je možné akcelerovat s využitím GP GPU? PV197 3/48 Sekce Enumerativní ověřování modelu PV197 4/48 Schéma metody ověřování modelu Paralelní systém & Graf stavového prostoru channel {byte} c[0]; process A { byte a; state ql,q2,q3; init ql; trans ql^q2 { effect a=a+l; }, q2^q3 { effect a=a+l; }, q3—>ql { sync c!a; effect a=0; }; } process B { byte b,x; state pl,p2,p3,p4; init pl; trans pl^p2 { effect b=b+l; }, p2^p3 { effect b=b+l; }, p3—>pA { sync c?x; }, p4^pl { guard x==b; effect b=0, x=0; }; Příklad konkrétního běhu paralelního programu State: []; A:[ql, a:0]; B:[pl, b:0, x:0] 0 (0.0): ql -> q2 { effect a = a+1; } 1 (1.0): pl -> p2 { effect b = b+1; } Command:! State: []; A:[ql, a:0]; B:[p2, b:l, x:0] 0 (0.0): ql -> q2 { effect a = a+1; } 1 (1.1): p2 -> p3 { effect b = b+1; } Command:! State: []; A:[ql, a:0]; B:[p3, b:2, x:0] 0 (0.0): ql -> q2 { effect a = a^ -i; I Command:0 State: []; A:[q2, a:l]; B:[p3, b:2, x:0] 0 (0.1): q2 -> q3 { effect a = a^ -i; } Command:0 State: []; A:[q3, a:2]; B:[p3, b:2, x:0] 0 (0.2&1.2): q3 -> ql { sync c!a; effect a = 0; } p3 —> p4 { syne c?x; } Command:0 State: []; A:[ql, a:0]; B:[p4, b:2, x:2] PV197 Specifikace vlastností Pozorování • Specifikace vstup/výstupního chování programu nepokrývá mnoho zajímavých vlastností reaktivních a paralelních programů. Lepší způsob specifikace vlastností • Požadavky na vlastnosti každého jednoho běhu systému. • Systém je množina (nekonečných) běhů. • Systém je korektní pokud specifikaci vyhovují všechny běhy. PV197 8/48 Pozorování • Pro popis vlastností jednoho běhu potřebujeme automatizovanou rozhodovací proceduru, která ověří, zda daný nekonečný běh systému má požadovanou vlastnost. Má běh 7T požadovanou vlastnost? a,b b a a,b b b 7T PV197 9/48 Ověřování modelu Pozorování • Pro popis vlastností jednoho běhu potřebujeme automatizovanou rozhodovací proceduru, která ověří, zda daný nekonečný běh systému má požadovanou vlastnost. Má běh 7T požadovanou vlastnost? a,b b a a,b Ověřování modelu s využitím teorie automatů • Biichi automat rozpoznávající neplatné běhy. • Synchronně spuštěn jako monitor se zkoumaným systémem. • Verifikace redukována na problém detekce neplatného běhu. • Detekce dosažitelného akceptujícího cyklu v grafu. PV197 9/48 Sekce Akcelerace detekce akceptujícího cyklu PV197 10/48 Algoritmy pro detekci akceptujících cyklů Sekvenční algoritmy • Rozklad grafu na komponenty • Vnořené prohledávání do hloubky (Nested DFS) • DFS-postorder =>- 0(\V\ + |E|) Paralelní algoritmy • Není známo jak realizovat škálovatelně v čase 0(| V\ + \E\) • Paralelní algoritmy jsou v obecném případě neoptimální • Tvořeny z jednoduchých grafových primitiv, které lze dobře paralelizovat: • dopředná a zpětná dosažitelnost v grafu • topologické třídění • propagace hodnot (value iteration) PV197 11/48 Algoritmus MAP Algoritmus MAP Akceptující stavy, akceptující stavy. PV197 12/48 Algoritmus MAP Uspořádání vrcholů grafu. PV197 12/48 Algoritmus MAP Maximální Akceptující Předchůdci (MAP) map(v) = max{_L, u \ (u, v) G E+ A A(u)} PV197 12/48 Algoritmus MAP map(v) = v =>■ akceptující cyklus PV197 12/48 Algoritmus MAP Co když 2 > 4 ? PV197 12/48 Algoritmus MAP Akceptující cyklus není detekován. PV197 12/48 Algoritmus MAP Pokud není nalezen akceptující cyklus, tak maximální akceptující předchůdci nemohou ležet na cyklu. PV197 12/48 Algoritmus MAP Maximální akceptující vrcholy označeny jako neakceptující. PV197 12/48 Algoritmus MAP Opakuje se dokud není nalezen akceptující cyklus, nebo se odznačí všechny akceptující vrcholy. PV197 12/48 Algoritmus MAP Následné iterace algoritmu mohou být omezeny na podgrafy se stejnou hodnotou funkce MAP. PV197 12/48 Algoritmus MAP - podgrafy Ukázka dekompozice na podgrafy. PV197 13/48 Algoritmus MAP - podgrafy První iterace. Nenalezen akceptující cyklus. Algoritmus MAP - podgrafy Vedoucí maximální vrcholy označeny jako neakceptuj Akceptující vrchol v je vedoucí, pokud Elu : map(u) = PV197 Algoritmus MAP - podgrafy Vedoucí maximální vrcholy označeny jako neakceptuj Akceptující vrchol v je vedoucí, pokud Elu : map(u) = PV197 Algoritmus MAP - podgrafy PV197 13/48 Algoritmus MAP - podgrafy Výpočet map hodnot - malé množství jader Rozdělení grafu. PV197 14/48 Výpočet map hodnot - malé množství jader Každé jádro zpracovává svoji část. PV197 14/48 Výpočet map hodnot - malé množství jader Každé jádro zpracovává svoji část. PV197 14/48 Výpočet map hodnot - malé množství jader Nelokální vrcholy jsou poslány jádrům, které je mají zpracovat. PV197 14/48 Výpočet map hodnot - malé množství jader Graf je zpracováván paralelně. PV197 14/48 Výpočet map hodnot - malé množství jader Graf je zpracováván paralelně. PV197 14/48 Výpočet map hodnot - malé množství jader Graf je zpracováván paralelně. PV197 14/48 Výpočet map hodnot - malé množství jader Dokud není nalezen akceptující cyklus. PV197 14/48 Výpočet map hodnot - velké množství jader Každému vrcholu přiřazeno jedno vlákno. PV197 15/48 Výpočet map hodnot - velké množství jader Vlákno zpracovává všechny příchozí hrany. PV197 15/48 Výpočet map hodnot - velké množství jader Vlákna pracují souběžně. PV197 15/48 Výpočet map hodnot - velké množství jader *K *K SK SK Vlákna pracují souběžně. PV197 15/48 Výpočet map hodnot - velké množství jader Vlákna pracují souběžně. PV197 15/48 Algoritmus MAP jako součin matice s vektorem 1/0 Vi V2 V3 v0 í 0 0 0 0 \ i/i 0 0 10 i/2 110 1 i/3 V 0 0 0 0 / Matice předchůdců PV197 16/48 Algoritmus MAP jako součin matice s vektorem V0 V1 V2 V3 v0 ( 0 0 0 0 \ Ví v2 0 0 10 110 1 i/3 y o o o o / Matice předchůdců m _L _L _L _L Přídavná data na vrchol m - map hodnoty PV197 16/48 Algoritmus MAP jako součin matice s vektorem V0 V1 V2 V3 v0 ( 0 0 0 0 \ Ví v2 0 0 10 110 1 i/3 y o o o o / Matice předchůdců m o _L _L _L _L _L _L _L _L Přídavná data na vrchol o - oldmap hodnoty PV197 16/48 Algoritmus MAP jako součin matice s vektorem V0 V1 V2 V3 v0 ( 0 0 0 0 \ Ví v2 0 0 10 110 1 i/3 y o o o o / Matice předchůdců m Ô A i. i. 0 _L _L 1 J. J. 0 _L _L 1 Přídavná data na vrchol A - akceptující vrcholy PV197 16/48 Algoritmus MAP jako součin matice s vektorem V0 V1 V2 V3 v0 ( 0 0 0 0 \ Ví v2 0 0 10 110 1 i/3 y o o o o / Matice předchůdců m o Á r ±±00 1110 ±±00 ±±10 Přídavná data na vrchol r - příznak modifikace PV197 16/48 Algoritmus MAP jako součin matice s vektorem M V V X PV197 17/48 Algoritmus MAP jako součin matice s vektorem M V V X = \ 1 V'[Í] = E0 maP(v)> u) if Au) ' \max{map(u), map(v)} otherwise. PV197 17/48 Algoritmus MAP jako součin matice s vektorem M V V X = \ 1 V'[f\ = Eo (V3J vq vi y 21/3 m 0 Ä m r /O 0 0 0\ _L _L 0 _L 0 Vl 0 0 10 _L 3 1 1 1 110 1 X 1 3 0 1 0 \0 0 0 0/ _L _L 0 _L 0 Nalezen akceptující cyklus map(vl) = vl PV197 18/48 Sekce Reprezentace a výpočet grafu PV197 19/48 Reprezentace grafu Generování stavového prostoru • Graf je zadán implicitně zdrojovým kódem programu. • Explicitní (maticovou) reprezentaci grafu, je třeba vypočítat. • Orientovaný, řídký graf. • Zpětné hrany nelze vypočítat (kvůli příkazu přiřazení). Reprezentace grafu • Matice souslednosti - prostorově náročná reprezentace. • Matice obsahuje pouze hodnoty 0 a 1. • Zjednodušený Compressed Sparse Row (CSR) formát. PV197 20/48 CSR reprezentace 1 2 3 4 5 1 / 1 O 1 O 0\ 2 0 1 0 0 1 3 0 0 0 1 0 4 0 1 0 0 0 5 \ 1 O O O 1 / PV197 21/48 CSR reprezentace 4 5 1 1 1 / 1 2 3 1/1 1 2 1 3 4 1 5 \ 1 PV197 21/48 CSR reprezentace 4 5 5 4 5/ 1 2 3 1/1 3 2 2 3 4 2 5 \ 1 PV197 21/48 CSR reprezentace 1 2 3 4 5 1/1^3 \ 2 <^2<-5 3 <-4 4 ^2 5 \ 1 <- -5/ PV197 21/48 CSR reprezentace 1 2 3 4 5 1/13 \ 2 2 5 3 4 4 2 5 \ 1 5 / PV197 21/48 CSR reprezentace 1 3 2 5 4 2 1 5 PV197 21/48 CSR reprezentace Mc=( 1 3 ) 2 5 4 2 1 5 PV197 21/48 CSR reprezentace Mc=( 1 3 2 5 ) 4 2 1 5 PV197 21/48 CSR reprezentace Mc=( 1 3 2 5 4 t í 2 1 5 PV197 21/48 CSR reprezentace Mc=( 1 3 2 5 4 2 t í T 1 5 PV197 21/48 CSR reprezentace Mc=( 1 3 2 5.4. 2 1 5 ) t í í t 21/48 CSR reprezentace Mc^l 3^2 5 4 2 1 5 ) Mr=( O ) PV197 21/48 CSR reprezentace Mc=( 1 3 2 5 4 2 1 5 ) í T í Mr=( O 2 ) PV197 21/48 CSR reprezentace Mc=( 1 3 2 5 4 2 1 5 ) T í Mr=( 0 2 4 ) PV197 21/48 CSR reprezentace Mc=( 1 3 2 5 4 2 1 5 ) Mr=( 0 2 4 5 6 ) PV197 21/48 CSR reprezentace / 1 0 1 0 0\ 0 10 0 1 0 0 0 1 0 0 10 0 0 \ 1 0 0 0 1 / Mc=( 1 3 2 5 4 2 1 5 ) Mr=( 0 2 4 5 6 ) PV197 21/48 CSR reprezentace a algoritmus MAP MAP vynucuje enumeraci předchůdců -6L \3X 4>2> ± CSR a MAP problém • Enumerace předchůdců v CSR formátu znamená prohledání celé CSR reprezentace grafu. • Pozorování: Enumerace následníků je v CSR reprezentaci snadná (následnicí vrcholu uloženy v jednom řádku matice). 22/48 CSR reprezentace a algoritmus MAP MAP vynucuje enumeraci předchůdců CSR a MAP řešení #1 • Vlákna místo "stahování" hodnot ostatních vrcholů směrem k sobě, " na hrávaj ľ' své hodnoty k sousedním vrcholům. • Problém souběžného zápisu na cílových vrcholech. PV197 22/48 CSR reprezentace a algoritmus MAP MAP vynucuje enumeraci předchůdců CSR a MAP řešení #2 • Transpozice grafu je zbytečná práce. • Je možné transponovat "algoritmus": MAP —> MAS (Maximální akceptující následník.) • MAS vyžaduje efektivní enumeraci následníků. Výpočet CSR reprezentace Pozorování • CSR reprezentaci je třeba vypočítat. • Část výpočtu není akcelerována pomocí GP GPU. • Negativní dopad na celkové zrychlení dosažené použitím technologie CUDA. Paralelizace výpočtu CSR reprezentace • CSR je možné počítat paralelním CPU algoritmem. • Problém unikátního číslování vrcholů. • Přečíslování pomocí CUDA kernelu: {CPU.ID, N) ->• N PV197 23/48 Časná detekce akceptujícího cyklu Časná detekce akceptujícího cyklu (On-The-Fly verifikace) • Schopnost detekce akceptujícího cyklu bez nutnosti generování kompletního grafu stavového prostoru. • Detekce akceptujícího cyklu v neúplné reprezentaci grafu. Pozorování • Akceptující cyklus je možné detekovat stejným GPU algoritmem i v neúplně vygenerovaném grafu. • Souběžné generování CSR reprezentace na CPU a detekce akceptujícího cyklu na GPU. PV197 24/48 Myšlenka on-the-fly verifikace s využitím GPGPU l/l. "O MAP 0 ^_ 01 time PV197 25/48 Myšlenka on-the-fly verifikace s využitím GPGPU l/l. "O MAP 0 ^_ 01 time PV197 25/48 Myšlenka on-the-fly verifikace s využitím GPGPU l/l. "O MAP 0 ^_ 01 start model checking on partial graph I data transfer time PV197 25/48 Myšlenka on-the-fly verifikace s využitím GPGPU •"i "O MAP 0 ^_ 01 M MAP finished cycle not found new execution time PV197 25/48 Myšlenka on-the-fly verifikace s využitím GPGPU •"i "O MAP 0 ^_ 01 MAP finished cycle not found new execution time PV197 25/48 Myšlenka on-the-fly verifikace s využitím GPGPU •"i "O MAP 0 ^_ 01 an accepting cycle completed in CSR MWKA time PV197 25/48 Myšlenka on-the-fly verifikace s využitím GPGPU •"i "O Ol MAP 0 ^_ 01 Ol MWIWVj MAP finished cycle not found new execution time PV197 25/48 Myšlenka on-the-fly verifikace s využitím GPGPU •"i "O MAP detects the cycle early termination MAP o 4-í CD MWIWVM time PV197 25/48 Sekce Využití více G P GPU karet PV197 26/48 Pamětové nároky na GPU Paměťová náročnost reprezentace • 12B na vrchol (4B CSR + 8B MAP map,oldmap,A,r) • 4B na hranu (CSR) / 1 0 1 0 0\ 0 10 0 1 0 0 0 1 0 0 10 0 0 \ 1 0 0 0 1 / Mc=( 1 3 2 5 4 2 1 5 ) Mr=( 0 2 4 5 6 ) 1 GB GPU karta • 30 miliónů vrcholů, 150 miliónů hran (outdegree 5) • 50 miliónů vrcholů, 100 miliónů hran (outdegree 2) PV197 27/48 Distribuce dat mezi více GPU karet - verze 1 Schéma l.GPU M1 V I_\ 2.GPU M2 V V 3.GPU M-, V V Výhody/Nevýhody • Pouze částečná distribuce. • Jednu iteraci (jedno násobení) je možné kompletně spočítat bez nutnosti další komunikace mezi GPU zařízeními. PV197 28/48 Distribuce dat mezi více GPU karet - verze 1 Schéma l.GPU M1 V V Ť 2.GPU M2 V V 3.GPU M3 V V Výhody/Nevýhody • Pouze částečná distribuce. • Jednu iteraci (jedno násobení) je možné kompletně spočítat bez nutnosti další komunikace mezi GPU zařízeními. • Další iterace vyžadují výměnu dat mezi GPU zařízeními. 28/48 Distribuce dat mezi více GPU karet - verze 2 Schéma l.GPU M1 V 2.GPU M2 V 3.GPU M3 V V Výhody/Nevýhody • Kompletní distribuce dat. • Ani jednu iteraci nelze dokončit bez nutnosti další komunikace mezi GPU zařízeními. PV197 29/48 Přístup k nelokálním vrcholům CSR representation 0 1 2 ; 3 4 5 ; 6 7 12 5 0 8 0 4 5 0 3 7 | 8 | 1 6 | 0 5 l.GPU 2. GPU i 3. GPU Vector of MAP values 0 1 2 3 4 5 6 7 8 l.GPU □ 0 1 2 3 4 5 6 7 8 2. GPU □ 0 1 2 3 4 5 6 7 8 3. GPU 1 PV197 30/48 Přístup k nelokálním vrcholům CSR representation 0 1 2 ; 3 4 5 ; 6 7 l.GPU Vector of MAP values 0 1 2 3 4 5 1. GPU I I I I 3 t 2. GPU I I I I 3. GPU r PV197 30/48 Přístup k nelokálním vrcholům CSR representation 0 1 2 ; 3 4 5 ; 6 7 3. gpu Vector of MAP values 0 12 4 5 8 1. gpu I I I I 0 3 4 5 7 2. gpu Q 0 3. gpu i r JJ □ 5 6 7 □ PV197 30/48 Přístup k nelokálním vrcholům CSR representation Vector of MAP values 0 12 4 5 8 1. GPU I I □□ fj 0 3 4 5 7 2. GPU I I I I I I I I 0 5 6 7 3. GPU (Foreign v 30/48 Kompakce nelokálních vrcholů Pozorování • Výměna všech nelokálních hodnot je drahá. • Výměna pouze požadovaných nelokálních hodnot je obtížná, neboť hodnoty jsou prostorově nespojité. Navržené řešení • Každé zařízení používá kompaktní vektor nelokálních vrcholů. • CSR reprezentace modifikována odpovídajícím způsobem. Foreign vertices CSR representation of edges 1 3 6 7 12 17 33 Compacted vector of foreign vertices PV197 31/48 Kompakce nelokálních vrcholů CSR representation l.GPU Vector of MAP values 0 1 2 Compacted vector 4 5 8 l.GPU 2. GPU 6 7 8 3. GPU [J (Foreign \ PV197 31/48 Příprava kompaktních vektorů nelokálních hodnot Omezení • Modifikace CSR reprezentace je výpočetně náročná, nutno akcelerovat pomocí GPU. • Některé nelokální vrcholy se v CSR opakují! • Nelze použít reduce (protorově náročné) ani AtomicCAS (časově náročné). Řešení • Kompaktní vektor (téměř) lze vytvořit opakovaným hašování do dynamicky rostoucího pole. (CUDA) • Kompaktní vektor se utřídí a ořeže (CPU). • Aktualizuje se CSR (binární prohledávání, CUDA). PV197 32/48 Příprava kompaktních vektorů nelokálních hodnot - demo Příprava kompaktních vektorů nelokálních hodnot - demo Příprava kompaktních vektorů nelokálních hodnot - demo Příprava kompaktních vektorů nelokálních hodnot - demo Příprava kompaktních vektorů nelokálních hodnot - demo Příprava kompaktních vektorů nelokálních hodnot - demo PV197 33/48 Příprava kompaktních vektorů nelokálních hodnot - demo PV197 33/48 Příprava kompaktních vektorů nelokálních hodnot - demo PV197 33/48 Příprava kompaktních vektorů nelokálních hodnot - demo Příprava kompaktních vektorů nelokálních hodnot - demo Příprava kompaktních vektorů nelokálních hodnot - demo CSR representation of edges i o-f~17 o I 1 I 3 J 6 I 7 J 12 J 17 J 33 J Compacted vector of foreign vertices 48 Poznámka o odolnosti vůči znovu-provedení Pozorování • Výpočet hodnot funkce MAP/MAS končí v okamžiku dosažení pevného bodu. • Hodnoty MAP/MAS monotónně rostou. • Znovu-provedení aktualizací nepokazí korektnost. (Maximum z hodnot a jejich maxima je jejich maximum.) Důsledek • Pořadí provedení výpočtů maxim může být libovolné, po dostatečně dlouhém opakování se vždy dosáhne pevného bodu. • Různé strategie pro výměny dat mezi jednotlivými GPU. PV197 34/48 Sekce Použití jiných algoritmů PV197 35/48 Algoritmus OWCTY Princip algoritmu • Alternace topologického třídění a výpočtu relace dosažitelnosti. Princip GPU akcelerace • Akcelerace identickým způsobem jako výpočet funkce MAP. • Operace převedeny na problém násobení matice vektorem, ve vzorečku pro násobení se použijí vhodné matematické operace. • Paměťové nároky algoritmu: 4B na vrchol + CSR. PV197 36/48 Kombinace algoritmů "O OWCTY MAP time PV197 37/48 generator i—1 ro co 2 n > H threads Kombinace algoritmů "O OWCTY MAP 0 01 start model checking on partial graph data transfer time PV197 37/48 Kombinace algoritmů "O OWCTY finished cycle not found OWCTY MAP o CD CD Pyk interrupt IXy1-' request time PV197 37/48 Kombinace algoritmů "O Ol OWCTY MAP 0 i_ 01 Ol rvi MAP finished (enforced) new execution time PV197 37/48 Kombinace algoritmů "O OWCTY MAP 0 01 K/iWI MAP finished cycle not found time PV197 37/48 Kombinace algoritmů "O OWCTY MAP 0 01 OWCTY finished (enforced) new execution time PV197 37/48 Kombinace algoritmů "O OWCTY MAP 0 01 IXAAAA an accepting cycle occured time PV197 37/48 Kombinace algoritmů OWCTY MAP 0 01 Ol both finished cycle not found new execution time PV197 37/48 Kombinace algoritmů "O OWCTY MAP 0 01 OWCTY found cycle early termination rwvwxAj K/iWIWW time PV197 37/48 Sekce Experimentální měření PV197 38/48 Experimentální prostředí Stanice • Linux OS • AMD Phenom(tm) II X4 940 Processor 0 3GHz • 8 GB DDR2 0 1066 MHz RAM • 2x NVIDIA GeForce GTX 280 s 1GB RAM V nových experimentech • GPU GTX480 with 1.5GB VRAM PV197 39/48 Akcelerace algoritmů na GPU (CPU nepoužívá CSR) programy s chybou detekce akceptujícího cyklu (s akceptujícím cyklem) CPU MAP [ ] CPU OWCTY [ ] CUDA MAP I I 40.9(14.4) speedup against MAP(OWCTY) jrogramy bez chyby ; (bez akceptujícího cyklu) CPU MAP [ □ CPU OWCTY [ CUDA MAP Q 61.1(161) speedup against MAP(OWCTY) PV197 40/48 Akcelerace algoritmů na GPU (CPU nepoužívá CSR) generovaní programy s chybou detekce akceptujícího cyklu (s akceptujícím cyklem) CPU MAP 1 1 CPU OWCTY CUDA MAP 1 | 4.92(2.32) speedup against MAP(OWCTY) jrogramy bez chyby ; (bez akceptujícího cyklu) CPU MAP [ □ CPU OWCTY [ CUDA MAP |~J 6.19(14.9) speedup against MAP(OWCTY) PV197 40/48 Dopad použití paralelní konstrukce CSR na MAP state space generation accepting cycle detection Využití více CUDA zařízení - redukce paměti 1 2 4 6 8 10 Number of CUDA devices PV197 42/48 Využití více CUDA zařízení - zpomalení Zpomalení Single Q 1st method C 2nd method ^ cializace ! CUDA výpočet Dopad na celkovou proceduru verifikace Single Q 1st method C 2nd method E ZI CUDA výpočet PV197 43/48 Porovnaní se state-of-the-art (bez akceptujícího cyklu) PV197 44/48 Porovnání se state-of-the-art (s akceptujícím cyklem) PV197 45/48 Sekce Shrnutí PV197 46/48 Závěrem V několika větách ... • Akcelerace samotných algoritmů a grafových primitiv je opodstatněná, nicméně v kontextu celé procedury je diskutabilní, zejména kvůli nákladnému generování grafu. • Akcelerace algoritmů v celočíselné aritmetice. • Dosaženo lepších časů s neoptimálními paralelními algoritmy na GPU, než s optimálními sekvenční algoritmy pracujícími na CPU. Kudy dál? • Jak akcelerovat generování stavového prostoru? • Je to vůbec možné? PV197 47/48 Bibliografie • J. Barnat and P. Bauch and L. Brim and M. Ceska: Designing Fast LTL Model Checking Algorithms for Many-Core GPUs, Journal PDC, 2012. • J. Barnat and P. Bauch and L. Brim and M. Ceska: Employing Multiple CUDA Devices to Accelerate LTL Model Checking 16th International Conference on Parallel and Distributed Systems (ICPADS 2010), IEEE Computer Society, 2010, 259-266. • J. Barnat and L. Brim and M. Ceska and T. Lamr: CUDA accelerated LTL Model Checking 15th International Conference on Parallel and Distributed Systems (ICPADS 2009), IEEE Computer Society, 2009, 34-41. • J. Barnat and L. Brim and M. Ceska: DiVinE-CUDA: A Tool for GPU Accelerated LTL Model Checking Electronic Proceedings in Theoretical Computer Science (PDMC 2009), volume 14, 2009, 107-111. PV197 48/48