Static Analysis of the Determinism of Multithreaded Programs

Threads communicate implicitly through shared memory. Because of the random interleaving during their parallel execution, nondeterministic behaviors possibly arise that is why multithreaded programming is strictly more difficult 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 deterministic 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 sequential 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 programs, mostly focused on properties like data race condition and absence of deadlocks.