Preserving program correctness through its transformations

title:Preserving program correctness through its transformations
contact:prof.dr. M. Huisman & S. Darabi MSc
to be started:any time


Writing correct parallel programs becomes more and more difficult as the complexity and heterogeneity of processors increase. This issue is addressed by parallelising compilers. They are designed to translate high level sequential code annotated by compiler directives into low-level parallel code. Specifically, in this project compilation of loops annotated by parallelisation directives [OpenMP, PENCIL] (parallel loops) to GPU kernels [OpenCL] as the low-level target language [CARP]. 

We developed a verification technique for reasoning about the correctness of parallel loops in high-level programing languages. We use formal specifications written in permission-based separation logic as our specification language [SL,PSL]. These formal specifications of loop iteraitons are called iteration contracts [FASE, CARP]. Also, we developed Vercors tool set which automates our verification techniuqes [Vercors]. 

The aim of this project is to transform itration contracts along with loop transformations performed by parallelizing compiler. Specifically, first we need to find out which kinds loop transformation would affect iteration contracts and then we need to propose  required rules to transform iteration contract. As a secondary goal, we also are interested to know who the iteratoin contracts can be transformed to kernel contracts.  

[FASE]  S. Blom, S. Darabi, M. Huisman, Verification of Loop Parallelisations, 18th International Conference, FASE 2015

[SCP] S. Blom, M. Huisman, and M. Mihelcic. Specification and verification of GPGPU programs. Science of Computer Programming, 2014.


[vercors] The VerCors toolset. https://fmt.ewi.utwente. nl/redmine/projects/vercors-verifier/wiki. Accessed: 14 March 2015

[OpenMP] L. Dagum and R. Menon. OpenMP: an industry standard API for shared-memory

programming. Computational Science & Engineering, IEEE, 5(1):46{55, 1998.

[PENCIL] R. Baghdadi, A. Cohen, S. Guelton, S. Verdoolaege, J. Inoue, T. Grosser, G. Kouveli,A. Kravets, A. Lokhmotov, C. Nugteren, F. Waters, and A. F. Donaldson.PENCIL: Towards a Platform-Neutral Compute Intermediate Language for DSLs. CoRR, abs/1302.5586, 2013.

[OpenCL] OpenCL the open standard for parallel programming of heterogeneous systems. Accessed: 13 March 2015.

[PSL] R. Bornat, C. Calcagno, P. O’Hearn, and M. Parkinson. Permission accounting in separation logic. In ACM SIGPLAN Notices, volume 40, pages 259–270. ACM, 2005.

[SL] J. C. Reynolds. Separation logic: A logic for shared mutable data structures. In Logic in Computer Science, 2002. Proceedings. 17th Annual IEEE Symposium on, pages 55–74. IEEE, 2002.