ConcAutInvariants: THEORY BEGIN IMPORTING ConcreteAut IMPORTING invariant[ConcreteAut.state, cc?] c, c0, c1: VAR ConcreteAut.state m, n, r, n0, n1, n2: VAR Node k: VAR Key p, q: VAR PROC w, w0, w1, w2, wn, wm: VAR nat alpha: VAR cc? lemma_pcin_and_pcout: LEMMA FORALL c0, alpha, c1: transition(c0, conc_ioa_inst, alpha, c1) IMPLIES c0`pc(proc(alpha)) = pcin(alpha) AND c1`pc(proc(alpha)) = pcout(alpha)(c0) lemma_pcin_and_pcout2: LEMMA FORALL c0, alpha, c1, p: transition(c0, conc_ioa_inst, alpha, c1) IMPLIES IF proc(alpha)=p THEN c0`pc(p) = pcin(alpha) AND c1`pc(p) = pcout(alpha)(c0) ELSE c1`pc(p) = c0`pc(p) ENDIF public(c, n): bool = c`allocated(n) AND (FORALL p: c`entry(p) = n IMPLIES (c`pc(p) /= pcAdd4 AND c`pc(p) /= pcAdd5 AND c`pc(p) /= pcAdd6)) lemma_dnm_locals: LEMMA FORALL c0, alpha, c1, p: transition(c0, conc_ioa_inst, alpha, c1) AND p /= proc(alpha) IMPLIES c1`pc(p) = c0`pc(p) AND c1`v(p) = c0`v(p) AND c1`res(p) = c0`res(p) AND c1`pred(p) = c0`pred(p) AND c1`curr(p) = c0`curr(p) AND c1`entry(p) = c0`entry(p) AND c1`ret_addr(p) = c0`ret_addr(p) lemma_dnm_v: LEMMA FORALL c0, alpha, c1, p: transition(c0, conc_ioa_inst, alpha, c1) AND c1`v(p) /= c0`v(p) IMPLIES proc(alpha)=p AND (cont?(alpha) OR add?(alpha) OR rem?(alpha)) lemma_dnm_pred: LEMMA FORALL c0, alpha, c1, p: transition(c0, conc_ioa_inst, alpha, c1) AND c1`pred(p) /= c0`pred(p) IMPLIES proc(alpha)=p AND (loc1?(alpha) OR loc4?(alpha)) lemma_dnm_curr: LEMMA FORALL c0, alpha, c1, p: transition(c0, conc_ioa_inst, alpha, c1) AND c1`curr(p) /= c0`curr(p) IMPLIES proc(alpha)=p AND (cont1?(alpha) OR cont3?(alpha) OR loc5?(alpha) OR loc2?(alpha)) lemma_dnm_entry: LEMMA FORALL c0, alpha, c1, p: transition(c0, conc_ioa_inst, alpha, c1) AND c1`entry(p) /= c0`entry(p) IMPLIES proc(alpha)=p AND (add3?(alpha) OR rem4?(alpha)) lemma_dnm_next2: LEMMA FORALL c0, alpha, c1, n: transition(c0, conc_ioa_inst, alpha, c1) AND c1`nextf(n) /= c0`nextf(n) IMPLIES ((add6?(alpha) OR rem5?(alpha)) AND c0`pred(proc(alpha))=n) OR (add5?(alpha) AND c0`entry(proc(alpha))=n) lemma_dnm_next: LEMMA FORALL c0, alpha, c1, n: transition(c0, conc_ioa_inst, alpha, c1) AND public(c0,n) AND c1`nextf(n) /= c0`nextf(n) IMPLIES (add6?(alpha) OR rem5?(alpha)) AND c0`pred(proc(alpha))=n lemma_dne_marked: LEMMA FORALL c0, alpha, c1, n: transition(c0, conc_ioa_inst, alpha, c1) AND c1`markedf(n) AND NOT c0`markedf(n) IMPLIES c0`curr(proc(alpha))=n AND rem3?(alpha) lemma_dnf_marked: LEMMA FORALL c0, alpha, c1, n: transition(c0, conc_ioa_inst, alpha, c1) AND NOT c1`markedf(n) AND c0`markedf(n) IMPLIES NOT public(c1,n) AND c1`entry(proc(alpha))=n AND add3?(alpha) lemma_dnm_entry_key: LEMMA FORALL c0, alpha, c1: transition(c0, conc_ioa_inst, alpha, c1) AND c1`keyf /= c0`keyf IMPLIES add4?(alpha) lemma_dne_public: LEMMA FORALL c0, alpha, c1, n: transition(c0, conc_ioa_inst, alpha, c1) AND public(c1,n) AND NOT public(c0,n) IMPLIES c0`entry(proc(alpha))=n AND add6?(alpha) lemma_public_stable: LEMMA FORALL alpha, c0, c1: reachable?(conc_ioa_inst, c0) AND transition(c0, conc_ioa_inst, alpha, c1) IMPLIES FORALL n: (public(c0,n) IMPLIES public(c1,n)) lemma_public_key_stable: LEMMA FORALL alpha, c0, c1, n: reachable?(conc_ioa_inst, c0) AND transition(c0, conc_ioa_inst, alpha, c1) AND public(c0,n) IMPLIES c1`keyf(n) = c0`keyf(n) lemma_public_marked_stable: LEMMA FORALL alpha, c0, c1, n: reachable?(conc_ioa_inst, c0) AND transition(c0, conc_ioa_inst, alpha, c1) AND public(c0,n) AND c0`markedf(n) IMPLIES c1`markedf(n) head_and_tail_public(c): bool = public(c,Head) AND public(c,Tail) inv_head_and_tail_public: LEMMA invariant(conc_ioa_inst, head_and_tail_public) head_and_tail_keys(c): bool = c`keyf(Head)=neg_inf AND c`keyf(Tail)=pos_inf inv_head_and_tail_keys: LEMMA invariant(conc_ioa_inst, head_and_tail_keys) add4_6(c,p): bool = LET pcval = c`pc(p) IN pcval = pcAdd4 OR pcval = pcAdd5 OR pcval = pcAdd6 lemma_dne_add4_6: LEMMA FORALL c0, alpha, c1, p: transition(c0, conc_ioa_inst, alpha, c1) AND add4_6(c1,p) AND NOT add4_6(c0,p) IMPLIES proc(alpha)=p AND add3?(alpha) lemma_allocated_stable: LEMMA FORALL alpha, c0, c1, n: reachable?(conc_ioa_inst, c0) AND transition(c0, conc_ioa_inst, alpha, c1) IMPLIES (c0`allocated(n) IMPLIES c1`allocated(n)) new_node_allocated(c): bool = FORALL p: add4_6(c,p) IMPLIES c`allocated(c`entry(p)) AND c`entry(p) /= Tail inv_new_node_allocated: LEMMA invariant(conc_ioa_inst, new_node_allocated) allocated_nodes_unique(c): bool = FORALL p, q: add4_6(c,p) AND add4_6(c,q) AND c`entry(p) = c`entry(q) IMPLIES p = q inv_allocated_nodes_unique: LEMMA invariant(conc_ioa_inst, allocated_nodes_unique) lemma_added_node_becomes_public: LEMMA add6?(alpha) AND reachable?(conc_ioa_inst, c0) AND transition(c0, conc_ioa_inst, alpha, c1) IMPLIES (NOT public(c0,c0`entry(proc(alpha))) AND public(c1,c0`entry(proc(alpha)))) pred_not_tail(c): bool = FORALL p: LET pcval = c`pc(p) IN pcval = pcLoc2 IMPLIES c`pred(p) /= Tail inv_pred_not_tail: LEMMA invariant(conc_ioa_inst, pred_not_tail) curr_not_tail(c): bool = FORALL p: LET pcval = c`pc(p) IN pcval = pcCont3 OR pcval = pcLoc4 OR pcval = pcLoc5 OR pcval = pcRem3 OR pcval = pcRem4 IMPLIES c`curr(p) /= Tail inv_curr_not_tail: LEMMA invariant(conc_ioa_inst, curr_not_tail) pred_defined(c,p): bool = LET pcval = c`pc(p) IN NOT (pcval=idle OR pcval=pcCont1 OR pcval=pcCont2 OR pcval=pcCont3 OR pcval=pcCont4 OR pcval=pcCont5 OR pcContResp?(c`pc(p)) OR pcval=pcLoc1 OR pcval=pcAdd1 OR pcval=pcRem1) curr_defined(c,p): bool = LET pcval = c`pc(p) IN NOT (pcval=idle OR pcval=pcCont1 OR pcval=pcLoc1 OR pcval=pcLoc2 OR pcval=pcAdd1 OR pcval=pcRem1) lemma_dne_pred_defined: LEMMA FORALL c0, alpha, c1, p: transition(c0, conc_ioa_inst, alpha, c1) AND pred_defined(c1,p) AND NOT pred_defined(c0,p) IMPLIES proc(alpha)=p AND loc1?(alpha) lemma_dne_curr_defined: LEMMA FORALL c0, alpha, c1, p: transition(c0, conc_ioa_inst, alpha, c1) AND curr_defined(c1,p) AND NOT curr_defined(c0,p) IMPLIES proc(alpha)=p AND (loc2?(alpha) OR cont1?(alpha)) public_nodes(c): bool = (FORALL p: (pred_defined(c,p) IMPLIES public(c,c`pred(p))) AND (curr_defined(c,p) IMPLIES public(c,c`curr(p))) AND (c`pc(p)=pcRem5 IMPLIES public(c,c`entry(p)))) AND (FORALL n: (public(c, n) AND n /= Tail IMPLIES public(c,c`nextf(n)))) AND (FORALL p: c`pc(p)=pcAdd6 IMPLIES c`nextf(c`entry(p))=c`curr(p)) inv_public_nodes: LEMMA invariant(conc_ioa_inst, public_nodes) pred_public(c): bool = FORALL p: pred_defined(c,p) IMPLIES public(c,c`pred(p)) inv_pred_public: LEMMA invariant(conc_ioa_inst, pred_public) curr_public(c): bool = FORALL p: curr_defined(c,p) IMPLIES public(c,c`curr(p)) inv_curr_public: LEMMA invariant(conc_ioa_inst, curr_public) pred_critsec(c,p): bool = LET pcval = c`pc(p) IN pcval=pcLoc7 OR pcval=pcLoc8 OR pcval=pcLoc9 OR pcval=pcLoc10 OR pcval=pcLoc11 OR pcval=pcLoc12 OR pcval=pcAdd2 OR pcval=pcAdd3 OR pcval=pcAdd4 OR pcval=pcAdd5 OR pcval=pcAdd6 OR pcval=pcAdd7 OR pcval=pcAdd8 OR pcval=pcAdd9 OR pcval=pcRem2 OR pcval=pcRem3 OR pcval=pcRem4 OR pcval=pcRem5 OR pcval=pcRem6 OR pcval=pcRem7 OR pcval=pcRem8 curr_critsec(c,p): bool = LET pcval = c`pc(p) IN pcval=pcLoc8 OR pcval=pcLoc9 OR pcval=pcLoc10 OR pcval=pcLoc11 OR pcval=pcLoc12 OR pcval=pcLoc13 OR pcval=pcAdd2 OR pcval=pcAdd3 OR pcval=pcAdd4 OR pcval=pcAdd5 OR pcval=pcAdd6 OR pcval=pcAdd7 OR pcval=pcAdd8 OR pcval=pcAdd9 OR pcval=pcAdd10 OR pcval=pcRem2 OR pcval=pcRem3 OR pcval=pcRem4 OR pcval=pcRem5 OR pcval=pcRem6 OR pcval=pcRem7 OR pcval=pcRem8 OR pcval=pcRem9 lemma_pred_critsec_implies_defined: LEMMA FORALL c,p: pred_critsec(c,p) IMPLIES pred_defined(c,p) lemma_curr_critsec_implies_defined: LEMMA FORALL c,p: curr_critsec(c,p) IMPLIES curr_defined(c,p) lemma_dnm_lock_acquire: LEMMA FORALL c0, alpha, c1, n: transition(c0, conc_ioa_inst, alpha, c1) AND c1`lockf(n) AND NOT c0`lockf(n) IMPLIES (c0`pred(proc(alpha))=n AND loc6?(alpha)) OR (c0`curr(proc(alpha))=n AND loc7?(alpha)) lemma_dnm_lock_release: LEMMA FORALL c0, alpha, c1, n: transition(c0, conc_ioa_inst, alpha, c1) AND NOT c1`lockf(n) AND c0`lockf(n) IMPLIES (c0`pred(proc(alpha))=n AND (loc12?(alpha) OR add9?(alpha) OR rem8?(alpha))) OR (c0`curr(proc(alpha))=n AND (loc13?(alpha) OR add10?(alpha) OR rem9?(alpha))) OR (getNode(c0)=n AND add3?(alpha)) lemma_dnm_pred_critsec_enter: LEMMA FORALL c0, alpha, c1, p: transition(c0, conc_ioa_inst, alpha, c1) AND pred_critsec(c1,p) AND NOT pred_critsec(c0,p) IMPLIES proc(alpha)=p AND loc6?(alpha) lemma_dnm_curr_critsec_enter: LEMMA FORALL c0, alpha, c1, p: transition(c0, conc_ioa_inst, alpha, c1) AND curr_critsec(c1,p) AND NOT curr_critsec(c0,p) IMPLIES proc(alpha)=p AND loc7?(alpha) node_owner(c,p,n): bool = (pred_critsec(c,p) AND c`pred(p)=n) OR (curr_critsec(c,p) AND c`curr(p)=n) lemma_dnm_node_acquire: LEMMA FORALL c0, alpha, c1, p, n: transition(c0, conc_ioa_inst, alpha, c1) AND node_owner(c1,p,n) AND NOT node_owner(c0,p,n) IMPLIES proc(alpha)=p AND ((c0`pred(p)=n AND loc6?(alpha)) OR (c0`curr(p)=n AND loc7?(alpha))) unique_node_owner(c,n): bool = FORALL p, q: node_owner(c,p,n) AND node_owner(c,q,n) IMPLIES p=q locked_when_owned(c,n): bool = (EXISTS p: node_owner(c,p,n)) IMPLIES c`lockf(n) proper_locking2(c): bool = (FORALL n: unique_node_owner(c,n) AND locked_when_owned(c,n)) AND (FORALL p: curr_critsec(c,p) IMPLIES NOT (c`curr(p)=c`pred(p))) inv_proper_locking2: LEMMA invariant(conc_ioa_inst,proper_locking2) proper_locking(c): bool = FORALL n: unique_node_owner(c,n) AND locked_when_owned(c,n) inv_proper_locking: LEMMA invariant(conc_ioa_inst,proper_locking) entry_next_is_curr(c): bool = FORALL p: c`pc(p)=pcAdd6 IMPLIES c`nextf(c`entry(p))=c`curr(p) inv_entry_next_is_curr: LEMMA invariant(conc_ioa_inst, entry_next_is_curr) lemma_dnm_curr_key: LEMMA FORALL c0, alpha, c1, p: reachable?(conc_ioa_inst, c0) AND transition(c0, conc_ioa_inst, alpha, c1) AND curr_defined(c0,p) AND c1`keyf(c1`curr(p)) /= c0`keyf(c0`curr(p)) IMPLIES proc(alpha)=p AND (cont1?(alpha) OR cont3?(alpha) OR loc5?(alpha) OR loc2?(alpha)) lemma_dnm_pred_key: LEMMA FORALL c0, alpha, c1, p: reachable?(conc_ioa_inst, c0) AND transition(c0, conc_ioa_inst, alpha, c1) AND pred_defined(c0,p) AND c1`keyf(c1`pred(p)) /= c0`keyf(c0`pred(p)) IMPLIES proc(alpha)=p AND (loc1?(alpha) OR loc4?(alpha)) rem3_6(c,p): bool = LET pcval = c`pc(p) IN pcval = pcRem3 OR pcval = pcRem4 OR pcval = pcRem5 OR pcval = pcRem6 key_unchanged_in_rem(c): bool = FORALL p: rem3_6(c,p) IMPLIES c`keyf(c`curr(p))=c`v(p) inv_key_unchanged_in_rem: LEMMA invariant(conc_ioa_inst, key_unchanged_in_rem) key_unchanged_in_add(c): bool = FORALL p: c`pc(p)=pcAdd8 IMPLIES c`keyf(c`curr(p))=c`v(p) inv_key_unchanged_in_add: LEMMA invariant(conc_ioa_inst, key_unchanged_in_add) add3_7(c,p): bool = LET pcval = c`pc(p) IN pcval = pcAdd3 OR pcval = pcAdd4 OR pcval = pcAdd5 OR pcval = pcAdd6 OR pcval = pcAdd7 key_unchanged_in_add_2(c): bool = FORALL p: add3_7(c,p) IMPLIES c`keyf(c`curr(p)) /= c`v(p) inv_key_unchanged_in_add_2: LEMMA invariant(conc_ioa_inst, key_unchanged_in_add_2) add5_6(c,p): bool = LET pcval = c`pc(p) IN pcval = pcAdd5 OR pcval = pcAdd6 key_unchanged_in_add_3(c): bool = FORALL p: add5_6(c,p) IMPLIES c`keyf(c`entry(p)) = c`v(p) inv_key_unchanged_in_add_3: LEMMA invariant(conc_ioa_inst, key_unchanged_in_add_3) key_unchanged_in_rem_2(c): bool = FORALL p: c`pc(p)=pcRem7 IMPLIES c`keyf(c`curr(p)) /= c`v(p) inv_key_unchanged_in_rem_2: LEMMA invariant(conc_ioa_inst, key_unchanged_in_rem_2) key_unchanged_in_cont(c): bool = FORALL p : c`pc(p)=pcCont5 IMPLIES c`keyf(c`curr(p)) = c`v(p) inv_key_unchanged_in_cont: LEMMA invariant(conc_ioa_inst, key_unchanged_in_cont) rem4_5(c,p): bool = LET pcval = c`pc(p) IN pcval = pcRem4 OR pcval = pcRem5 marked_unchanged_in_rem(c): bool = FORALL p: rem4_5(c,p) IMPLIES c`markedf(c`curr(p)) inv_marked_unchanged_in_rem: LEMMA invariant(conc_ioa_inst, marked_unchanged_in_rem) entry_unchanged_in_rem(c): bool = FORALL p: c`pc(p)=pcRem5 IMPLIES c`entry(p) = c`nextf(c`curr(p)) inv_entry_unchanged_in_rem: LEMMA invariant(conc_ioa_inst, entry_unchanged_in_rem) curr_key_too_small(c): bool = FORALL p: c`pc(p)=pcLoc4 IMPLIES c`keyf(c`curr(p)) < c`v(p) inv_curr_key_too_small: LEMMA invariant(conc_ioa_inst, curr_key_too_small) pred_key_smaller(c): bool = FORALL p: pred_defined(c,p) IMPLIES c`keyf(c`pred(p)) < c`v(p) inv_pred_key_smaller: LEMMA invariant(conc_ioa_inst, pred_key_smaller) looking_for_curr(c,p):bool = LET pcval=c`pc(p) IN pcval=pcCont2 OR pcval=pcCont3 OR pcval=pcLoc3 OR pcval=pcLoc4 OR pcval=pcLoc5 curr_found(c,p): bool = curr_defined(c,p) AND NOT looking_for_curr(c,p) lemma_dne_curr_found: LEMMA FORALL c0, alpha, c1, p: transition(c0, conc_ioa_inst, alpha, c1) AND curr_found(c1,p) AND NOT curr_found(c0,p) IMPLIES proc(alpha)=p AND (loc3F?(alpha) OR cont2F?(alpha)) curr_key_big_enough(c): bool = FORALL p: curr_found(c,p) IMPLIES c`keyf(c`curr(p)) >= c`v(p) inv_curr_key_big_enough: LEMMA invariant(conc_ioa_inst, curr_key_big_enough) before_setting_next(c,p): bool = LET pcval = c`pc(p) IN pcval=pcLoc11 OR pcval=pcAdd2 OR pcval=pcAdd3 OR pcval=pcAdd4 OR pcval=pcAdd5 OR pcval=pcAdd6 OR pcval=pcAdd8 OR pcval=pcRem2 OR pcval=pcRem3 OR pcval=pcRem4 OR pcval=pcRem5 OR pcval=pcRem7 lemma_crit_before_setting_next: LEMMA FORALL c, p: before_setting_next(c,p) IMPLIES pred_critsec(c,p) lemma_dne_before_setting_next: LEMMA FORALL c0, alpha, c1, p: transition(c0,conc_ioa_inst,alpha,c1) AND before_setting_next(c1,p) AND NOT before_setting_next(c0,p) IMPLIES proc(alpha)=p AND loc10T?(alpha) pred_next_is_curr(c): bool = FORALL p: before_setting_next(c,p) IMPLIES c`nextf(c`pred(p)) = c`curr(p) inv_pred_next_is_curr: LEMMA invariant(conc_ioa_inst, pred_next_is_curr) live_node(c, n): bool = public(c,n) AND NOT c`markedf(n) pred_not_marked(c): bool = FORALL p: pred_critsec(c,p) AND NOT (c`pc(p)=pcLoc7 OR c`pc(p)=pcLoc8 OR c`pc(p)=pcLoc12) IMPLIES NOT c`markedf(c`pred(p)) inv_pred_not_marked: LEMMA invariant(conc_ioa_inst, pred_not_marked) pred_is_live(c): bool = FORALL p: pred_critsec(c,p) AND NOT (c`pc(p)=pcLoc7 OR c`pc(p)=pcLoc8 OR c`pc(p)=pcLoc12) IMPLIES live_node(c,c`pred(p)) inv_pred_is_live: LEMMA invariant(conc_ioa_inst, pred_is_live) before_marking_curr(c,p): bool = LET pcval = c`pc(p) IN pcval=pcLoc10 OR pcval=pcLoc11 OR pcval=pcAdd2 OR pcval=pcAdd3 OR pcval=pcAdd4 OR pcval=pcAdd5 OR pcval=pcAdd6 OR pcval=pcAdd7 OR pcval=pcAdd8 OR pcval=pcAdd9 OR pcval=pcAdd10 OR pcval=pcRem2 OR pcval=pcRem3 OR pcval=pcRem7 lemma_crit_before_marking: LEMMA FORALL c,p: before_marking_curr(c,p) IMPLIES curr_critsec(c,p) lemma_dne_before_marking_curr: LEMMA FORALL c0, alpha, c1, p: transition(c0,conc_ioa_inst,alpha,c1) AND before_marking_curr(c1,p) AND NOT before_marking_curr(c0,p) IMPLIES proc(alpha)=p AND loc9T?(alpha) curr_not_marked(c): bool = FORALL p: before_marking_curr(c,p) IMPLIES NOT c`markedf(c`curr(p)) inv_curr_not_marked: LEMMA invariant(conc_ioa_inst, curr_not_marked) curr_is_live(c): bool = FORALL p: before_marking_curr(c,p) IMPLIES live_node(c,c`curr(p)) inv_curr_is_live: LEMMA invariant(conc_ioa_inst, curr_is_live) back_from_locate(c,p): bool = LET pcval = c`pc(p) IN pcval=pcAdd2 OR pcval=pcAdd3 OR pcval=pcAdd4 OR pcval=pcAdd5 OR pcval=pcAdd6 OR pcval=pcRem2 OR pcval=pcRem3 OR pcval=pcRem7 locate_works(c): bool = FORALL p: back_from_locate(c, p) IMPLIES live_node(c,c`pred(p)) AND live_node(c,c`curr(p)) AND c`keyf(c`pred(p)) < c`v(p) AND c`keyf(c`curr(p)) >= c`v(p) AND c`nextf(c`pred(p)) = c`curr(p) inv_locate_works: LEMMA invariant(conc_ioa_inst, locate_works) leadsfromsteps(c, n, m, w): INDUCTIVE bool = n /= Tail AND ((w=1 AND c`nextf(n) = m) OR (w>1 AND c`nextf(n) /= m AND leadsfromsteps(c,c`nextf(n),m,w-1))) leadsfrom(c, n, m): bool = EXISTS w: leadsfromsteps(c, n, m, w) next_node_greater_and_public(c): bool = FORALL n: public(c, n) AND n /= Tail IMPLIES (c`keyf(c`nextf(n)) > c`keyf(n) AND public(c,c`nextf(n))) inv_next_node_greater_and_public: LEMMA invariant(conc_ioa_inst, next_node_greater_and_public) later_nodes_greater(c): bool = FORALL n, m, w: n/=Tail AND public(c,n) AND leadsfromsteps(c,n,m,w) IMPLIES (public(c,m) AND c`keyf(n) < c`keyf(m)) inv_later_nodes_greater: LEMMA invariant(conc_ioa_inst, later_nodes_greater) later_nodes_greater_strong(c): bool = FORALL n, m: n/=Tail AND public(c,n) AND leadsfrom(c,n,m) IMPLIES (public(c,m) AND c`keyf(n) < c`keyf(m)) inv_later_nodes_greater_strong: LEMMA invariant(conc_ioa_inst, later_nodes_greater_strong) common_ancestor_distance(c): bool = FORALL n, m, r, wn, wm: public(c,n) AND public(c,m) AND n /= Tail AND m /= Tail AND leadsfromsteps(c,r,n,wn) AND leadsfromsteps(c,r,m,wm) AND c`keyf(n) < c`keyf(m) IMPLIES wm > wn AND leadsfromsteps(c,n,m,wm-wn) inv_common_ancestor_distance: LEMMA invariant(conc_ioa_inst, common_ancestor_distance) common_ancestor(c): bool = FORALL n, m, r, w: public(c,n) AND public(c,m) AND n /= Tail AND m /= Tail AND leadsfromsteps(c,r,n,w) AND leadsfrom(c,r,m) AND c`keyf(n) < c`keyf(m) IMPLIES leadsfrom(c,n,m) inv_common_ancestor: LEMMA invariant(conc_ioa_inst, common_ancestor) common_ancestor_strong(c): bool = FORALL n, m, r: public(c,n) AND public(c,m) AND n /= Tail AND m /= Tail AND leadsfrom(c,r,n) AND leadsfrom(c,r,m) AND c`keyf(n) < c`keyf(m) IMPLIES leadsfrom(c,n,m) inv_common_ancestor_strong: LEMMA invariant(conc_ioa_inst, common_ancestor_strong) leadsfromsteps_transitive(c): bool = FORALL n,m,r,w0,w1: public(c,n) AND public(c,m) AND leadsfromsteps(c,n,m,w0) AND leadsfromsteps(c,m,r,w1) IMPLIES leadsfromsteps(c,n,r,w0+w1) inv_leadsfromsteps_transitive: LEMMA invariant(conc_ioa_inst, leadsfromsteps_transitive) leadsfrom_transitive(c): bool = FORALL n,m,r: public(c,n) AND leadsfrom(c,n,m) AND leadsfrom(c,m,r) IMPLIES leadsfrom(c,n,r) inv_leadsfrom_transitive: LEMMA invariant(conc_ioa_inst, leadsfrom_transitive) leadsfromsteps_unique(c): bool = FORALL n,m,w1,w2: n /= Tail AND leadsfromsteps(c,n,m,w1) AND leadsfromsteps(c,n,m,w2) IMPLIES w1 = w2 inv_leadsfromsteps_unique: LEMMA invariant(conc_ioa_inst, leadsfromsteps_unique) leadsfromsteps_two_pieces_shorter(c): bool = FORALL n1,n2,m,w0,w1,w2: public(c,n1) AND leadsfromsteps(c,n1,n2,w0) AND leadsfromsteps(c,n2,m,w1) AND leadsfromsteps(c,n1,m,w2) IMPLIES (w0 < w2 AND w1 < w2) inv_leadsfromsteps_two_pieces_shorter: LEMMA invariant(conc_ioa_inst, leadsfromsteps_two_pieces_shorter) lemma_direct_leadsfrom: LEMMA FORALL c, n, m: public(c,n) AND n /= Tail AND c`nextf(n)=m IMPLIES leadsfrom(c,n,m) lemma_build_pub_leadsfrom: LEMMA FORALL c, n, m: public(c,n) AND n /= Tail AND leadsfrom(c,c`nextf(n),m) IMPLIES leadsfrom(c,n,m) build_pub_leadsfromsteps(c): bool = FORALL n, m, w: public(c,n) AND n /= Tail AND leadsfromsteps(c,c`nextf(n),m,w) IMPLIES leadsfromsteps(c,n,m,w+1) inv_build_pub_leadsfromsteps: LEMMA invariant(conc_ioa_inst, build_pub_leadsfromsteps) build_last_pub_leadsfromsteps(c): bool = FORALL n, m, w: public(c,n) AND n /= Tail AND m /= Tail AND leadsfromsteps(c,n,m,w) IMPLIES leadsfromsteps(c,n,c`nextf(m),w+1) inv_build_last_pub_leadsfromsteps: LEMMA invariant(conc_ioa_inst, build_last_pub_leadsfromsteps) lemma_leadsfrom_pres_unless_public_next_changes: LEMMA FORALL alpha, c0, c1, m, n, w: public(c0,n) AND reachable?(conc_ioa_inst, c0) AND transition(c0, conc_ioa_inst, alpha, c1) AND leadsfromsteps(c0,n,m,w) AND (FORALL r: public(c0,r) IMPLIES c1`nextf(r) = c0`nextf(r)) IMPLIES leadsfrom(c1,n,m) lemma_leadsfrom_pres_unless_inrange_next_changes: LEMMA FORALL alpha, c0, c1, m, n, w: public(c0,n) AND reachable?(conc_ioa_inst, c0) AND transition(c0, conc_ioa_inst, alpha, c1) AND leadsfromsteps(c0,n,m,w) AND (FORALL r: public(c0,r) AND c0`keyf(n) <= c0`keyf(r) AND c0`keyf(r) < c0`keyf(m) IMPLIES c1`nextf(r) = c0`nextf(r)) IMPLIES leadsfromsteps(c1,n,m,w) lemma_others_preserve_leadsfrom: LEMMA FORALL alpha, c0, c1, m, n, w: public(c0,n) AND reachable?(conc_ioa_inst, c0) AND transition(c0, conc_ioa_inst, alpha, c1) AND leadsfromsteps(c0,n,m,w) AND NOT add6?(alpha) AND NOT rem5?(alpha) IMPLIES leadsfrom(c1,n,m) % Note this proof uses invariants from above in the poststate lemma_add6_preserves_leadsfrom: LEMMA FORALL alpha, c0, c1, m, n, w: public(c0,n) AND reachable?(conc_ioa_inst, c0) AND transition(c0, conc_ioa_inst, alpha, c1) AND leadsfromsteps(c0,n,m,w) AND add6?(alpha) IMPLIES leadsfrom(c1,n,m) % Note this proof uses invariants from above in the poststate lemma_rem5_usually_preserves_leadsfrom: LEMMA FORALL alpha, c0, c1, m, n, w: public(c0,n) AND reachable?(conc_ioa_inst, c0) AND transition(c0, conc_ioa_inst, alpha, c1) AND leadsfromsteps(c0,n,m,w) AND rem5?(alpha) AND NOT leadsfrom(c1,n,m) IMPLIES c0`nextf(c0`pred(proc(alpha))) = m % Note this proof uses invariants from above in the poststate lemma_leadsfromsteps_preserved: LEMMA FORALL alpha, c0, c1, m, n, w: public(c0,n) AND reachable?(conc_ioa_inst, c0) AND transition(c0, conc_ioa_inst, alpha, c1) AND leadsfromsteps(c0,n,m,w) AND NOT leadsfrom(c1,n,m) IMPLIES LET p=proc(alpha) IN rem5?(alpha) AND c0`nextf(c0`pred(p)) = m % Note this proof uses invariants from above in the poststate lemma_leadsfrom_preserved_strong: LEMMA public(c0,n) AND reachable?(conc_ioa_inst, c0) AND transition(c0, conc_ioa_inst, alpha, c1) AND leadsfrom(c0,n,m) AND NOT leadsfrom(c1,n,m) IMPLIES LET p=proc(alpha) IN rem5?(alpha) AND c0`nextf(c0`pred(p)) = m AND c0`markedf(m) lemma_leadsfrom_preserved_stronger: LEMMA FORALL c0, alpha, c1, n, m: public(c0,n) AND reachable?(conc_ioa_inst, c0) AND transition(c0, conc_ioa_inst, alpha, c1) AND leadsfrom(c0,n,m) AND NOT leadsfrom(c1,n,m) IMPLIES LET p=proc(alpha) IN rem5?(alpha) AND c0`nextf(c0`pred(p)) = m AND c0`markedf(m) new_node_allocated_strong(c): bool = FORALL p: add4_6(c,p) IMPLIES c`allocated(c`entry(p)) AND c`entry(p) /= Tail AND NOT c`markedf(c`entry(p)) AND NOT c`lockf(c`entry(p)) inv_new_node_allocated_strong: LEMMA invariant(conc_ioa_inst, new_node_allocated_strong) live_nodes_in_list(c): bool = FORALL n: live_node(c, n) IMPLIES leadsfrom(c,Head,n) inv_live_nodes_in_list: LEMMA invariant(conc_ioa_inst, live_nodes_in_list) one_from_other(c): bool = FORALL n, m: n /= Tail AND m /= Tail AND live_node(c,n) AND live_node(c,m) AND c`keyf(n) < c`keyf(m) IMPLIES leadsfrom(c,n,m) inv_one_from_other: LEMMA invariant(conc_ioa_inst, one_from_other) live_nodes_unique_per_key(c): bool = FORALL n1, n2: live_node(c,n1) AND live_node(c,n2) AND c`keyf(n1) = c`keyf(n2) IMPLIES n1 = n2 inv_live_nodes_unique_per_key: LEMMA invariant(conc_ioa_inst, live_nodes_unique_per_key) lemma_dnm_aux_keys_add: LEMMA FORALL c0, alpha, c1, k: transition(c0, conc_ioa_inst, alpha, c1) AND c1`aux_keys(k) AND NOT c0`aux_keys(k) IMPLIES c0`v(proc(alpha))=k AND add6?(alpha) lemma_dnm_aux_keys_remove: LEMMA FORALL c0, alpha, c1, k: transition(c0, conc_ioa_inst, alpha, c1) AND NOT c1`aux_keys(k) AND c0`aux_keys(k) IMPLIES c0`v(proc(alpha))=k AND rem3?(alpha) lemma_dnf_seen_out: LEMMA FORALL c0, alpha, c1, p: transition(c0, conc_ioa_inst, alpha, c1) AND NOT c1`aux_seen_out(p) AND c0`aux_seen_out(p) IMPLIES proc(alpha)=p AND cont?(alpha) InList(c,k): bool = EXISTS n: live_node(c, n) AND c`keyf(n)=k % The following property is really part of the simulation proof, % but is stated as an invariant of the concrete automaton (augmented % with auxiliary variables) to allow model checking of the proof aux_keys_accurate(c): bool = c`aux_keys = {k | InList(c,k)} inv_aux_keys_accurate: LEMMA invariant(conc_ioa_inst, aux_keys_accurate) % should have used this for cont_val_still_in, but didn't have it then lemma_live_and_not_seen_out_unless_seen_out: LEMMA FORALL c0, alpha, c1, n, p: reachable?(conc_ioa_inst, c0) AND transition(c0, conc_ioa_inst, alpha, c1) AND cont_before_doCont(p,c0) AND NOT c0`aux_seen_out(p) AND live_node(c0,n) AND c0`keyf(n)=c0`v(p) IMPLIES ((live_node(c1,n) AND c1`keyf(n)=c0`v(p)) OR c1`aux_seen_out(p)) cont_val_still_in_before_reading_head(c): bool = FORALL p: c`pc(p)=pcCont1 AND NOT c`aux_seen_out(p) IMPLIES c`aux_keys(c`v(p)) inv_cont_val_still_in_before_reading_head: LEMMA invariant(conc_ioa_inst, cont_val_still_in_before_reading_head) cont_val_still_in(c): bool = FORALL p: ((c`pc(p)=pcCont2 AND c`keyf(c`curr(p)) < c`v(p)) OR c`pc(p)=pcCont3) AND NOT c`aux_seen_out(p) IMPLIES EXISTS n: live_node(c,n) AND leadsfrom(c,c`curr(p),n) AND c`keyf(n) = c`v(p) inv_cont_val_still_in: LEMMA invariant(conc_ioa_inst, cont_val_still_in) cont_val_still_in2(c): bool = FORALL p: c`pc(p)=pcCont2 AND c`keyf(c`curr(p)) >= c`v(p) AND NOT c`aux_seen_out(p) IMPLIES live_node(c,c`curr(p)) AND c`keyf(c`curr(p)) = c`v(p) inv_cont_val_still_in2: LEMMA invariant(conc_ioa_inst, cont_val_still_in2) cont_val_still_in3(c): bool = FORALL p: (c`pc(p)=pcCont4 OR c`pc(p) = pcCont5) AND NOT c`aux_seen_out(p) IMPLIES live_node(c,c`curr(p)) AND c`keyf(c`curr(p)) = c`v(p) inv_cont_val_still_in3: LEMMA invariant(conc_ioa_inst, cont_val_still_in3) % ------------ Main invariants required for forward simulation proof ------- precond_cont4F_and_cont5F(c): bool = FORALL p: (pre(cont4F(p))(c) OR (pre(cont4T(p))(c) AND c`markedf(c`curr(p))) OR pre(cont5F(p))(c)) IMPLIES c`aux_seen_out(p) inv_precond_cont4F_and_cont5F: LEMMA invariant(conc_ioa_inst, precond_cont4F_and_cont5F) precond_cont5T(c): bool = FORALL p: pre(cont5T(p))(c) IMPLIES member(c`v(p), c`aux_keys) inv_precond_cont5T: LEMMA invariant(conc_ioa_inst, precond_cont5T) precond_add6_and_rem7(c): bool = FORALL p: (pre(add6(p))(c) OR pre(rem7(p))(c)) IMPLIES NOT member(c`v(p), c`aux_keys) inv_precond_add6_and_rem7: LEMMA invariant(conc_ioa_inst, precond_add6_and_rem7) precond_add8_and_rem3(c): bool = FORALL p: (pre(add8(p))(c) OR pre(rem3(p))(c)) IMPLIES member(c`v(p), c`aux_keys) inv_precond_add8_and_rem3: LEMMA invariant(conc_ioa_inst, precond_add8_and_rem3) END ConcAutInvariants