Static analysis of the determinism of multithreaded programs

Threads communicate implicitly through shared mem-ory. Because of the random interleaving during their par-allel execution, nondeterministic behaviors possibly arise that is why multithreaded programming is strictly more dif-ficult than programming in sequential languages. Moreover the random interleaving may lead to subtle bugs, that are really hard to be detected and fixed. We propose a novel de-terministic property focused on multithreading. We define it as difference among concrete traces, and then we abstract it in two separate steps in order to statically analyze it. At the intermediate level of abstraction, we propose the new idea of weak determinism. We sketch how the proposed property may be used in order to semi-automatically parallelize se-quential programs. Finally, we present some experimental results when applying the analysis to a set of well-known benchmarks. We believe that our approach, dealing directly with the source of the problem (i.e. the nondeterministic interactions via shared memory) is in position to bypass the actual limits of the static analysis of multithreaded pro-grams, mostly focused on properties like data race condi-tion and absence of deadlocks. 1