%% Untimed abstraction of the lease sub-protocol of the DHCP Failover protocol %% Written by Shinya Umeno %% dhcpf_lease_seq_num: CONTEXT = BEGIN %% The number of users USER_SIZE: NATURAL = 2; FIRST_USER_ID: NATURAL = 1; LAST_USER_ID: NATURAL = FIRST_USER_ID + USER_SIZE - 1; USER_ID: TYPE = [FIRST_USER_ID .. LAST_USER_ID]; %% The number of servers SERVER_SIZE: NATURAL = 2; FIRST_SERVER_ID: NATURAL = USER_SIZE + 1; LAST_SERVER_ID: NATURAL = FIRST_SERVER_ID + SERVER_SIZE - 1; SERVER_ID: TYPE = [FIRST_SERVER_ID .. LAST_SERVER_ID]; %% Sequence numbers SEQ_NUM_SIZE: NATURAL = 15; SEQ_NUMBER: TYPE = [0 .. SEQ_NUM_SIZE]; %% 0 represents a special symbol for initialization. %% A vector of sequence numbers that servers are currently using. %% This vector is used for finding out an unused sequence number. SERVER_SN_VECTOR: TYPE = ARRAY SERVER_ID OF SEQ_NUMBER; %% A vector of sequence numbers that users are currently using. %% This vector is used for finding out an unused sequence number. USER_SN_VECTOR: TYPE = ARRAY USER_ID OF SEQ_NUMBER; %%%%%% Timing related information (Time Data) %%%%%%%%%%%%%%%%%%%%%%% %% A timing related value is symbolically represented by a timing-value ID. %% We distinguish a snapshot of a local clock value (a time stamp) %% and a timing value arbitrarily chosen by a user (a time nonce). NUMBER_OF_TIME_NONCES: NATURAL = 8; FIRST_TN_ID: NATURAL = 1; LAST_TN_ID: NATURAL = FIRST_TN_ID + NUMBER_OF_TIME_NONCES - 1; TIME_NONCE_ID: TYPE = [FIRST_TN_ID .. LAST_TN_ID]; NUMBER_OF_TIME_STAMPS: NATURAL = 6; FIRST_TS_ID: NATURAL = 1; LAST_TS_ID: NATURAL = FIRST_TS_ID + NUMBER_OF_TIME_STAMPS - 1; TIME_STAMP_ID: TYPE = [FIRST_TS_ID .. LAST_TS_ID]; %% A set of timing values, represented by an array of Booleans. TIME_NONCE_SET: TYPE = ARRAY TIME_NONCE_ID OF BOOLEAN; empty_time_nonce_set: TIME_NONCE_SET = [[id: TIME_NONCE_ID] FALSE]; singleton_tn_set(tn_id: TIME_NONCE_ID): TIME_NONCE_SET = [[id: TIME_NONCE_ID] tn_id = id]; %% A set of time stamps. TIME_STAMP_SET: TYPE = ARRAY TIME_STAMP_ID OF BOOLEAN; empty_time_stamp_set: TIME_STAMP_SET = [[id: TIME_STAMP_ID] FALSE]; singleton_ts_set(ts_id: TIME_STAMP_ID): TIME_STAMP_SET = [[id: TIME_STAMP_ID] ts_id = id]; %% A timing value stored in a non-timeout timing variable is represented by %% the following record that has a set of timing values (representing max(t1,t2, ..., tk)) %% and a set of time stamps (representing max(clock1, ..., clockl) + u). %% If both sets are not empty, then the record represents a maximum of %% max(t ...) and max(clock ...) + u. TIMING_VALUE: TYPE = [# tnset: TIME_NONCE_SET, tsset: TIME_STAMP_SET #]; bottom_timing_value: TIMING_VALUE = (# tnset := empty_time_nonce_set, tsset:= empty_time_stamp_set #); %% Compute the union of two time nonce sets. union_tn_sets(tn_set1, tn_set2: TIME_NONCE_SET): TIME_NONCE_SET = [[tn_id: TIME_NONCE_ID] tn_set1[tn_id] OR tn_set2[tn_id]]; %% Compute the union of two time stamp sets. union_ts_sets(ts_set1, ts_set2: TIME_STAMP_SET): TIME_STAMP_SET = [[ts_id: TIME_STAMP_ID] ts_set1[ts_id] OR ts_set2[ts_id]]; %% max_tn_tv(tn_set: TIME_NONCE_SET, tv: TIMING_VALUE): TIMING_VALUE = (# tnset := union_tn_sets(tn_set, tv.tnset), tsset := tv.tsset #); max_ts_tv(ts_set: TIME_STAMP_SET, tv: TIMING_VALUE): TIMING_VALUE = (# tnset := tv.tnset, tsset := union_ts_sets(ts_set, tv.tsset) #); max_tv(tv1, tv2: TIMING_VALUE): TIMING_VALUE = (# tnset := union_tn_sets(tv1.tnset, tv2.tnset), tsset := union_ts_sets(tv1.tsset, tv2.tsset) #); %% union_tv(tv1, tv2: TIMING_VALUE): TIMING_VALUE = %% The implementation is actually same as max_tv. (# tnset := union_tn_sets(tv1.tnset, tv2.tnset), tsset := union_ts_sets(tv1.tsset, tv2.tsset) #); %% Remove the given time nonce from the given timing value remove_tn(tn_to_be_removed: TIME_NONCE_ID, tn_ts_set: TIMING_VALUE): TIMING_VALUE = (# tnset := [[tn_id: TIME_NONCE_ID] tn_ts_set.tnset(tn_id) AND (tn_id /= tn_to_be_removed)], tsset := tn_ts_set.tsset #); %% Remove the given time stamp from the given timing value remove_ts(ts_to_be_removed: TIME_STAMP_ID, tn_ts_set: TIMING_VALUE): TIMING_VALUE = (# tnset := tn_ts_set.tnset, tsset := [[ts_id: TIME_STAMP_ID] tn_ts_set.tsset(ts_id) AND (ts_id /= ts_to_be_removed)] #); %% A timing value stored in a user's timeout variable is simply a timing value, %% with a boolean that specifies whether the timeout is actually set or not. USER_TIMEOUT_VALUE: TYPE = [# tv: TIMING_VALUE, is_set: BOOLEAN #]; unset_user_timeout: USER_TIMEOUT_VALUE = (# tv := bottom_timing_value, is_set := FALSE #); %% A vector of timing values in timeout variables of users. %% This vector is used for finding out an unused time nonce/stamp ID. USER_TO_VECTOR: TYPE = ARRAY USER_ID OF USER_TIMEOUT_VALUE; %% A timing value stored in a server's timeout variable may have %% a slack value e (epsilon clock skew). SERVER_TIMEOUT_VALUE: TYPE = [# tv: TIMING_VALUE, slack_added: BOOLEAN, is_set: BOOLEAN #]; unset_server_timeout: SERVER_TIMEOUT_VALUE = (# tv := bottom_timing_value, slack_added := FALSE, is_set := FALSE #); %% A vector of timing values in timeout variables of users. %% This vector is used for finding out an unused time nonce/stamp ID. SERVER_TO_VECTOR: TYPE = ARRAY SERVER_ID OF SERVER_TIMEOUT_VALUE; %% The number of timing variables (excluding timeout variables) in the server automaton SERVER_TV_NUM: NATURAL = 3; %% {potlease, acklease, bcast_value} %% Non-timeout timing variables in servers are indexed, and are regarded as %% an array of timing variables. SERVER_TV_INDEX: TYPE = [1 .. SERVER_TV_NUM]; SERVER_TIMING_VALUES: TYPE = ARRAY SERVER_TV_INDEX OF TIMING_VALUE; %% A vector of arrays of timing values in non-timeout variables of servers. SERVER_TV_VECTOR: TYPE = ARRAY SERVER_ID OF SERVER_TIMING_VALUES; %%%%%%% Messages, Channel Buffers %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %% The type of a message from a user to a server is either a request message or a renew message. %% A message also contains a timing information. This is always a time nonce that a user %% arbitrarily chooses. U2S_MESSAGE_TYPE: TYPE = {REQUEST, RENEW}; U2S_MESSAGE: TYPE = [# tn: TIME_NONCE_ID, msg_type: U2S_MESSAGE_TYPE, seq_num: SEQ_NUMBER #]; %% Dummy initial value, not actually used by a process. init_u2s_msg: U2S_MESSAGE = (# tn := FIRST_TN_ID, msg_type := REQUEST, seq_num := 0 #); %% A message from a server to a user contains a offered lease time. %% The message type is always 'ACK', and thus is not modeled here. S2U_MESSAGE: TYPE = [# td: TIMING_VALUE, seq_num: SEQ_NUMBER #]; %% Dummy initial value, not actually used by a process. init_s2u_msg: S2U_MESSAGE = (# td := bottom_timing_value, seq_num := 0 #); %% A message communicated between servers contains a conservative estimate of %% a timing value that a user uses for a lease timeout. When a backup server %% gets a message from a leading server, it updates its conservative estimate %% by over-writing the 'potlease' variable. %% The message type is either 'WRITE' or 'WRITE_ACK'. S2S_MESSAGE_TYPE: TYPE = {WRITE, WRITE_ACK}; S2S_MESSAGE: TYPE = [# potlease: TIMING_VALUE, msg_type: S2S_MESSAGE_TYPE, seq_num: SEQ_NUMBER #]; %% Dummy initial value, not actually used by a process. init_s2s_msg: S2S_MESSAGE = (# potlease := bottom_timing_value, msg_type := WRITE, seq_num := 0 #); %% The buffer of channels, user -> server U2S_BUFFER_SIZE: NATURAL = 1; U2S_BUFFER_RANGE: TYPE = [1 .. U2S_BUFFER_SIZE]; U2S_BUFFER_POINTER: TYPE = [0 .. U2S_BUFFER_SIZE]; U2S_BUFFER: TYPE = ARRAY U2S_BUFFER_RANGE OF U2S_MESSAGE; u2s_empty_buffer: U2S_BUFFER = [[entry: U2S_BUFFER_RANGE] init_u2s_msg]; %% Making two dimensional array of buffers U2S_BUFFERS_AUX: TYPE = ARRAY SERVER_ID OF U2S_BUFFER; U2S_BUFFERS: TYPE = ARRAY USER_ID OF U2S_BUFFERS_AUX; %% Making two dimensional array of buffer pointers U2S_BPS_AUX: TYPE = ARRAY SERVER_ID OF U2S_BUFFER_POINTER; U2S_BPS: TYPE = ARRAY USER_ID OF U2S_BPS_AUX; %% The buffer of channels, server -> user S2U_BUFFER_SIZE: NATURAL = 1; S2U_BUFFER_RANGE: TYPE = [1 .. S2U_BUFFER_SIZE]; S2U_BUFFER_POINTER: TYPE = [0 .. S2U_BUFFER_SIZE]; S2U_BUFFER: TYPE = ARRAY S2U_BUFFER_RANGE OF S2U_MESSAGE; s2u_empty_buffer: S2U_BUFFER = [[entry: S2U_BUFFER_RANGE] init_s2u_msg]; %% Making two dimensional array of buffers S2U_BUFFERS_AUX: TYPE = ARRAY USER_ID OF S2U_BUFFER; S2U_BUFFERS: TYPE = ARRAY SERVER_ID OF S2U_BUFFERS_AUX; %% Making two dimensional array of buffer pointers S2U_BPS_AUX: TYPE = ARRAY USER_ID OF S2U_BUFFER_POINTER; S2U_BPS: TYPE = ARRAY SERVER_ID OF S2U_BPS_AUX; %% The buffer of channels, server -> server S2S_BUFFER_SIZE: NATURAL = 1; S2S_BUFFER_RANGE: TYPE = [1 .. S2S_BUFFER_SIZE]; S2S_BUFFER_POINTER: TYPE = [0 .. S2S_BUFFER_SIZE]; S2S_BUFFER: TYPE = ARRAY S2S_BUFFER_RANGE OF S2S_MESSAGE; s2s_empty_buffer: S2S_BUFFER = [[entry: S2S_BUFFER_RANGE] init_s2s_msg]; %% Making two dimensional array of buffers S2S_BUFFERS_AUX: TYPE = ARRAY SERVER_ID OF S2S_BUFFER; S2S_BUFFERS: TYPE = ARRAY SERVER_ID OF S2S_BUFFERS_AUX; %% Making two dimensional array of buffer pointers S2S_BPS_AUX: TYPE = ARRAY SERVER_ID OF S2S_BUFFER_POINTER; S2S_BPS: TYPE = ARRAY SERVER_ID OF S2S_BPS_AUX; %%%%%% Checking availability of a sequence number, finding the smallest available seq number %%%%%%%%%%%%%%%%%%%% %% Checking availability of a sequence number this_seq_num_available(this_seq_num: SEQ_NUMBER, user_sn_vec: USER_SN_VECTOR, server_sn_vec: SERVER_SN_VECTOR, u2s_buff: U2S_BUFFERS, u2s_bps: U2S_BPS, s2u_buff: S2U_BUFFERS, s2u_bps: S2U_BPS, s2s_buff: S2S_BUFFERS, s2s_bps: S2S_BPS ): BOOLEAN = (FORALL (user_id: USER_ID): user_sn_vec[user_id] /= this_seq_num) AND (FORALL (server_id: SERVER_ID): server_sn_vec[server_id] /= this_seq_num) AND (FORALL (user_id: USER_ID, server_id: SERVER_ID, u2s_buffer_entry: U2S_BUFFER_RANGE): ((u2s_buffer_entry <= u2s_bps[user_id][server_id]) => %% If this entry is not an empty entry u2s_buff[user_id][server_id][u2s_buffer_entry].seq_num /= this_seq_num)) AND (FORALL (server_id: SERVER_ID, user_id: USER_ID, s2u_buffer_entry: S2U_BUFFER_RANGE): ((s2u_buffer_entry <= s2u_bps[server_id][user_id]) => %% If this entry is not an empty entry s2u_buff[server_id][user_id][s2u_buffer_entry].seq_num /= this_seq_num)) AND (FORALL (server_id1, server_id2: SERVER_ID, s2s_buffer_entry: S2S_BUFFER_RANGE): ((s2s_buffer_entry <= s2s_bps[server_id1][server_id2]) => %% If this entry is not an empty entry (server_id1 /= server_id2 => s2s_buff[server_id1][server_id2][s2s_buffer_entry].seq_num /= this_seq_num))); %% Compusing the smallest available sequence number in the current state of the composed system smallest_seq_num_rec(seq_num_rec: SEQ_NUMBER, user_sn_vec: USER_SN_VECTOR, server_sn_vec: SERVER_SN_VECTOR, u2s_buff: U2S_BUFFERS, u2s_bps: U2S_BPS, s2u_buff: S2U_BUFFERS, s2u_bps: S2U_BPS, s2s_buff: S2S_BUFFERS, s2s_bps: S2S_BPS ): SEQ_NUMBER = IF this_seq_num_available(seq_num_rec, user_sn_vec, server_sn_vec, u2s_buff, u2s_bps, s2u_buff, s2u_bps, s2s_buff, s2s_bps) THEN seq_num_rec ELSIF seq_num_rec < SEQ_NUM_SIZE THEN smallest_seq_num_rec(seq_num_rec + 1, user_sn_vec, server_sn_vec, u2s_buff, u2s_bps, s2u_buff, s2u_bps, s2s_buff, s2s_bps) ELSE 0 %% an available sequence number is not found ENDIF; smallest_seq_num(user_sn_vec: USER_SN_VECTOR, server_sn_vec: SERVER_SN_VECTOR, u2s_buff: U2S_BUFFERS, u2s_bps: U2S_BPS, s2u_buff: S2U_BUFFERS, s2u_bps: S2U_BPS, s2s_buff: S2S_BUFFERS, s2s_bps: S2S_BPS ): SEQ_NUMBER = smallest_seq_num_rec(1, user_sn_vec, server_sn_vec, u2s_buff, u2s_bps, s2u_buff, s2u_bps, s2s_buff, s2s_bps); %%%%%% Checking availability of Time Data IDs, finding the smallest available ID, finding a compression, %%%%%%%%% %%%%%% compressing time data. %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %% Checking availability of a time nonce ID this_tn_ID_available(this_tn_id: TIME_NONCE_ID, user_to_vec: USER_TO_VECTOR, server_to_vec: SERVER_TO_VECTOR, server_tv_vec: SERVER_TV_VECTOR, u2s_buff: U2S_BUFFERS, u2s_bps: U2S_BPS, s2u_buff: S2U_BUFFERS, s2u_bps: S2U_BPS, s2s_buff: S2S_BUFFERS, s2s_bps: S2S_BPS ): BOOLEAN = (FORALL (user_id: USER_ID): (user_to_vec[user_id].is_set => NOT user_to_vec[user_id].tv.tnset(this_tn_id))) AND (FORALL (server_id: SERVER_ID): (server_to_vec[server_id].is_set => NOT server_to_vec[server_id].tv.tnset(this_tn_id)) AND (FORALL (server_tv_index: SERVER_TV_INDEX): (NOT server_tv_vec[server_id][server_tv_index].tnset(this_tn_id)))) AND (FORALL (user_id: USER_ID, server_id: SERVER_ID, u2s_buffer_entry: U2S_BUFFER_RANGE): ((u2s_buffer_entry <= u2s_bps[user_id][server_id]) => %% If this entry is not an empty entry NOT u2s_buff[user_id][server_id][u2s_buffer_entry].tn = this_tn_id)) AND (FORALL (server_id: SERVER_ID, user_id: USER_ID, s2u_buffer_entry: S2U_BUFFER_RANGE): ((s2u_buffer_entry <= s2u_bps[server_id][user_id]) => %% If this entry is not an empty entry NOT s2u_buff[server_id][user_id][s2u_buffer_entry].td.tnset(this_tn_id))) AND (FORALL (server_id1, server_id2: SERVER_ID, s2s_buffer_entry: S2S_BUFFER_RANGE): ((s2s_buffer_entry <= s2s_bps[server_id1][server_id2]) => %% If this entry is not an empty entry (server_id1 /= server_id2 => NOT s2s_buff[server_id1][server_id2][s2s_buffer_entry].potlease.tnset(this_tn_id)))); %% Checking availability of a time stamp ID this_ts_ID_available(this_ts_id: TIME_STAMP_ID, user_to_vec: USER_TO_VECTOR, server_to_vec: SERVER_TO_VECTOR, server_tv_vec: SERVER_TV_VECTOR, s2u_buff: S2U_BUFFERS, s2u_bps: S2U_BPS, s2s_buff: S2S_BUFFERS, s2s_bps: S2S_BPS ): BOOLEAN = (FORALL (user_id: USER_ID): (user_to_vec[user_id].is_set => NOT user_to_vec[user_id].tv.tsset(this_ts_id))) AND (FORALL (server_id: SERVER_ID): (server_to_vec[server_id].is_set => NOT server_to_vec[server_id].tv.tsset(this_ts_id)) AND (FORALL (server_tv_index: SERVER_TV_INDEX): (NOT server_tv_vec[server_id][server_tv_index].tsset(this_ts_id)))) AND (FORALL (server_id: SERVER_ID, user_id: USER_ID, s2u_buffer_entry: S2U_BUFFER_RANGE): ((s2u_buffer_entry <= s2u_bps[server_id][user_id]) => %% If this entry is not an empty entry NOT s2u_buff[server_id][user_id][s2u_buffer_entry].td.tsset(this_ts_id))) AND (FORALL (server_id1, server_id2: SERVER_ID, s2s_buffer_entry: S2S_BUFFER_RANGE): ((s2s_buffer_entry <= s2s_bps[server_id1][server_id2]) => %% If this entry is not an empty entry (server_id1 /= server_id2 => NOT s2s_buff[server_id1][server_id2][s2s_buffer_entry].potlease.tsset(this_ts_id)))); %% Time-nonce-ID type augmented with a "not-found" Boolean. %% This type is used for a return value of the function 'smallest_tn_ID' that computes %% the smallest available time nonce ID. TIME_NONCE_ID_WITH_NOT_FOUND: TYPE = [# tn_id: TIME_NONCE_ID, not_found: BOOLEAN #]; init_tn_id_with_not_found: TIME_NONCE_ID_WITH_NOT_FOUND = (# tn_id := FIRST_TN_ID, not_found := false #); init_tn_id_with_not_found_true: TIME_NONCE_ID_WITH_NOT_FOUND = (# tn_id := FIRST_TN_ID, not_found := true #); %% Compute the smallest available time nonce ID in the system. smallest_tn_ID_rec(tn_id_rec: TIME_NONCE_ID, user_to_vec: USER_TO_VECTOR, server_to_vec: SERVER_TO_VECTOR, server_tv_vec: SERVER_TV_VECTOR, u2s_buff: U2S_BUFFERS, u2s_bps: U2S_BPS, s2u_buff: S2U_BUFFERS, s2u_bps: S2U_BPS, s2s_buff: S2S_BUFFERS, s2s_bps: S2S_BPS): TIME_NONCE_ID_WITH_NOT_FOUND = IF this_tn_ID_available(tn_id_rec, user_to_vec, server_to_vec, server_tv_vec, u2s_buff, u2s_bps, s2u_buff, s2u_bps, s2s_buff, s2s_bps) THEN (# tn_id := tn_id_rec, not_found := FALSE #) ELSIF tn_id_rec < LAST_TN_ID %FIRST_TN_ID + NUMBER_OF_TIME_NONCES - 1 THEN smallest_tn_ID_rec(tn_id_rec+1, user_to_vec, server_to_vec, server_tv_vec, u2s_buff, u2s_bps, s2u_buff, s2u_bps, s2s_buff, s2s_bps) ELSE (# tn_id := FIRST_TN_ID, not_found := TRUE #) ENDIF; smallest_tn_ID(user_to_vec: USER_TO_VECTOR, server_to_vec: SERVER_TO_VECTOR, server_tv_vec: SERVER_TV_VECTOR, u2s_buff: U2S_BUFFERS, u2s_bps: U2S_BPS, s2u_buff: S2U_BUFFERS, s2u_bps: S2U_BPS, s2s_buff: S2S_BUFFERS, s2s_bps: S2S_BPS): TIME_NONCE_ID_WITH_NOT_FOUND = smallest_tn_ID_rec(FIRST_TN_ID, user_to_vec, server_to_vec, server_tv_vec, u2s_buff, u2s_bps, s2u_buff, s2u_bps, s2s_buff, s2s_bps); %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %% Time-stamp-ID type augmented with a "not-found" Boolean. %% This type is used for a return value of the function 'smallest_ts_ID' that computes %% the smallest available time stamp ID. TIME_STAMP_ID_WITH_NOT_FOUND: TYPE = [# ts_id: TIME_STAMP_ID, not_found: BOOLEAN #]; init_ts_id_with_not_found: TIME_STAMP_ID_WITH_NOT_FOUND = (# ts_id := FIRST_TS_ID, not_found := FALSE #); init_ts_id_with_not_found_true: TIME_STAMP_ID_WITH_NOT_FOUND = (# ts_id := FIRST_TS_ID, not_found := TRUE #); %% Compute the smallest available time stamp ID in the system. %%%%%%%%%%%%%%%%%%%%%%%%%% smallest_ts_ID_rec(ts_id_rec: TIME_STAMP_ID, user_to_vec: USER_TO_VECTOR, server_to_vec: SERVER_TO_VECTOR, server_tv_vec: SERVER_TV_VECTOR, s2u_buff: S2U_BUFFERS, s2u_bps: S2U_BPS, s2s_buff: S2S_BUFFERS, s2s_bps: S2S_BPS): TIME_STAMP_ID_WITH_NOT_FOUND = IF this_ts_ID_available(ts_id_rec, user_to_vec, server_to_vec, server_tv_vec, s2u_buff, s2u_bps, s2s_buff, s2s_bps) THEN (# ts_id := ts_id_rec, not_found := FALSE #) ELSIF ts_id_rec < LAST_TS_ID %FIRST_TS_ID + NUMBER_OF_TIME_STAMPS - 1 THEN smallest_ts_ID_rec(ts_id_rec+1, user_to_vec, server_to_vec, server_tv_vec, s2u_buff, s2u_bps, s2s_buff, s2s_bps) ELSE (# ts_id := FIRST_TS_ID, not_found := TRUE #) ENDIF; smallest_ts_ID(user_to_vec: USER_TO_VECTOR, server_to_vec: SERVER_TO_VECTOR, server_tv_vec: SERVER_TV_VECTOR, s2u_buff: S2U_BUFFERS, s2u_bps: S2U_BPS, s2s_buff: S2S_BUFFERS, s2s_bps: S2S_BPS): TIME_STAMP_ID_WITH_NOT_FOUND = smallest_ts_ID_rec(FIRST_TS_ID, user_to_vec, server_to_vec, server_tv_vec, s2u_buff, s2u_bps, s2s_buff, s2s_bps); %% Construct a set of time stamp IDs that are used in the system. %%%%%%%%%%%%%%%%%%%%%%% construct_existing_ts_set(user_to_vec: USER_TO_VECTOR, server_to_vec: SERVER_TO_VECTOR, server_tv_vec: SERVER_TV_VECTOR, s2u_buff: S2U_BUFFERS, s2u_bps: S2U_BPS, s2s_buff: S2S_BUFFERS, s2s_bps: S2S_BPS): TIME_STAMP_SET = [[ts_id: TIME_STAMP_ID] NOT this_ts_ID_available(ts_id, user_to_vec, server_to_vec, server_tv_vec, s2u_buff, s2u_bps, s2s_buff, s2s_bps)]; %% setting a server's timeout with slack (epsilon) added. set_server_timeout_with_slack(given_tv: TIMING_VALUE): SERVER_TIMEOUT_VALUE = (# tv := given_tv, slack_added := TRUE, is_set := TRUE #); %% setting a server's timeout using max(clock + u + 2e, TIMEDATA). set_server_timeout_with_double_slacks(given_tv: TIMING_VALUE, user_to_vec: USER_TO_VECTOR, server_to_vec: SERVER_TO_VECTOR, server_tv_vec: SERVER_TV_VECTOR, s2u_buff: S2U_BUFFERS, s2u_bps: S2U_BPS, s2s_buff: S2S_BUFFERS, s2s_bps: S2S_BPS): SERVER_TIMEOUT_VALUE = LET existing_ts_set: TIME_STAMP_SET = construct_existing_ts_set(user_to_vec,server_to_vec,server_tv_vec,s2u_buff,s2u_bps,s2s_buff,s2s_bps) IN (# tv := max_ts_tv(existing_ts_set, given_tv), slack_added := TRUE, is_set := TRUE #); %% COMPRESSION %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% COMPRESSION: TYPE = [# tn: TIME_NONCE_ID_WITH_NOT_FOUND, ts: TIME_STAMP_ID_WITH_NOT_FOUND #]; init_compression: COMPRESSION = (# tn := init_tn_id_with_not_found_true, ts := init_ts_id_with_not_found_true #); find_tn_compression_rec(tn1, tn2: TIME_NONCE_ID, my_ID: SERVER_ID, my_server_to: SERVER_TIMEOUT_VALUE, my_server_tv1, my_server_tv2, my_server_tv3: TIMING_VALUE, user_to_vec: USER_TO_VECTOR, server_to_vec: SERVER_TO_VECTOR, server_tv_vec: SERVER_TV_VECTOR, u2s_buff: U2S_BUFFERS, u2s_bps: U2S_BPS, s2u_buff: S2U_BUFFERS, s2u_bps: S2U_BPS, s2s_buff: S2S_BUFFERS, s2s_bps: S2S_BPS ): TIME_NONCE_ID_WITH_NOT_FOUND = %% Case: a compression is found, IF %==== For all timed variables, tn1 = tn2 ======== %% my timeout / tv my_server_to.is_set => (my_server_to.tv.tnset(tn1) = my_server_to.tv.tnset(tn2)) AND my_server_tv1.tnset(tn1) = my_server_tv1.tnset(tn2) AND my_server_tv2.tnset(tn1) = my_server_tv2.tnset(tn2) AND my_server_tv3.tnset(tn1) = my_server_tv3.tnset(tn2) AND %% user_to_vec (FORALL (i: USER_ID): user_to_vec[i].is_set => user_to_vec[i].tv.tnset(tn1) = user_to_vec[i].tv.tnset(tn2)) AND %% server_to_vec, server_tv_vec (FORALL (j: SERVER_ID): j /= my_ID => (server_to_vec[j].is_set => server_to_vec[j].tv.tnset(tn1) = server_to_vec[j].tv.tnset(tn2)) AND (FORALL (j_tv: SERVER_TV_INDEX): server_tv_vec[j][j_tv].tnset(tn1) = server_tv_vec[j][j_tv].tnset(tn2))) AND %% u2s_buff (just one tn is used, thus tn1 or tn2 should not match with a buffer entry) (FORALL (i: USER_ID, j: SERVER_ID, buff_entry: U2S_BUFFER_RANGE): buff_entry <= u2s_bps[i][j] => %% If this entry is not empty tn1 /= u2s_buff[i][j][buff_entry].tn AND tn2 /= u2s_buff[i][j][buff_entry].tn) AND %% s2u_buff (FORALL (j: SERVER_ID, i: USER_ID, buff_entry: S2U_BUFFER_RANGE): buff_entry <= s2u_bps[j][i] => %% If this entry is not empty s2u_buff[j][i][buff_entry].td.tnset(tn1) = s2u_buff[j][i][buff_entry].td.tnset(tn2)) AND %% s2s_buff (FORALL (j1, j2: SERVER_ID, buff_entry: S2S_BUFFER_RANGE): buff_entry <= s2s_bps[j1][j2] => %% If this entry is not empty s2s_buff[j1][j2][buff_entry].potlease.tnset(tn1) = s2s_buff[j1][j2][buff_entry].potlease.tnset(tn2)) AND %==== Some process/channel actually uses this tn1 (= tn2)========== %% my timeout / tv (my_server_to.is_set AND my_server_to.tv.tnset(tn1) OR my_server_tv1.tnset(tn1) OR my_server_tv2.tnset(tn1) OR my_server_tv3.tnset(tn1) OR %% user_to_vec (EXISTS (i: USER_ID): user_to_vec[i].is_set AND user_to_vec[i].tv.tnset(tn1)) OR %% server_to_vec, server_tv_vec (EXISTS (j: SERVER_ID): j/= my_ID AND server_to_vec[j].is_set AND (server_to_vec[j].tv.tnset(tn1) OR EXISTS (j_tv: SERVER_TV_INDEX): server_tv_vec[j][j_tv].tnset(tn1))) OR %% s2u_buff (EXISTS (j: SERVER_ID, i: USER_ID, buff_entry: S2U_BUFFER_RANGE): buff_entry <= s2u_bps[j][i] AND s2u_buff[j][i][buff_entry].td.tnset(tn1)) OR %% s2s_buff (EXISTS (j1, j2: SERVER_ID, buff_entry: S2S_BUFFER_RANGE): buff_entry <= s2s_bps[j1][j2] AND s2s_buff[j1][j2][buff_entry].potlease.tnset(tn1))) THEN (# tn_id := tn2, not_found := false #) %% Case: a compression is not found, and tn2 < last_tn ELSIF tn2 < LAST_TN_ID THEN find_tn_compression_rec (tn1, tn2 + 1, my_ID, my_server_to, my_server_tv1, my_server_tv2, my_server_tv3, user_to_vec, server_to_vec, server_tv_vec, u2s_buff, u2s_bps, s2u_buff, s2u_bps, s2s_buff, s2s_bps) %% Case: a compression is not found, and tn2 = last_tn, and tn1 < last_tn - 1 ELSIF tn1 < LAST_TN_ID - 1 THEN find_tn_compression_rec (tn1 + 1, tn1 + 2, my_ID, my_server_to, my_server_tv1, my_server_tv2, my_server_tv3, user_to_vec, server_to_vec, server_tv_vec, u2s_buff, u2s_bps, s2u_buff, s2u_bps, s2s_buff, s2s_bps) %% Case: a compression is not found, and tn2 = last_tn, and tn1 = last_tn - 1 ELSE (# tn_id := FIRST_TN_ID, not_found := true #) ENDIF; %%%%%%%%%%%%%%%%%%% find_tn_compression(my_ID: SERVER_ID, my_server_to: SERVER_TIMEOUT_VALUE, my_server_tv1, my_server_tv2, my_server_tv3: TIMING_VALUE, user_to_vec: USER_TO_VECTOR, server_to_vec: SERVER_TO_VECTOR, server_tv_vec: SERVER_TV_VECTOR, u2s_buff: U2S_BUFFERS, u2s_bps: U2S_BPS, s2u_buff: S2U_BUFFERS, s2u_bps: S2U_BPS, s2s_buff: S2S_BUFFERS, s2s_bps: S2S_BPS ): TIME_NONCE_ID_WITH_NOT_FOUND = find_tn_compression_rec(FIRST_TN_ID, FIRST_TN_ID + 1, my_ID, my_server_to, my_server_tv1, my_server_tv2, my_server_tv3, user_to_vec, server_to_vec, server_tv_vec, u2s_buff, u2s_bps, s2u_buff, s2u_bps, s2s_buff, s2s_bps); %%%%%%%%%%%%%%%%%% find_ts_compression_rec(ts1, ts2: TIME_STAMP_ID, my_ID: SERVER_ID, my_server_to: SERVER_TIMEOUT_VALUE, my_server_tv1, my_server_tv2, my_server_tv3: TIMING_VALUE, user_to_vec: USER_TO_VECTOR, server_to_vec: SERVER_TO_VECTOR, server_tv_vec: SERVER_TV_VECTOR, s2u_buff: S2U_BUFFERS, s2u_bps: S2U_BPS, s2s_buff: S2S_BUFFERS, s2s_bps: S2S_BPS ): TIME_STAMP_ID_WITH_NOT_FOUND = %% Case: a compression is found, IF %==== For all timed variables, ts1 = ts2 ======== %% my timeout / tv my_server_to.is_set => (my_server_to.tv.tsset(ts1) = my_server_to.tv.tsset(ts2)) AND my_server_tv1.tsset(ts1) = my_server_tv1.tsset(ts2) AND my_server_tv2.tsset(ts1) = my_server_tv2.tsset(ts2) AND my_server_tv3.tsset(ts1) = my_server_tv3.tsset(ts2) AND %% user_to_vec (FORALL (i: USER_ID): user_to_vec[i].is_set => user_to_vec[i].tv.tsset(ts1) = user_to_vec[i].tv.tsset(ts2)) AND %% server_to_vec, server_tv_vec (FORALL (j: SERVER_ID): j /= my_ID => (server_to_vec[j].is_set => server_to_vec[j].tv.tsset(ts1) = server_to_vec[j].tv.tsset(ts2)) AND (FORALL (j_tv: SERVER_TV_INDEX): server_tv_vec[j][j_tv].tsset(ts1) = server_tv_vec[j][j_tv].tsset(ts2))) AND %% s2u_buff (FORALL (j: SERVER_ID, i: USER_ID, buff_entry: S2U_BUFFER_RANGE): buff_entry <= s2u_bps[j][i] => %% If this entry is not empty s2u_buff[j][i][buff_entry].td.tsset(ts1) = s2u_buff[j][i][buff_entry].td.tsset(ts2)) AND %% s2s_buff (FORALL (j1, j2: SERVER_ID, buff_entry: S2S_BUFFER_RANGE): buff_entry <= s2s_bps[j1][j2] => %% If this entry is not empty s2s_buff[j1][j2][buff_entry].potlease.tsset(ts1) = s2s_buff[j1][j2][buff_entry].potlease.tsset(ts2)) AND %==== Some process/channel actually uses this ts1 (= ts2)========== %% my timeout / tv (my_server_to.is_set AND my_server_to.tv.tsset(ts1) OR my_server_tv1.tsset(ts1) OR my_server_tv2.tsset(ts1) OR my_server_tv3.tsset(ts1) OR %% user_to_vec (EXISTS (i: USER_ID): user_to_vec[i].is_set AND user_to_vec[i].tv.tsset(ts1)) OR %% server_to_vec, server_tv_vec (EXISTS (j: SERVER_ID): j/= my_ID AND server_to_vec[j].is_set AND (server_to_vec[j].tv.tsset(ts1) OR EXISTS (j_tv: SERVER_TV_INDEX): server_tv_vec[j][j_tv].tsset(ts1))) OR %% s2u_buff (EXISTS (j: SERVER_ID, i: USER_ID, buff_entry: S2U_BUFFER_RANGE): buff_entry <= s2u_bps[j][i] AND s2u_buff[j][i][buff_entry].td.tsset(ts1)) OR %% s2s_buff (EXISTS (j1, j2: SERVER_ID, buff_entry: S2S_BUFFER_RANGE): buff_entry <= s2s_bps[j1][j2] AND s2s_buff[j1][j2][buff_entry].potlease.tsset(ts1))) THEN (# ts_id := ts2, not_found := false #) %% Case: a compression is not found, and ts2 < last_ts ELSIF ts2 < LAST_TS_ID THEN find_ts_compression_rec (ts1, ts2 + 1, my_ID, my_server_to, my_server_tv1, my_server_tv2, my_server_tv3, user_to_vec, server_to_vec, server_tv_vec, s2u_buff, s2u_bps, s2s_buff, s2s_bps) %% Case: a compression is not found, and ts2 = last_ts, and ts1 < last_ts - 1 ELSIF ts1 < LAST_TS_ID - 1 THEN find_ts_compression_rec (ts1 + 1, ts1 + 2, my_ID, my_server_to, my_server_tv1, my_server_tv2, my_server_tv3, user_to_vec, server_to_vec, server_tv_vec, s2u_buff, s2u_bps, s2s_buff, s2s_bps) %% Case: a compression is not found, and ts2 = last_ts, and ts1 = last_ts - 1 ELSE (# ts_id := FIRST_TS_ID, not_found := true #) ENDIF; %%%%%%%%%%%%%%%%% find_ts_compression(my_ID: SERVER_ID, my_server_to: SERVER_TIMEOUT_VALUE, my_server_tv1, my_server_tv2, my_server_tv3: TIMING_VALUE, user_to_vec: USER_TO_VECTOR, server_to_vec: SERVER_TO_VECTOR, server_tv_vec: SERVER_TV_VECTOR, s2u_buff: S2U_BUFFERS, s2u_bps: S2U_BPS, s2s_buff: S2S_BUFFERS, s2s_bps: S2S_BPS ): TIME_STAMP_ID_WITH_NOT_FOUND = find_ts_compression_rec(FIRST_TS_ID, FIRST_TS_ID + 1, my_ID, my_server_to, my_server_tv1, my_server_tv2, my_server_tv3, user_to_vec, server_to_vec, server_tv_vec, s2u_buff, s2u_bps, s2s_buff, s2s_bps); %%%%%%%%%%%%%%%%%%%%% find_compression(my_ID: SERVER_ID, my_server_to: SERVER_TIMEOUT_VALUE, my_server_tv1, my_server_tv2, my_server_tv3: TIMING_VALUE, user_to_vec: USER_TO_VECTOR, server_to_vec: SERVER_TO_VECTOR, server_tv_vec: SERVER_TV_VECTOR, u2s_buff: U2S_BUFFERS, u2s_bps: U2S_BPS, s2u_buff: S2U_BUFFERS, s2u_bps: S2U_BPS, s2s_buff: S2S_BUFFERS, s2s_bps: S2S_BPS ): COMPRESSION = (# tn := find_tn_compression(my_ID, my_server_to, my_server_tv1, my_server_tv2, my_server_tv3, user_to_vec, server_to_vec, server_tv_vec, u2s_buff, u2s_bps, s2u_buff, s2u_bps, s2s_buff, s2s_bps), ts := find_ts_compression(my_ID, my_server_to, my_server_tv1, my_server_tv2, my_server_tv3, user_to_vec, server_to_vec, server_tv_vec, s2u_buff, s2u_bps, s2s_buff, s2s_bps) #); %%%%%%%%%%%%%%%%%% compress_tv(tv: TIMING_VALUE, compression: COMPRESSION): TIMING_VALUE = (# tnset := [[tn_id: TIME_NONCE_ID] tv.tnset(tn_id) AND %% If the compression for tn is found, then remove that tn_id. (NOT compression.tn.not_found => tn_id /= compression.tn.tn_id)], tsset := [[ts_id: TIME_STAMP_ID] tv.tsset(ts_id) AND %% If the compression for ts is found, then remove that ts_id. (NOT compression.ts.not_found => ts_id /= compression.ts.ts_id)] #); %%%%%%%%%%%%%%%% compress_server_timeout(timeout: SERVER_TIMEOUT_VALUE, compression: COMPRESSION): SERVER_TIMEOUT_VALUE = timeout WITH .tv := compress_tv(timeout.tv, compression); compress_user_timeout(timeout: USER_TIMEOUT_VALUE, compression: COMPRESSION): USER_TIMEOUT_VALUE = timeout WITH .tv := compress_tv(timeout.tv, compression); %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %%%%%% Modules %%%%%%%%%%%%%%%%%%%%%%%%%% %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% ACTIONS: TYPE = {%% Server's actions S_rcv_REQ, S_send_ACK, S_bcast_WRITE, S_rcv_WRITE, S_send_WRITE_ACK, S_rcv_WRITE_ACK, S_rcv_RENEW, S_lease_expired, S_fail, S_recover, S_lead, %% User's actions U_bcast_REQ, U_rcv_ACK, U_send_RENEW, U_lease_expired}; %% ------ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %% Server %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %% ------ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% SERVER_PROGRAM_COUNTER: TYPE = {waiting, ack_to_user, bcast_potlease, send_potlease_ack, down, preparing}; %% The following array is used as an initialized list of backup servers from which %% the primary server receives a "potlease-write-ack". The primary server %% consider that it received an ack from itself. %% For example, if j = 2, [F,T,F,F, ..., F]. potlease_ack_initialized_list(j: SERVER_ID): ARRAY SERVER_ID OF BOOLEAN = [[server_id: SERVER_ID] (server_id = j)]; Server[j: SERVER_ID, initialLead: BOOLEAN]: MODULE = BEGIN OUTPUT pc: SERVER_PROGRAM_COUNTER OUTPUT timeout: SERVER_TIMEOUT_VALUE LOCAL timeout_set: BOOLEAN OUTPUT leading: BOOLEAN LOCAL current_user: USER_ID LOCAL current_user_set: BOOLEAN LOCAL current_seq_num: SEQ_NUMBER LOCAL acklease: TIMING_VALUE LOCAL potlease: TIMING_VALUE LOCAL bcast_value: TIMING_VALUE LOCAL potlease_ack_rcvd: ARRAY SERVER_ID OF BOOLEAN LOCAL potlease_ack_leader: SERVER_ID %% For synchronization %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %%% Scheduling control INPUT last_action: ACTIONS INPUT last_S_sender_actor: SERVER_ID %% sender, or actor for 'lead', etc. INPUT last_S_receiver: SERVER_ID INPUT last_U_actor: USER_ID %%% Auxiliary variables for value passing by action synchronization. INPUT last_u2s_msg: ARRAY USER_ID OF U2S_MESSAGE %% \ Each represents the first entry of the channel buffer. INPUT last_s2s_rcvd_msg: ARRAY SERVER_ID OF S2S_MESSAGE %% / Use it as it is, instead of u2s_msg' (the next state value). OUTPUT last_s2u_msg: S2U_MESSAGE OUTPUT last_s2s_sending_msg: S2S_MESSAGE OUTPUT last_s2u_sending_target: USER_ID OUTPUT last_s2s_sending_target: SERVER_ID %%% Precondition (guard) of sever actions OUTPUT S_send_ACK_enabled: BOOLEAN OUTPUT S_bcast_WRITE_enabled: BOOLEAN OUTPUT S_send_WRITE_ACK_enabled: BOOLEAN OUTPUT S_lease_expired_enabled: BOOLEAN %% For finding an available time nonce/stamp ID %%%%%%%%%%%%%%%%%%%%%%%%%%%% INPUT user_to_vec: USER_TO_VECTOR INPUT server_to_vec: SERVER_TO_VECTOR INPUT server_tv_vec: SERVER_TV_VECTOR INPUT u2s_buff: U2S_BUFFERS INPUT u2s_bps: U2S_BPS INPUT s2u_buff: S2U_BUFFERS INPUT s2u_bps: S2U_BPS INPUT s2s_buff: S2S_BUFFERS INPUT s2s_bps: S2S_BPS OUTPUT server_tvs: SERVER_TIMING_VALUES %% For outputing time data in this server %% For outputing a newly picked time stamp ID OUTPUT new_time_stamp_id: TIME_STAMP_ID_WITH_NOT_FOUND OUTPUT new_time_stamp_id_picked: BOOLEAN OUTPUT new_time_stamp_unavailable_error: BOOLEAN %% For outputing the ts/tn ids for time data compression OUTPUT compression: COMPRESSION INITIALIZATION timeout = unset_server_timeout; pc = waiting; leading = initialLead; current_user_set = FALSE; current_user = 1; %% * (Current user is not set, thus this user ID is a dummy.) current_seq_num = 0; acklease = bottom_timing_value; potlease = bottom_timing_value; bcast_value = bottom_timing_value; potlease_ack_rcvd = potlease_ack_initialized_list(j); potlease_ack_leader = USER_SIZE + 1; %% * last_s2u_msg = init_s2u_msg; %% * last_s2s_sending_msg = init_s2s_msg; %% * last_s2u_sending_target = 1; %% * last_s2s_sending_target = FIRST_SERVER_ID; %% * new_time_stamp_id = (# ts_id := FIRST_TS_ID, not_found := false #); %% * new_time_stamp_id_picked = FALSE; %% * compression = init_compression; %% * %% * -- These initializations are just for reducing the number of initial states. %% The actual initial values do not affect the behavior of the system. DEFINITION timeout_set = timeout.is_set; %% Preconditions of actions S_send_ACK_enabled = (pc = ack_to_user); S_bcast_WRITE_enabled = (pc = bcast_potlease); S_send_WRITE_ACK_enabled = (pc = send_potlease_ack); S_lease_expired_enabled = (timeout_set); %% For outputing time data in this server server_tvs = [[i:SERVER_TV_INDEX] IF i = 1 THEN acklease ELSIF i = 2 THEN potlease ELSE bcast_value ENDIF]; new_time_stamp_unavailable_error = new_time_stamp_id.not_found; %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% TRANSITION [ S_rcv_REQ: last_action' = S_rcv_REQ AND last_S_receiver' = j --> new_time_stamp_id_picked' = (leading AND NOT current_user_set AND pc = waiting); current_user' = IF new_time_stamp_id_picked' THEN last_U_actor' ELSE current_user ENDIF; current_user_set' = IF new_time_stamp_id_picked' THEN TRUE ELSE current_user_set ENDIF; current_seq_num' = IF new_time_stamp_id_picked' THEN last_u2s_msg[last_U_actor'].seq_num ELSE current_seq_num ENDIF; new_time_stamp_id' = IF new_time_stamp_id_picked' %% Pick a new time stamp ID. THEN smallest_ts_ID(user_to_vec, server_to_vec, server_tv_vec, s2u_buff, s2u_bps, s2s_buff, s2s_bps) ELSE new_time_stamp_id ENDIF; acklease' = IF new_time_stamp_id_picked' THEN (# tnset := empty_time_nonce_set, tsset := singleton_ts_set(new_time_stamp_id'.ts_id) #) ELSE acklease ENDIF; potlease' = IF new_time_stamp_id_picked' THEN acklease' ELSE potlease ENDIF; bcast_value' = IF new_time_stamp_id_picked' THEN max_tn_tv(singleton_tn_set(last_u2s_msg[last_U_actor'].tn), acklease') ELSE bcast_value ENDIF; timeout' = IF new_time_stamp_id_picked' THEN set_server_timeout_with_slack(potlease') %% potlease' + e ELSE timeout ENDIF; pc' = IF new_time_stamp_id_picked' THEN ack_to_user ELSE pc ENDIF; [] S_send_ACK: last_action' = S_send_ACK AND last_S_sender_actor' = j --> pc' = bcast_potlease; %% The following is for synchronization. last_s2u_msg' = (# td := acklease, seq_num := current_seq_num #); last_s2u_sending_target' = current_user; [] S_bcast_WRITE: last_action' = S_bcast_WRITE AND last_S_sender_actor' = j --> pc' = waiting; potlease_ack_rcvd' = potlease_ack_initialized_list(j); %% The following is for synchronization. last_s2s_sending_msg' = (# potlease := bcast_value, msg_type := WRITE, seq_num := current_seq_num #); %% The following is for a special case (# of server = 1). %% In the case that # of server = 1, the server immediately updates acklease (no waiting for other servers' ack). % acklease' = IF SERVER_SIZE = 1 THEN max_tv(acklease, bcast_value) ELSE acklease ENDIF; [] S_rcv_WRITE: last_action' = S_rcv_WRITE AND last_S_receiver' = j --> bcast_value' = IF (NOT leading AND pc /= down) THEN last_s2s_rcvd_msg[last_S_sender_actor'].potlease ELSE bcast_value ENDIF; potlease' = IF (NOT leading AND pc /= down) THEN max_tv(potlease, last_s2s_rcvd_msg[last_S_sender_actor'].potlease) ELSE potlease ENDIF; current_seq_num' = IF (NOT leading AND pc /= down) THEN last_s2s_rcvd_msg[last_S_sender_actor'].seq_num ELSE current_seq_num ENDIF; potlease_ack_leader' = IF (NOT leading AND pc /= down) THEN last_S_sender_actor' ELSE potlease_ack_leader ENDIF; pc' = IF (NOT leading AND pc /= down) THEN send_potlease_ack ELSE pc ENDIF; [] S_send_WRITE_ACK: last_action' = S_send_WRITE_ACK AND last_S_sender_actor' = j --> pc' = waiting; %% The following is for synchronization. last_s2s_sending_msg' = (# potlease := bcast_value, msg_type := WRITE_ACK, seq_num := current_seq_num #); last_s2s_sending_target' = potlease_ack_leader; [] S_rcv_WRITE_ACK: last_action' = S_rcv_WRITE_ACK AND last_S_receiver' = j --> potlease_ack_rcvd'[last_S_sender_actor'] = LET rcvd_msg: S2S_MESSAGE = last_s2s_rcvd_msg[last_S_sender_actor'] IN IF (rcvd_msg.seq_num = current_seq_num AND leading AND pc /= down) THEN TRUE ELSE potlease_ack_rcvd[last_S_sender_actor'] ENDIF; acklease' = LET rcvd_msg: S2S_MESSAGE = last_s2s_rcvd_msg[last_S_sender_actor'] IN IF (rcvd_msg.seq_num = current_seq_num AND leading AND pc /= down) THEN IF (FORALL (j_:SERVER_ID): potlease_ack_rcvd'[j_]) THEN max_tv(acklease, rcvd_msg.potlease) ELSE acklease ENDIF ELSE acklease ENDIF; [] S_rcv_RENEW: last_action' = S_rcv_RENEW AND last_S_receiver' = j --> new_time_stamp_id_picked' = (leading AND last_U_actor' = current_user AND current_user_set); new_time_stamp_id' = IF new_time_stamp_id_picked' %% Pick a new time stamp ID. THEN smallest_ts_ID(user_to_vec, server_to_vec, server_tv_vec, s2u_buff, s2u_bps, s2s_buff, s2s_bps) ELSE new_time_stamp_id ENDIF; %% find compression compression' = IF new_time_stamp_id_picked' THEN %% Pre-compusing the results of the assignments by this transition. LET acklease_p: TIMING_VALUE = max_ts_tv(singleton_ts_set(new_time_stamp_id'.ts_id), acklease) IN LET potlease_p: TIMING_VALUE= max_tv(potlease,acklease_p) IN LET bcast_value_p: TIMING_VALUE = max_tn_tv(singleton_tn_set(last_u2s_msg[last_U_actor'].tn), acklease_p) IN LET timeout_p: SERVER_TIMEOUT_VALUE = set_server_timeout_with_slack(potlease_p) IN %% find a compression using the pre-computed assignment results. find_compression(j, timeout_p, acklease_p, potlease_p, bcast_value_p, user_to_vec, server_to_vec, server_tv_vec, u2s_buff, u2s_bps, s2u_buff, s2u_bps, s2s_buff, s2s_bps) ELSE init_compression ENDIF; %% assign TVs and timeout with consideration of a compression. acklease' = IF new_time_stamp_id_picked' THEN compress_tv( max_ts_tv(singleton_ts_set(new_time_stamp_id'.ts_id), acklease), compression') ELSE acklease ENDIF; potlease' = IF new_time_stamp_id_picked' THEN compress_tv( max_tv(potlease,acklease'), compression') ELSE potlease ENDIF; bcast_value' = IF new_time_stamp_id_picked' THEN compress_tv( max_tn_tv(singleton_tn_set(last_u2s_msg[last_U_actor'].tn), acklease'), compression') ELSE bcast_value ENDIF; timeout' = IF new_time_stamp_id_picked' THEN compress_server_timeout( set_server_timeout_with_slack(potlease'), compression') %% potlease' + e ELSE timeout ENDIF; current_seq_num' = IF new_time_stamp_id_picked' THEN last_u2s_msg[last_U_actor'].seq_num ELSE current_seq_num ENDIF; pc' = IF new_time_stamp_id_picked' THEN ack_to_user ELSE pc ENDIF; [] S_lease_expired: last_action'= S_lease_expired AND last_S_sender_actor' = j --> timeout' = unset_server_timeout; current_user_set' = FALSE; pc' = waiting; [] S_fail: last_action' = S_fail AND last_S_sender_actor' = j --> pc' = down; timeout' = unset_server_timeout; leading' = FALSE; current_user' = 1; current_user_set' = FALSE; current_seq_num' = 0; acklease' = bottom_timing_value; bcast_value' = bottom_timing_value; potlease_ack_rcvd' = potlease_ack_initialized_list(j); %% potlease is not reset in this version. % potlease' = bottom_timing_value; [] S_recover: last_action' = S_recover AND last_S_sender_actor' = j --> pc' = waiting; [] S_lead: last_action' = S_lead AND last_S_sender_actor' = j --> leading' = TRUE; % The following line executes: timeout' = max(clock + u + ``2e'', potlease + e); timeout' = set_server_timeout_with_double_slacks(potlease, user_to_vec, server_to_vec, server_tv_vec, s2u_buff, s2u_bps, s2s_buff, s2s_bps); pc' = preparing; [] ELSE --> ] END; %% ---- %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %% User %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %% ---- %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% already_passed(offered_time: TIMING_VALUE, expired_tn_ts_set: TIMING_VALUE): BOOLEAN = (FORALL (tn_id: TIME_NONCE_ID): offered_time.tnset(tn_id) => expired_tn_ts_set.tnset(tn_id)) AND (FORALL (ts_id: TIME_STAMP_ID): offered_time.tsset(ts_id) => expired_tn_ts_set.tsset(ts_id)); USER_PROGRAM_COUNTER: TYPE = {requesting, leasing}; User[i: USER_ID]: MODULE = BEGIN OUTPUT pc: USER_PROGRAM_COUNTER OUTPUT timeout: USER_TIMEOUT_VALUE OUTPUT current_seq_num: SEQ_NUMBER LOCAL timeout_set: BOOLEAN LOCAL current_server: SERVER_ID LOCAL current_server_set: BOOLEAN %% For synchronization %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %%% Scheduling control INPUT last_action: ACTIONS INPUT last_U_actor: USER_ID INPUT last_S_sender_actor: SERVER_ID %%% Auxiliary variables for value passing by action synchronization. OUTPUT last_u2s_msg: U2S_MESSAGE INPUT last_s2u_msg: ARRAY SERVER_ID OF S2U_MESSAGE OUTPUT last_u2s_sending_target: SERVER_ID %%% Precondition (guard) of user actions OUTPUT U_bcast_REQ_enabled: BOOLEAN OUTPUT U_send_RENEW_enabled: BOOLEAN OUTPUT U_lease_expired_enabled: BOOLEAN %% For finding an available sequence number %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% INPUT user_sn_vec: USER_SN_VECTOR INPUT server_sn_vec: SERVER_SN_VECTOR INPUT u2s_buff: U2S_BUFFERS INPUT u2s_bps: U2S_BPS INPUT s2u_buff: S2U_BUFFERS INPUT s2u_bps: S2U_BPS INPUT s2s_buff: S2S_BUFFERS INPUT s2s_bps: S2S_BPS %% For finding an available time nonce/stamp ID %%%%%%%%%%%%%%%%%%%%%%%%%%%% INPUT user_to_vec: USER_TO_VECTOR INPUT server_to_vec: SERVER_TO_VECTOR INPUT server_tv_vec: SERVER_TV_VECTOR %% also uses buffers (u2s_buff, etc). %% For implication relation among the servers time and the users time LOCAL offered_time_gt_now: BOOLEAN INPUT expired_tn_ts_list: TIMING_VALUE %% For outputing a newly picked time nonce. OUTPUT new_time_nonce_id: TIME_NONCE_ID_WITH_NOT_FOUND OUTPUT new_time_nonce_unavailable_error: BOOLEAN %% For outputing availability information of sequence numbers OUTPUT new_seq_num_unavailable_error: BOOLEAN %% For timeout compression INPUT compression_: ARRAY SERVER_ID OF COMPRESSION INPUT last_S_receiver: SERVER_ID INITIALIZATION timeout = unset_user_timeout; current_seq_num = 0; pc = requesting; current_server_set = FALSE; current_server = FIRST_SERVER_ID; %% * (Current user is not set, thus this server ID is a dummy.) last_u2s_msg = init_u2s_msg; offered_time_gt_now = FALSE; %% * new_time_nonce_id = init_tn_id_with_not_found; %% * new_seq_num_unavailable_error = FALSE; %% * -- These initializations are just for reducing the number of initial states. %% The actual initial values do not affect the behavior of the system. DEFINITION timeout_set = timeout.is_set; new_time_nonce_unavailable_error = new_time_nonce_id.not_found; %% Preconditions of actions U_bcast_REQ_enabled = (pc = requesting); U_send_RENEW_enabled = (pc = leasing); U_lease_expired_enabled = (timeout_set); TRANSITION [ U_bcast_REQ: last_action' = U_bcast_REQ AND last_U_actor' = i --> pc' = requesting; current_seq_num' = smallest_seq_num(user_sn_vec, server_sn_vec, u2s_buff, u2s_bps, s2u_buff, s2u_bps, s2s_buff, s2s_bps); new_seq_num_unavailable_error' = (current_seq_num' = 0); new_time_nonce_id' = smallest_tn_ID(user_to_vec, server_to_vec, server_tv_vec, u2s_buff, u2s_bps, s2u_buff, s2u_bps, s2s_buff, s2s_bps); last_u2s_msg' = (# tn := new_time_nonce_id'.tn_id, msg_type := REQUEST, seq_num := current_seq_num'#); [] U_rcv_ACK: last_action' = U_rcv_ACK AND last_U_actor' = i --> offered_time_gt_now' in IF already_passed(last_s2u_msg[last_S_sender_actor'].td,expired_tn_ts_list) THEN {b: BOOLEAN | b = FALSE} %% If the offered time is already passed, then offered_time_gt_now' becomes FALSE. ELSE {b: BOOLEAN| TRUE} ENDIF; %% Else, nondeterministic choice of TRUE and FALSE. timeout' = IF offered_time_gt_now' AND (pc = requesting OR pc = leasing) AND last_s2u_msg[last_S_sender_actor'].seq_num = current_seq_num THEN (# tv := last_s2u_msg[last_S_sender_actor'].td, is_set := TRUE #) ELSE timeout ENDIF; pc' = IF offered_time_gt_now' AND (pc = requesting OR pc = leasing) AND last_s2u_msg[last_S_sender_actor'].seq_num = current_seq_num THEN leasing ELSE pc ENDIF; current_server' = IF offered_time_gt_now' AND (pc = requesting OR pc = leasing) AND last_s2u_msg[last_S_sender_actor'].seq_num = current_seq_num THEN last_S_sender_actor' ELSE current_server ENDIF; current_server_set' = IF offered_time_gt_now' AND (pc = requesting OR pc = leasing) AND last_s2u_msg[last_S_sender_actor'].seq_num = current_seq_num THEN TRUE ELSE current_server_set ENDIF; [] U_send_RENEW: last_action' = U_send_RENEW AND last_U_actor' = i --> current_seq_num' = smallest_seq_num(user_sn_vec, server_sn_vec, u2s_buff, u2s_bps, s2u_buff, s2u_bps, s2s_buff, s2s_bps); new_seq_num_unavailable_error' = (current_seq_num' = 0); new_time_nonce_id' = smallest_tn_ID(user_to_vec, server_to_vec, server_tv_vec, u2s_buff, u2s_bps, s2u_buff, s2u_bps, s2s_buff, s2s_bps); last_u2s_msg' = (# tn := new_time_nonce_id'.tn_id, msg_type := RENEW, seq_num := current_seq_num'#); last_u2s_sending_target' = current_server; [] U_lease_expired: last_action' = U_lease_expired AND last_U_actor' = i --> timeout' = unset_user_timeout; pc' = requesting; [] Compression_S_rcv_RENEW: last_action' = S_rcv_RENEW --> timeout' = compress_user_timeout(timeout, compression_'[last_S_receiver']); [] ELSE --> ] END; %% ----------- %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %% S2U Channel %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %% ----------- %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %% Buffer Operations s2u_buffer_add(buffer: S2U_BUFFER, msg: S2U_MESSAGE, pointer: U2S_BUFFER_POINTER): S2U_BUFFER = buffer WITH [pointer+1] := msg; s2u_buffer_remove(buffer: S2U_BUFFER): S2U_BUFFER = [[i: S2U_BUFFER_RANGE] IF i = S2U_BUFFER_SIZE THEN init_s2u_msg ELSE buffer[i+1] ENDIF]; %% S2U Channel Module S2U_Channel[j: SERVER_ID, i: USER_ID]: MODULE = BEGIN OUTPUT buffer: S2U_BUFFER OUTPUT pointer: S2U_BUFFER_POINTER %% Pointer for the smallest filled entry. Zero if the buffer is empty. OUTPUT head: S2U_MESSAGE %% Head entry of the buffer FIFO queue. %% For synchronization %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% INPUT last_action: ACTIONS INPUT last_s2u_sending_target: USER_ID INPUT last_s2u_msg: S2U_MESSAGE INPUT last_U_actor: USER_ID INPUT last_S_sender_actor: SERVER_ID OUTPUT buffer_full: BOOLEAN %%% Precondition (guard) of the buffer action OUTPUT U_rcv_ACK_enabled: BOOLEAN %% For tv compression INPUT compression_: ARRAY SERVER_ID OF COMPRESSION INPUT last_S_receiver: SERVER_ID INITIALIZATION buffer = s2u_empty_buffer; pointer = 0; %% The buffer is empty DEFINITION head = buffer[1]; U_rcv_ACK_enabled = (pointer > 0); buffer_full = (pointer = S2U_BUFFER_SIZE); TRANSITION [ Channel_S_send_ACK: last_action' = S_send_ACK AND last_S_sender_actor' = j AND last_s2u_sending_target' = i AND NOT buffer_full --> buffer' = s2u_buffer_add(buffer, last_s2u_msg', pointer); pointer' = pointer + 1; % Send is performed only when pointer < BUFFER_SIZE. [] Channel_U_rcv_ACK: last_action' = U_rcv_ACK AND last_S_sender_actor' = j AND last_U_actor' = i --> buffer' = s2u_buffer_remove(buffer); pointer' = pointer - 1; % Receive is performed only when pointer > 0. [] Compression_S_rcv_RENEW: last_action' = S_rcv_RENEW --> buffer' = [[entry: S2U_BUFFER_RANGE] (# td := compress_tv(buffer[entry].td, compression_'[last_S_receiver']), seq_num := buffer[entry].seq_num #) ]; [] ELSE --> ]; END; %% ----------- %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %% U2S Channel %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %% ----------- %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %% Buffer Operations u2s_buffer_add(buffer: U2S_BUFFER, msg: U2S_MESSAGE, pointer: U2S_BUFFER_POINTER): U2S_BUFFER = buffer WITH [pointer+1] := msg; u2s_buffer_remove(buffer: U2S_BUFFER): U2S_BUFFER = [[i: U2S_BUFFER_RANGE] IF i = U2S_BUFFER_SIZE THEN init_u2s_msg ELSE buffer[i+1] ENDIF]; %% U2S Channel Module U2S_Channel[i: USER_ID, j: SERVER_ID]: MODULE = BEGIN OUTPUT buffer: U2S_BUFFER OUTPUT pointer: U2S_BUFFER_POINTER %% Pointer for the smallest filled entry. Zero if the buffer is empty. OUTPUT head: U2S_MESSAGE %% Head entry of the buffer FIFO queue. %% For synchronization %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% INPUT last_action: ACTIONS INPUT last_u2s_sending_target: SERVER_ID INPUT last_u2s_msg: U2S_MESSAGE INPUT last_U_actor: USER_ID INPUT last_S_sender_actor: SERVER_ID INPUT last_S_receiver: SERVER_ID OUTPUT buffer_full: BOOLEAN %%% Precondition (guard) of the buffer action OUTPUT S_rcv_REQ_enabled: BOOLEAN OUTPUT S_rcv_RENEW_enabled: BOOLEAN INITIALIZATION buffer = u2s_empty_buffer; pointer = 0; %% The buffer is empty DEFINITION head = buffer[1]; S_rcv_REQ_enabled = (pointer > 0 AND head.msg_type = REQUEST); S_rcv_RENEW_enabled = (pointer > 0 AND head.msg_type = RENEW); buffer_full = (pointer = U2S_BUFFER_SIZE); TRANSITION [ Channel_U_bcast_REQ: last_action' = U_bcast_REQ AND last_U_actor' = i AND NOT buffer_full --> buffer' = u2s_buffer_add(buffer, last_u2s_msg', pointer); pointer' = pointer + 1; % Send is performed only when pointer < BUFFER_SIZE. [] Channel_U_send_RENEW: last_action' = U_send_RENEW AND last_U_actor' = i AND last_u2s_sending_target' = j AND NOT buffer_full --> buffer' = u2s_buffer_add(buffer, last_u2s_msg', pointer); pointer' = pointer + 1; % Send is performed only when pointer < BUFFER_SIZE. [] Channel_S_rcv_REQ: last_action' = S_rcv_REQ AND last_U_actor' = i AND last_S_receiver' = j --> buffer' = u2s_buffer_remove(buffer); pointer' = pointer - 1; % Receive is performed only when pointer > 0. [] Channel_S_rcv_RENEW: last_action' = S_rcv_RENEW AND last_U_actor' = i AND last_S_receiver' = j --> buffer' = u2s_buffer_remove(buffer); pointer' = pointer - 1; % Receive is performed only when pointer > 0. [] ELSE --> ]; END; %% ----------- %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %% S2S Channel %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %% ----------- %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %% Buffer Operations s2s_buffer_add(buffer: S2S_BUFFER, msg: S2S_MESSAGE, pointer: S2S_BUFFER_POINTER): S2S_BUFFER = buffer WITH [pointer+1] := msg; s2s_buffer_remove(buffer: S2S_BUFFER): S2S_BUFFER = [[i: S2S_BUFFER_RANGE] IF i = S2S_BUFFER_SIZE THEN init_s2s_msg ELSE buffer[i+1] ENDIF]; %% S2S Channel Module. A message goes: j1 => j2. S2S_Channel[j1, j2: SERVER_ID]: MODULE = BEGIN OUTPUT buffer: S2S_BUFFER OUTPUT pointer: S2S_BUFFER_POINTER %% Pointer for the smallest filled entry. Zero if the buffer is empty. OUTPUT head: S2S_MESSAGE %% Head entry of the buffer FIFO queue. %% For synchronization %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% INPUT last_action: ACTIONS INPUT last_s2s_sending_target: SERVER_ID INPUT last_s2s_sending_msg: S2S_MESSAGE INPUT last_S_sender_actor: SERVER_ID INPUT last_S_receiver: SERVER_ID OUTPUT buffer_full: BOOLEAN %%% Precondition (guard) of the buffer action OUTPUT S_rcv_WRITE_enabled: BOOLEAN OUTPUT S_rcv_WRITE_ACK_enabled: BOOLEAN %% For tv compression INPUT compression_: ARRAY SERVER_ID OF COMPRESSION INITIALIZATION buffer = s2s_empty_buffer; pointer = 0; %% The buffer is empty DEFINITION head = buffer[1]; S_rcv_WRITE_enabled = (pointer > 0 AND head.msg_type = WRITE); S_rcv_WRITE_ACK_enabled = (pointer > 0 AND head.msg_type = WRITE_ACK); buffer_full = (pointer = S2S_BUFFER_SIZE); TRANSITION [ Channel_S_bcast_WRITE: %% broadcast message for all servers except for the broadcaster. last_action' = S_bcast_WRITE AND last_S_sender_actor' = j1 AND NOT buffer_full AND last_S_sender_actor' /= j2 --> buffer' = s2s_buffer_add(buffer, last_s2s_sending_msg', pointer); pointer' = pointer + 1; % Send is performed only when pointer < BUFFER_SIZE [] Channel_S_send_WRITE_ACK: last_action' = S_send_WRITE_ACK AND last_S_sender_actor' = j1 AND last_s2s_sending_target' = j2 AND NOT buffer_full AND last_s2s_sending_target' /= j1 --> buffer' = s2s_buffer_add(buffer, last_s2s_sending_msg', pointer); pointer' = pointer + 1; % Send is performed only when pointer < BUFFER_SIZE [] Channel_S_rcv_WRITE: last_action' = S_rcv_WRITE AND last_S_sender_actor' = j1 AND last_S_receiver' = j2 --> buffer' = s2s_buffer_remove(buffer); pointer' = pointer - 1; % Receive is performed only when pointer > 0. [] Channel_S_rcv_WRITE_ACK: last_action' = S_rcv_WRITE_ACK AND last_S_sender_actor' = j1 AND last_S_receiver' = j2 --> buffer' = s2s_buffer_remove(buffer); pointer' = pointer - 1; % Receive is performed only when pointer > 0. [] Compression_S_rcv_RENEW: last_action' = S_rcv_RENEW --> buffer' = [[entry: S2S_BUFFER_RANGE] buffer[entry] WITH .potlease := compress_tv(buffer[entry].potlease, compression_'[last_S_receiver'])]; [] ELSE --> ]; END; %% ----------- %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %% Environment %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %% ----------- %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %% This module creates the `fail' and `recover' inputs to servers. %% In this SAL implementation, it outputs the enabling condition for the two inputs. Environment: MODULE = BEGIN INPUT server_pc: ARRAY SERVER_ID OF SERVER_PROGRAM_COUNTER OUTPUT S_fail_enabled_: ARRAY SERVER_ID OF BOOLEAN OUTPUT S_recover_enabled_: ARRAY SERVER_ID OF BOOLEAN DEFINITION S_fail_enabled_ = [[j: SERVER_ID] server_pc[j] /= down]; S_recover_enabled_ = [[j: SERVER_ID] server_pc[j] = down]; END; %% ---------------- %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %% Failure Detector %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %% ---------------- %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %% This module represents the failure detector. %% The failure detector tells a server to be a new leading server %% when it detects that the previous leading server becomes down. %% The new leading server is the alive server with the minimun server ID. FailureDetector: MODULE = BEGIN INPUT last_action: ACTIONS INPUT last_S_sender_actor: SERVER_ID INPUT server_pc: ARRAY SERVER_ID OF SERVER_PROGRAM_COUNTER INPUT server_leading: ARRAY SERVER_ID OF BOOLEAN OUTPUT S_lead_enabled_: ARRAY SERVER_ID OF BOOLEAN LOCAL stimulate_lead: BOOLEAN INITIALIZATION stimulate_lead = FALSE; DEFINITION S_lead_enabled_ = IF stimulate_lead THEN [[j: SERVER_ID] %% If j is the smallest-ID alive server, then true. Else false. (FORALL (j2: SERVER_ID): j2 < j => server_pc[j2] = down) AND server_pc[j] /= down ] ELSE [[j: SERVER_ID] FALSE] ENDIF; %% lead in not enabled for any server. TRANSITION [ S_fail: last_action' = S_fail --> stimulate_lead' = IF server_leading(last_S_sender_actor') THEN TRUE ELSE stimulate_lead ENDIF; [] S_lead: last_action' = S_lead --> stimulate_lead' = FALSE; [] ELSE --> ]; END; %% --------- %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %% Scheduler %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %% --------- %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %% * enabling condition %% * timeout ordering %% * FIFO queue overflow/underflow earlier_scheduled_user_timeout_exists(j: SERVER_ID, server_to_vec: SERVER_TO_VECTOR, user_to_vec: USER_TO_VECTOR): BOOLEAN = %% Assuming that server_to_vec[j].is_set is true. EXISTS (i:USER_ID): %% user_to_vec[i] + e <= server_to_vec[j] user_to_vec[i].is_set AND server_to_vec[j].slack_added AND %% If the user i's timeout contains a certain tn or ts id, then the server %% also contains the same tn/ts id. (FORALL (tn_id: TIME_NONCE_ID): (user_to_vec[i].tv.tnset[tn_id] => server_to_vec[j].tv.tnset[tn_id])) AND (FORALL (ts_id: TIME_STAMP_ID): (user_to_vec[i].tv.tsset[ts_id] => server_to_vec[j].tv.tsset[ts_id])); add_to_expired_tn_ts_list(server_to: SERVER_TIMEOUT_VALUE, expired_tn_ts_list: TIMING_VALUE): TIMING_VALUE = union_tv(server_to.tv, expired_tn_ts_list); %% Taking a union of the just-expired ts/tn set and the already-expired ts/tn set. Scheduler: MODULE = BEGIN OUTPUT last_action: ACTIONS OUTPUT last_S_sender_actor: SERVER_ID %% sender, or actor for 'lead', etc. OUTPUT last_S_receiver: SERVER_ID OUTPUT last_U_actor: USER_ID OUTPUT deadlock: BOOLEAN %% Sending target INPUT last_s2u_sending_target_: ARRAY SERVER_ID OF USER_ID INPUT last_s2s_sending_target_: ARRAY SERVER_ID OF SERVER_ID INPUT last_u2s_sending_target_: ARRAY USER_ID OF SERVER_ID %% Input for the precondition of actions INPUT S_rcv_REQ_enabled_ : ARRAY USER_ID OF ARRAY SERVER_ID OF BOOLEAN INPUT S_send_ACK_enabled_ : ARRAY SERVER_ID OF BOOLEAN INPUT S_bcast_WRITE_enabled_ : ARRAY SERVER_ID OF BOOLEAN INPUT S_rcv_WRITE_enabled_ : ARRAY SERVER_ID OF ARRAY SERVER_ID OF BOOLEAN INPUT S_send_WRITE_ACK_enabled_ : ARRAY SERVER_ID OF BOOLEAN INPUT S_rcv_WRITE_ACK_enabled_ : ARRAY SERVER_ID OF ARRAY SERVER_ID OF BOOLEAN INPUT S_rcv_RENEW_enabled_ : ARRAY USER_ID OF ARRAY SERVER_ID OF BOOLEAN INPUT S_lease_expired_enabled_ : ARRAY SERVER_ID OF BOOLEAN INPUT S_fail_enabled_ : ARRAY SERVER_ID OF BOOLEAN INPUT S_recover_enabled_ : ARRAY SERVER_ID OF BOOLEAN INPUT S_lead_enabled_ : ARRAY SERVER_ID OF BOOLEAN INPUT U_bcast_REQ_enabled_ : ARRAY USER_ID OF BOOLEAN INPUT U_rcv_ACK_enabled_ : ARRAY SERVER_ID OF ARRAY USER_ID OF BOOLEAN INPUT U_send_RENEW_enabled_ : ARRAY USER_ID OF BOOLEAN INPUT U_lease_expired_enabled_ : ARRAY USER_ID OF BOOLEAN %% server_to_vec, server_tv_vec, server_sn_vec INPUT server_to_vec_out: SERVER_TO_VECTOR INPUT server_tv_vec_out: SERVER_TV_VECTOR INPUT server_sn_vec_out: SERVER_SN_VECTOR OUTPUT server_to_vec: SERVER_TO_VECTOR OUTPUT server_tv_vec: SERVER_TV_VECTOR OUTPUT server_sn_vec: SERVER_SN_VECTOR %% user_to_vec, user_sn_vec INPUT user_to_vec_out: USER_TO_VECTOR INPUT user_sn_vec_out: USER_SN_VECTOR OUTPUT user_to_vec: USER_TO_VECTOR OUTPUT user_sn_vec: USER_SN_VECTOR %% buffer information INPUT s2u_buffer_full: ARRAY SERVER_ID OF ARRAY USER_ID OF BOOLEAN INPUT s2s_buffer_full: ARRAY SERVER_ID OF ARRAY SERVER_ID OF BOOLEAN INPUT u2s_buffer_full: ARRAY USER_ID OF ARRAY SERVER_ID OF BOOLEAN %% For recording expired time nonce/stamp ID (i.e. server_clock >= time nonce/stamp in the list). %% The list contains of a set of tn and a set of ts. Thus I use the TIMING_VALUE type. OUTPUT expired_tn_ts_list: TIMING_VALUE INPUT server_new_time_stamp_id_picked: ARRAY SERVER_ID OF BOOLEAN INPUT server_new_time_stamp_id: ARRAY SERVER_ID OF TIME_STAMP_ID_WITH_NOT_FOUND INPUT user_new_time_nonce_id: ARRAY USER_ID OF TIME_NONCE_ID_WITH_NOT_FOUND %% For adjusting expired_tn_ts_list to the executed compression INPUT compression_: ARRAY SERVER_ID OF COMPRESSION DEFINITION server_to_vec = server_to_vec_out; server_tv_vec = server_tv_vec_out; server_sn_vec = server_sn_vec_out; user_to_vec = user_to_vec_out; user_sn_vec = user_sn_vec_out; INITIALIZATION last_action = S_rcv_REQ; % * last_S_sender_actor = FIRST_SERVER_ID; % * last_S_receiver = FIRST_SERVER_ID; % * last_U_actor = 1; % * deadlock = FALSE; expired_tn_ts_list = bottom_timing_value; %% The list is empty. %% * -- These initializations are just for reducing the number of initial states. %% The actual initial values do not affect the behavior of the system. TRANSITION [ Schedule_S_rcv_REQ: EXISTS (i: USER_ID, j: SERVER_ID): S_rcv_REQ_enabled_[i][j] --> last_action' = S_rcv_REQ; last_S_receiver' in {j: SERVER_ID | EXISTS (i:USER_ID): S_rcv_REQ_enabled_[i][j]}; last_U_actor' in {i: USER_ID | S_rcv_REQ_enabled_[i][last_S_receiver']}; %% Remove a newly picked time stamp from the expired ts list. expired_tn_ts_list' = IF server_new_time_stamp_id_picked'[last_S_receiver'] THEN remove_ts(server_new_time_stamp_id'[last_S_receiver'].ts_id, expired_tn_ts_list) ELSE expired_tn_ts_list ENDIF; [] Schedule_S_send_ACK: EXISTS (j: SERVER_ID): S_send_ACK_enabled_[j] %% Send is enabled when the buffer is not full % AND s2u_buffer_full[j][last_s2u_sending_target_'[j]] --> last_action' = S_send_ACK; last_S_sender_actor' in {j: SERVER_ID | S_send_ACK_enabled_[j]}; last_U_actor' = last_s2u_sending_target_'[last_S_sender_actor']; [] Schedule_S_bcast_WRITE: EXISTS (j: SERVER_ID): S_bcast_WRITE_enabled_[j] %% Broadcast is enabled when all buffers are not full % AND FORALL (j2: SERVER_ID): s2s_buffer_full[j][j2] --> last_action' = S_bcast_WRITE; last_S_sender_actor' in {j: SERVER_ID | S_bcast_WRITE_enabled_[j]}; [] Schedule_S_rcv_WRITE: EXISTS (j1, j2: SERVER_ID): S_rcv_WRITE_enabled_[j1][j2] --> last_action' = S_rcv_WRITE; last_S_sender_actor' in {j1: SERVER_ID | EXISTS (j2:SERVER_ID): S_rcv_WRITE_enabled_[j1][j2]}; last_S_receiver' in {j2: SERVER_ID | S_rcv_WRITE_enabled_[last_S_sender_actor'][j2]}; [] Schedule_S_send_WRITE_ACK: EXISTS (j: SERVER_ID): S_send_WRITE_ACK_enabled_[j] %% Send is enabled when the buffer is not full % AND s2s_buffer_full[j][last_s2s_sending_target_'[j]] --> last_action' = S_send_WRITE_ACK; last_S_sender_actor' in {j: SERVER_ID | S_send_WRITE_ACK_enabled_[j]}; last_S_receiver' = last_s2s_sending_target_'[last_S_sender_actor']; [] Schedule_S_rcv_WRITE_ACK: EXISTS (j1, j2: SERVER_ID): S_rcv_WRITE_ACK_enabled_[j1][j2] --> last_action' = S_rcv_WRITE_ACK; last_S_sender_actor' in {j1: SERVER_ID | EXISTS (j2:SERVER_ID): S_rcv_WRITE_ACK_enabled_[j1][j2]}; last_S_receiver' in {j2: SERVER_ID | S_rcv_WRITE_ACK_enabled_[last_S_sender_actor'][j2]}; [] Schedule_S_rcv_RENEW: EXISTS (i: USER_ID, j: SERVER_ID): S_rcv_RENEW_enabled_[i][j] --> last_action' = S_rcv_RENEW; last_S_receiver' in {j: SERVER_ID | EXISTS (i:USER_ID): S_rcv_RENEW_enabled_[i][j]}; last_U_actor' in {i: USER_ID | S_rcv_RENEW_enabled_[i][last_S_receiver']}; %% Remove a newly picked time stamp from the expired ts list. expired_tn_ts_list' = compress_tv( IF server_new_time_stamp_id_picked'[last_S_receiver'] THEN remove_ts(server_new_time_stamp_id'[last_S_receiver'].ts_id, expired_tn_ts_list) ELSE expired_tn_ts_list ENDIF, compression_'[last_S_receiver']); [] Schedule_S_lease_expired: EXISTS (j: SERVER_ID): (S_lease_expired_enabled_[j] AND NOT earlier_scheduled_user_timeout_exists(j, server_to_vec, user_to_vec)) --> last_action' = S_lease_expired; last_S_sender_actor' in {j: SERVER_ID | S_lease_expired_enabled_[j] AND NOT earlier_scheduled_user_timeout_exists(j, server_to_vec, user_to_vec)}; expired_tn_ts_list' = add_to_expired_tn_ts_list(server_to_vec[last_S_sender_actor'], expired_tn_ts_list); [] Schedule_S_fail: EXISTS (j: SERVER_ID): S_fail_enabled_[j] --> last_action' = S_fail; last_S_sender_actor' in {j: SERVER_ID | S_fail_enabled_[j]}; [] Schedule_S_recover: EXISTS (j: SERVER_ID): S_recover_enabled_[j] --> last_action' = S_recover; last_S_sender_actor' in {j: SERVER_ID | S_recover_enabled_[j]}; [] Schedule_S_lead: EXISTS (j: SERVER_ID): S_lead_enabled_[j] --> last_action' = S_lead; last_S_sender_actor' in {j: SERVER_ID | S_lead_enabled_[j]}; [] Schedule_U_bcast_REQ: EXISTS (i: USER_ID): U_bcast_REQ_enabled_[i] --> last_action' = U_bcast_REQ; last_U_actor' in {i: USER_ID | U_bcast_REQ_enabled_[i]}; %% Remove a newly picked time nonce from the expired tn list. expired_tn_ts_list' = remove_tn(user_new_time_nonce_id'[last_U_actor'].tn_id, expired_tn_ts_list); [] Schedule_U_rcv_ACK: EXISTS (j: SERVER_ID, i: USER_ID): U_rcv_ACK_enabled_[j][i] --> last_action' = U_rcv_ACK; last_S_sender_actor' in {j: SERVER_ID | EXISTS (i:USER_ID): U_rcv_ACK_enabled_[j][i]}; last_U_actor' in {i: USER_ID | U_rcv_ACK_enabled_[last_S_sender_actor'][i]}; [] Schedule_U_send_RENEW: EXISTS (i: USER_ID): U_send_RENEW_enabled_[i] --> last_action' = U_send_RENEW; last_U_actor' in {i: USER_ID | U_send_RENEW_enabled_[i]}; last_S_receiver' = last_u2s_sending_target_'[last_U_actor']; %% Remove a newly picked time nonce from the expired tn list. expired_tn_ts_list' = remove_tn(user_new_time_nonce_id'[last_U_actor'].tn_id, expired_tn_ts_list); [] Schedule_U_lease_expired: EXISTS (i: USER_ID): U_lease_expired_enabled_[i] --> last_action' = U_lease_expired; last_U_actor' in {i: USER_ID | U_lease_expired_enabled_[i]}; [] ELSE --> deadlock' = TRUE; ]; END; %% --------------- %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %% Composed System %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %% --------------- %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %% Server composition Servers: MODULE = WITH OUTPUT server_pc: ARRAY SERVER_ID OF SERVER_PROGRAM_COUNTER WITH OUTPUT server_leading: ARRAY SERVER_ID OF BOOLEAN %% Server TOs, TVs, SNs are output once, and are input by the Scheduler. WITH OUTPUT server_to_vec_out: SERVER_TO_VECTOR WITH OUTPUT server_tv_vec_out: SERVER_TV_VECTOR WITH OUTPUT server_sn_vec_out: SERVER_SN_VECTOR WITH INPUT last_u2s_msg_channel_out: ARRAY SERVER_ID OF ARRAY USER_ID OF U2S_MESSAGE WITH INPUT last_s2s_rcvd_msg_channel_out: ARRAY SERVER_ID OF ARRAY SERVER_ID OF S2S_MESSAGE WITH OUTPUT last_s2u_msg_channel_in: ARRAY SERVER_ID OF S2U_MESSAGE WITH OUTPUT last_s2s_sending_msg_channel_in: ARRAY SERVER_ID OF S2S_MESSAGE WITH OUTPUT last_s2u_sending_target_: ARRAY SERVER_ID OF USER_ID WITH OUTPUT last_s2s_sending_target_: ARRAY SERVER_ID OF SERVER_ID WITH OUTPUT S_send_ACK_enabled_: ARRAY SERVER_ID OF BOOLEAN WITH OUTPUT S_bcast_WRITE_enabled_: ARRAY SERVER_ID OF BOOLEAN WITH OUTPUT S_send_WRITE_ACK_enabled_: ARRAY SERVER_ID OF BOOLEAN WITH OUTPUT S_lease_expired_enabled_: ARRAY SERVER_ID OF BOOLEAN WITH OUTPUT server_new_time_stamp_id: ARRAY SERVER_ID OF TIME_STAMP_ID_WITH_NOT_FOUND WITH OUTPUT server_new_time_stamp_id_picked: ARRAY SERVER_ID OF BOOLEAN WITH OUTPUT server_new_time_stamp_unavailable_error: ARRAY SERVER_ID OF BOOLEAN WITH OUTPUT compression_: ARRAY SERVER_ID OF COMPRESSION (|| (j: SERVER_ID): RENAME pc to server_pc[j] IN RENAME leading to server_leading[j] IN RENAME timeout TO server_to_vec_out[j] IN RENAME server_tvs TO server_tv_vec_out[j] IN RENAME current_seq_num to server_sn_vec_out[j] IN RENAME last_u2s_msg TO last_u2s_msg_channel_out[j] IN RENAME last_s2s_rcvd_msg TO last_s2s_rcvd_msg_channel_out[j] IN RENAME last_s2u_msg TO last_s2u_msg_channel_in[j] IN RENAME last_s2s_sending_msg TO last_s2s_sending_msg_channel_in[j] IN RENAME last_s2u_sending_target TO last_s2u_sending_target_[j] IN RENAME last_s2s_sending_target TO last_s2s_sending_target_[j] IN RENAME S_send_ACK_enabled TO S_send_ACK_enabled_[j] IN RENAME S_bcast_WRITE_enabled TO S_bcast_WRITE_enabled_[j] IN RENAME S_send_WRITE_ACK_enabled TO S_send_WRITE_ACK_enabled_[j] IN RENAME S_lease_expired_enabled TO S_lease_expired_enabled_[j] IN RENAME new_time_stamp_id TO server_new_time_stamp_id[j] IN RENAME new_time_stamp_id_picked TO server_new_time_stamp_id_picked[j] IN RENAME new_time_stamp_unavailable_error TO server_new_time_stamp_unavailable_error[j] IN RENAME compression TO compression_[j] IN Server[j, (j=FIRST_SERVER_ID)]); %% User composition Users: MODULE = WITH OUTPUT user_pc: ARRAY USER_ID OF USER_PROGRAM_COUNTER %% User TOs and SNs are output once, and are input by the Scheduler. WITH OUTPUT user_to_vec_out: USER_TO_VECTOR WITH OUTPUT user_sn_vec_out: USER_SN_VECTOR WITH OUTPUT last_u2s_msg_channel_in: ARRAY USER_ID OF U2S_MESSAGE WITH INPUT last_s2u_msg_channel_out: ARRAY USER_ID OF ARRAY SERVER_ID OF S2U_MESSAGE WITH OUTPUT last_u2s_sending_target_: ARRAY USER_ID OF SERVER_ID WITH OUTPUT U_bcast_REQ_enabled_: ARRAY USER_ID OF BOOLEAN WITH OUTPUT U_send_RENEW_enabled_: ARRAY USER_ID OF BOOLEAN WITH OUTPUT U_lease_expired_enabled_: ARRAY USER_ID OF BOOLEAN WITH OUTPUT user_new_time_nonce_id: ARRAY USER_ID OF TIME_NONCE_ID_WITH_NOT_FOUND WITH OUTPUT user_new_time_nonce_unavailable_error: ARRAY USER_ID OF BOOLEAN WITH OUTPUT user_new_seq_num_unavailable_error: ARRAY USER_ID OF BOOLEAN (|| (i: USER_ID): RENAME pc TO user_pc[i] IN RENAME timeout TO user_to_vec_out[i] IN RENAME current_seq_num TO user_sn_vec_out[i] IN RENAME last_u2s_msg TO last_u2s_msg_channel_in[i] IN RENAME last_s2u_msg TO last_s2u_msg_channel_out[i] IN RENAME last_u2s_sending_target TO last_u2s_sending_target_[i] IN RENAME U_bcast_REQ_enabled TO U_bcast_REQ_enabled_[i] IN RENAME U_send_RENEW_enabled TO U_send_RENEW_enabled_[i] IN RENAME U_lease_expired_enabled TO U_lease_expired_enabled_[i] IN RENAME new_time_nonce_id TO user_new_time_nonce_id[i] IN RENAME new_time_nonce_unavailable_error TO user_new_time_nonce_unavailable_error[i] IN RENAME new_seq_num_unavailable_error TO user_new_seq_num_unavailable_error[i] IN User[i]); %% Apparently, the current version of SAL does not support the composition using %% more than two variables. Therefore I cannot do: %% || (i: USER_ID, j: SERVER_ID): %% Thus I combine users and servers once using the following record type, and %% compose the channel using this record type. USER_SERVER: TYPE = [# i: USER_ID, j: SERVER_ID #]; %% S2U channel composition S2U_Channels: MODULE = WITH OUTPUT s2u_buff: S2U_BUFFERS WITH OUTPUT s2u_bps: S2U_BPS WITH OUTPUT last_s2u_msg_channel_out: ARRAY USER_ID OF ARRAY SERVER_ID OF S2U_MESSAGE WITH INPUT last_s2u_sending_target_: ARRAY SERVER_ID OF USER_ID WITH INPUT last_s2u_msg_channel_in: ARRAY SERVER_ID OF S2U_MESSAGE WITH OUTPUT s2u_buffer_full: ARRAY SERVER_ID OF ARRAY USER_ID OF BOOLEAN WITH OUTPUT U_rcv_ACK_enabled_: ARRAY SERVER_ID OF ARRAY USER_ID OF BOOLEAN (|| (r: USER_SERVER): %% r.i: USER_ID, r.j: SERVER_ID RENAME buffer TO s2u_buff[r.j][r.i] IN RENAME pointer TO s2u_bps[r.j][r.i] IN RENAME head TO last_s2u_msg_channel_out[r.i][r.j] IN RENAME last_s2u_sending_target TO last_s2u_sending_target_[r.j] IN RENAME last_s2u_msg TO last_s2u_msg_channel_in[r.j] IN RENAME buffer_full TO s2u_buffer_full[r.j][r.i] IN RENAME U_rcv_ACK_enabled TO U_rcv_ACK_enabled_[r.j][r.i] IN S2U_Channel[r.j,r.i]); %% U2S channel composition U2S_Channels: MODULE = WITH OUTPUT u2s_buff: U2S_BUFFERS WITH OUTPUT u2s_bps: U2S_BPS WITH OUTPUT last_u2s_msg_channel_out: ARRAY SERVER_ID OF ARRAY USER_ID OF U2S_MESSAGE WITH INPUT last_u2s_sending_target_: ARRAY USER_ID OF SERVER_ID WITH INPUT last_u2s_msg_channel_in: ARRAY USER_ID OF U2S_MESSAGE WITH OUTPUT u2s_buffer_full: ARRAY USER_ID OF ARRAY SERVER_ID OF BOOLEAN WITH OUTPUT S_rcv_REQ_enabled_: ARRAY USER_ID OF ARRAY SERVER_ID OF BOOLEAN WITH OUTPUT S_rcv_RENEW_enabled_: ARRAY USER_ID OF ARRAY SERVER_ID OF BOOLEAN (|| (r: USER_SERVER): %% r.i: USER_ID, r.j: SERVER_ID RENAME buffer TO u2s_buff[r.i][r.j] IN RENAME pointer TO u2s_bps[r.i][r.j] IN RENAME head TO last_u2s_msg_channel_out[r.j][r.i] IN RENAME last_u2s_sending_target TO last_u2s_sending_target_[r.i] IN RENAME last_u2s_msg TO last_u2s_msg_channel_in[r.i] IN RENAME buffer_full TO u2s_buffer_full[r.i][r.j] IN RENAME S_rcv_REQ_enabled TO S_rcv_REQ_enabled_[r.i][r.j] IN RENAME S_rcv_RENEW_enabled TO S_rcv_RENEW_enabled_[r.i][r.j] IN U2S_Channel[r.i, r.j]); %% This type is also for composition. SERVER_SERVER: TYPE = [# j1: SERVER_ID, j2: SERVER_ID #]; %% S2S channel composition S2S_Channels: MODULE = WITH OUTPUT s2s_buff: S2S_BUFFERS WITH OUTPUT s2s_bps: S2S_BPS WITH OUTPUT last_s2s_rcvd_msg_channel_out: ARRAY SERVER_ID OF ARRAY SERVER_ID OF S2S_MESSAGE WITH INPUT last_s2s_sending_target_: ARRAY SERVER_ID OF SERVER_ID WITH INPUT last_s2s_sending_msg_channel_in: ARRAY SERVER_ID OF S2S_MESSAGE WITH OUTPUT s2s_buffer_full: ARRAY SERVER_ID OF ARRAY SERVER_ID OF BOOLEAN WITH OUTPUT S_rcv_WRITE_enabled_: ARRAY SERVER_ID OF ARRAY SERVER_ID OF BOOLEAN WITH OUTPUT S_rcv_WRITE_ACK_enabled_: ARRAY SERVER_ID OF ARRAY SERVER_ID OF BOOLEAN (|| (r: SERVER_SERVER): %% A message goes: r.j1 => r.j2 RENAME buffer TO s2s_buff[r.j1][r.j2] IN RENAME pointer TO s2s_bps[r.j1][r.j2] IN RENAME head TO last_s2s_rcvd_msg_channel_out[r.j2][r.j1] IN RENAME last_s2s_sending_target TO last_s2s_sending_target_[r.j1] IN RENAME last_s2s_sending_msg TO last_s2s_sending_msg_channel_in[r.j1] IN RENAME buffer_full TO s2s_buffer_full[r.j1][r.j2] IN RENAME S_rcv_WRITE_enabled TO S_rcv_WRITE_enabled_[r.j1][r.j2] IN RENAME S_rcv_WRITE_ACK_enabled TO S_rcv_WRITE_ACK_enabled_[r.j1][r.j2] IN S2S_Channel[r.j1, r.j2]); ComposedSystem: Module = Servers || Users || S2U_Channels || U2S_Channels || S2S_Channels || Scheduler || Environment || FailureDetector; %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %%%%%% Lemmas & Theorems %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% NO_DUPLICATED_LEASING_AND_CORRECT_TIME_DATA_ANDSEQ_NUM: THEOREM ComposedSystem |- G( (FORALL (i1, i2: USER_ID): (i1 /= i2 AND user_pc[i1] = leasing) => user_pc[i2] /= leasing) AND (FORALL (i: USER_ID): NOT user_new_time_nonce_unavailable_error[i]) AND (FORALL (j: SERVER_ID): NOT server_new_time_stamp_unavailable_error[j]) AND (FORALL (i: USER_ID): NOT user_new_seq_num_unavailable_error[i]) ); END