Question about fence(SC) & Promise

[kyeongmincho]

T1:
r2 = Y
fence(SC)
X = 1

T2:
r1 = X
Y = r1

// r1 = r2 = 1  allowed?

I tried:

1. Suppose I promise and certify X = 1@1 at T1.
2. I execute T2 sequentially.
3. I execute T1 to re-certify X = 1. At that moment, r2 becomes 1 read from Y and move the global view { X: 0@0, Y: 0@0 } to { X: 0@0, Y: 1@2} since T1's view is also { X: 0@0, Y: 1@2}.
4. Finally, I can re-certify X = 1@1 and judge this behavior is allowed.

Question

However, It's weird because, as I know, it cannot be reordered by store-hoisting due to fence(SC) which forbids to reorder the program order back and forth. But it seems to be allowed on Promising Semantics. Did I miss something?

[tomtomjhj]

From the Promising semantic paper,

When a thread T executes an SC fence, in addition to the effect of both an acquire and a release fence, T increases both its cur view and the global timemap to the maximum of the two.

In order to avoid cases where execution gets stuck, we must ensure that some message can be read for every location. Thus we require that the view attached to a promise message includes only timestamps of messages that exist in memory at the time the promise is made. [...] Hence, release fences effectively serve also as barriers for promises. We find it convenient to explicitly require this in our semantics: whenever a release fence is performed, the set of promises of the executing thread must be empty.

So T1 can't promise x=1 across the fence in the first place. But I'm not sure how allowing such a promise in this particular case can make the execution get stuck.

[kyeongmincho]

• Thanks, @tomtomjhj !
• I'll give a thought, either.

[jeehoonkang]

@tomtomjhj Thanks for a thoughtful answer.