We develop compositional analysis algorithms for discovering fair non-terminating executions in multithreaded programs. In particular, our analysis finds fair and ultimately-periodic executions—i.e., those that ultimately repeat the same sequence of actions indefinitely with each enabled thread participating. Further, we limit the number of context-switches each thread is allowed along any repeating sequence of actions; one expects that this number is usually small for bugs in practice. Bounding context-switches leads to a compositional analysis in which each thread is considered separately, in isolation. We implement our analysis by a systematic code-to-code translation from multithreaded programs to sequential programs, such that one requires a safety analysis of the latter to find liveness bugs in the former. Then by using standard sequential analysis tools, we are able to discover fair non-terminating executions in multithreaded programs.

PDF file

In  Computer-Aided Verification (CAV)

Details