ComputingComputer EngineeringComputer ScienceAlgorithmsFormal MethodsSchedulingConcurrency AnalysisConcurrent ProgrammingCpu SchedulingSoftware TestingConcurrency Bug DetectionConcurrent Program TestingModel Checking For ConcurrencyRandom TestingSchedule ExplorationState Space ExplorationState Space ExplosionState-space Structure
Multithreaded concurrent programs often exhibit wrong behaviors due to unintended interferences among the concurrent threads. Such errors are often hard to find because they typically manifest under very specific thread schedules. Traditional testing, which pays no attention to thread schedules and non-deterministically exercises a few arbitrary schedules, often misses such bugs. Traditional model checking techniques, which try to systematically explore all thread schedules, give very high confidence in the correctness of the system, but, unfortunately, they suffer from the state explosion problem. Recently, dynamic partial order techniques have been proposed to alleviate the problem. However, such techniques fail for large programs because the state space remains large in spite of reduction. An inexpensive and a simple alternative approach is to perform random testing by choosing thread schedules at random. We show that such a naive approach often explores some states with very high probability compared to the others. We propose a random partial order sampling algorithm (or RAPOS) that partly removes this non-uniformity in sampling the state space. We empirically compare the proposed algorithm with the simple random testing algorithm and show that the former outperforms the latter
26
E. M. Clarke, Orna Grümberg, D. Long · 1996 · 6.9K citations
Gerard J. Holzmann · IEEE Transactions on Software Engineering · 1997 · 3.8K citations
Willem Visser, Klaus Havelund, Guillaume Brat et al. · Automated Software Engineering · 2003 · 1.4K citations
Koen Claessen, John Hughes · ACM SIGPLAN Notices · 2011 · 1K citations