TSO: rmw old_ts 재변경

[kyeongmincho]

문제

이전에 rmw step의 old_ts에 대한 조건으로 exclusive를 사용하기로 한 적이 있음:
"old_ts부터 ts까지 tid가 아닌 곳에서 쓴 메시지는 없다"

• 그런데 같은 스레드에서 rmw 이전에 메시지를 썼다면, 그 이전 메시지를 old_ts로 잡는 게 가능하다
• 또한 TsoPFtoA1 에서 RPROP1 증명이 안 된다(혹은 복잡해진다)

예시

X = 666
r1 = CAS(X, 0, 42) # success

성공시켜주면 안 된다..

경과

• 이전 제안대로 "old_ts부터 ts-1 까지 메시지가 없다" 로 조건을 바꿈
• 증명은 잘 됨

질문

• ARM 에서는 ex read와 ex write 사이에 또 다른 write이 들어가도 허용되는 것 같은데 원래 그런 건가요?

[sunghwanl]

안녕하세요,
지나가다가 이슈를 발견하여 답변 달아봅니다.

ARM의 atomic axiom을 보시면 rmw & (fre; coe) = empty로, read와 write 사이에 external write만 금지하고 있습니다.
예를 들어, 다음과 같은 코드가 가능할 것입니다.

c = load-exclusive X
store X 1
s = store-exclusive X (c + 1)

다만 compile을 통해 나오는 어셈블리에 저런 형태는 없지 않을까 예상합니다.

[jeehoonkang]

이거 @drzix 님이랑 제가 전화로 이야기했던 것 같은데.. 경민님 우리가 애기했던 결론을 답으로 남겨주시기 부탁드립니다.

(일반적으로, remote coworking을 해야하므로, 지금처럼 그랬던 것처럼 앞으로도 구두로 논의된 내용을 모두 github에 정리해주시길 부탁드립니다.)

[kyeongmincho]

@Sung-HwanLee
안녕하세요,

지금 정의된 tso의 rmw 상으로는 이슈와 같이 정의되어 있고, 때문에 이슈와 같은 행동이 가능하게 되어버려 이를 막고자 룰 변경을 하려고 한 맥락이었습니다.

• 성환님 말씀대로 arm에서는 성환님 예시코드 같은 행동이 가능하다는 걸 알게 되었습니다.
• tso에서는 이슈와 같은 행동을 불가능하게 해주어야하는데
  • 교수님과 상의 결과 제가 제안한 latest old_ts (ts-1)은 arm과의 유사성을 위해서 (즉, exclusive를 살리기 위하여) 사용하지 않기로 하였고,
  • 대신 coh(x) <= oldts 라는 조건을 추가하기로 하였습니다.

[kyeongmincho]

2020/5/26 미팅 결론:

• COH: latest old_ts coh(x) mem 을 추가하기로 함
  • 약간 돌아가는 느낌이 있긴 하나,
  • read에서의 COH와의 일관성을 위해서라는 결론