Modeling Non-deterministic C Code with Active Objects.

Cheap and ubiquitous availability of multi-processor hardware provides a strong incentive to parallelize existing software. We aim to annotate existing sequential applications written in C with OpenMP directives that can be processed by compilers on high performance parallel computers. We adopt a model-based approach, where from sequential C-code a software model is extracted in a largely automatic fashion. The target is the modeling language ABS (Abstract Behavioral Specification), an active objects-language with formal semantics. ABS has been designed to be statically analyzable. We focus on the first stages of model-based parallelization: model extraction and validation. We define a behavior-preserving, fully automatic translation of a large fragment of sequential C that explicitly renders all possible execution sequences, then use automated test case generation to produce validation test cases.