linearizability / sequential consistency

1. linearizability

history H의 method invocation에 response를 만들거나, invocation을 삭제해서 만든 어떤 history G가 있을 때, equivalent legal sequential history S에게 →_G ⊂→_S인 경우가 있는 history H를 linearizable 하다고 한다.

다시 설명하면, linearizability가 있다는 것은, 어떤 history H가 extended history G가 될 수 있다는 것이다. history G는 모든 method가 invocation과 response가 있고, 그 사이에 순간적으로 영향을 미치는 시각이 있으며, 그러한 sequential behavior가 옳아야 한다. 

첨에 무슨 소리인가 전혀 감도 안왔는데, 그냥 외우면 된다. atomic register를 사용한 history는 linearizable 하므로 병렬화가 쉽게 되기 때문에 atomic register를 만들려고 하는 것이다.

 - 참고 -

sequential history: 모든 method invocation 바로 뒤에 response가 있는 것.

legal history: 모든 object q에 대해 H|q가 sequential history인 것.

따라서 equivalent legal sequential history는 원래 history와 똑같은 결과가 실행되는 legal, sequential history 이다.

2. sequential consistency

history가 linearizability를 가진다면 shared objects에 대해 강력한 분석도구가 될 수 있지만(shared objects의 atomic한 실행이 언제 이루어지는지 알 수 있으므로), hardware manufacturer에게는 큰 제약이다. 따라서 약한 제약을 가진 sequential consistency에 대해 알아보자. 근데 이것도 큰 제약이라서 결국 못쓴다.

linearizability의 조건에서 →_G ⊂→_S를 제외하고 다 만족하면, sequential consistency한 것이다. 풀어서 말하자면, 다른 쓰레드가 한 쓰레드보다 실행될 수 있는 범위가 뒤에 있지만, 먼저 실행할 수 있다고 보고 history를 만드는 것이다. 그런데 linearizability는 composability가 있어서 divide and conquer가 가능하지만, sequential consistency는 불가능하다. 그래서 linearizability보다는 쓸모가 없다.

sequential consistency 또한 큰 제약이라서 hardware manufacturer가 지원하지 못하므로, memory barrier를 대신 제공하여 compiler optimization을 막아서 sequential consistency를 가능하게 한다. 

Total Store Ordering도 언급되긴 했는데 그냥저냥 하다가 넘어갔다. TSO와 memory barrier를 적절히 섞어쓰면 sequential consistency를 만들 수 있다고 한다.

TSO부터 뭔소린가 싶지만 그냥 그렇다고 외웠다... 책에서조차 제대로 된 설명이 너무 부족하다.