SC declarative model

基于Leslie Lamport 的定义，限定存在一个所有事件上的全序关系：

(sc应该是strict total order)

或者等价地，用modification order来定义：

（mo是strict total order，rb定义中排除id是因为有RMW的存在）

注意上述定义要求rf不自反，故不会出现RMW的读来自自己的写的情况。