P. Ferrara.
Static analysis of the determinism of multithreaded programs

In Proceedings of the Sixth IEEE International Conference on Software Engineering and Formal Methods (SEFM 2008), IEEE Computer Society, Cape Town, South Africa, November 10-14, 2008

Final version: Pdf (179 KB)
Extended version (with complete proofs): Pdf (202 KB)
Slides: Pdf (425 KB)

Abstract: 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.

Bibtex:

@inproceedings{Ferr08b,
  author = {Pietro Ferrara},
  title = {Static analysis of the determinism of multithreaded programs},
  booktitle = {Proceedings of the Sixth IEEE International Conference on Software
			Engineering and Formal Methods (SEFM 2008)},
  year = {2008},
  publisher = {IEEE Computer Society},
  month = {November},
}