Concise analysis using implication algebras for task-local memory optimisation

Abstract

OpenMP is a pragma-based extension to C to support parallelism. The OpenMP standard recently added support for task-based parallelism but in a richer way than languages such as Cilk. Naïve implementations give each task its own stack for task-local memory, which is very inefficient. We detail a program analysis for OpenMP to enable tasks to share stacks without synchronisation - either unconditionally or dependent on some cheap run-time condition which is very likely to hold in busy systems. The analysis is based on a novel implication-algebra generalisation of logic programming which allows concise but easily readable encodings of the various constraints. The formalism enables us to show that the analysis has a unique solution and polynomial-time complexity. We conclude with performance figures. © 2013 Springer-Verlag.