Promising semantics for 20 causality test cases and some supplementary materials

[poppindouble]

Hello guys:

I made my own proof regarding 20 causality test cases, here is the link for it.

Also, concurrency is one of my favourite topic, I have been writing down my own understanding regarding Rust programming language features and how Rust is handling concurrency, this blog is one of my current work. I try my best to use plain English(means no blur industrial terms or over complicated academic terms) to describe the problem, hope you will enjoy it. The blog is still W.I.P, but it should have some solid contents already.

Hope those supplementary materials could help you with your current course! Good Luck!

If I made any mistakes in my blog or my proof, you are more than welcome to leave me a message here.

[poppindouble]

slides updated with more detailed explanation

[blue-int]

In causality test case 7, thread 1 should promise value 1 to not execute r1=Z before thread 2's Z=r3.

[poppindouble]

@integerblue sorry for my late reply. Yes, you are correct, as long as we can find a way(no matter it is the execution order of different threads, or operation reordering without violating the RR,WW,WR,RW coherence within a thread, even with the certified value’s influence on other threads) to re-certify the desired output, then we are good.

[jeehoonkang]

Relatedly: https://github.com/poppindouble/lock-free/blob/master/lock_free.md

[kyeongmincho]

@jeehoonkang

How about adding the link into this slide and closing this issue?