Deprecated: The each() function is deprecated. This message will be suppressed on further calls in /home/zhenxiangba/zhenxiangba.com/public_html/phproxy-improved-master/index.php on line 456
MODEL ibm_cache (* This file describes the uclid version of the cache coherence * protocol described by Steve German. Follows Murphi semantics * of selecting a single rule to evaluate on each step. * 3/29/01 *) typedef message : enum{EMPTY, REQ_SHARED, REQ_EXCLUSIVE, INVALIDATE, INVALIDATE_ACK, GRANT_SHARED, GRANT_EXCLUSIVE}; typedef cache_state : enum{INVALID, SHARED, EXCLUSIVE}; MODULE c INPUT VAR (* STATE VARIABLES *) cid : TERM; (* ID of Client chosen to run in the current step *) ctr : TERM; (* counter used to choose arbitrary client ID *) num_sharers : TERM ; (* number of 1s in the home_sharer_list *) channel1 : FUNC[1] of message; channel2 : FUNC[1] of message; (* ERROR *) channel4 : FUNC[1] of message; (* ERROR *) channel3 : FUNC[1] of message; home_sharer_list : PRED[1]; home_invalidate_list : PRED[1]; home_exclusive_granted: TRUTH; home_current_command : message; (* home_current_client is of type 1..num_clients *) home_current_client : TERM; cache : FUNC[1] of cache_state; (* MACRO VARIABLES *) home_sends_reply_client_ex : TRUTH; home_sends_reply_client_sh : TRUTH; client_receives_ex_grant : PRED[1]; client_receives_sh_grant : PRED[1]; sharer_invalidates_cache : PRED[1]; home_receives_invalid_ack : PRED[1]; home_sends_invalid_mesg : PRED[1]; home_picks_new_req : PRED[1]; client_requests_ex_access : PRED[1]; client_requests_sh_access : PRED[1]; (* Choice variables in order to model Murphi semantics that only one rule fires every step. This rule is nondeterministically chosen. *) x0 : TRUTH; x1 : TRUTH; x2 : TRUTH; x3 : TRUTH; rule1 : TRUTH; rule2 : TRUTH; rule3 : TRUTH; rule4 : TRUTH; rule5 : TRUTH; rule6 : TRUTH; rule7 : TRUTH; rule8 : TRUTH; rule9 : TRUTH; rule10 : TRUTH; CONST c0 : TERM; i : TERM; cl : TERM; cl0 : TERM; (* Initial value of home_current_client *) ArbVal : FUNC[1]; (* arbitrary value generator *) newCl : FUNC[1]; (* maps a Client ID to a new value *) (* Arbitrary truth value generators: X0-X3 *) X0 : PRED[1]; X1 : PRED[1]; X2 : PRED[1]; X3 : PRED[1]; ZERO : TERM; DEFINE rule1 := ~x0 & ~x1 & ~x2 & ~x3; rule2 := x0 & ~x1 & ~x2 & ~x3; rule3 := ~x0 & x1 & ~x2 & ~x3; rule4 := x0 & x1 & ~x2 & ~x3; rule5 := ~x0 & ~x1 & x2 & ~x3; rule6 := x0 & ~x1 & x2 & ~x3; rule7 := ~x0 & x1 & x2 & ~x3; rule8 := x0 & x1 & x2 & ~x3; rule9 := ~x2 & x3; rule10 := x2 & x3; (***************************** DEFINITION OF RULES ******************************) (* client_requests_sh_access *) client_requests_sh_access := Lambda(cl). rule1 & ((cache(cl) = INVALID) & (channel1(cl) = EMPTY)); (* client_requests_ex_access *) client_requests_ex_access := Lambda(cl). rule2 & (((cache(cl) = INVALID) | (cache(cl) = SHARED)) & (channel1(cl) = EMPTY)); (* home_picks_new_req *) home_picks_new_req := Lambda(cl). rule3 & ((home_current_command = EMPTY ) & (channel1(cl) != EMPTY)); (* home_sends_invalid_mesg *) home_sends_invalid_mesg := Lambda(cl). rule4 & ((((home_current_command = REQ_SHARED ) & (home_exclusive_granted)) | (home_current_command = REQ_EXCLUSIVE)) & home_invalidate_list(cl) & (channel2(cl) = EMPTY)); (* home_receives_invalid_ack *) home_receives_invalid_ack := Lambda(cl). rule5 & ((home_current_command != EMPTY) & (channel3(cl) = INVALIDATE_ACK)); (* sharer_invalidates_cache *) sharer_invalidates_cache := Lambda(cl). rule6 & ((channel2(cl) = INVALIDATE) & (channel3(cl) = EMPTY)); (* client_receives_sh_grant *) client_receives_sh_grant := Lambda(cl). rule7 & (channel4(cl) = GRANT_SHARED); (* client_receives_ex_grant *) client_receives_ex_grant := Lambda(cl). rule8 & (channel4(cl) = GRANT_EXCLUSIVE); (* home_sends_reply_client_sh *) home_sends_reply_client_sh := rule9 & ((home_current_command = REQ_SHARED) & (~home_exclusive_granted) & (channel4(home_current_client) = EMPTY)); (* home_sends_reply_client_ex *) home_sends_reply_client_ex := rule10 & ((home_current_command = REQ_EXCLUSIVE) & (num_sharers = ZERO) & (channel4(home_current_client) = EMPTY)); (* cid is the ID of the client that is chosen to run in the current step *) cid := ArbVal(ctr); ASSIGN (* Choice variables for sync with Murphi semantics *) init[x0] := {1,0}; (* next[x0] := {1,0}; *) next[x0] := X0(ctr); init[x1] := {1,0}; (* next[x1] := {1,0}; *) next[x1] := X1(ctr); init[x2] := {1,0}; (* next[x2] := {1,0}; *) next[x2] := X2(ctr); init[x3] := {1,0}; (* next[x3] := {1,0}; *) next[x3] := X3(ctr); (******************************* HOME PROCESS ********************************) (* The components of home process are (i) home_sharer_list[] of bool (ii) home_invalidate_list[] of bool (iii) home_exclusive_granted of bool (iv) home_current_command of mesg (v) home_current_client of client *) (* number of sharers - i.e., the number of bits in the home_sharer_list that are set to 1 *) init[num_sharers] := ZERO; next[num_sharers] := case home_receives_invalid_ack(cid) : pred(num_sharers); home_sends_reply_client_sh & (~home_sharer_list(home_current_client)) : succ(num_sharers); home_sends_reply_client_ex & (~home_sharer_list(home_current_client)) : succ(num_sharers); default : num_sharers; esac; (* home sharer list *) init[home_sharer_list] := Lambda(i). 0; next[home_sharer_list] := Lambda(i). case home_receives_invalid_ack(cid) & (i = cid) : 0 ; home_sends_reply_client_sh & (i = home_current_client) : 1 ; home_sends_reply_client_ex & (i = home_current_client) : 1 ; default : home_sharer_list (i) ; esac; (* home invalidate list *) init[home_invalidate_list] := Lambda(i). 0; next[home_invalidate_list] := Lambda(i). case home_picks_new_req(cid) : home_sharer_list(i); home_sends_invalid_mesg(cid) & (i = cid) : 0 ; default : home_invalidate_list(i); esac; (* home excl granted *) init[home_exclusive_granted] := 0 ; next[home_exclusive_granted] := case home_receives_invalid_ack(cid) : 0; home_sends_reply_client_ex : 1; default : home_exclusive_granted; esac; (* counter used in generating arbitrary client ID on each step *) init[ctr] := c0; next[ctr] := newCl(ctr); (* home current command *) init[home_current_command] := EMPTY ; next[home_current_command] := case home_picks_new_req(cid) : channel1(cid); home_sends_reply_client_sh : EMPTY ; home_sends_reply_client_ex : EMPTY ; default : home_current_command ; esac; (* home current client *) init[home_current_client] := cl0; next[home_current_client] := case home_picks_new_req(cid) : cid ; default : home_current_client ; esac; (******************************** CLIENT PROCESS *********************************) (* The component of each client process are (i) cache of cache_state (ii) channel1 of message (iii) channel2_4 of message (iv) channel3 of message *) (* client channel1 *) init[channel1] := Lambda(i). EMPTY ; next[channel1] := Lambda(i). case (i != cid ) : channel1(i); client_requests_sh_access(cid) : REQ_SHARED; client_requests_ex_access(cid) : REQ_EXCLUSIVE; home_picks_new_req(cid) : EMPTY; default : channel1(i); esac; (* client channel2 *) init[channel2] := Lambda(i). EMPTY; next[channel2] := Lambda(i). case (i != cid ) : channel2(i); home_sends_invalid_mesg(cid) : INVALIDATE ; sharer_invalidates_cache(cid) : EMPTY ; default : channel2(i); esac; (* client channel4 *) init[channel4] := Lambda(i). EMPTY; next[channel4] := Lambda(i). case (i = home_current_client) & home_sends_reply_client_sh : GRANT_SHARED ; (i = home_current_client) & home_sends_reply_client_ex : GRANT_EXCLUSIVE ; (i != cid ) : channel4(i); client_receives_sh_grant(cid) : EMPTY ; client_receives_ex_grant(cid) : EMPTY ; default : channel4(i); esac; (* client channel3 *) init[channel3] := Lambda(i). EMPTY; next[channel3] := Lambda (i). case (i != cid) : channel3(i); home_receives_invalid_ack(cid) : EMPTY ; sharer_invalidates_cache(cid) : INVALIDATE_ACK ; default : channel3(i); esac; (* client cache *) init[cache] := Lambda(i). INVALID; next[cache] := Lambda(i). case (i != cid) : cache(i); sharer_invalidates_cache(cid) : INVALID; client_receives_sh_grant(cid) : SHARED; client_receives_ex_grant(cid) : EXCLUSIVE; default : cache(i); esac; SPEC (*****************************************************************) (*********** CONTROL MODULE ******************) (*****************************************************************) CONTROL EXTVAR STOREVAR init_inv : PRED[2]; next_inv : PRED[2]; VAR inv : PRED[2]; CONST c1 : TERM; c2 : TERM; DEFINE inv := Lambda(c1,c2). (((c1 != c2) & (c.cache(c1) = EXCLUSIVE)) => (c.cache(c2) = INVALID)); EXEC simulate(11); print("****************** After 11 steps ******************"); decide(inv(c1,c2));