Electronic Notes in Theoretical Computer Science · 2002 · 119 citations · 25 references
ComputingComputer EngineeringComputer ScienceFormal MethodsProgramming LanguagesSchedulingConcurrency AnalysisConcurrency VerificationConcurrent ProgrammingConcurrent System VerificationRace Condition VulnerabilitiesSoftware TestingAssertion CheckingConcurrent Program TestingConcurrent Program VerificationDeadlockDeadlock ResolutionModel Checking For ConcurrencyPseudo-random Number GenerationPseudo-random Number Generators
The difficulty of finding errors caused by unexpected interleavings of threads in concurrent programs is well known. Model checkers can pinpoint such errors and verify correctness but are not easily scalable to large programs. The approach discussed here is more scalable but less systematic. We transform a given Java program by inserting calls to a scheduling function at selected points. The scheduling function either does nothing or causes a context switch. The simplest scheduling function makes the choice blindly using a pseudo-random number generator; more sophisticated scheduling functions use heuristics to weight the choices. We try to insert as few calls as possible while still ensuring that for each reachable deadlock and assertion violation, there is a sequence of choices by the scheduling function that leads to it; thus, there is a non-zero probability of finding it by testing the transformed program, regardless of the scheduling policies of the underlying Java Virtual Machine.
25
Gerard J. Holzmann · IEEE Transactions on Software Engineering · 1997 · 3.8K citations
Stefan Savage, Michael T. Burrows, Greg Nelson et al. · ACM Transactions on Computer Systems · 1997 · 1.6K citations · Full text
Willem Visser, Klaus Havelund, Guillaume Brat et al. · Automated Software Engineering · 2003 · 1.4K citations
Model checking for programming languages using VeriSoft
Patrice Godefroid · 1997 · 829 citations · Full text