PP-L: Semantics and Verification of Parallel Systems
To benefit from modern processor hardware, software applications must scale with the number of available processor cores. However, many software applications evolved over years and mainly consist of sequential components, i.e., they do not scale. Since software applications incorporate business knowledge, it is better to parallelize existing applications than to develop a new, parallel application that should replace the existing one.
Incomplete information during parallelization or human mistakes in a manual or semi-automatic parallelization process may alter the behavior of the parallelized program. Thus, it must be checked that the parallelized program is still functional correct. Program errors in parallel programs may show up rarely and only in particular executions. To detect such errors, program verification is well-suited. While verification often suffers from the problem of a missing, formal specification of the functional behavior, the original, sequential program is a well-suited specification for the parallelized program.
Part project L aims at verifying whether the sequential and parallelized program are functionally equivalent, i.e., they compute the same output when given the same output. The left box of the following figure describes this verification task. The following two boxes sketch the challenge of and the approach for functional equivalence checking and are explained in the following.
The main challenge for equivalence checking is that it must efficiently deal with the numerous amount of possible executions in the parallelized program, which are even increased when using weak memory models. To deal with this challenge, the equivalence check is divided into the following three checks, which furthermore allows one to only repeat the third check when the memory model changes.
- Partial equivalence: assuming sequential consistency it should be checked whether the sequential and the parallelized program produce the same output when giving the same input and both terminate
- Termination: assuming sequential consistency it should be proven that the parallel program always terminates, e.g., does not contain deadlocks
- Sequential consistency guarantee:
- via checking if the parallelized program behaves as if executed under sequential consistency
- via enforcement of sequential consistency
Additionally, parallel patterns should be used to
- further decompose the above checks,
- check certain properties only once for a certain class of programs, or
- choose the most suitable method for a particular subcheck.