happend-before
定義
$ e_iと$ e_jを分散システム内のプロセスで起こるイベントとする。ここで、以下のいずれかの条件を充足するとき、イベント$ e_iはイベント$ e_jに先行する($ e_i happend-before $ e_j)
イベント$ e_i, $ e_jは同じプロセスで起きて、$ e_iの命令は$ e_jの命令より前に実行されている。
イベント$ e_iはプロセス$ p_iでのメッセージ$ mの送信イベント$ s_i \lbrack m \rbrackであり、$ e_jはプロセス$ p_jでのメッセージ$ mの受信イベント$ r_j \lbrack m \rbrackである
$ e_i \Rightarrow e_kかつ$ e_k \Rightarrow e_jからなるイベント$ e_kが存在する
メモ
Transitive relation(推移関係)が成り立つ
a -> b かつ b -> cなら、a -> c