Problem with event.replaceBy()

[hernanponcedeleon]

./Dartagnan-SVCOMP.sh ../../sv-benchmarks/c/properties/no-data-race.prp ../../sv-benchmarks/c/pthread-lit/fk2012.i


--------------------------------------------------------------------------------


17:17:33 [INFO ] GitInfo.CreateGitInfo - Git branch: svcomp-2024
17:17:33 [INFO ] GitInfo.CreateGitInfo - Git commit ID: 17eeec33cbc9c310519b08551b317469f878ce8c
17:17:33 [INFO ] GlobalSettings.LogGlobalSettings - REFINEMENT_GENERATE_GRAPHVIZ_DEBUG_FILES: false
17:17:33 [INFO ] GlobalSettings.LogGlobalSettings - REFINEMENT_SYMMETRIC_LEARNING: FULL
17:17:33 [INFO ] Dartagnan.main - Program path: /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_b414a49d-eac3-45a1-9363-6c833d1617c8/bin/dartagnan-verify-smqyFgON4Q/output/fk2012-opt.ll
17:17:33 [INFO ] Dartagnan.main - CAT file path: cat/svcomp.cat
17:17:34 [INFO ] Wmm.configureAll - encoding.wmm.reduceAcyclicityEncodeSets: true
17:17:34 [INFO ] LoopFormVerification.run - Detected 3 loops in the program.
17:17:34 [INFO ] Compilation.run - Program compiled to C11
17:17:34 [INFO ] LoopUnrolling.run - Program unrolled 1 times
17:17:34 [INFO ] DynamicPureLoopCutting.run - Found 0 static spin loops and 1 potential spin loops.
17:17:34 [ERROR] Dartagnan.main - Cannot replace event that is still in use.
java.lang.IllegalStateException: Cannot replace event that is still in use.
	at com.google.common.base.Preconditions.checkState(Preconditions.java:512) ~[guava-32.1.2-jre.jar:?]
	at com.dat3m.dartagnan.program.event.core.AbstractEvent.replaceBy(AbstractEvent.java:228) ~[dartagnan.jar:?]
	at com.dat3m.dartagnan.program.processing.ThreadCreation.run(ThreadCreation.java:144) ~[dartagnan.jar:?]
	at com.dat3m.dartagnan.program.processing.ProcessingManager.lambda$run$0(ProcessingManager.java:142) ~[dartagnan.jar:?]
	at java.util.ArrayList.forEach(ArrayList.java:1511) ~[?:?]
	at com.dat3m.dartagnan.program.processing.ProcessingManager.run(ProcessingManager.java:142) ~[dartagnan.jar:?]
	at com.dat3m.dartagnan.verification.solving.ModelChecker.preprocessProgram(ModelChecker.java:71) ~[dartagnan.jar:?]
	at com.dat3m.dartagnan.verification.solving.DataRaceSolver.run(DataRaceSolver.java:50) ~[dartagnan.jar:?]
	at com.dat3m.dartagnan.verification.solving.DataRaceSolver.run(DataRaceSolver.java:40) ~[dartagnan.jar:?]
	at com.dat3m.dartagnan.Dartagnan.main(Dartagnan.java:157) [dartagnan.jar:?]
ERROR

[hernanponcedeleon]

I think I found the source of the problem.

while(1) {
	if(__VERIFIER_nondet_int()) {
	    pthread_create(&t, 0, producer, 0);
	} else {
	    pthread_create(&t, 0, consumer, 0);
	}
    }

The DynamicPureLoopCutting pass creates an ExecutionStatus event execCheck having the ThreadCreate as an user. Then, when the ThreadCreation pass tries to remove the ThreadCreate, it complains that execCheck still uses it.

However, many other benchmarks have pthread_create inside loops, so I don't fully understand why those do not cause problems and this particular one does.

[ThomasHaas]

Just pthread_create inside a loop is no problem by itself, because it will always cause a side-effect and so the loop cutting won't even place the ExecutionStatus event. It is the combination of pthread_create and conditionals that breaks the code.

I guess it is time to rewrite the loop cutting code more properly.

[ThomasHaas]

Fixed by #619