Skip to content

Dekker algorithm fixed

csanadtelbisz requested to merge csanadtelbisz/sv-benchmarks:main into main

Dekker's algorithm was incorrectly implemented in the sv-benchmarks. The second thread must set the turn variable to 0 instead of 1 (see Dekker's algorithm) otherwise, the first thread cannot enter the critical section after the second thread has entered.

In this PR, the original versions are preserved by adding a suffix buggy and the bug is fixed in the original files. The expected verdict of the verification does not change with this fix verified by the Theta model checker for the concurrent tasks. Since no tool could produce a correct result for the sequentialized version (cs_dekker.yml results) I was not able to verify the expected verdict for this task.

Merge request reports