ldv-races/race-4_1-thread_local_vars has a data race

[tautschnig]

thread_usb and ath9k_flush read/write pdev without any synchronisation mechanism between them. For example, thread_usb's ldv_assert(pdev == 8) can be violated by ath8k_flush's pdev = 6.

The file name and comments suggest that there be some thread-local variables, but none of the global variables is actually marked thread-local.

[tautschnig]

@mutilin @PavelAndrianov Would either of you have an idea why this benchmark was labelled as not having a data race?

[hernanponcedeleon]

If the problem is related with a data rac, why are you changing the verdict for reachability?

My understanding is that you should: 1) keep this version of the program as it is, remove the reachability property from yml file (if the program has undefined behavior, we cannot say anything about other properties) and add the no-datarace property with expected result false 2) create a new version of the program where the data race is solved (I did this for several programs in the same folder so you can take a look there), keep the expected result for reachability as it is and add true as the expected result for no-data-race property

[PavelAndrianov]

@tautschnig, I do not catch, what is the racy path.

For example, thread_usb's ldv_assert(pdev == 8) can be violated by ath8k_flush's pdev = 6

ldv_assert(pdev == 8) is performed after ath_ahb_disconnect, which performs pthread_join, thus the ath9k_flush thread can not be executed. Condition ldv_usb_state==1 means that the thread was successfully created. So, the assert check can not be performed in parallel with the assignment.

The same for ldv_assert(pdev==9). The thread ath9k_flush can not be executed here.

Look at .c file, there are some hints in comments.

[tautschnig]

Thank you for clarifying @PavelAndrianov, my apologies for the false alarm.