Причинно-следственное упорядочение, логические часы, репликация конечного автомата: различия между версиями

Лэмпорт [5] определяет элегантную систему организации логических часов, удовлетворяющую условию, изложенному в определении 3. Часы процессы <math>p_i \;</math> представлены регистром <math>C_i \;</math>, таким, что <math>C_i \langle a \rangle</math>  представляет собой значение, хранящееся в <math>C_i \;</math> в момент выполнения события <math>a \;</math>. Каждое сообщение m несет временную метку <math>T_m \;</math>, которая равна времени отправки m. Система часов может быть описана при помощи следующих правил:

 

1. Каждый процесс <math>p_i \;</math> увеличивает <math>C_i \;</math> между любыми двумя последовательными событиями.

 

2. Если событие <math>a \;</math> заключается в отправке сообщения m процессом <math>p_i \;</math>, то сообщение m содержит временную метку <math>T_m = C_i \langle a \rangle</math>.

 

3. После получения сообщения m процесс <math>p_j \;</math> присваивает регистру <math>C_j \;</math> значение <math>max(C_j, T_m + 1) \;</math> (еще до выполнения события получения).

Алгоритм взаимного исключения основывается на следующей идее: каждый процесс поддерживает копию очереди запросов, а алгоритм гарантирует, что копии во всех процессах остаются согласованными. Это достигается за счет полного упорядочения сообщений с запросами согласно временным меткам, полученным от логических часов процессов-отправителей.

• Для любых процессов <math>p_i \;</math> и <math>p_j \;</math> сообщения от <math>p_i \;</math> к <math>p_j \;</math> оказываются получены в том же порядке, в котором они были отправлены.