Correctness of multi-threaded programs typically requires that they satisfy liveness properties. For example, a program may require that no thread is starved of a shared resource, or that all threads eventually agree on a single value. This paper presents a method for proving that such liveness properties hold. Two particular challenges addressed in this work are that (1) the correctness argument may rely on global behaviour of the system (e.g., the correctness argument may require that all threads collectively progress towards "the good thing" rather than one thread progressing while the others do not interfere), and (2) such programs are often designed to be executed by any number of threads, and the desired liveness properties must hold regardless of the number of threads that are active in the program.
Termination analyses have been developed for the setting of concurrent programs @cite_27 @cite_28 @cite_6 . Our work differs in two respects. First, our technique handles the case that there are unboundedly many threads operating simultaneously in the system. Second, the aforementioned techniques prove termination using arguments. A thread-local termination argument expresses that each thread individually progresses towards some goal assuming that its environment (formed by the other threads) is either passive or at least does not disrupt its progress. In contrast, the technique proposed in the paper is able to reason about termination that requires coordination between all threads (that is, all threads together progress towards some goal). This enables our approach to prove liveness for programs such as the Ticket protocol (Figure ): proving that some distinguished thread will eventually enter its critical section requires showing that all threads collectively make progress on increasing the value of the service number until the distinguished thread's ticket is reached.
@cite_28 @cite_27 @cite_6
182717014 2145062333 2270988982
Automated verification of multi-threaded programs is difficult. Direct treatment of all possible thread interleavings by reasoning about the program globally is a prohibitively expensive task, even for small programs. Rely-guarantee reasoning is a promising technique to address this challenge by reducing the verification problem to reasoning about each thread individually with the help of assertions about other threads. In this paper, we propose a proof rule that uses rely-guarantee reasoning for compositional verification of termination properties. The crux of our proof rule lies in its compositionality wrt. the thread structure of the program and wrt. the applied termination arguments --- transition invariants. We present a method for automating the proof rule using an abstraction refinement procedure that is based on solving recursion-free Horn clauses. To deal with termination, we extend an existing Horn-clause solver with the capability to handle well-foundedness constraints. Finally, we present an experimental evaluation of our algorithm on a set of micro-benchmarks. 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. We describe a method for proving termination of massively parallel GPU kernels. An implementation in KITTeL is able to show termination of 94 of the 598 kernels in our benchmark suite.