Abstract

Abstract
Directive-drive programming models, such as OpenMP, are one solution for exploiting the potential of multi-core architectures, and enable developers to accelerate software applications by adding annotations on for-type loops and other code regions. However, manual parallelization of applications is known to be a non trivial and time consuming process, requiring parallel programming skills. Automatic parallelization approaches can reduce the burden on the application development side. This paper presents an OpenMP based automatic parallelization compiler, named AutoPar-Clava, for automatic identification and annotation of loops in C code. By using static analysis, parallelizable regions are detected, and a compilable OpenMP parallel code from the sequential version is produced. In order to reduce the accesses to shared memory by each thread, each variable is categorized into the proper OpenMP scoping. Also, AutoPar-Clava is able to support reduction on arrays, which is available since OpenMP 4.5. The effectiveness of AutoPar-Clava is evaluated by means of the Polyhedral Benchmark suite, and targeting a N-cores x86-based computing platform. The achieved results are very promising and compare favorably with closely related auto-parallelization compilers such as Intel C/C++ Compiler (i.e., icc), ROSE, TRACO, and Cetus.

Abstract
Compared to general purpose programming languages, domain specific languages (DSLs) targeting adaptive embedded software development provide a very promising alternative for developing clean and error free run-time adaptations. However, the ability to use several rules in a single adaptation strategy, as allowed by some DSLs, may lead to conflicts and reachability issues, which can eventually lead to functional bugs. Traditionally, such conflict analysis is done using software testing or manual manipulation of automata based models of rules. However, both of these techniques are error-prone and thus can lead to unwanted situations. As an accurate alternative, we propose to use model checking for rule conflict and reachability analysis in DSL adaptation. In particular, this paper provides an approach to formally model DSL adaptation specifications, along with their rules, and identifies a set of generic temporal properties to check for reachability and other rule conflicts, using the finite and infinite state-space based model checking capabilities of nuXmv model checker. For illustration, formal analyses of an energy aware CPU scheduling algorithm, i.e, PAST, for adaptivity rules for a stereo navigation system and for a context aware application are presented. © 2018 IEEE.

Abstract

Abstract

Abstract