Verification of parallelizability of sequential programs using data dependence analysis

  • Context: The existence of date dependences in sequential programs prevents parallelization. Knowing the data dependences we can reason whether a parallelization approach suggested by an auto-parallelizer is applicable or would it result in data races.


    Goal: Formal definition of the relation between different types of data dependences and OpenMP parallelization directives for having a sound parallelization of sequential programs.


    Prerequisites: Understanding of formal verification (at the level of Formale Systeme 1 course)