Hilfe Wegweiser Impressum Kontakt Einloggen





Proving Thread Termination


Podelski,  Andreas
Programming Logics, MPI for Informatics, Max Planck Society;

Rybalchenko,  Andrey
Programming Logics, MPI for Informatics, Max Planck Society;

Externe Ressourcen
Es sind keine Externen Ressourcen verfügbar
Volltexte (frei zugänglich)
Es sind keine frei zugänglichen Volltexte verfügbar
Ergänzendes Material (frei zugänglich)
Es sind keine frei zugänglichen Ergänzenden Materialien verfügbar

Cook, B., Podelski, A., & Rybalchenko, A. (2007). Proving Thread Termination. In J. Ferrante, & K. S. McKinley (Eds.), PLDI'07: Proceedings of the 2007 Conference on Programming Language Design and Implementation (pp. 320-330). New York, NY, USA: ACM.

Concurrent programs are often designed such that certain functions executing within critical threads must terminate. Examples of such cases can be found in operating systems, web servers, e-mail clients, etc. Unfortunately, no known automatic program termination prover supports a practical method of proving the termination of threads. In this paper we describe such a procedure. The procedure's scalability is achieved through the use of environment models that abstract away the surrounding threads. The procedure's accuracy is due to a novel method of incrementally constructing environment abstractions. Our method finds the conditions that a thread requires of its environment in order to establish termination by looking at the conditions necessary to prove that certain paths through the thread represent well-founded relations if executed in isolation of the other threads. The paper gives a description of experimental results using an implementation of our procedureon Windows device drivers and adescription of a previously unknown bug found withthe tool.