Program Correctness by Transformation

  • Marieke HuismanEmail author
  • Stefan Blom
  • Saeed Darabi
  • Mohsen Safari
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 11244)


Deductive program verification can be used effectively to verify high-level programs, but can be challenging for low-level, high-performance code. In this paper, we argue that compilation and program transformations should be made annotation-aware, i.e. during compilation and program transformation, not only the code should be changed, but also the corresponding annotations. As a result, if the original high-level program could be verified, also the resulting low-level program can be verified. We illustrate this approach on a concrete case, where loop annotations that capture possible loop parallelisations are translated into specifications of an OpenCL kernel that corresponds to the parallel loop. We also sketch how several commonly used OpenCL kernel transformations can be adapted to also transform the corresponding program annotations. Finally, we conclude the paper with a list of research challenges that need to be addressed to further develop this approach.



We are indebted to Jeroen Vonk, who started studying some of the annotation-aware program transformations as part of his Bachelor project. This work is supported by the ERC 258405 VerCors project (Huisman, Blom), the EU FP7 STREP 287767 CARP project (Huisman, Blom, Darabi), and the NWO VICI 639.023.710 Mercedes project (Huisman, Safari).


  1. 1.
    Amighi, A., Haack, C., Huisman, M., Hurlin, C.: Permission-based separation logic for multithreaded Java programs. LMCS 11(1) (2015)Google Scholar
  2. 2.
    Amini, M.: Source-to-source automatic program transformations for GPU-like hardware accelerators. Master’s thesis, Ecole Nationale Supérieure des Mines de Paris (2012)Google Scholar
  3. 3.
    Baghdadi, R., et al.: PENCIL: towards a platform-neutral compute intermediate language for DSLs. CoRR, abs/1302.5586 (2013)Google Scholar
  4. 4.
    Blom, S., Darabi, S., Huisman, M.: Verification of loop parallelisations. In: Egyed, A., Schaefer, I. (eds.) FASE 2015. LNCS, vol. 9033, pp. 202–217. Springer, Heidelberg (2015). Scholar
  5. 5.
    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). Scholar
  6. 6.
    Blom, S., Huisman, M., Mihelčić, M.: Specification and verification of GPGPU programs. Sci. Comput. Program. 95, 376–388 (2014)CrossRefGoogle Scholar
  7. 7.
    Bornat, R., Calcagno, C., O’Hearn, P.W., Parkinson, M.J.: Permission accounting in separation logic. In: POPL, pp. 259–270 (2005)Google Scholar
  8. 8.
    Boyland, J.: Checking interference with fractional permissions. In: Cousot, R. (ed.) SAS 2003. LNCS, vol. 2694, pp. 55–72. Springer, Heidelberg (2003). Scholar
  9. 9.
    da Rocha Pinto, P., Dinsdale-Young, T., Gardner, P.: TaDA: a logic for time and data abstraction. In: Jones, R. (ed.) ECOOP 2014. LNCS, vol. 8586, pp. 207–231. Springer, Heidelberg (2014). Scholar
  10. 10.
    Darabi, S.: Verification of program parallelization. Ph.D. thesis, University of Twente (2018)Google Scholar
  11. 11.
    Darabi, S., Blom, S.C.C., Huisman, M.: A verification technique for deterministic parallel programs. In: Barrett, C., Davies, M., Kahsai, T. (eds.) NFM 2017. LNCS, vol. 10227, pp. 247–264. Springer, Cham (2017). Scholar
  12. 12.
    de Gouw, S., Rot, J., de Boer, F.S., Bubel, R., Hähnle, R.: OpenJDK’s Java.utils.Collection.sort() is broken: the good, the bad and the worst case. In: Kroening, D., Păsăreanu, C.S. (eds.) CAV 2015. LNCS, vol. 9206, pp. 273–289. Springer, Cham (2015). Scholar
  13. 13.
    Huang, D., et al.: Automated transformation of GPU-specific OpenCL kernels targeting performance portability on multi-core/many-core CPUs. In: Silva, F., Dutra, I., Santos Costa, V. (eds.) Euro-Par 2014. LNCS, vol. 8632, pp. 210–221. Springer, Cham (2014). Scholar
  14. 14.
    Jung, R., et al.: Iris: monoids and invariants as an orthogonal basis for concurrent reasoning. In: POPL, pp. 637–650. ACM (2015)Google Scholar
  15. 15.
    Krebbers, R., Jung, R., Bizjak, A., Jourdan, J.-H., Dreyer, D., Birkedal, L.: The essence of higher-order concurrent separation logic. In: Yang, H. (ed.) ESOP 2017. LNCS, vol. 10201, pp. 696–723. Springer, Heidelberg (2017). Scholar
  16. 16.
    Leavens, G.T., et al.: JML Reference Manual. Department of Computer Science, Iowa State University, February 2007.
  17. 17.
    Nandakumar, D.: Automatic translation of CUDA to OpenCL and comparison of performance optimizations on GPUs. Master’s thesis, University of Illinois at Urbana-Champaign (2011)Google Scholar
  18. 18.
    Sergey, I., Nanevski, A., Banerjee, A.: Specifying and verifying concurrent algorithms with histories and subjectivity. In: Vitek, J. (ed.) ESOP 2015. LNCS, vol. 9032, pp. 333–358. Springer, Heidelberg (2015). Scholar
  19. 19.
    Shen, J.: Efficient high performance computing on heterogeneous platforms. Ph.D. thesis, Technical University of Delft (2015)Google Scholar
  20. 20.
    Wu, B., Chen, G., Li, D., Shen, X., Vetter, J.: Enabling and exploiting flexible task assignment on GPU through SM-centric program transformations. In: ICS 2015 Proceedings of the 29th ACM on International Conference on Supercomputing, pp. 119–130. ACM (2015)Google Scholar

Copyright information

© Springer Nature Switzerland AG 2018

Authors and Affiliations

  • Marieke Huisman
    • 1
    Email author
  • Stefan Blom
    • 2
  • Saeed Darabi
    • 3
  • Mohsen Safari
    • 1
  1. 1.University of TwenteEnschedeThe Netherlands
  2. 2.BetterBeEnschedeThe Netherlands
  3. 3.ASMLVeldhovenThe Netherlands

Personalised recommendations