Abstract:
The ongoing effort of transforming multi-core CPUs towards many integrated core APUs (Accelerated Computation Unit) by converging CPUs and GPUs into one single chip, changes the previously linear growth of CPU power towards exponential growth in APU computational power. Addressing the complexity of concurrency programming in the context of changing hardware remains an ongoing challenge. In order to overcome limitations of conventional concurrency programming as part of main stream programming languages, I have investigated ways to verify the correctness of the concurrency code in Scala. Initially, I investigated the transformation of software contracts into test-oracles in order to perform fully automated testing, a concept known from ongoing research in Eiffel. In order to do that, I investigated several Design by Contracts tools and finally developed f-DBC, a novel tool based on a flexible component architecture for supporting functional Design by Contract in Scala. An analysis of f-DBC benchmark results provides evidence that contracts written in f-DBC do not cause any measurable reduction in runtime performance compared to the same application without contracts. However, an empirical analysis of eight Eiffel and twelve Scala projects has provided evidence that contracts are seldom written in real world projects. Based on this insight, I have developed the main contribution of this thesis: a macro for the Scala compiler that replaces the initial approach with compiler checks on pure functions. Even though the concept of function purity is already known, surprisingly little work has been done for verifying function purity. The developed macro introduces a first compiler-based verification of function purity and a few more aspects relevant to concurrency programming. Altogether, the macro reports nine categories of threadsafety issues. Once a function guarded by the macro compiles, it is verified to be thread-safe in any concurrent execution model. A set of examples for each category illustrates the usefulness of the compiler macro. Future work may extend the approach further into other fields such as distributed programming.