Causality test case 3 and 19 about cs431 HOT 6 CLOSED

@efenniht
Actually I meant maybe there shoud be a constraint that t cannot be written on the other threads, but yes, I agree with you!

from cs431.

I found that problem 19 is already asked in the other question(#9), but I confused that how message passing works. I think y=42 should means that x=42. But, how to enforce it?

from cs431.

On test case 3: Thread 1 is able to read different values from x for r1 and r2 thanks to Thread 3, but Thread 1 is also able to read the same value from x for r1 and r2. Certification requires the ability---not necessity---to fulfill the thread's promises, and the promise to write y=1 is justified by the certification in which Thread 1 reads the same value from x for r1 and r2.

from cs431.

FYI, my interpretation of "join thread" is:

join thread 2                     || x = 1
r1 = x
~>
while (t.load(acquire) == 0) {}   || x = 1
r1 = x                            || t.store(1, release)

where t is initialized with 0.

from cs431.

@efenniht
You mean, of course, "where t is also a unique virtual variable that only exists on the pair of joinee-joiner threads?

from cs431.

@drzix, I think it's enough that such t exists for each joinee thread:

a = 1 || join thread 1 || join thread 1
~>
a = 1                || while (t.load(acquire) == 0) {} || while (t.load(acquire) == 0) {}
t.store(1, release)

from cs431.