作者: Shaz Qadeer , Madanlal Musuvathi
DOI:
关键词:
摘要: Concurrency is used pervasively in the development of large systems programs. However, concurrent programming difficult because possibility unexpected interference among concurrently executing tasks. Such often results “Heisenbugs” that appear rarely and are extremely to reproduce debug. Stress testing, which system run under heavy load for a long time, method commonly employed flush out such concurrency bugs. This form testing provides inadequate coverage has unpredictable results. paper proposes an alternative called scenario relies on systematic exhaustive We have implemented tool CHESS performing uses model checking techniques systematically generate all interleaving given scenario. scales programs found numerous previously unknown bugs had been stress tested many months prior being by CHESS. For each bug, able consistently erroneous execution manifesting thereby making it significantly easier debug problem. integrated into test frameworks code bases inside Microsoft testers daily basis.