Open jprotze opened 1 year ago
@LChenGit can you explain, why this code is marked as having a data race? The locking pattern really looks like in DRB186-barrier2-no.c. Thread 0 cannot pass until Thread 1 releases l1 and Thread 1 cannot pass until Thread 0 releases l0. Did you mean to comment l1?
In addition, the code would have way more data race pairs than listed - if the barrier would not synchronize. Both threads read x in lines 99 and 106.
Ok, as soon as thread 0 releases l0, thread 1 can run through multiple barrier_wait cycles, so that both threads can actually end up in any epoch concurrently. Besides the data race, this can actually can lead to a deadlock.
With the printf statements in the code, any pair of conflicting read/write accesses should be listed in the comment. I also suggest to include a better description of the issue in the comment.
I updated #151 to provide this description and added the missing data race pairs
Hi,
Sorry for the late reply. I was communicating with the original author for this code. We tried with CIVL and here is the output:
Thread 0: phase 1, i=0, x=1 Thread 1: phase 1, i=0, x=1 t0 released l0 t1 obtained l0 t1 released l1 t1 released l0 t1 obtained l1 t1 obtained l0 t1 released l1 t1 released l0 t1 obtained l1 Thread 1: phase 3, i=0, x=1 t1 obtained l0 t1 released l1 t1 released l0 t0 obtained l1 t0 obtained l0 t0 released l1 Thread 0 wrote t1 obtained l1 Thread 1 wrote Data-race detected: {x} written by thread 1 intersects {x} written by thread 0
We also used inspector to test the code and inspector reported no data race.
I think your comment matches the CIVL output.
The lock-based barrier is effectively the same pattern as DRB186-barrier2-no.c. The commented lock is not necessary to provide the barrier semantics.