nach oben

Erschienen in:

2021 | OriginalPaper | Buchkapitel

Towards a Spatial Model Checker on GPU

verfasst von : Laura Bussi, Vincenzo Ciancia, Fabio Gadducci

Erschienen in: Formal Techniques for Distributed Objects, Components, and Systems

Verlag: Springer International Publishing

Einloggen

Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.

search-config

KI-gestützte Suche

Aus

Abstract

The tool VoxLogicA merges the state-of-the-art library of computational imaging algorithms ITK with the combination of declarative specification and optimised execution provided by spatial logic model checking. The analysis of an existing benchmark for segmentation of brain tumours via a simple logical specification reached very high accuracy. We introduce a new, GPU-based version of VoxLogicA and present preliminary results on its implementation, scalability, and applications.

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

über 102.000 Bücher
über 537 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Finance + Banking
Management + Führung
Marketing + Vertrieb
Maschinenbau + Werkstoffe
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 390 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Maschinenbau + Werkstoffe

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 340 Zeitschriften

aus folgenden Fachgebieten:

Bauwesen + Immobilien
Business IT + Informatik
Finance + Banking
Management + Führung
Marketing + Vertrieb
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Vorheriges Kapitel Off-the-Shelf Automated Analysis of Liveness Properties for Just Paths

Nächstes Kapitel Formal Verification of HotStuff

VoxLogicA: see https://github.com/vincenzoml/VoxLogicA.

VoxLogicA-GPU is Free and Open Source software. Its source code is currently available at https://github.com/vincenzoml/VoxLogicA/tree/experimental-gpu.

FSharp: see https://fsharp.org. NET Core: see https://dotnet.microsoft.com. OpenCL: see https://www.khronos.org/opencl. ITK: see https://itk.org.

Pointer jumping or path doubling is a design technique for parallel algorithms that operate on pointer structures, such as linked lists and directed graphs. It allows an algorithm to follow paths with a time complexity that is logarithmic with respect to the length of the longest path. It does this by “jumping” to the end of the path computed by neighbors. See https://en.wikipedia.org/wiki/Pointer_jumping.

See e.g. https://en.wikipedia.org/wiki/MapReduce.

Since checking termination takes log(N) iterations, instead of waiting for mainIteration to converge, reconnect is called each k iterations (\(k = 8\) in the current implementation, which experimentally proved to be a reasonable compromise).

All the tests we present, and the script to run them, are available in the source code repository https://github.com/vincenzoml/VoxLogicA/tree/experimental-gpu.

Allegretti, S., Bolelli, F., Grana, C.: Optimized block-based algorithms to label connected components on GPUs. IEEE Trans. Parallel Distrib. Syst. 31(2), 423–438 (2020)CrossRef

Bakas, S., et al.: Advancing the cancer genome atlas glioma MRI collections with expert segmentation labels and radiomic features. Sci. Data 4, 1–13 (2017)CrossRef

Banci Buonamici, F., Belmonte, G., Ciancia, V., Latella, D., Massink, M.: Spatial logics and model checking for medical imaging. Softw. Tools Technol. Transf. 22(2), 195–217 (2020). https://doi.org/10.1007/s10009-019-00511-9CrossRef

Bartocci, E., Bortolussi, L., Loreti, M., Nenzi, L.: Monitoring mobile and spatially distributed cyber-physical systems. In: Talpin, J., Derler, P., Schneider, K. (eds.) MEMOCODE 2017, pp. 146–155. ACM (2017)

Bartocci, E., Gol, E., Haghighi, I., Belta, C.: A formal methods approach to pattern recognition and synthesis in reaction diffusion networks. IEEE Trans. Control Netw. Syst. 5(1), 308–320 (2016)MathSciNetCrossRef

Belmonte, G., Broccia, G., Ciancia, V., Latella, D., Massink, M.: Feasibility of spatial model checking for nevus segmentation. In: Bliudze, S., Semini, L. (eds.) FORMALISE@ICSE 2021 (2021, to appear)

Belmonte, G., Ciancia, V., Latella, D., Massink, M.: VoxLogicA: a spatial model checker for declarative image analysis. In: Vojnar, T., Zhang, L. (eds.) TACAS 2019. LNCS, vol. 11427, pp. 281–298. Springer, Cham (2019). https://doi.org/10.1007/978-3-030-17462-0_16CrossRef

Berkovich, S., Bonakdarpour, B., Fischmeister, S.: GPU-based runtime verification. In: IPDPS 2013, pp. 1025–1036. IEEE Computer Society (2013)

Broccia, G., Milazzo, P., Ölveczky, P.C.: Formal modeling and analysis of safety-critical human multitasking. Innovations Syst. Softw. Eng. 15(3–4), 169–190 (2019). https://doi.org/10.1007/s11334-019-00333-7CrossRef

10.

Bussi, L., Ciancia, V., Gadducci, F.: A spatial model checker in GPU (extended version). CoRR abs/2010.07284 (2020)

11.

Ciancia, V., Latella, D., Massink, M., Paškauskas, R., Vandin, A.: A tool-chain for statistical spatio-temporal model checking of bike sharing systems. In: Margaria, T., Steffen, B. (eds.) ISoLA 2016. LNCS, vol. 9952, pp. 657–673. Springer, Cham (2016). https://doi.org/10.1007/978-3-319-47166-2_46CrossRef

12.

Ciancia, V., Gilmore, S., Grilletti, G., Latella, D., Loreti, M., Massink, M.: Spatio-temporal model checking of vehicular movement in public transport systems. Softw. Tools Technol. Transf. 20(3), 289–311 (2018). https://doi.org/10.1007/s10009-018-0483-8CrossRef

13.

Grosu, R., Smolka, S., Corradini, F., Wasilewska, A., Entcheva, E., Bartocci, E.: Learning and detecting emergent behavior in networks of cardiac myocytes. Commun. ACM 52(3), 97–105 (2009)CrossRef

14.

Gustafson, J.L.: Reevaluating Amdahl’s law. Commun. ACM 31(5), 532–533 (1988)CrossRef

15.

Ma, M., Bartocci, E., Lifland, E., Stankovic, J., Feng, L.: SaSTl: spatial aggregation signal temporal logic for runtime monitoring in smart cities. In: ICCPS 2020, pp. 51–62. IEEE (2020)

16.

Neele, T., Wijs, A., Bošnački, D., van de Pol, J.: Partial-order reduction for GPU model checking. In: Artho, C., Legay, A., Peled, D. (eds.) ATVA 2016. LNCS, vol. 9938, pp. 357–374. Springer, Cham (2016). https://doi.org/10.1007/978-3-319-46520-3_23CrossRef

17.

Nenzi, L., Bortolussi, L., Ciancia, V., Loreti, M., Massink, M.: Qualitative and quantitative monitoring of spatio-temporal properties with SSTL. Log. Methods Comput. Sci. 14(4), 2:1–2:38 (2018)

18.

Osama, M., Wijs, A.: Parallel SAT simplification on GPU architectures. In: Vojnar, T., Zhang, L. (eds.) TACAS 2019. LNCS, vol. 11427, pp. 21–40. Springer, Cham (2019). https://doi.org/10.1007/978-3-030-17462-0_2CrossRef

19.

Shiloach, Y., Vishkin, U.: An O(logn) parallel connectivity algorithm. J. Algorithms 3(1), 57–67 (1982)MathSciNetCrossRef

20.

Tsigkanos, C., Kehrer, T., Ghezzi, C.: Modeling and verification of evolving cyber-physical spaces. In: Bodden, E., Schäfer, W., van Deursen, A., Zisman, A. (eds.) ESEC/FSE 2017, pp. 38–48. ACM (2017)

21.

Wijs, A., Bošnački, D.: Many-core on-the-fly model checking of safety properties using GPUs. Softw. Tools Technol. Transf. 18(2), 169–185 (2016). https://doi.org/10.1007/s10009-015-0379-9CrossRef

22.

Wijs, A., Neele, T., Bošnački, D.: GPUexplore 2.0: unleashing GPU explicit-state model checking. In: Fitzgerald, J., Heitmeyer, C., Gnesi, S., Philippou, A. (eds.) FM 2016. LNCS, vol. 9995, pp. 694–701. Springer, Cham (2016). https://doi.org/10.1007/978-3-319-48989-6_42CrossRef

Titel: Towards a Spatial Model Checker on GPU
verfasst von: Laura Bussi
Vincenzo Ciancia
Fabio Gadducci
Verlag: Springer International Publishing
Buch: Formal Techniques for Distributed Objects, Components, and Systems
Print ISBN: 978-3-030-78088-3

Electronic ISBN: 978-3-030-78089-0

Copyright-Jahr: 2021
DOI: https://doi.org/10.1007/978-3-030-78089-0_12

Springer Professional

Abstract

Bitte loggen Sie sich ein, um Zugang zu Ihrer Lizenz zu erhalten.

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

Springer Professional "Wirtschaft+Technik"

Springer Professional "Technik"

Springer Professional "Wirtschaft"