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.
Research partially supported by the MIUR Project PRIN 2017FTXR7S “IT- MaTTerS” and by POR FESR Toscana 2014–2020 As. 1 - Az. 1.1.5 – S.A. A1 N. 7165 project STINGRAY. The authors are thankful to: Raffaele Perego, Franco Maria Nardini and the HPC-Lab at ISTI-CNR for a powerful GPU used in early development; Gina Belmonte, Diego Latella, and Mieke Massink, for fruitful discussions. The authors are listed in alphabetical order, having equally contributed to this work.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Similar content being viewed by others
Notes
- 1.
VoxLogicA: see https://github.com/vincenzoml/VoxLogicA.
- 2.
VoxLogicA-GPU is Free and Open Source software. Its source code is currently available at https://github.com/vincenzoml/VoxLogicA/tree/experimental-gpu.
- 3.
FSharp: see https://fsharp.org. NET Core: see https://dotnet.microsoft.com. OpenCL: see https://www.khronos.org/opencl. ITK: see https://itk.org.
- 4.
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.
- 5.
See e.g. https://en.wikipedia.org/wiki/MapReduce.
- 6.
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).
- 7.
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.
References
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)
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)
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-9
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)
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_16
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-7
Bussi, L., Ciancia, V., Gadducci, F.: A spatial model checker in GPU (extended version). CoRR abs/2010.07284 (2020)
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_46
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-8
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)
Gustafson, J.L.: Reevaluating Amdahl’s law. Commun. ACM 31(5), 532–533 (1988)
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)
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_23
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)
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_2
Shiloach, Y., Vishkin, U.: An O(logn) parallel connectivity algorithm. J. Algorithms 3(1), 57–67 (1982)
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)
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-9
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_42
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2021 IFIP International Federation for Information Processing
About this paper
Cite this paper
Bussi, L., Ciancia, V., Gadducci, F. (2021). Towards a Spatial Model Checker on GPU. In: Peters, K., Willemse, T.A.C. (eds) Formal Techniques for Distributed Objects, Components, and Systems. FORTE 2021. Lecture Notes in Computer Science(), vol 12719. Springer, Cham. https://doi.org/10.1007/978-3-030-78089-0_12
Download citation
DOI: https://doi.org/10.1007/978-3-030-78089-0_12
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-030-78088-3
Online ISBN: 978-3-030-78089-0
eBook Packages: Computer ScienceComputer Science (R0)