Abstract
This paper describes a case study to verify memory safety of a radio telescope pipeline, which was targeted with the PADRE project of Astron, SURF and the Netherlands eScienceCenter. As performance is important for this application, the implementation of the radio telescope pipeline should run on a GPU device. Therefore, we encoded the radio telescope pipeline using the Halide scheduling language, which achieved a significant speedup. Next, we used the HaliVer tool to automatically generate formal pre- and postconditions, loop invariants and assertions, which the deductive verifier VerCors can use to prove memory safety. We identified two challenges for the automatic generation of formal annotations for a tool such as VerCors. The first challenge was related to the flattening of multi-dimensional arrays to single arrays and the second challenge concerns the use of many arrays in a program in combination with many quantifiers to specify read and write permissions. For both challenges, we propose solutions, and implemented these. Not every solution proved successful. We discuss the lessons learned and future plans to solve a core scalability issue for large optimised parallel programs.
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
Notes
- 1.
We only briefly touch upon the definitions here. For examples with more explanation, please refer to the online tutorial at https://vercors.ewi.utwente.nl/wiki/.
- 2.
A Halide tutorial can be found here: https://halide-lang.org/tutorials/.
- 3.
- 4.
- 5.
The complete implementation in Halide together with optimization schedules can be found at https://github.com/sakehl/padre-casestudy together with the original code.
- 6.
An example program can be found at https://github.com/sakehl/padre-casestudy/blob/main/verification_goals/Quant/data/quant9.pvl.
- 7.
We confirmed this here github.com/viperproject/silicon/issues/831. Although some heuristics could be applied, the scaling issue stands.
References
Blom, S., Darabi, S., Huisman, M., Oortwijn, W.: The VerCors tool set: verification of parallel and concurrent software. In: Polikarpova, N., Schneider, S. (eds.) IFM 2017. LNCS, vol. 10510, pp. 102–110. Springer, Cham (2017). https://doi.org/10.1007/978-3-319-66845-1_7
Bornat, R., Calcagno, C., O’Hearn, P., Parkinson, M.: Permission accounting in separation logic. In: POPL, pp. 259–270 (2005)
Cimatti, A., Griggio, A., Irfan, A., Roveri, M., Sebastiani, R.: Experimenting on solving nonlinear integer arithmetic with incremental linearization. In: Beyersdorff, O., Wintersteiger, C. (eds.) SAT 2018. LNCS, vol. 10929, pp. 383–398. Springer, Cham (2018). https://doi.org/10.1007/978-3-319-94144-8_23
Clément, B., Cohen, A.: End-to-end translation validation for the halide language. Proc. ACM Program. Lang. 6(OOPSLA1), 1–30 (2022). https://doi.org/10.1145/3527328
de Moura, L., Bjørner, N.: Z3: an efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 337–340. Springer, Heidelberg (2008). https://doi.org/10.1007/978-3-540-78800-3_24
Gan, H., et al.: Assessing the impact of two independent direction-dependent calibration algorithms on the LOFAR 21 cm signal power spectrum - and applications to an observation of a field flanking the north celestial pole. Astron. Astrophys. 669, A20 (2023). https://doi.org/10.1051/0004-6361/202244316
Gödel, K.: Über formal unentscheidbare Sätze der principia mathematica und verwandter Systeme I. Monatshefte Math. Phys. 38, 173–198 (1931)
Hamaker, J.P., Bregman, J.D., Sault, R.J.: Understanding radio polarimetry. I. Mathematical foundations. Astron. Astrophys. Suppl. Ser. 117(1), 137–147 (1996). https://doi.org/10.1051/aas:1996146
Hozzová, P., Bendík, J., Nutz, A., Rodeh, Y.: Overapproximation of non-linear integer arithmetic for smart contract verification. In: EPiC Series in Computing, vol. 94, pp. 257–269. EasyChair (2023). https://doi.org/10.29007/h4p7
Jovanović, D.: Solving nonlinear integer arithmetic with MCSAT. In: Bouajjani, A., Monniaux, D. (eds.) VMCAI 2017. LNCS, vol. 10145, pp. 330–346. Springer, Cham (2017). https://doi.org/10.1007/978-3-319-52234-0_18
Kremer, G., Corzilius, F., Ábrahám, E.: A generalised branch-and-bound approach and its application in SAT modulo nonlinear integer arithmetic. In: Gerdt, V., Koepf, W., Seiler, W., Vorozhtsov, E. (eds.) CASC 2016. LNCS, vol. 9890, pp. 315–335. Springer, Cham (2016). https://doi.org/10.1007/978-3-319-45641-6_21
Leiserson, C.E., et al.: There’s plenty of room at the top: what will drive computer performance after Moore’s law? Sci. (New York, N.Y.) 368(6495) (2020). https://doi.org/10.1126/science.aam9744
Liu, A., Bernstein, G.L., Chlipala, A., Ragan-Kelley, J.: Verified tensor-program optimization via high-level scheduling rewrites. Proc. ACM on Program. Lang. 6(POPL), 55:1–55:28 (2022). https://doi.org/10.1145/3498717
Müller, P., Schwerhoff, M., Summers, A.: Viper - a verification infrastructure for permission-based reasoning. In: Jobstmann, B., Leino, K. (eds.) VMCAI 2016. LNCS, vol. 9583, pp. 41–62. Springer, Heidelberg (2016). https://doi.org/10.1007/978-3-662-49122-5_2
Müller, P., Schwerhoff, M., Summers, A.J.: Automatic verification of iterated separating conjunctions using symbolic execution. In: Chaudhuri, S., Farzan, A. (eds.) CAV 2016. LNCS, vol. 9779, pp. 405–425. Springe, Cham (2016). https://doi.org/10.1007/978-3-319-41528-4_22
Ragan-Kelley, J., et al.: Halide: decoupling algorithms from schedules for high-performance image processing. Commun. ACM 61(1), 106–115 (2017). https://doi.org/10.1145/3150211
Ragan-Kelley, J., Barnes, C., Adams, A., Paris, S., Durand, F., Amarasinghe, S.: Halide: a language and compiler for optizing parallelism, locality, and recomputation in image processing pipelines. SIGPLAN Not. 48(6), 519–530 (2013). https://doi.org/10.1145/2499370.2462176
Sakar, Ö., Safari, M., Huisman, M., Wijs, A.: Alpinist: an annotation-aware GPU program optimizer. In: Fisman, D., Rosu, G. (eds.) TACAS 2022. LNCS, vol. 13244, pp. 332–332. Springer, Cham (2022). https://doi.org/10.1007/978-3-030-99527-0_18
van den Haak, L.B.: Artifact for: HaliVer: deductive verification and scheduling languages join forces. Zenodo (2023). https://doi.org/10.5281/zenodo.10047853
van den Haak, L.B., Wijs, A., Huisman, M., van den Brand, M.: HaliVer: deductive verification and scheduling languages join forces. In: Finkbeiner, B., Kovács, L. (eds.) TACAS 2024. LNCS, vol. 14572, pp. 71–89. Springer, Cham (2024). https://doi.org/10.1007/978-3-031-57256-2_4
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2024 The Author(s), under exclusive license to Springer Nature Switzerland AG
About this paper
Cite this paper
van den Haak, L.B., Wijs, A., Huisman, M., van den Brand, M. (2024). Verifying a Radio Telescope Pipeline Using HaliVer: Solving Nonlinear and Quantifier Challenges. In: Haxthausen, A.E., Serwe, W. (eds) Formal Methods for Industrial Critical Systems. FMICS 2024. Lecture Notes in Computer Science, vol 14952. Springer, Cham. https://doi.org/10.1007/978-3-031-68150-9_9
Download citation
DOI: https://doi.org/10.1007/978-3-031-68150-9_9
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-031-68149-3
Online ISBN: 978-3-031-68150-9
eBook Packages: Computer ScienceComputer Science (R0)