$$$pvs-strategies (defstep simp () (then (flatten)(assert)(simplify)(flatten)) " Flatten, assert, simplify" " ") (defstep spsi (&optional (fnum +)) (then (split fnum)(simp)) "split then simp" "split then simp" ) (defstep LazyGrind () (then (grind$ :if-match nil)(grind$)) " Grind with the instantiation postponed to the end" " ") (defstep MyGrind () (grind$ :if-match nil) " Grind with no instantiation" " ") (defstep grind-best () (grind$ :if-match best) " Grind with best instantiation" " Grind with best instantiation") (defstep replace-all (fnums into) (let ((fnum (car fnums)) (rems (cdr fnums))) (if fnum (then (replace fnum into)(replace-all$ rems into)) (skip-msg " "))) " " " " ) (defstep rep-plus(&optional (fnum +)) (let ((fnums (gather-fnums (s-forms (current-goal *ps*)) * +)) (first (when fnums (car fnums)))) (if first (then (replace-all fnums fnum)(simp)) (skip-msg "Nothing to replace"))) " replace into consequents" " replace into consequents" ) (defstep expand-rho (&optional (inv nil)) (then (EXPAND "rho") (EXPAND inv) (SKOSIMP*) (REPLACE*) (simp)) "Expands out rho, skosimps, replaces and hides" " " ) (defstep exp-inv () (then (expand "reachable") (expand "memhistCorrect")(expand "cacheEqualMemhist ") (expand "queuesNonNeg")(expand "inQmatchHist")(expand "outQpcInc") (expand "localTimeEarlier")(expand "starImpliesID") (expand "QtimeInc")(expand "queuesMatchProg")(expand "histMatchPC") (expand "histComplete")(expand "firstExists")(expand "readValuesCorrect") (expand "histLt")(expand "histMatchTime")(expand "histJ0write") (expand "nextExists")) "expand all properties" "expand all properties" ) (defstep split-rho () (then (repeat* (then (lift-if "rho")(split "rho")))(simp)) "Splits `rho' on `action' type" "Splits `rho' on `action' type" ) (defstep split-rho-all () (then (repeat* (then (lift-if "rho")(split "rho")))(simp)(replace*)(simp)(split-all)) "Splits `rho' on `action' type, replace and split-all" "Splits `rho' on `action' type, replace and split-all" ) (defstep exp-rho (&optional (split f)(hide? t)(exp t)) (then (skosimp*)(label "orig" (-1 -2 1))(hide -1 -2 1)(reveal -1 -2 1) (expand "rho")(exp-inv)(skosimp*)(expand "addQentry")(expand "insert")(expand "timestamp")(simp) (label "rho" -1) (label "memhistCorrect" -2) (label "memhistCorrect" -3) (label "memhistCorrectInit" -4) (label "cacheEqualMemhist" -5) (label "queuesNonNeg" -6) (label "inQmatchHistP" -7) (label "inQmatchHistT" -8) (label "outQpcInc" -9) (label "localTimeEarlier" -10) (label "QtimeInc" -11) (label "queuesMatchProg" -12) (label "histCompleteR" -13) (label "histCompleteJ" -13 :push? t) (label "histCompleteNumRead" -14) (label "histCompletePC" -15) (label "histMatchPC" -15 :push? t) (label "histCompletePCe" -16) (label "histMatchPCe" -16 :push? t) (label "histCompleteTstime" -17) (label "histMatchTime" -17 :push? t ) (label "histMatchTimeE" -18) (label "histLt" -19) (label "histJ0write" -20) (label "firstExists" -21) (label "readValuesCorrect" -22) (label "toProve" +) (simp) (if (eq exp 't)(then (expand "cacheLoad")(expand "occEntry"))(skip)) (if (eq hide? 't) (hide -2 -3 -4 -5 -6 -7 -8 -9 -10 -11 -12 -13 -14 -15 -16 -17 -18 -19 -20 -21 -22 )(skip)) (if (eq split 't)(split-rho)(skip)) ) " exp-rho" "exp-rho" ) (defstep lift-split(&optional (num +)) (then (lift-if +)(split num)(simp)(replace*)(simp)) "Lift, split, replace and simplify " " " ) (defstep instbest (&optional (fnum *)) (then (inst? fnum :if-match best)) "Applies inst? :if-match best to the optional line number (num, +, -)" " " ) (defstep lazy-grind (&optional (if-match t) (defs !) rewrites theories exclude (updates? t)) (then (grind$ :if-match nil :defs defs :rewrites rewrites :theories theories :exclude exclude :updates? updates?) (reduce$ :if-match if-match :updates? updates?)) "Equiv. to (grind) with the instantiations postponed until after simplification." "By skolemization, if-lifting, simplification and instantiation") (defstep split-if (&optional (fnum *)) (then (lift-if) (let ((fnums (gather-fnums (s-forms (current-goal *ps*)) fnum nil #'(lambda (sform) (or (branch? (formula sform)) (and (negation? (formula sform)) (branch? (args1 (formula sform)))))))) (fnum (when fnums (car fnums)))) (if fnum (split fnum) (skip-msg "No IF-THEN-ELSE in the sequent.")))) "Applies LIFT-IF and splits only an IF-THEN-ELSE sequent formula in the result." "Lifting IF-THEN-ELSEs and splitting on an IF-THEN-ELSE") (defstep new-split-if (&optional (fnum +)) (then (split-if fnum)(simp)(replace*)(simp)) "Lift, split, replace and simplify " " " ) (defstep split-if-simp (&optional (fnum +)) (then (lift-if fnum)(then (split fnum)(simp))) "Lift, split and simplify " " " ) (defstep clean-up () (let ( ;(fmla (formula sform)) (fnums (gather-fnums (s-forms (current-goal *ps*)) * nil #'(lambda (sform) (or (and (negation? (formula sform)) (and (implication? (args1 (formula sform))) (tc-eq (args1 (args1 (formula sform))) *false*))) (and (conjunction? (formula sform)) (or (tc-eq (args1 (formula sform)) *false*) (tc-eq (args2 (formula sform)) *false*))))))) (fnum (when fnums (car fnums)))) (if fnum (hide fnums)(skip-msg "No formulae to clean-up"))) "Hide all antecedents of the form FALSE IMPLIES X and consequents FALSE AND Y " "Hide all antecedents of the form FALSE IMPLIES X and consequents FALSE AND Y" ) (defstep reduce-if (&optional (toreplace nil)(exclude nil)) (let ( ;(fmla (formula sform)) (fnums (gather-fnums (s-forms (current-goal *ps*)) * exclude #'(lambda (sform) (and (negation? (formula sform)) (and (branch? (args1 (formula sform))) (or (tc-eq (then-part (args1 (formula sform))) *false*) (tc-eq (else-part (args1 (formula sform))) *false*))))))) (fnum (when fnums (car fnums)))) (if fnum (then (split fnum)(flatten)(replace toreplace)) (skip-msg "Nothing to reduce if"))) "Split an antecedent if-formula if either the then-part or the else-part is false" "Reducing void if-formulae" ) (defstep split-all (&optional (fnum nil)(sko t)) (repeat* (then (split-if$ +)(simp$)(if (eq sko 't)(skosimp*)(skip))(replace*)(simp$)(reduce-if$) (then (split-if$ fnum)(simp$)(replace*)(simp$)))) "Lift, splits consequents and those in fnum, if specified. Antecedents with FALSE then or else-parts also split" "Splitting consequents and antecedents with FALSE then- or else-parts " ) (defstep reduce-all (&optional (fnum nil)(sko t)) (repeat* (then (reduce-if$ +)(simp$)(if (eq sko 't)(skosimp*)(skip))(replace*)(simp$))) "Split all antecedent if-formulae where either the then-part or the else-part is false. Skolemizes and replaces" "Splitting all if-then antecedents with false" ) (defstep simp-split (&optional (fnum +)) (then (lift-if)(then (split fnum)(simp))) "lift-if, split, simp" "lift-if, split, simp" ) (defstep hide-all-but (&optional (hidefrom *) keepnums) (let ((fnums (gather-fnums (s-forms (current-goal *ps*)) hidefrom keepnums))) (hide :fnums fnums)) "Hides all sequent formulas from FNUMS except those listed in KEEP-FNUMS. Useful when all but a few formulas need to be hidden." "Hiding ~a but keeping ~a") (defstep lem (inv1) (then (lemma inv1)(inst? -1)(simp)(exp-inv)) "lem" "lem" ) (defstep lemOE () (then (lemma "occEqual")(inst? -1)(simp)(expand "occEqual")(flatten) (label "oer1" -1)(label "oer2" -2)(label "oem1" -3)(label "oem2" -4) (label "oes1" -5)(label "oes2" -6)) "introduces occEqual lemma, and labels" "introduces occEqual lemma, and labels" ) (defstep lemLtStrict () (then (lemma "ltIsStrict")(label "ltIsStrict" -1)(flatten)(label "linear" -1 :push? t)(label "trans" -2 :push? t)) "introduces ltIsStrict lemma" "introduces ltIsStrict lemma" ) (defstep introNext () (then (skip)(CASE "exists (next : posnat): next(hist!1, (# t := t(procs!1(p_id!1)), r := 1 + numRead(procs!1(p_id!1)), id := p_id!1 #)) = next") (label "next" -1)(SKOSIMP*)(replace*)(LEMMA "nextSize") (label "nextSize" -1)(INST? -)(replace*)) "introduces next!1" "introduces next!1" ) $$$refine3.pvs refine3[U : posnat]: THEORY % This theory proves the refinement. % Using the history table, and the invariants about reachable lazy caching states, % we construct a serial execution, stored in the serRun array. % Each entry of serRun contains a copy of the processors and memory of the serial % system and is related to the previous entry by the serial.rho relation. % We property "Match" defines a relationship between a serial run, stored in serRun % and a reachable lazy caching state. % This relationship is proved inductively: we first show that Match holds between % the initial states of the two systems, and then that if Match(L, serRun) holds % where L are the lazy caching data structures and reachable(L), for every L' a % successor state of L, there exists serRun' s.t. rho_lazy(L, L') and match(L',serRun'). % Amongst other things, Match ensures that the memory of the lazy and serial systems % agree at the end of the run, and that every read in the two systems returns the % same value. % The noDeadlock lemma proves that for every processor it is always possible either % to remove one entry from either the in or out queue, or for a processor to complete % a read or a write. This ensures that progress can be made. BEGIN IMPORTING propsPrf[U], serial[U] procs, procs1, procs2, procs3, procs_p: VAR [PROC_ID -> PROC_INFO] memhist, memhist1, memhist2, memhist_p: VAR MEM_HIST_TYPE mem, mem1, mem2, mem_p: VAR MEM_TYPE hist, hist1, hist2, hist3, hist_p: VAR HISTORY_TYPE time, t, time_p: VAR TIME proc: VAR PROC_INFO id, p_id: VAR PROC_ID action: VAR actionType addr: VAR ADDRESS pc: VAR PC_RANGE ol: VAR posnat serOrderedList_TYPE: TYPE = [# sprocs: [PROC_ID -> SERIAL_PROC_TYPE], smem: MEM_TYPE #] serRun, serRun_p: VAR [nat -> serOrderedList_TYPE] % The properties relating the data structures of the lazy caching algorithm % and the serial run Match(hist, mem, memhist, procs, time, serRun): bool = % The first state in serRun fulfills the intial conditions for serial serial.theta(smem(serRun(0)), sprocs(serRun(0))) AND % Every state in serRun is related to its successor by serial.rho (FORALL (sr: nat): sr < size(hist) IMPLIES serial.rho (smem(serRun(sr)), sprocs(serRun(sr)), smem(serRun(sr + 1)), sprocs(serRun(sr + 1)), id(lst(hist)(sr + 1)))) AND % the finals serRun memory is the lazy caching memory smem(serRun(size(hist))) = mem AND % the values read, stored in readValues, agree in the two systems (FORALL id, pc: op(instlist(id, pc)) = READ IMPLIES readValues(sprocs(serRun(size(hist)))(id))(pc) = readValues(procs(id))(pc)) AND % if Out_id is empty then the program counters for P_id are identical in the % two systesm. Otherwise, the program counter in the serial system equal the % pc field in the top outQ entry. (FORALL id: IF empty(outQ(procs(id))) THEN pc(sprocs(serRun(size(hist)))(id)) = pc(procs(id)) ELSE pc(sprocs(serRun(size(hist)))(id)) = pc(QE(outQ(procs(id)))(head(outQ(procs(id))))) ENDIF) AND % For every entry sr of serRun, its memory equals that stored in memhist at the % time of the sr'th element of hist. (FORALL (sr: posnat): sr <= size(hist) IMPLIES smem(serRun(sr)) = mem(memhist(t(lst(hist)(sr))))) % The program counters in the serial run increase, for all processors. % The program counter of P_i only increases if there is a preceding element nsr in which % hist[nsr].id = i. That is, there is some element in which P_i took a transition, thus % increasing the program counter. pcSeqRun: LEMMA (FORALL id, (sr: nat): Match(hist, mem, memhist, procs, time, serRun) AND sr <= size(hist) IMPLIES (FORALL (srs: nat): srs < sr IMPLIES pc(sprocs(serRun(srs))(id)) <= pc(sprocs(serRun(sr))(id)) AND (pc(sprocs(serRun(srs))(id)) < pc(sprocs(serRun(sr))(id)) IFF (EXISTS (newsr: posnat): srs < newsr AND newsr <= sr AND id(lst(hist)(newsr)) = id)))) % The next 2 lemmas prove that Match is inductive over reachable lazy caching states: % Base case: There is a serial execution matching the initial lazy caching state. thetaSeq: LEMMA theta(hist, mem, memhist, procs, time) IMPLIES (EXISTS serRun: Match(hist, mem, memhist, procs, time, serRun)) % Inductive step : If L is a reachable lazy caching state, and rho(L, L') then there is % a serial run such that Match(L, serRun) reachSeq: LEMMA rho(hist, mem, memhist, procs, time, hist_p, mem_p, memhist_p, procs_p, p_id, time_p, action, addr) AND reachable(hist, mem, memhist, procs, time) AND (EXISTS serRun: Match(hist, mem, memhist, procs, time, serRun)) IMPLIES (EXISTS serRun_p: Match(hist_p, mem_p, memhist_p, procs_p, time_p, serRun_p)) % Count the total number of occupied entries in the in and out queues of % a processor numEntries(proc):int = tail(inQ(proc)) - head(inQ(proc)) + tail(outQ(proc)) - head(outQ(proc)) % In this lemma we show that "meaningful" progress can be made. % That is, for every processor P_i: % If either the out or in queues of P_i are non-empty then it is % possible to decrease the total number of entries in the two queues. % That is, a cache update must eventually occur. % If both queues are empty then either a read or write can occur. % If the next instruction is a read, to a non-cache address, it is first % brought into the cache and then read. % If the next instruction is a write, then it is possible to do a write, % a memory write and finally a cache update. % noDeadlock : lemma reachable(hist, mem, memhist, procs, time) implies (forall id: if not empty(inQ(procs(id))) then (exists procs1 : rho(hist, mem, memhist, procs, time, hist, mem, memhist, procs1, id, time, cacheUpdate, 1) and inQ(procs1(id)) = inQ(procs(id)) with [head := head(inQ(procs(id))) + 1] and numEntries(procs1(id)) = numEntries(procs(id))-1) elsif not empty(outQ(procs(id))) then (exists procs1, hist1, memhist1, mem1 : rho(hist, mem, memhist, procs, time, hist1, mem1, memhist1, procs1, id, time + 1, memWrite, 1) and outQ(procs1(id)) = outQ(procs(id)) with [head := head(outQ(procs(id))) + 1] and numEntries(procs1(id)) = numEntries(procs(id))) else % inQ and outQ both empty (let newaddr = a(instlist(id, pc(procs(id)))), newval = v(instlist(id, pc(procs(id)))) in if op(instlist(id, pc(procs(id)))) = READ then if oc(cache(procs(id))(newaddr)) then % if address in cache do the read (exists procs1, hist1 : rho(hist, mem, memhist, procs, time, hist1, mem, memhist, procs1, id, time, read, newaddr)) else (exists procs1: % else get it into the cache rho(hist, mem, memhist, procs, time, hist, mem, memhist, procs1, id, time, memRead, newaddr) and occEntry(inQ(procs1(id)), head(inQ(procs1(id)))) and a(QE(inQ(procs1(id)))(head(inQ(procs1(id))))) = newaddr and (exists procs2 : rho(hist, mem, memhist, procs1, time, hist, mem, memhist, procs2, id, time, cacheUpdate, newaddr) and oc(cache(procs2(id))(newaddr)) and (exists procs3, hist3 : % and then do the read rho(hist, mem, memhist, procs2, time, hist3, mem, memhist, procs3, id, time, read, newaddr)))) endif else % op = WRITE (exists procs1 : rho(hist, mem, memhist, procs, time, hist, mem, memhist, procs1, id, time, write, newaddr) and occEntry(outQ(procs1(id)), head(outQ(procs1(id)))) and a(QE(outQ(procs1(id)))(head(outQ(procs1(id))))) = newaddr and v(QE(outQ(procs1(id)))(head(outQ(procs1(id))))) = newval and empty(inQ(procs1(id))) and (exists procs2, hist2, mem2, memhist2 : rho(hist, mem, memhist, procs1, time, hist2, mem2, memhist2, procs2, id, time +1, memWrite, newaddr) and occEntry(inQ(procs2(id)), head(inQ(procs2(id)))) and a(QE(inQ(procs2(id)))(head(inQ(procs2(id))))) = newaddr and v(QE(inQ(procs2(id)))(head(inQ(procs2(id))))) = newval and mem2(newaddr) = newval and (exists procs3 : rho(hist2, mem2, memhist2, procs2, time +1, hist2, mem2, memhist2, procs3, id, time +1, cacheUpdate, newaddr) and mem2(newaddr) = newval and oc(cache(procs3(id))(newaddr)) and v(cache(procs3(id))(newaddr)) = newval))) endif ) endif ) END refine3 $$$refine3.prf (|refine3| (|pcSeqRun| "" (SKOSIMP*) (("" (LABEL "Match" -1) (("" (LABEL "toProve" 1) (("" (CASE "Forall (offset: nat): forall (sr : nat): sr <= size(hist!1) and offset <= sr IMPLIES pc(sprocs(serRun!1(sr - offset))(id!1)) <= pc(sprocs(serRun!1(sr))(id!1))") (("1" (LABEL "PCinc" -1) (("1" (INST - "sr!1 - srs!1") (("1" (INST - "sr!1") (("1" (SIMP) (("1" (CASE "FORALL (offset: nat): offset <= sr!1 IMPLIES (pc(sprocs(serRun!1(sr!1 - offset))(id!1)) < pc(sprocs(serRun!1(sr!1))(id!1)) IFF (EXISTS (newsr: posnat): sr!1 - offset < newsr AND newsr <= sr!1 AND id(lst(hist!1)(newsr)) = id!1))") (("1" (INST -1 "sr!1 - srs!1") (("1" (SIMP) NIL NIL)) NIL) ("2" (HIDE 2) (("2" (INDUCT "offset") (("1" (SIMP) (("1" (SKOSIMP*) (("1" (SIMP) NIL NIL)) NIL)) NIL) ("2" (SKOSIMP*) (("2" (REVEAL "PCinc") (("2" (HIDE -1) (("2" (SPSI) (("1" (SPSI -) (("1" (SKOSIMP*) (("1" (INST? +) (("1" (SIMP) NIL NIL)) NIL)) NIL) ("2" (APPLY (THEN (CASE "pc(sprocs(serRun!1(-1 - j!1 + sr!1))(id!1)) < pc(sprocs(serRun!1(sr!1 - j!1))(id!1))") (SIMP))) (("2" (HIDE "PCinc" -2 1) (("2" (EXPAND "Match") (("2" (FLATTEN) (("2" (INST - "-1 - j!1 + sr!1") (("2" (EXPAND "rho") (("2" (INST 1 "sr!1 - j!1") (("2" (SIMP) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (SKOSIMP*) (("2" (INST - "1") (("2" (INST - "sr!1 - j!1") (("2" (SIMP) (("2" (INST + "newsr!1") (("2" (SIMP) (("2" (APPLY (THEN (CASE "newsr!1 = sr!1 - j!1") (REPLACE*) (SIMP))) (("2" (APPLY (THEN (CASE "pc(sprocs(serRun!1(sr!1 - j!1 -1))(id!1)) < pc(sprocs(serRun!1(sr!1 -j!1))(id!1))") (SIMP))) (("1" (REVEAL "PCinc") (("1" (HIDE -1 -2) (("1" (INST - "j!1") (("1" (INST - "sr!1") (("1" (SIMP) NIL NIL)) NIL)) NIL)) NIL)) NIL) ("2" (EXPAND "Match") (("2" (EXPAND "rho") (("2" (FLATTEN) (("2" (INST "Match" "-1 - j!1 + sr!1") (("2" (SIMP) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("3" (SKOSIMP*) (("3" (SIMP) NIL NIL)) NIL) ("4" (SKOSIMP*) (("4" (SIMP) NIL NIL)) NIL)) NIL)) NIL) ("3" (SKOSIMP*) (("3" (SIMP) NIL NIL)) NIL)) NIL)) NIL)) NIL) ("2" (SIMP) NIL NIL)) NIL)) NIL) ("2" (HIDE "toProve") (("2" (INDUCT "offset") (("1" (SKOSIMP*) (("1" (SIMP) NIL NIL)) NIL) ("2" (SKOSIMP*) (("2" (INST - "sr!2") (("2" (SIMP) (("2" (APPLY (THEN (CASE " pc(sprocs(serRun!1(-1 - j!1 + sr!2))(id!1)) <= pc(sprocs(serRun!1(sr!2 - j!1))(id!1))") (SIMP))) (("2" (HIDE -1 2) (("2" (EXPAND "Match") (("2" (EXPAND "rho") (("2" (SIMP) (("2" (INST - "-1 - j!1 + sr!2") (("2" (SIMP) (("2" (SPLIT-ALL -) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("3" (SKOSIMP*) (("3" (SIMP) NIL NIL)) NIL)) NIL)) NIL) ("3" (SKOSIMP*) (("3" (SIMP) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|thetaSeq| "" (SKOSIMP*) (("" (INST 1 "(lambda (sr:nat) : (# smem := initmem, sprocs := initsprocs #))") (("" (LAZYGRIND) NIL NIL)) NIL)) NIL) (|reachSeq| "" (SKOSIMP*) (("" (LABEL "Match" -3) (("" (LABEL "toProve" 1) (("" (HIDE -1 -2 -3 1) (("" (REVEAL -1 -2 -3 1) (("" (EXP-RHO) (("" (EXPAND "Match") (("" (EXPAND "empty") (("" (SPLIT-RHO) (("1" (LABEL "canRead" -2) (("1" (EXPAND "canRead") (("1" (REPLACE*) (("1" (SIMP) (("1" (INTRONEXT) (("1" (HIDE "rho") (("1" (INST + "(lambda (n : nat): if n < next!1 then serRun!1(n) else (# smem := smem(serRun!1(n - 1)), sprocs:= (lambda (id : PROC_ID) : (let oldpc = pc(sprocs(serRun!1(next!1 - 1))(p_id!1)), val = smem(serRun!1(next!1 - 1))(a(instlist(p_id!1, pc(sprocs(serRun!1(next!1 - 1))(p_id!1))))) in (if id = p_id!1 then sprocs(serRun!1(next!1 - 1))(id) with [pc := oldpc + 1, readValues := (lambda pc : if pc = oldpc then val else readValues(sprocs(serRun!1(next!1 - 1))(id))(pc) endif) ] else sprocs(serRun!1(n-1))(id) endif )))#) endif)") (("1" (HIDE 1) (("1" (LEMMA "pcSeqRun") (("1" (REVEAL "Match") (("1" (INST?) (("1" (SIMP) (("1" (LABEL "pcSeq" -2) (("1" (HIDE -1 -2) (("1" (REVEAL "orig") (("1" (LEMMA "reachable") (("1" (INST?) (("1" (SIMP) (("1" (HIDE "orig") (("1" (LABEL "newReach" -1) (("1" (HIDE -1) (("1" (REVEAL "newReach") (("1" (EXPAND "reachable") (("1" (FLATTEN) (("1" (LABEL "histMatchPCnew" -10) (("1" (LABEL "histMatchPCnew" -10) (("1" (LABEL "new_histMatchPC" -10) (("1" (HIDE "newReach" "new_histMatchPC") (("1" (REVEAL 1) (("1" (SIMP) (("1" (CASE "(EXISTS (idsr: nat): size(hist!1) > 0 and idsr <= size(hist!1) AND idsr >= next!1 - 1 AND (pc(serRun!1(idsr)`sprocs(p_id!1)) /= pc(procs!1(p_id!1))))") (("1" (HIDE 1 "next" "nextSize") (("1" (INST? "Match") (("1" (INST? "Match") (("1" (INST? "Match") (("1" (SIMP) (("1" (REVEAL "pcSeq") (("1" (INST - "size(hist!1)") (("1" (INST -1 "p_id!1" "size(hist!1)") (("1" (SIMP) (("1" (SKOSIMP*) (("1" (INST - "idsr!1") (("1" (SIMP) (("1" (SIMP) (("1" (SKOSIMP*) (("1" (HIDE "canRead" -5) (("1" (REVEAL "new_histMatchPC") (("1" (EXPAND "histMatchPC") (("1" (FLATTEN) (("1" (INST -1 "newsr!1 + 1") (("1" (SIMP) (("1" (SIMP) (("1" (INST - "next!1") (("1" (HIDE -3 -4) (("1" (REVEAL "rho") (("1" (REPLACE*) (("1" (SIMP) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (SKOSIMP*) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (LABEL "pcConst" 1) (("2" (SPSI) (("1" (SKOSIMP*) (("1" (NEW-SPLIT-IF) (("1" (INST "Match" "sr!1") (("1" (NEW-SPLIT-IF) (("1" (APPLY (THEN (CASE "next!1 = 1 + sr!1") (REPLACE*) (SIMP))) (("1" (EXPAND "rho" +) (("1" (INST? "Match") (("1" (SPSI) (("1" (APPLY-EXTENSIONALITY 1 :HIDE? T) (("1" (NEW-SPLIT-IF) (("1" (APPLY-EXTENSIONALITY 1 :HIDE? T) (("1" (APPLY-EXTENSIONALITY 1 :HIDE? T) (("1" (NEW-SPLIT-IF) NIL NIL)) NIL)) NIL)) NIL)) NIL) ("2" (HIDE 2) (("2" (APPLY (THEN (CASE "pc(serRun!1(sr!1)`sprocs(p_id!1)) = pc(procs!1(p_id!1))") (SIMP))) (("2" (INST? "Match") (("2" (SIMP) (("2" (REVEAL "pcSeq") (("2" (INST - "p_id!1" "size(hist!1)") (("2" (SIMP) (("2" (INST - "sr!1") (("2" (SIMP) (("2" (SIMP) (("2" (SKOSIMP*) (("2" (HIDE "next" "nextSize" "canRead") (("2" (CLEAN-UP) (("2" (REVEAL "new_histMatchPC") (("2" (EXPAND "histMatchPC") (("2" (FLATTEN) (("2" (INST -1 "newsr!1 + 1") (("2" (SIMP) (("2" (INST - "next!1") (("2" (HIDE -3 -4) (("2" (REVEAL "rho") (("2" (REPLACE*) (("2" (SIMP) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (CASE "sr!1 = next!1") (("1" (INST-CP "pcConst" "next!1") (("1" (INST "pcConst" "next!1 - 1") (("1" (EXPAND "rho" +) (("1" (INST "Match" "next!1 - 1") (("1" (EXPAND "rho") (("1" (NEW-SPLIT-IF) (("1" (NEW-SPLIT-IF) (("1" (APPLY-EXTENSIONALITY 1 :HIDE? T) (("1" (NEW-SPLIT-IF) NIL NIL)) NIL) ("2" (APPLY-EXTENSIONALITY 2 :HIDE? T) (("2" (NEW-SPLIT-IF) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (HIDE "next" "nextSize") (("2" (INST "Match" "sr!1 - 1") (("2" (INST-CP "pcConst" "sr!1 - 1") (("2" (INST "pcConst" "sr!1") (("2" (SIMP) (("2" (EXPAND "rho") (("2" (NEW-SPLIT-IF) (("2" (NEW-SPLIT-IF) (("1" (APPLY-EXTENSIONALITY 1 :HIDE? T) (("1" (NEW-SPLIT-IF) NIL NIL)) NIL) ("2" (APPLY-EXTENSIONALITY 2 :HIDE? T) (("2" (NEW-SPLIT-IF) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (NEW-SPLIT-IF) NIL NIL) ("3" (SKOSIMP*) (("3" (INST? "Match") (("3" (INST? "Match") (("3" (INST? "Match") (("3" (SIMP) (("3" (HIDE "canRead") (("3" (NEW-SPLIT-IF) (("3" (INST "pcConst" "next!1 - 1") (("3" (SIMP) (("3" (SPSI) (("3" (CLEAN-UP) (("3" (SPSI "pcConst") (("1" (NEW-SPLIT-IF) (("1" (APPLY (THEN (CASE "next!1 = 1") (SIMP))) (("1" (REPLACE*) (("1" (EXPAND "theta") (("1" (EXPAND "initsprocs") (("1" (SIMP) (("1" (REPLACE*) (("1" (SIMP) (("1" (REVEAL "canRead") (("1" (REVEAL "cacheEqualMemhist") (("1" (INST?) (("1" (SIMP) (("1" (REPLACE*) (("1" (REVEAL "memhistCorrectInit") (("1" (APPLY (THEN (CASE "t(procs!1(p_id!1)) = 0") (SIMP))) (("1" (HIDE "next" "Match") (("1" (HIDE "canRead") (("1" (REVEAL "histMatchTimeE") (("1" (INST - "t(procs!1(p_id!1))") (("1" (SPSI -) (("1" (REVEAL "localTimeEarlier") (("1" (INST?) (("1" (SIMP) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (NEW-SPLIT-IF) (("1" (REVEAL "cacheEqualMemhist") (("1" (REVEAL "canRead") (("1" (INST? "cacheEqualMemhist") (("1" (SIMP) (("1" (HIDE "canRead") (("1" (REPLACE*) (("1" (CASE "next!1 = 1") (("1" (EXPAND "theta") (("1" (EXPAND "initsprocs") (("1" (SIMP) (("1" (REPLACE*) (("1" (REVEAL "memhistCorrectInit") (("1" (APPLY (THEN (CASE "t(procs!1(p_id!1)) = 0") (SIMP))) (("1" (HIDE "Match" "toProve") (("1" (REVEAL "localTimeEarlier") (("1" (INST?) (("1" (SIMP) (("1" (HIDE -2 -3) (("1" (REVEAL "histMatchTimeE") (("1" (INST -1 "t(procs!1(p_id!1))") (("1" (SIMP) (("1" (SKOSIMP*) (("1" (SIMP) (("1" (CASE "index!1 = 1") (("1" (EXPAND "timestamp") (("1" (EXPAND "lt") (("1" (SIMP) NIL NIL)) NIL)) NIL) ("2" (CASE "lt((# t := t(procs!1(p_id!1)), r := 1 + numRead(procs!1(p_id!1)), id := p_id!1 #), timestamp(lst(hist!1)(index!1)))") (("1" (EXPAND "lt" -1) (("1" (EXPAND "timestamp") (("1" (PROPAX) NIL NIL)) NIL)) NIL) ("2" (LEMLTSTRICT) (("2" (REVEAL "histLt") (("2" (INST -1 "1" "index!1") (("2" (SIMP) (("2" (EXPAND "timestamp") (("2" (INST? "trans" :WHERE 2) (("2" (INST "trans" "(# t := t(lst(hist!1)(1)), r := r(lst(hist!1)(1)), id := id(lst(hist!1)(1)) #)") (("2" (SIMP) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (SIMP) (("2" (INST "Match" "next!1 - 1") (("2" (SIMP) (("2" (CASE "t(lst(hist!1)(next!1 - 1)) = t(procs!1(p_id!1))") (("1" (SIMP) NIL NIL) ("2" (HIDE "Match" "toProve") (("2" (REVEAL "histCompleteNumRead") (("2" (INST -1 "p_id!1") (("2" (SIMP) (("2" (REVEAL "localTimeEarlier") (("2" (INST?) (("2" (REVEAL "histMatchTimeE") (("2" (INST -1 "t(procs!1(p_id!1))") (("2" (SIMP) (("2" (CASE "1 <= t(procs!1(p_id!1))") (("1" (SIMP) (("1" (SKOSIMP*) (("1" (HIDE "histCompleteNumRead") (("1" (HIDE "localTimeEarlier") (("1" (CASE "not lt(timestamp(lst(hist!1)(index!1)), (# t := t(procs!1(p_id!1)), r := 1 + numRead(procs!1(p_id!1)), id := p_id!1 #))") (("1" (EXPAND "timestamp" +) (("1" (EXPAND "lt") (("1" (SIMP) NIL NIL)) NIL)) NIL) ("2" (SPSI "nextSize") (("1" (LEMMA "nextExists") (("1" (INST? -) (("1" (REPLACE*) (("1" (NEW-SPLIT-IF -) (("1" (INST + "size(hist!1)") (("1" (SIMP) (("1" (EXPAND "lt" +) (("1" (EXPAND "timestamp") (("1" (REVEAL "histLt") (("1" (INST -1 "index!1" "size(hist!1)") (("1" (SIMP) (("1" (EXPAND "lt") (("1" (PROPAX) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (INST - "next!1 - 1") (("2" (SIMP) (("2" (EXPAND "lt" +) (("2" (EXPAND "timestamp") (("2" (LEMLTSTRICT) (("2" (INST -1 "(# t := t(procs!1(p_id!1)), r := 1 + numRead(procs!1(p_id!1)), id := p_id!1 #)" "timestamp(lst(hist!1)(next!1 - 1))") (("2" (EXPAND "timestamp") (("2" (SIMP) (("2" (SPSI -) (("1" (EXPAND "lt") (("1" (PROPAX) NIL NIL)) NIL) ("2" (CASE "lt((# t := t(lst(hist!1)(next!1 - 1)), r := r(lst(hist!1)(next!1 - 1)), id := id(lst(hist!1)(next!1 - 1)) #),(# t := t(lst(hist!1)(index!1)), r := r(lst(hist!1)(index!1)), id := id(lst(hist!1)(index!1)) #))") (("1" (HIDE "ltIsStrict") (("1" (REVEAL "histLt") (("1" (INST-CP -1 "next!1" "index!1") (("1" (INST -1 "index!1" "next!1 - 1") (("1" (SIMP) (("1" (REVEAL "linear") (("1" (INST? :WHERE "histLt") (("1" (SIMP) (("1" (HIDE "linear") (("1" (CASE "index!1 = next!1") (("1" (REVEAL "linear") (("1" (INST? "linear" :WHERE "nextSize") (("1" (SIMP) NIL NIL)) NIL)) NIL) ("2" (SIMP) (("2" (REVEAL "trans") (("2" (INST -1 "(# t := t(lst(hist!1)(index!1)), r := r(lst(hist!1)(index!1)), id := id(lst(hist!1)(index!1)) #)" "(# t := t(procs!1(p_id!1)), r := 1 + numRead(procs!1(p_id!1)), id := p_id!1 #)" "(# t := t(lst(hist!1)(next!1)), r := r(lst(hist!1)(next!1)), id := id(lst(hist!1)(next!1)) #)") (("2" (SIMP) (("2" (REVEAL "linear") (("2" (INST? :WHERE "trans") (("2" (SIMP) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (EXPAND "lt") (("2" (PROPAX) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (SIMP) (("2" (APPLY (THEN (CASE "t(procs!1(p_id!1)) = 0") (SIMP))) (("2" (CLEAN-UP) (("2" (REPLACE*) (("2" (HIDE -3 -4 "histCompleteNumRead") (("2" (CASE "lt((# t := 0, r := 1 + numRead(procs!1(p_id!1)), id := p_id!1 #), timestamp(lst(hist!1)(next!1 - 1)))") (("1" (LEMMA "nextExists") (("1" (INST?) (("1" (REPLACE*) (("1" (NEW-SPLIT-IF -) (("1" (INST - "next!1 - 1") (("1" (SIMP) NIL NIL)) NIL) ("2" (INST + "size(hist!1)") (("2" (SIMP) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (EXPAND "timestamp") (("2" (EXPAND "lt") (("2" (PROPAX) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (REPLACE -9 :DIR RL) (("2" (CASE " FORALL (offset: nat): size(hist!1) - offset >= next!1 - 1 IMPLIES readValues(sprocs(serRun!1(size(hist!1) - offset))(p_id!1))(pc!1) = readValues(sprocs(serRun!1(size(hist!1)))(p_id!1))(pc!1)") (("1" (INST -1 "size(hist!1) - next!1 + 1") (("1" (SIMP) NIL NIL)) NIL) ("2" (INDUCT "offset") (("1" (SIMP) NIL NIL) ("2" (SKOSIMP*) (("2" (SIMP) (("2" (HIDE "next" "nextSize") (("2" (REVEAL "Match") (("2" (HIDE -1 -2 -3) (("2" (INST -1 "size(hist!1) - 1 - j!1") (("2" (SIMP) (("2" (EXPAND "rho") (("2" (REPLACE -3 :DIR RL) (("2" (SPSI -) (("1" (REPLACE -3) (("1" (SIMP) (("1" (LIFT-IF) (("1" (SPSI) (("1" (HIDE 1 3) (("1" (HIDE -4 -5 -6 -13) (("1" (REVEAL "pcSeq") (("1" (INST -1 "p_id!1" "size(hist!1)") (("1" (SIMP) (("1" (INST -1 "size(hist!1) - j!1 - 1") (("1" (SIMP) (("1" (SPSI -) (("1" (SPSI -) (("1" (REVEAL "pcConst") (("1" (INST + "size(hist!1) - 1 - j!1") (("1" (SIMP) NIL NIL)) NIL)) NIL)) NIL) ("2" (INST? +) (("2" (SIMP) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (REPLACE -2) (("2" (NEW-SPLIT-IF) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("3" (SKOSIMP*) (("3" (SIMP) NIL NIL)) NIL) ("4" (SKOSIMP*) (("4" (SIMP) NIL NIL)) NIL) ("5" (SKOSIMP*) (("5" (SIMP) NIL NIL)) NIL) ("6" (SKOSIMP*) (("6" (SIMP) NIL NIL)) NIL)) NIL) ("3" (SKOSIMP*) (("3" (SIMP) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("4" (SKOSIMP*) (("4" (NEW-SPLIT-IF) (("1" (INST "pcConst" "next!1 - 1") (("1" (NEW-SPLIT-IF) (("1" (APPLY (THEN (CASE "next!1 = 1") (SIMP))) (("1" (EXPAND "theta") (("1" (EXPAND "initsprocs") (("1" (SIMP) (("1" (REPLACE*) (("1" (SIMP) (("1" (REVEAL "histMatchPCe") (("1" (INST?) (("1" (INST -1 "1") (("1" (INST? "Match") (("1" (SIMP) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (NEW-SPLIT-IF) (("2" (INST? "Match") (("2" (INST? "Match") (("2" (INST? "Match") NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("5" (SKOSIMP*) (("5" (NEW-SPLIT-IF) (("1" (INST? "Match") (("1" (INST? "Match") (("1" (INST? "Match") (("1" (INST? "Match") (("1" (SIMP) NIL NIL)) NIL)) NIL)) NIL)) NIL) ("2" (INST? "Match") (("2" (INST? "Match") (("2" (INST? "Match") (("2" (NEW-SPLIT-IF) (("1" (HIDE "canRead" "pcConst") (("1" (CASE "next!1 = 1") (("1" (EXPAND "theta") (("1" (EXPAND "initsprocs") (("1" (SIMP) (("1" (REPLACE*) (("1" (REVEAL "memhistCorrectInit") (("1" (APPLY (THEN (CASE "t(procs!1(p_id!1)) = 0") (SIMP))) (("1" (HIDE "Match" "toProve") (("1" (REVEAL "localTimeEarlier") (("1" (INST?) (("1" (SIMP) (("1" (HIDE -2 -3) (("1" (REVEAL "histMatchTimeE") (("1" (INST -1 "t(procs!1(p_id!1))") (("1" (SIMP) (("1" (SKOSIMP*) (("1" (SIMP) (("1" (CASE "index!1 = 1") (("1" (EXPAND "timestamp") (("1" (EXPAND "lt") (("1" (SIMP) NIL NIL)) NIL)) NIL) ("2" (CASE "lt((# t := t(procs!1(p_id!1)), r := 1 + numRead(procs!1(p_id!1)), id := p_id!1 #), timestamp(lst(hist!1)(index!1)))") (("1" (EXPAND "lt" -1) (("1" (EXPAND "timestamp") (("1" (PROPAX) NIL NIL)) NIL)) NIL) ("2" (LEMLTSTRICT) (("2" (REVEAL "histLt") (("2" (INST -1 "1" "index!1") (("2" (SIMP) (("2" (EXPAND "timestamp") (("2" (INST? "trans" :WHERE 2) (("2" (INST "trans" "(# t := t(lst(hist!1)(1)), r := r(lst(hist!1)(1)), id := id(lst(hist!1)(1)) #)") (("2" (SIMP) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (SIMP) (("2" (INST "Match" "next!1 - 1") (("2" (SIMP) (("2" (CASE "t(lst(hist!1)(next!1 - 1)) = t(procs!1(p_id!1))") (("1" (SIMP) NIL NIL) ("2" (HIDE "Match" "toProve") (("2" (REVEAL "localTimeEarlier") (("2" (INST?) (("2" (REVEAL "histMatchTimeE") (("2" (INST -1 "t(procs!1(p_id!1))") (("2" (SIMP) (("2" (CASE "1 <= t(procs!1(p_id!1))") (("1" (SIMP) (("1" (SKOSIMP*) (("1" (HIDE "localTimeEarlier") (("1" (CASE "not lt(timestamp(lst(hist!1)(index!1)), (# t := t(procs!1(p_id!1)), r := 1 + numRead(procs!1(p_id!1)), id := p_id!1 #))") (("1" (EXPAND "timestamp" +) (("1" (EXPAND "lt") (("1" (SIMP) NIL NIL)) NIL)) NIL) ("2" (SPSI "nextSize") (("1" (LEMMA "nextExists") (("1" (INST? -) (("1" (REPLACE*) (("1" (NEW-SPLIT-IF -) (("1" (INST + "size(hist!1)") (("1" (SIMP) (("1" (EXPAND "lt" +) (("1" (EXPAND "timestamp") (("1" (REVEAL "histLt") (("1" (INST -1 "index!1" "size(hist!1)") (("1" (SIMP) (("1" (EXPAND "lt") (("1" (PROPAX) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (INST - "next!1 - 1") (("2" (SIMP) (("2" (EXPAND "lt" +) (("2" (EXPAND "timestamp") (("2" (LEMLTSTRICT) (("2" (INST -1 "(# t := t(procs!1(p_id!1)), r := 1 + numRead(procs!1(p_id!1)), id := p_id!1 #)" "timestamp(lst(hist!1)(next!1 - 1))") (("2" (EXPAND "timestamp") (("2" (SIMP) (("2" (SPSI -) (("1" (EXPAND "lt") (("1" (PROPAX) NIL NIL)) NIL) ("2" (CASE "lt((# t := t(lst(hist!1)(next!1 - 1)), r := r(lst(hist!1)(next!1 - 1)), id := id(lst(hist!1)(next!1 - 1)) #),(# t := t(lst(hist!1)(index!1)), r := r(lst(hist!1)(index!1)), id := id(lst(hist!1)(index!1)) #))") (("1" (HIDE "ltIsStrict") (("1" (REVEAL "histLt") (("1" (INST-CP -1 "next!1" "index!1") (("1" (INST -1 "index!1" "next!1 - 1") (("1" (SIMP) (("1" (REVEAL "linear") (("1" (INST? :WHERE "histLt") (("1" (SIMP) (("1" (HIDE "linear") (("1" (CASE "index!1 = next!1") (("1" (REVEAL "linear") (("1" (INST? "linear" :WHERE "nextSize") (("1" (SIMP) NIL NIL)) NIL)) NIL) ("2" (SIMP) (("2" (REVEAL "trans") (("2" (INST -1 "(# t := t(lst(hist!1)(index!1)), r := r(lst(hist!1)(index!1)), id := id(lst(hist!1)(index!1)) #)" "(# t := t(procs!1(p_id!1)), r := 1 + numRead(procs!1(p_id!1)), id := p_id!1 #)" "(# t := t(lst(hist!1)(next!1)), r := r(lst(hist!1)(next!1)), id := id(lst(hist!1)(next!1)) #)") (("2" (SIMP) (("2" (REVEAL "linear") (("2" (INST? :WHERE "trans") (("2" (SIMP) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (EXPAND "lt") (("2" (PROPAX) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (SIMP) (("2" (APPLY (THEN (CASE "t(procs!1(p_id!1)) = 0") (SIMP))) (("2" (CLEAN-UP) (("2" (REPLACE*) (("2" (HIDE -3 -4 "histCompleteNumRead") (("2" (CASE "lt((# t := 0, r := 1 + numRead(procs!1(p_id!1)), id := p_id!1 #), timestamp(lst(hist!1)(next!1 - 1)))") (("1" (LEMMA "nextExists") (("1" (INST?) (("1" (REPLACE*) (("1" (NEW-SPLIT-IF -) (("1" (INST - "next!1 - 1") (("1" (SIMP) NIL NIL)) NIL) ("2" (INST + "size(hist!1)") (("2" (SIMP) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (EXPAND "timestamp") (("2" (EXPAND "lt") (("2" (PROPAX) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (INST? "Match") (("2" (SIMP) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (SKOSIMP*) (("2" (SIMP) NIL NIL)) NIL) ("3" (SKOSIMP*) (("3" (SIMP) NIL NIL)) NIL)) NIL)) NIL) ("2" (INST + "next(hist!1, (# t := t(procs!1(p_id!1)), r := 1 + numRead(procs!1(p_id!1)), id := p_id!1 #))") NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (INST + "serRun!1") (("2" (SIMP) (("2" (REPLACE*) (("2" (HIDE "rho") (("2" (APPLY (THEN (SPSI) (SKOSIMP*))) (("1" (INST?) (("1" (INST?) (("1" (SPLIT-ALL) NIL NIL)) NIL)) NIL) ("2" (INST?) (("2" (INST?) (("2" (INST - "id!1") (("2" (SPLIT-ALL) (("2" (REVEAL "queuesNonNeg") (("2" (INST?) (("2" (SIMP) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("3" (INST + "serRun!1") (("3" (REPLACE*) (("3" (HIDE "rho") (("3" (SPSI) (("1" (SKOSIMP*) (("1" (INST?) (("1" (INST?) (("1" (SPLIT-ALL) NIL NIL)) NIL)) NIL)) NIL) ("2" (SKOSIMP*) (("2" (INST?) (("2" (INST?) (("2" (INSTBEST) (("2" (INST - "id!1") (("2" (SPLIT-ALL) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("4" (REPLACE*) (("4" (INST + "serRun!1") (("4" (SPSI) (("1" (SKOSIMP*) (("1" (INST?) (("1" (INST?) (("1" (SIMP) (("1" (SPLIT-ALL) NIL NIL)) NIL)) NIL)) NIL)) NIL) ("2" (SKOSIMP*) (("2" (HIDE "rho") (("2" (INSTBEST) (("2" (INST?) (("2" (INSTBEST) (("2" (INST - "id!1") (("2" (SPLIT-ALL) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("5" (INST + "serRun!1 with [(size(hist_p!1)) := (# smem := mem_p!1, sprocs := sprocs(serRun!1(size(hist!1))) WITH [(p_id!1) := sprocs(serRun!1(size(hist!1)))(p_id!1) with [pc := pc(sprocs(serRun!1(size(hist!1)))(p_id!1)) + 1]] #)]") (("5" (REPLACE*) (("5" (HIDE "rho") (("5" (SIMP) (("5" (SPSI) (("1" (SKOSIMP*) (("1" (INST - "sr!1") (("1" (CASE "sr!1 = size(hist!1)") (("1" (REPLACE*) (("1" (SIMP) (("1" (REPLACE*) (("1" (CLEAN-UP) (("1" (REVEAL "Match") (("1" (CASE "size(hist!1) = 0") (("1" (REPLACE*) (("1" (EXPAND "rho") (("1" (CLEAN-UP) (("1" (EXPAND "theta") (("1" (EXPAND "initsprocs") (("1" (SIMP) (("1" (REPLACE*) (("1" (SIMP) (("1" (INST?) (("1" (REVEAL "queuesMatchProg") (("1" (INST?) (("1" (FLATTEN) (("1" (HIDE -1) (("1" (INST?) (("1" (REVEAL "queuesNonNeg") (("1" (INST?) (("1" (SIMP) (("1" (APPLY (THEN (CASE "pc(QE(outQ(procs!1(p_id!1)))(head(outQ(procs!1(p_id!1))))) = 1") (SIMP))) (("1" (HIDE 2) (("1" (REVEAL "histMatchPCe") (("1" (INST -1 "p_id!1" "1") (("1" (SIMP) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (CLEAN-UP) (("2" (INST - "size(hist!1) - 1") (("1" (SIMP) (("1" (EXPAND "rho" +) (("1" (REVEAL "queuesMatchProg") (("1" (INST?) (("1" (FLATTEN) (("1" (HIDE -1) (("1" (INST?) (("1" (REVEAL "queuesNonNeg") (("1" (INST?) (("1" (SIMP) (("1" (APPLY (THEN (CASE "pc(QE(outQ(procs!1(p_id!1)))(head(outQ(procs!1(p_id!1))))) = pc(sprocs(serRun!1(size(hist!1)))(p_id!1))") (SIMP))) (("1" (NEW-SPLIT-IF) (("1" (APPLY-EXTENSIONALITY 2 :HIDE? T) (("1" (NEW-SPLIT-IF) (("1" (APPLY-EXTENSIONALITY 1 :HIDE? T) NIL NIL)) NIL)) NIL)) NIL) ("2" (HIDE 3) (("2" (REVEAL "histMatchPCe") (("2" (REPLACE*) (("2" (INST? "Match") (("2" (INST "Match" "p_id!1") (("2" (SIMP) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (SIMP) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (SIMP) NIL NIL)) NIL)) NIL)) NIL) ("2" (SKOSIMP*) (("2" (INST?) (("2" (INST?) (("2" (SIMP) (("2" (NEW-SPLIT-IF) NIL NIL)) NIL)) NIL)) NIL)) NIL) ("3" (SKOSIMP*) (("3" (INST?) (("3" (INST?) (("3" (INSTBEST) (("3" (INST?) (("3" (SIMP) (("3" (NEW-SPLIT-IF) (("3" (CLEAN-UP) (("3" (REVEAL "outQpcInc") (("3" (INST?) (("3" (SIMP) (("3" (REVEAL "queuesNonNeg") (("3" (INST?) (("3" (SIMP) (("3" (INST - "1 + head(outQ(procs!1(p_id!1)))") (("3" (INST - "1 + pc(QE(outQ(procs!1(p_id!1)))(head(outQ(procs!1(p_id!1)))))") (("3" (SIMP) (("3" (NEW-SPLIT-IF) (("1" (SKOSIMP*) (("1" (SIMP) NIL NIL)) NIL) ("2" (REVEAL "outQpcInc") (("2" (INST -3 "1 + head(outQ(procs!1(p_id!1)))") (("2" (SIMP) (("2" (SIMP) (("2" (SKOSIMP*) (("2" (SIMP) (("2" (HIDE -1) (("2" (INST -1 "qPoint2!1") (("2" (INST -3 "qPoint2!1") (("2" (SIMP) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("4" (SKOSIMP*) (("4" (INST? "Match") (("4" (INST? "Match") (("4" (INST? "Match") (("4" (INST? "Match") (("4" (NEW-SPLIT-IF) (("4" (INST? "Match") (("4" (NEW-SPLIT-IF) (("4" (REVEAL "histMatchTime") (("4" (INST?) (("4" (SIMP) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("6" (INST + "serRun!1") (("6" (REPLACE*) (("6" (HIDE "rho") (("6" (SPSI) (("1" (SKOSIMP*) (("1" (INST?) (("1" (INST?) (("1" (SPLIT-ALL) NIL NIL)) NIL)) NIL)) NIL) ("2" (SKOSIMP*) (("2" (INST?) (("2" (INSTBEST) (("2" (INSTBEST) (("2" (INST - "id!1") (("2" (SPLIT-ALL) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("7" (INST + "serRun!1") (("7" (REPLACE*) (("7" (SIMP) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|noDeadlock| "" (SKOSIMP*) (("" (EXPAND "numEntries") (("" (SPSI) (("1" (EXPAND "rho") (("1" (INST 2 "procs!1 WITH [(id!1) := (# inQ := inQ(procs!1(id!1)) WITH [head := 1 + head(inQ(procs!1(id!1)))], outQ := outQ(procs!1(id!1)), t := IF id (QE(inQ(procs!1(id!1))) (head(inQ(procs!1(id!1))))) = id!1 AND NOT star (QE(inQ(procs!1(id!1))) (head(inQ(procs!1(id!1))))) THEN t(procs!1(id!1)) ELSE 1 + t(procs!1(id!1)) ENDIF, numRead := IF id (QE(inQ(procs!1(id!1))) (head(inQ(procs!1(id!1))))) = id!1 AND NOT star (QE(inQ(procs!1(id!1))) (head(inQ(procs!1(id!1))))) THEN numRead(procs!1(id!1)) ELSE 0 ENDIF, readValues := readValues(procs!1(id!1)), pc := pc(procs!1(id!1)), cache := LAMBDA (a: ADDRESS[U]): IF a = a (QE(inQ(procs!1(id!1))) (head(inQ(procs!1(id!1))))) THEN (# oc := TRUE, v := v (QE(inQ(procs!1(id!1))) (head(inQ(procs!1(id!1))))) #) ELSE cache(procs!1(id!1))(a) ENDIF #)]") (("1" (EXPAND "empty") (("1" (SPSI) NIL NIL)) NIL)) NIL)) NIL) ("2" (SPSI) (("1" (EXPAND "empty") (("1" (EXPAND "rho") (("1" (SPSI) (("1" (INST 2 "(LAMBDA (proc_id: PROC_ID[U]): procs!1(proc_id) WITH [outQ := IF proc_id = id!1 THEN outQ(procs!1(proc_id)) WITH [head := 1 + head(outQ(procs!1(proc_id)))] ELSE outQ(procs!1(proc_id)) ENDIF, inQ := addQentry(inQ(procs!1(proc_id)), QE(outQ(procs!1(id!1)))(head(outQ(procs!1(id!1)))) WITH [t := 1 + time!1, id := id!1, (star) := proc_id = id!1])])" "(# size := 1 + size(hist!1), lst := lst(hist!1) WITH [(1 + size(hist!1)) := (# t := 1 + time!1, r := 0, id := id!1, op := WRITE, pc := QE(outQ(procs!1(id!1))) (head(outQ(procs!1(id!1))))`pc, v := QE(outQ(procs!1(id!1))) (head(outQ(procs!1(id!1))))`v, a := QE(outQ(procs!1(id!1))) (head(outQ(procs!1(id!1))))`a #)] #)" " memhist!1 WITH [(1 + time!1) := (# pc := QE(outQ(procs!1(id!1)))(head(outQ(procs!1(id!1))))`pc, id := id!1, mem := mem!1 WITH [(QE(outQ(procs!1(id!1)))(head(outQ(procs!1(id!1))))`a) := QE(outQ(procs!1(id!1))) (head(outQ(procs!1(id!1))))`v] #)]" " mem!1 WITH [(QE(outQ(procs!1(id!1)))(head(outQ(procs!1(id!1))))`a) := QE(outQ(procs!1(id!1)))(head(outQ(procs!1(id!1))))`v]") (("1" (SPSI) (("1" (EXPAND "addQentry") (("1" (PROPAX) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (SPSI) (("1" (SPSI) (("1" (EXPAND "rho") (("1" (INST 1 "procs!1 WITH [(id!1) := procs!1(id!1) WITH [pc := 1 + pc(procs!1(id!1)), numRead := 1 + numRead(procs!1(id!1)), readValues := readValues(procs!1(id!1)) WITH [(pc(procs!1(id!1))) := v (cache(procs!1(id!1)) (a (instlist (id!1, pc(procs!1(id!1))))))]]]" "insert(hist!1,(# t:= t(procs!1(id!1)), r:= numRead(procs!1(id!1)) + 1, id := id!1, op := READ, pc := pc(procs!1(id!1)), v := v(cache(procs!1(id!1))(a(instlist(id!1, pc(procs!1(id!1)))))), a := a(instlist(id!1, pc(procs!1(id!1)))) #)) ") (("1" (SPSI) (("1" (EXPAND "canRead") (("1" (EXPAND "empty") (("1" (SIMP) (("1" (SKOSIMP*) (("1" (SIMP) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (EXPAND "occEntry") (("2" (EXPAND "empty") (("2" (INST 2 " procs!1 WITH [(id!1) := procs!1(id!1) WITH [inQ := addQentry(inQ(procs!1(id!1)), (# a := a (instlist (id!1, pc(procs!1(id!1)))), v := mem!1 (a (instlist (id!1, pc(procs!1(id!1))))), t := time!1, id := id!1, pc := pc(procs!1(id!1)), star := FALSE #))]]") (("2" (SIMP) (("2" (EXPAND "rho") (("2" (EXPAND "addQentry") (("2" (INST 2 "procs!1 WITH [(id!1) := (# inQ := (# head := 1 + head(inQ(procs!1(id!1))), tail := 1 + tail(inQ(procs!1(id!1))), QE := QE(inQ(procs!1(id!1))) WITH [(tail(inQ(procs!1(id!1)))) := (# a := a (instlist (id!1, pc(procs!1(id!1)))), v := mem!1 (a (instlist (id!1, pc(procs!1(id!1))))), t := time!1, id := id!1, pc := pc(procs!1(id!1)), star := FALSE #)] #), outQ := procs!1(id!1)`outQ, t := procs!1(id!1)`t, numRead := procs!1(id!1)`numRead, readValues := procs!1(id!1)`readValues, pc := procs!1(id!1)`pc, cache := LAMBDA (a: ADDRESS[U]): IF a = a(instlist(id!1, pc(procs!1(id!1)))) THEN (# oc := TRUE, v := mem!1 (a (instlist (id!1, pc(procs!1(id!1))))) #) ELSE procs!1(id!1)`cache(a) ENDIF #)]") (("2" (SIMP) (("2" (EXPAND "canRead") (("2" (INST 2 "procs!1 WITH [(id!1) := (# inQ := (# head := 1 + head(inQ(procs!1(id!1))), tail := 1 + tail(inQ(procs!1(id!1))), QE := QE(inQ(procs!1(id!1))) WITH [(tail(inQ(procs!1(id!1)))) := (# a := a (instlist (id!1, pc(procs!1(id!1)))), v := mem!1 (a (instlist (id!1, pc (procs!1(id!1))))), t := time!1, id := id!1, pc := pc(procs!1(id!1)), star := FALSE #)] #), outQ := procs!1(id!1)`outQ, t := procs!1(id!1)`t, numRead := 1 + procs!1(id!1)`numRead, readValues := procs!1(id!1)`readValues WITH [(procs!1(id!1)`pc) := mem!1 (a (instlist (id!1, pc(procs!1(id!1)))))], pc := 1 + procs!1(id!1)`pc, cache := LAMBDA (a: ADDRESS[U]): IF a = a(instlist(id!1, pc(procs!1(id!1)))) THEN (# oc := TRUE, v := mem!1 (a (instlist (id!1, pc(procs!1(id!1))))) #) ELSE procs!1(id!1)`cache(a) ENDIF #)]" "insert(hist!1, (# t := procs!1(id!1)`t, r := 1 + procs!1(id!1)`numRead, id := id!1, op := READ, pc := procs!1(id!1)`pc, v := mem!1(a(instlist(id!1, pc(procs!1(id!1))))), a := a(instlist(id!1, procs!1(id!1)`pc)) #))") (("2" (SPSI) (("2" (SKOSIMP*) (("2" (SIMP) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (EXPAND "empty") (("2" (EXPAND "occEntry") (("2" (INST 2 "procs!1 WITH [(id!1) := procs!1(id!1) WITH [pc := 1 + pc(procs!1(id!1)), outQ := addQentry(outQ(procs!1(id!1)), (# a := a (instlist (id!1, pc(procs!1(id!1)))), v := v (instlist (id!1, pc(procs!1(id!1)))), t := 0, id := id!1, pc := pc(procs!1(id!1)), star := TRUE #))]]") (("2" (EXPAND "rho") (("2" (EXPAND "addQentry") (("2" (SIMP) (("2" (EXPAND "canWrite") (("2" (SPSI) (("2" (INST 2 "(LAMBDA (proc_id: PROC_ID[U]): procs!1 WITH [(id!1) := procs!1(id!1) WITH [pc := 1 + pc(procs!1(id!1)), outQ := (# head := head(outQ(procs!1(id!1))), tail := 1 + tail(outQ(procs!1(id!1))), QE := QE(outQ(procs!1(id!1))) WITH [(tail(outQ(procs!1(id!1)))) := (# a := a (instlist (id!1, pc (procs!1 (id!1)))), v := v (instlist (id!1, pc (procs!1 (id!1)))), t := 0, id := id!1, pc := pc(procs!1(id!1)), star := TRUE #)] #)]] (proc_id) WITH [outQ := IF proc_id = id!1 THEN (# head := 1 + head(outQ(procs!1(id!1))), tail := 1 + tail(outQ(procs!1(id!1))), QE := QE(outQ(procs!1(id!1))) WITH [(tail(outQ(procs!1(id!1)))) := (# a := a (instlist (id!1, pc(procs!1(id!1)))), v := v (instlist (id!1, pc(procs!1(id!1)))), t := 0, id := id!1, pc := pc(procs!1(id!1)), star := TRUE #)] #) ELSE outQ(procs!1(proc_id)) ENDIF, inQ := (# head := head (inQ (procs!1 WITH [(id!1) := procs!1(id!1) WITH [pc := 1 + pc(procs!1(id!1)), outQ := (# head := head (outQ (procs!1 (id!1))), tail := 1 + tail (outQ (procs!1 (id!1))), QE := QE (outQ (procs!1 (id!1))) WITH [(tail (outQ (procs!1 (id!1)))) := (# a := a (instlist (id!1, pc (procs!1 (id!1)))), v := v (instlist (id!1, pc (procs!1 (id!1)))), t := 0, id := id!1, pc := pc (procs!1 (id!1)), star := TRUE #)] #)]] (proc_id))), tail := 1 + tail (inQ (procs!1 WITH [(id!1) := procs!1(id!1) WITH [pc := 1 + pc(procs!1(id!1)), outQ := (# head := head (outQ (procs!1 (id!1))), tail := 1 + tail (outQ (procs!1 (id!1))), QE := QE (outQ (procs!1 (id!1))) WITH [(tail (outQ (procs!1 (id!1)))) := (# a := a (instlist (id!1, pc (procs!1 (id!1)))), v := v (instlist (id!1, pc (procs!1 (id!1)))), t := 0, id := id!1, pc := pc (procs!1 (id!1)), star := TRUE #)] #)]] (proc_id))), QE := QE (inQ (procs!1 WITH [(id!1) := procs!1(id!1) WITH [pc := 1 + pc(procs!1(id!1)), outQ := (# head := head (outQ (procs!1 (id!1))), tail := 1 + tail (outQ (procs!1 (id!1))), QE := QE (outQ (procs!1 (id!1))) WITH [(tail (outQ (procs!1 (id!1)))) := (# a := a (instlist (id!1, pc (procs!1 (id!1)))), v := v (instlist (id!1, pc (procs!1 (id!1)))), t := 0, id := id!1, pc := pc (procs!1 (id!1)), star := TRUE #)] #)]] (proc_id))) WITH [(tail (inQ (procs!1 WITH [(id!1) := procs!1(id!1) WITH [pc := 1 + pc (procs!1 (id!1)), outQ := (# head := head (outQ (procs!1 (id!1))), tail := 1 + tail (outQ (procs!1 (id!1))), QE := QE (outQ (procs!1 (id!1))) WITH [(tail (outQ (procs!1 (id!1)))) := (# a := a (instlist (id!1, pc (procs!1 (id!1)))), v := v (instlist (id!1, pc (procs!1 (id!1)))), t := 0, id := id!1, pc := pc (procs!1 (id!1)), star := TRUE #)] #)]] (proc_id)))) := (# a := a (instlist (id!1, pc(procs!1(id!1)))), v := v (instlist (id!1, pc(procs!1(id!1)))), t := 1 + time!1, id := id!1, pc := pc(procs!1(id!1)), star := proc_id = id!1 #)] #)])" "(# size := 1 + size(hist!1), lst := lst(hist!1) WITH [(1 + size(hist!1)) := (# t := 1 + time!1, r := 0, id := id!1, op := WRITE, pc := pc(procs!1(id!1)), v := v(instlist(id!1, pc(procs!1(id!1)))), a := a (instlist (id!1, pc(procs!1(id!1)))) #)] #)" "mem!1 WITH [(a(instlist(id!1, pc(procs!1(id!1))))) := v(instlist(id!1, pc(procs!1(id!1))))]" "memhist!1 WITH [(1 + time!1) := (# pc := pc(procs!1(id!1)), id := id!1, mem := mem!1 WITH [(a(instlist(id!1, pc(procs!1(id!1))))) := v (instlist (id!1, pc(procs!1(id!1))))] #)]") (("2" (SPSI) (("2" (INST 1 "(LAMBDA (proc_id: PROC_ID[U]): procs!1 WITH [(id!1) := procs!1(id!1) WITH [pc := 1 + pc(procs!1(id!1)), outQ := (# head := head(outQ(procs!1(id!1))), tail := 1 + tail(outQ(procs!1(id!1))), QE := QE(outQ(procs!1(id!1))) WITH [(tail(outQ(procs!1(id!1)))) := (# a := a (instlist (id!1, pc (procs!1(id!1)))), v := v (instlist (id!1, pc (procs!1(id!1)))), t := 0, id := id!1, pc := pc(procs!1(id!1)), star := TRUE #)] #)]] (proc_id) WITH [outQ := IF proc_id = id!1 THEN (# head := 1 + head(outQ(procs!1(id!1))), tail := 1 + tail(outQ(procs!1(id!1))), QE := QE(outQ(procs!1(id!1))) WITH [(tail(outQ(procs!1(id!1)))) := (# a := a (instlist (id!1, pc(procs!1(id!1)))), v := v (instlist (id!1, pc(procs!1(id!1)))), t := 0, id := id!1, pc := pc(procs!1(id!1)), star := TRUE #)] #) ELSE outQ(procs!1(proc_id)) ENDIF, inQ := (# head := head (inQ (procs!1 WITH [(id!1) := procs!1(id!1) WITH [pc := 1 + pc(procs!1(id!1)), outQ := (# head := head (outQ (procs!1 (id!1))), tail := 1 + tail (outQ (procs!1 (id!1))), QE := QE (outQ (procs!1 (id!1))) WITH [(tail (outQ (procs!1 (id!1)))) := (# a := a (instlist (id!1, pc (procs!1 (id!1)))), v := v (instlist (id!1, pc (procs!1 (id!1)))), t := 0, id := id!1, pc := pc (procs!1 (id!1)), star := TRUE #)] #)]] (proc_id))), tail := 1 + tail (inQ (procs!1 WITH [(id!1) := procs!1(id!1) WITH [pc := 1 + pc(procs!1(id!1)), outQ := (# head := head (outQ (procs!1 (id!1))), tail := 1 + tail (outQ (procs!1 (id!1))), QE := QE (outQ (procs!1 (id!1))) WITH [(tail (outQ (procs!1 (id!1)))) := (# a := a (instlist (id!1, pc (procs!1 (id!1)))), v := v (instlist (id!1, pc (procs!1 (id!1)))), t := 0, id := id!1, pc := pc (procs!1 (id!1)), star := TRUE #)] #)]] (proc_id))), QE := QE (inQ (procs!1 WITH [(id!1) := procs!1(id!1) WITH [pc := 1 + pc(procs!1(id!1)), outQ := (# head := head (outQ (procs!1 (id!1))), tail := 1 + tail (outQ (procs!1 (id!1))), QE := QE (outQ (procs!1 (id!1))) WITH [(tail (outQ (procs!1 (id!1)))) := (# a := a (instlist (id!1, pc (procs!1 (id!1)))), v := v (instlist (id!1, pc (procs!1 (id!1)))), t := 0, id := id!1, pc := pc (procs!1 (id!1)), star := TRUE #)] #)]] (proc_id))) WITH [(tail (inQ (procs!1 WITH [(id!1) := procs!1(id!1) WITH [pc := 1 + pc (procs!1(id!1)), outQ := (# head := head (outQ (procs!1 (id!1))), tail := 1 + tail (outQ (procs!1 (id!1))), QE := QE (outQ (procs!1 (id!1))) WITH [(tail (outQ (procs!1 (id!1)))) := (# a := a (instlist (id!1, pc (procs!1 (id!1)))), v := v (instlist (id!1, pc (procs!1 (id!1)))), t := 0, id := id!1, pc := pc (procs!1 (id!1)), star := TRUE #)] #)]] (proc_id)))) := (# a := a (instlist (id!1, pc(procs!1(id!1)))), v := v (instlist (id!1, pc(procs!1(id!1)))), t := 1 + time!1, id := id!1, pc := pc(procs!1(id!1)), star := proc_id = id!1 #)] #)]) WITH [(id!1) := (# inQ := (# head := 1 + head(procs!1(id!1)`inQ), tail := 1 + tail(procs!1(id!1)`inQ), QE := QE(procs!1(id!1)`inQ) WITH [(tail(procs!1(id!1)`inQ)) := (# a := a (instlist (id!1, pc(procs!1(id!1)))), v := v (instlist (id!1, pc(procs!1(id!1)))), t := 1 + time!1, id := id!1, pc := pc(procs!1(id!1)), star := TRUE #)] #), outQ := (# head := 1 + head(outQ(procs!1(id!1))), tail := 1 + tail(outQ(procs!1(id!1))), QE := QE(outQ(procs!1(id!1))) WITH [(tail(outQ(procs!1(id!1)))) := (# a := a (instlist (id!1, pc(procs!1(id!1)))), v := v (instlist (id!1, pc(procs!1(id!1)))), t := 0, id := id!1, pc := pc(procs!1(id!1)), star := TRUE #)] #), t := 1 + procs!1(id!1)`t, numRead := 0, readValues := procs!1(id!1)`readValues, pc := 1 + pc(procs!1(id!1)), cache := LAMBDA (a: ADDRESS[U]): IF a = a(instlist(id!1, pc(procs!1(id!1)))) THEN (# oc := TRUE, v := v (instlist (id!1, pc(procs!1(id!1)))) #) ELSE procs!1(id!1)`cache(a) ENDIF #)]") (("2" (SPSI) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) $$$serial.pvs serial[U : posnat]: THEORY % Definition of the serial system. % There is an array procs of processors. % At each step process p_id performs the next access in the instlist (either a % read or a write.) % The global memory, mem, is updated if the access is a write. % The auxiliary variable readValues records the values returned by reads. BEGIN IMPORTING shared[U] SERIAL_PROC_TYPE : TYPE = [# pc : PC_RANGE, readValues : [PC_RANGE -> VALUE] #] mem, mem_p : VAR MEM_TYPE proc_id, p_id, id : VAR PROC_ID procs, procs_p : VAR [PROC_ID -> SERIAL_PROC_TYPE] a, addr : VAR ADDRESS pc : VAR PC_RANGE initsprocs : [PROC_ID -> SERIAL_PROC_TYPE] = (lambda proc_id : (# pc := 1, readValues := (lambda pc : 0) #)) theta(mem, procs): bool = procs = initsprocs and mem = initmem rho(mem, procs, mem_p, procs_p, p_id): bool = (let proc = procs(p_id), pc = pc(procs(p_id)), a = a(instlist(p_id, pc(procs(p_id)))), v = v(instlist(p_id, pc(procs(p_id)))) in if op(instlist(p_id, pc)) = READ then mem_p = mem and procs_p = procs with [(p_id) := (# pc := pc + 1, readValues := readValues(proc) with [(pc) := mem(a)] #)] else mem_p = mem with [(a) := v] and procs_p = procs with [(p_id) := (# pc := pc + 1, readValues := readValues(proc) #)] endif ) END serial $$$more_nat_types.pvs more_nat_types[m: posnat]: THEORY BEGIN upto_nz : TYPE = {i: upto[m] | NOT i = 0} CONTAINING m greater_one_nat : TYPE = {i : posnat | NOT i = 1} containing 2 END more_nat_types $$$more_nat_types.prf (|more_nat_types| (|upto_nz_TCC1| "" (SUBTYPE-TCC) NIL NIL) (|greater_one_nat_TCC1| "" (SUBTYPE-TCC) NIL NIL)) $$$shared.pvs shared[U : posnat]: THEORY % Structures common to the lazy caching and serial algorithms BEGIN IMPORTING more_nat_types % The range of instruction indices PC_RANGE: TYPE = posnat OP_TYPE: TYPE = {READ, WRITE} ADDRESS : TYPE = nat VALUE : TYPE = real TIME : TYPE = nat % Processor identities are in the range 1..U PROC_ID : TYPE = upto_nz[U] % A memory is an function from ADDRESS to VALUE MEM_TYPE: TYPE = [ADDRESS -> VALUE] % Instructions have operations, addresses, and values. INST: TYPE = [# op: OP_TYPE, a: ADDRESS, v: VALUE #] % This data structure stores the instruction lists ("programs") % for all processors instlist: [PROC_ID, PC_RANGE -> INST] % The initial memory state. It is undefined, but must be the % same in both systems. initmem : [ADDRESS -> VALUE] END shared $$$lazy.pvs lazy[U : posnat]: THEORY % In this file we define the lazy caching algorithm. % We note a couple of terminology differences between the PVS code % and the article. % article PVS % memHist memhist of type MEM_HIST_TYPE. % mem(memhist(t)) gives the memory at time t, id and pc identify the instruction % that upated memhist(t-1) to memhist(t). % history, H hist of HISTORY_TYPE % size(hist) gives the number of occupied entries in hist, lst is the list % of entries. % Each entry is of type HIST_RECORD_TYPE, containing an operation, pc, time, % reads(r), address and processor id field. % P_i (processor with id i). % The $U$ processors are in a array procs of PROC_INFO, where PROC_INFO is % the information stored for each processor. % PROC_INFO has a program counter pc, in and out queues inQ, outQ, a cache % numRead, the number of reads since the last countable cache update, % and the array numValues of values read. % C_i cache of CACHE_TYPE. Accessed as procs[i].cache. % Each entry has a value v and a flag oc, which is true % iff the value is valid i.e. is "in" the cache. Entries which are not % valid (occupied) are "not in the cache." % Out_i, In_i queues of type QUEUE_TYPE. Accessed as procs[i].inQ, procs[i].outQ % Each queue entry is of type QUEUE_ENTRY_TYPE. In additional to % the "star", address and value fields, they also contain auxiliary % operation, time, pc and processor id fields. % The top entry of the queue is pointed to by head, and tail points % to the next free slot. % The queues are implictly assumed to be unbounded, however a bound % could easily be imposed, if so desired, by adding constraints to the % conditions on which read, memWrite, and memRead occur. % Actions % read (R) read % write (W) write % memory read (MR) memRead % memory write (MW) memWrite % cache update (CU) cacheUpdate % cache invalidate (CI) cacheInv % idle idle BEGIN IMPORTING shared[U] % memHist MEM_HIST_TYPE: TYPE = [TIME -> [# mem : MEM_TYPE, id : PROC_ID, pc : PC_RANGE #]] CACHE_TYPE : TYPE = [ADDRESS -> [# v : VALUE, oc : boolean #]] HIST_RECORD_TYPE : TYPE = [# op : OP_TYPE, pc : PC_RANGE, t : TIME, r : nat, v : VALUE, a : ADDRESS, id : PROC_ID #] HISTORY_TYPE : TYPE = [# size : nat, lst : [posnat -> HIST_RECORD_TYPE] #] QUEUE_ENTRY_TYPE : TYPE = [# a : ADDRESS, v : VALUE, t : TIME, id : PROC_ID, pc : PC_RANGE, star : boolean #] QUEUE_TYPE : TYPE = [# head, tail : posnat, QE : [posnat -> QUEUE_ENTRY_TYPE] #] PROC_INFO : TYPE = [# pc : PC_RANGE, inQ, outQ : QUEUE_TYPE, cache : CACHE_TYPE, t : TIME, numRead : nat, readValues : [PC_RANGE -> VALUE] #] actionType : TYPE = {read, write, memRead, cacheInv, memWrite, cacheUpdate, idle} % t is the time, r is the number of reads since the last countable cache update, and % id is the processor id. TIMESTAMP : TYPE = [# t : TIME, r : nat, id : PROC_ID #] procs, procs_p : VAR [PROC_ID -> PROC_INFO] memhist, memhist_p : VAR MEM_HIST_TYPE mem, mem_p : VAR MEM_TYPE hist, hist_p : VAR HISTORY_TYPE time, time_p, t : VAR TIME proc, proc2 : VAR PROC_INFO proc_id, p_id, id : VAR PROC_ID qPoint : VAR posnat action : VAR actionType queue : VAR QUEUE_TYPE qEntry : VAR QUEUE_ENTRY_TYPE a, addr : VAR ADDRESS h, h1, h2, h3 : VAR TIMESTAMP index, index2, rank : VAR posnat hrec, newrec : VAR HIST_RECORD_TYPE; % Extract the timestamp from a history table entry. timestamp(hrec): TIMESTAMP = (# t := t(hrec), r := r(hrec), id := id(hrec) #) % Defines an ordering over timestamps. Lt is the \prec relationship of the article lt(h1, h2: TIMESTAMP) : bool = t(h1) < t(h2) or (t(h1) = t(h2) and (r(h1) < r(h2) or (r(h1) = r(h2) and id(h1) < id(h2)))) % lte(h1, h2: TIMESTAMP) : bool = % h1 = h2 or % t(h1) < t(h2) or % (t(h1) = t(h2) and (r(h1) < r(h2) % or (r(h1) = r(h2) and id(h1) < id(h2)))) % returns the correct position of a record with timestamp h1 in a history table next(hist, h1): posnat = if (exists index : index <= size(hist) and lt(h1, timestamp(lst(hist)(index))) and (forall index2: index2 <= size(hist) and lt(h1, timestamp(lst(hist)(index2))) implies index <= index2)) then (choose (lambda index : index <= size(hist) and lt(h1, timestamp(lst(hist)(index))) and (forall index2: index2 <= size(hist) and lt(h1, timestamp(lst(hist)(index2))) implies index <= index2))) else size(hist) + 1 endif % Places entry hrec in its correct position in the history table, shifting % any succeeding entries up by one insert(hist, hrec): HISTORY_TYPE = (let rank = next(hist, timestamp(hrec)) in (# size := size(hist) + 1, lst := (lambda index: if index < rank then lst(hist)(index) elsif index = rank then hrec else lst(hist)(index-1) endif) #)) % adds an entry to a queue. addQentry(queue, qEntry): QUEUE_TYPE = (# head := head(queue), tail := tail(queue) + 1, QE := QE(queue) with [(tail(queue)) := qEntry] #) % returns true iff entry qPoint of queue is occupied occEntry(queue, qPoint) : bool = qPoint < tail(queue) and qPoint >= head(queue) empty(queue) : bool = head(queue) = tail(queue) % The conditions under which a read can be performed canRead(proc, proc_id) : bool = op(instlist(proc_id, pc(proc))) = READ and oc(cache(proc)(a(instlist(proc_id, pc(proc))))) and head(outQ(proc)) = tail(outQ(proc)) and (forall qPoint: qPoint >= head(inQ(proc)) and qPoint < tail(inQ(proc)) implies not star(QE(inQ(proc))(qPoint))) % the conditios under which a write can be performed canWrite(proc, proc_id): bool = op(instlist(proc_id, pc(proc))) = WRITE % The initial state theta(hist, mem, memhist, procs, time): bool = time = 0 and size(hist) = 0 and mem(memhist(time)) = initmem and mem = initmem and (forall proc_id : (let proc = procs(proc_id) in head(inQ(proc)) = 1 and tail(inQ(proc)) = 1 and head(outQ(proc)) = 1 and tail(outQ(proc)) = 1 and pc(proc) = 1 and numRead(proc) = 0 and t(proc) = time and readValues(proc) =(lambda (pc : PC_RANGE) : 0) and (forall addr : oc(cache(proc)(addr)) implies v(cache(proc)(addr)) = mem(addr)))) % The lazy caching transition. rho(hist, mem, memhist, procs, time, hist_p, mem_p, memhist_p, procs_p, p_id, time_p, action, addr): bool = (let proc = procs(p_id), pc = pc(procs(p_id)), a = a(instlist(p_id, pc(procs(p_id)))), v = v(instlist(p_id, pc(procs(p_id)))) in CASES (action) of read : canRead(procs(p_id), p_id) and procs_p = procs with [ (p_id) := procs(p_id) with [pc := pc + 1, numRead := numRead(proc) + 1, readValues := readValues(proc) with [(pc) := v(cache(proc)(a))]]] and (let newrec = (# t:= t(proc), r:= numRead(proc) + 1, id := p_id, op := READ, pc := pc, v := v(cache(proc)(a)), a := a #) in hist_p = insert(hist, newrec)) and memhist_p = memhist and time_p = time and mem_p = mem, write : canWrite(procs(p_id), p_id) and procs_p = procs with [(p_id) := proc with [pc := pc + 1, outQ := addQentry(outQ(proc), (# a := a, v := v, t := 0, id := p_id, pc := pc, star := true #))]] and memhist_p = memhist and time_p = time and hist_p = hist and mem_p = mem, memRead : not oc(cache(proc)(addr)) and procs_p = procs with [(p_id) := proc with [inQ := addQentry(inQ(proc), (# a := addr, v := mem(addr), t := time, id := p_id, pc := pc, star := false #))]] and memhist_p = memhist and mem_p = mem and hist_p = hist and time_p = time, cacheInv : oc(cache(proc)(addr)) and procs_p = procs with [(p_id) := proc with [ cache := (lambda a: if a = addr then (# oc := false, v := v(cache(proc)(addr)) #) else cache(proc)(a) endif ) ]] and memhist_p = memhist and hist_p = hist and mem_p = mem and time_p = time, memWrite : head(outQ(proc)) /= tail(outQ(proc)) and (let qEntry = QE(outQ(proc))(head(outQ(proc))) with [ t := time + 1, id := p_id ] in procs_p = (lambda proc_id: procs(proc_id) with [outQ := if proc_id = p_id then outQ(procs(proc_id)) with [head := head(outQ(procs(proc_id))) + 1] else outQ(procs(proc_id)) endif, inQ := addQentry(inQ(procs(proc_id)), (qEntry with [(star) := proc_id = p_id])) ]) and memhist_p = memhist with [(time + 1) := (# pc := pc(qEntry), id := p_id, mem := mem with [(a(qEntry)) := v(qEntry)] #)] and mem_p = mem with [(a(qEntry)) := v(qEntry)] and (let newrec = (# t:= time + 1, r:= 0, id := p_id, op := WRITE, pc := pc(qEntry), v := v(qEntry), a := a(qEntry) #) in hist_p = (# size := size(hist) + 1, lst := lst(hist) with [(size(hist) + 1) := newrec] #))) and time_p = time + 1, cacheUpdate : head(inQ(proc)) /= tail(inQ(proc)) and (let qEntry = QE(inQ(proc))(head(inQ(proc))) in procs_p = procs with [(p_id) := (# inQ := inQ(proc) with [head := head(inQ(proc)) + 1], outQ := outQ(proc), t := if id(qEntry) = p_id and not star(qEntry) then t(proc) else t(proc) + 1 endif, numRead := if id(qEntry) = p_id and not star(qEntry) then numRead(proc) else 0 endif, readValues := readValues(proc), pc := pc(proc), cache := (lambda a: if a = a(qEntry) then (# oc := true, v := v(qEntry) #) else cache(proc)(a) endif ) #) ]) and hist_p = hist and memhist_p = memhist and time_p = time and mem_p = mem, idle : procs_p = procs and hist_p = hist and memhist_p = memhist and time_p = time and mem_p = mem endcases ) END lazy $$$lazy.prf (|lazy| (|next_TCC1| "" (SKOSIMP*) (("" (EXPAND "nonempty?") (("" (EXPAND "empty?") (("" (INST? -4) (("" (EXPAND "member") (("" (SIMP) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|insert_TCC1| "" (SUBTYPE-TCC) NIL NIL) (|rho_TCC1| "" (SUBTYPE-TCC) NIL NIL) (|rho_TCC2| "" (SUBTYPE-TCC) NIL NIL)) $$$props.pvs props[U : posnat]: THEORY % A list of properties which are proved invariant in propsPrf.pvs BEGIN IMPORTING lazy[U] procs, procs_p : VAR [PROC_ID -> PROC_INFO] memhist, memhist_p : VAR MEM_HIST_TYPE mem, mem_p : VAR MEM_TYPE hist, hist_p : VAR HISTORY_TYPE time, time_p, t, t1, te, ts : VAR TIME proc, proc2 : VAR PROC_INFO proc_id, p_id, id, id2, id3, ids, ide : VAR PROC_ID qPoint, qPoint2, point : VAR posnat action : VAR actionType queue : VAR QUEUE_TYPE qEntry : VAR QUEUE_ENTRY_TYPE a, addr : VAR ADDRESS pc, pc2 : VAR PC_RANGE hEntry : VAR HIST_RECORD_TYPE h, h1, h2, hs, he : VAR TIMESTAMP r, r2 : VAR nat index, index2, next : VAR posnat timestamp(t,r,id): TIMESTAMP = (# t:= t, r:= r, id := id #) % rank(hist, h1): nat = % if (exists index : % index <= size(hist) and % timestamp(lst(hist)(index)) = h1) % then (choose (lambda index : % index <= size(hist) and % timestamp(lst(hist)(index)) = h1)) % else 0 % endif % rankLtSize : lemma % rank(hist, h) <= size(hist) oc(hist, h1) : bool = (exists index : index <= size(hist) and timestamp(lst(hist)(index)) = h1) cacheLoad(qEntry, p_id) : bool = id(qEntry) = p_id and not star(qEntry) emptyQueues(procs, id): bool = head(inQ(procs(id))) = tail(inQ(procs(id))) and head(outQ(procs(id))) = tail(outQ(procs(id))) memhistCorrect(hist, mem, memhist, time) : bool = mem(memhist(time)) = mem and (forall t: t < time implies mem(memhist(t+1)) = mem(memhist(t)) with [(a(instlist(id(memhist(t+1)), pc(memhist(t+1))))) := v(instlist(id(memhist(t+1)), pc(memhist(t+1))))] and (exists index : index <= size(hist) and timestamp(lst(hist)(index)) = timestamp(t+1, 0, id(memhist(t+1))) and pc(lst(hist)(index)) = pc(memhist(t+1)))) and mem(memhist(0)) = initmem queuesMatchProg(memhist, procs) : bool = (forall p_id: (let proc = procs(p_id) in (forall qPoint : (let qEntry = QE(inQ(proc))(qPoint) in occEntry(inQ(proc), qPoint) and not cacheLoad(qEntry, p_id) implies a(qEntry) = a(instlist(id(qEntry), pc(qEntry))) and v(qEntry) = v(instlist(id(qEntry), pc(qEntry))) and op(instlist(id(qEntry), pc(qEntry))) = WRITE and id(memhist(t(qEntry))) = id(qEntry) and % +1 removed pc(memhist(t(qEntry))) = pc(qEntry))) and % + 1 removed (forall qPoint : occEntry(outQ(proc), qPoint) implies (let qEntry = QE(outQ(proc))(qPoint) in a(qEntry) = a(instlist(id(qEntry), pc(qEntry))) and v(qEntry) = v(instlist(id(qEntry), pc(qEntry))) and op(instlist(id(qEntry), pc(qEntry))) = WRITE and id(qEntry) = p_id)))) cacheEqualMemhist(memhist, procs) : bool = (forall p_id: (let proc = procs(p_id) in (forall a : oc(cache(proc)(a)) implies v(cache(proc)(a)) = mem(memhist(t(proc)))(a)) )) queuesNonNeg(procs) : bool = (forall p_id: head(outQ(procs(p_id))) <= tail(outQ(procs(p_id))) and head(inQ(procs(p_id))) <= tail(inQ(procs(p_id))) ) inQmatchHist(hist, memhist, procs, time) : bool = (forall p_id: (let queue = inQ(procs(p_id)) in (forall qPoint : occEntry(queue, qPoint) implies t(QE(queue)(qPoint)) <= time and t(QE(queue)(qPoint)) >= t(procs(p_id)) and (t(QE(queue)(qPoint)) = t(procs(p_id)) implies cacheLoad(QE(queue)(qPoint), p_id)) and (not cacheLoad(QE(queue)(qPoint), p_id) implies (exists index : index <= size(hist) and timestamp(lst(hist)(index)) = timestamp(t(QE(queue)(qPoint)), 0, id(QE(queue)(qPoint))) and (let hEntry = lst(hist)(index) in v(hEntry) = v(QE(queue)(qPoint)) and a(hEntry) = a(QE(queue)(qPoint)))) and id(QE(queue)(qPoint)) = id(memhist(t(QE(queue)(qPoint)))) and pc(QE(queue)(qPoint)) = pc(memhist(t(QE(queue)(qPoint))))) and v(QE(queue)(qPoint)) = mem(memhist(t(QE(queue)(qPoint))))(a(QE(queue)(qPoint)))))) and (forall p_id: (let queue = inQ(procs(p_id)) in (forall t : t >= 1 and t <= time and t > t(procs(p_id)) implies (exists qPoint : occEntry(queue, qPoint) and t(QE(queue)(qPoint)) = t and not cacheLoad(QE(queue)(qPoint), p_id))))) QtimeInc(procs) : bool = (forall p_id: (let queue = inQ(procs(p_id)) in (forall qPoint, qPoint2: occEntry(queue, qPoint) and occEntry(queue, qPoint2) and qPoint2 > qPoint implies t(QE(queue)(qPoint2)) >= t(QE(queue)(qPoint)) and (t(QE(queue)(qPoint2)) = t(QE(queue)(qPoint)) iff (forall point: point > qPoint and point <= qPoint2 implies cacheLoad(QE(queue)(point), p_id)))))) localTimeEarlier(procs, time):bool = (forall p_id: (let proc = procs(p_id) in time >= t(proc) and (time = t(proc) iff (forall qPoint2: occEntry(inQ(proc), qPoint2) implies cacheLoad(QE(inQ(proc))(qPoint2), p_id))))) outQpcInc(procs) : bool = (forall p_id: (let queue = outQ(procs(p_id)), proc = procs(p_id) in (forall qPoint: occEntry(queue, qPoint) implies pc(QE(queue)(qPoint)) < pc(proc) and (forall qPoint2: occEntry(queue, qPoint2) implies (qPoint < qPoint2 iff pc(QE(queue)(qPoint)) < pc(QE(queue)(qPoint2)))) and (forall pc: pc > pc(QE(queue)(qPoint)) and pc < pc(proc) implies (exists qPoint2: occEntry(queue, qPoint2) and pc(QE(queue)(qPoint2)) = pc))))) histLt(hist) : bool = forall index, index2 : index < index2 and index2 <= size(hist) implies timestamp(lst(hist)(index)) /= timestamp(lst(hist)(index2)) and lt(timestamp(lst(hist)(index)), timestamp(lst(hist)(index2))) histComplete(hist, procs): bool = (forall index: index <= size(hist) implies (let h = timestamp(lst(hist)(index)) in if r(h) = 0 then forall index2: index2 <= size(hist) and r(lst(hist)(index2)) = 0 and t(lst(hist)(index2)) = t(h) implies index2 = index else (forall r2 : r2 < r(h) and r2 > 0 implies oc(hist, h with [r := r2])) endif)) and (forall id : (forall r2 : r2 < numRead(procs(id)) implies oc(hist, timestamp(t(procs(id)), r2 + 1, id))) and (t(procs(id)) > 0 and numRead(procs(id)) > 0 implies (exists id2 : oc(hist, timestamp(t(procs(id)), 0, id2))))) histMatchPC(hist, procs) : bool = (forall index: index <= size(hist) implies (let hrec = lst(hist)(index) in pc(hrec) < if head(outQ(procs(hrec`id))) < tail(outQ(procs(hrec`id))) then pc(QE(outQ(procs(hrec`id)))(head(outQ(procs(hrec`id))))) else pc(procs(hrec`id)) endif and (forall index2 : (let hrec2 = lst(hist)(index2) in index2 <= size(hist) and hrec2`id = hrec`id implies (pc(hrec2) < pc(hrec) iff index2 < index))) and (forall pc: pc < pc(hrec) implies (exists index2 : (let hrec2 = lst(hist)(index2) in index2 < index and hrec2`id = hrec`id and hrec2`pc = pc ))))) and (forall id, pc: pc < if head(outQ(procs(id))) < tail(outQ(procs(id))) then pc(QE(outQ(procs(id)))(head(outQ(procs(id))))) else pc(procs(id)) endif implies (exists index : index <= size(hist) and pc(lst(hist)(index)) = pc and (lst(hist)(index))`id = id)) histMatchTime(hist, procs, time) : bool = (forall index: index <= size(hist) implies (let hrec = lst(hist)(index) in t(hrec) <= time and if t(hrec) > t(procs(hrec`id)) then r(hrec) = 0 and (exists qPoint : occEntry(inQ(procs(hrec`id)), qPoint) and t(QE(inQ(procs(hrec`id)))(qPoint)) = t(hrec) and pc(QE(inQ(procs(hrec`id)))(qPoint)) = pc(hrec) and id(QE(inQ(procs(hrec`id)))(qPoint)) = hrec`id and star(QE(inQ(procs(hrec`id)))(qPoint))) else t(hrec) = t(procs(hrec`id)) implies r(hrec) <= numRead(procs(hrec`id)) endif)) and (forall t: 1 <= t and t <= time implies (exists index : index <= size(hist) and t(lst(hist)(index)) = t and r(lst(hist)(index)) = 0)) firstExists(hist) : bool = size(hist) > 0 implies (t(lst(hist)(1)) = 0 and r(lst(hist)(1)) = 1 or t(lst(hist)(1)) = 1 and r(lst(hist)(1)) = 0) histJ0write(hist): bool = (forall index: index <= size(hist) implies (op(instlist(lst(hist)(index)`id, pc(lst(hist)(index)))) = WRITE iff r(lst(hist)(index)) = 0)) readValuesCorrect(hist, memhist, procs): bool = (forall id: (let proc = procs(id) in (forall pc: if pc < pc(proc) and op(instlist(id, pc)) = READ then (exists index : index <= size(hist) and pc(lst(hist)(index)) = pc and (lst(hist)(index))`id = id and readValues(proc)(pc) = mem(memhist(t(lst(hist)(index))))(a(instlist(id, pc)))) else readValues(proc)(pc) = 0 endif ))) nextSize : lemma forall hist, h: next(hist, h) = 1 + size(hist) or next(hist, h) <= size(hist) and lt(h, timestamp(lst(hist)(next(hist, h)))) and (forall index2: index2 <= size(hist) and lt(h, timestamp(lst(hist)(index2))) implies next(hist, h) <= index2) reachable(hist, mem, memhist, procs, time) : bool = memhistCorrect(hist, mem, memhist, time) and cacheEqualMemhist(memhist, procs) and queuesNonNeg(procs) and inQmatchHist(hist, memhist, procs, time) and outQpcInc(procs) and localTimeEarlier(procs, time) and QtimeInc(procs) and queuesMatchProg(memhist, procs) and histComplete(hist, procs) and histMatchPC(hist, procs) and histMatchTime(hist, procs, time) and histLt(hist) and histJ0write(hist) and firstExists(hist) and readValuesCorrect(hist, memhist, procs) END props $$$props.prf (|props| (|rank_TCC1| "" (SUBTYPE-TCC) NIL NIL) (|rankLtSize| "" (EXPAND "rank") (("" (SKOSIMP*) (("" (NEW-SPLIT-IF) NIL NIL)) NIL)) NIL) (|nextIsNext| "" (SKOSIMP*) (("" (CASE "not (exists (next : posnat) : next(hist!1, h!1) = next)") (("1" (INST + "next(hist!1, h!1)") NIL NIL) ("2" (SKOSIMP*) (("2" (REPLACE*) (("2" (EXPAND "next") (("2" (NEW-SPLIT-IF -) (("2" (EXPAND "choose") (("2" (USE "epsilon_ax[posnat]") (("2" (SPSI -) (("2" (SKOSIMP*) (("2" (INST - "index2!1") (("2" (SIMP) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|nextSize| "" (SKOSIMP*) (("" (CASE "not (exists (next : posnat) : next(hist!1, h!1) = next)") (("1" (INST + "next(hist!1, h!1)") NIL NIL) ("2" (SKOSIMP*) (("2" (REPLACE*) (("2" (EXPAND "next") (("2" (NEW-SPLIT-IF -) (("2" (EXPAND "choose") (("2" (USE "epsilon_ax[posnat]") (("2" (SPSI -) (("2" (SKOSIMP*) (("2" (INST - "index2!1") (("2" (SIMP) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) $$$propsPrf.pvs propsPrf[U: posnat]: THEORY % Proofs of the invariance of the properties in props.pvs BEGIN IMPORTING props[U] procs, procs_p: VAR [PROC_ID -> PROC_INFO] memhist, memhist_p: VAR MEM_HIST_TYPE mem, mem_p: VAR MEM_TYPE hist, hist_p: VAR HISTORY_TYPE time, time_p, t: VAR TIME proc, proc2: VAR PROC_INFO proc_id, p_id: VAR PROC_ID qPoint, qPoint2: VAR posnat action: VAR actionType queue: VAR QUEUE_TYPE qEntry: VAR QUEUE_ENTRY_TYPE a, addr: VAR ADDRESS pc: VAR PC_RANGE h, h1, h2, h3: VAR TIMESTAMP ltIsStrict : lemma (forall h1, h2: % linear (lt(h1, h2) or lt(h2, h1) or h1 = h2) and % anti-symmetric not (lt(h1, h2) and lt(h2, h1)) and % irreflexive not lt(h1, h1)) and (forall h1, h2, h3: % transitive lt(h1, h2) and lt(h2, h3) implies lt(h1, h3)) nextExists: LEMMA forall h: if (exists (index : posnat): index <= size(hist) and lt(h, timestamp(lst(hist)(index)))) then next(hist, h) <= size(hist) and (forall (index2: posnat): index2 <= size(hist) and lt(h, timestamp(lst(hist)(index2))) implies next(hist, h) <= index2) else next(hist, h) = 1 + size(hist) endif thetaReachable: LEMMA theta(hist, mem, memhist, procs, time) IMPLIES reachable(hist, mem, memhist, procs, time) queuesNonNeg: LEMMA rho(hist, mem, memhist, procs, time, hist_p, mem_p, memhist_p, procs_p, p_id, time_p, action, addr) AND reachable(hist, mem, memhist, procs, time) IMPLIES queuesNonNeg(procs_p) localTimeEarlier: LEMMA rho(hist, mem, memhist, procs, time, hist_p, mem_p, memhist_p, procs_p, p_id, time_p, action, addr) AND reachable(hist, mem, memhist, procs, time) IMPLIES localTimeEarlier(procs_p, time_p) cacheEqualMemhist: LEMMA rho(hist, mem, memhist, procs, time, hist_p, mem_p, memhist_p, procs_p, p_id, time_p, action, addr) AND reachable(hist, mem, memhist, procs, time) IMPLIES cacheEqualMemhist(memhist_p, procs_p) queuesMatchProg: LEMMA rho(hist, mem, memhist, procs, time, hist_p, mem_p, memhist_p, procs_p, p_id, time_p, action, addr) AND reachable(hist, mem, memhist, procs, time) IMPLIES queuesMatchProg(memhist_p, procs_p) QtimeInc: LEMMA rho(hist, mem, memhist, procs, time, hist_p, mem_p, memhist_p, procs_p, p_id, time_p, action, addr) AND reachable(hist, mem, memhist, procs, time) IMPLIES QtimeInc(procs_p) % rankInc : LEMMA % rho(hist, mem, memhist, procs, time, hist_p, mem_p, % memhist_p, procs_p, p_id, time_p, action, addr) % AND reachable(hist, mem, memhist, procs, time) % and rank(hist, h) > 0 and rank(hist, h) <= size(hist) % implies rank(hist_p, h) <= size(hist_p) and % (rank(hist_p, h) = rank(hist, h) or % (rank(hist_p, h) = rank(hist, h) + 1 and action = read and % lte(timestamp(t(procs(p_id)), numRead(procs(p_id)) + 1, p_id), h))) memhistCorrect: LEMMA rho(hist, mem, memhist, procs, time, hist_p, mem_p, memhist_p, procs_p, p_id, time_p, action, addr) AND reachable(hist, mem, memhist, procs, time) IMPLIES memhistCorrect(hist_p, mem_p, memhist_p, time_p) inQmatchHist: LEMMA rho(hist, mem, memhist, procs, time, hist_p, mem_p, memhist_p, procs_p, p_id, time_p, action, addr) AND reachable(hist, mem, memhist, procs, time) IMPLIES inQmatchHist(hist_p, memhist_p, procs_p, time_p) outQpcInc: LEMMA rho(hist, mem, memhist, procs, time, hist_p, mem_p, memhist_p, procs_p, p_id, time_p, action, addr) AND reachable(hist, mem, memhist, procs, time) IMPLIES outQpcInc(procs_p) histComplete: LEMMA rho(hist, mem, memhist, procs, time, hist_p, mem_p, memhist_p, procs_p, p_id, time_p, action, addr) AND reachable(hist, mem, memhist, procs, time) IMPLIES histComplete(hist_p, procs_p) histMatchPC: LEMMA rho(hist, mem, memhist, procs, time, hist_p, mem_p, memhist_p, procs_p, p_id, time_p, action, addr) AND reachable(hist, mem, memhist, procs, time) IMPLIES histMatchPC(hist_p, procs_p) histMatchTime: LEMMA rho(hist, mem, memhist, procs, time, hist_p, mem_p, memhist_p, procs_p, p_id, time_p, action, addr) AND reachable(hist, mem, memhist, procs, time) IMPLIES histMatchTime(hist_p, procs_p, time_p) histJ0write: LEMMA rho(hist, mem, memhist, procs, time, hist_p, mem_p, memhist_p, procs_p, p_id, time_p, action, addr) AND reachable(hist, mem, memhist, procs, time) IMPLIES histJ0write(hist_p) histLt: LEMMA rho(hist, mem, memhist, procs, time, hist_p, mem_p, memhist_p, procs_p, p_id, time_p, action, addr) AND reachable(hist, mem, memhist, procs, time) IMPLIES histLt(hist_p) firstExists: LEMMA rho(hist, mem, memhist, procs, time, hist_p, mem_p, memhist_p, procs_p, p_id, time_p, action, addr) AND reachable(hist, mem, memhist, procs, time) IMPLIES firstExists(hist_p) readValuesCorrect: LEMMA rho(hist, mem, memhist, procs, time, hist_p, mem_p, memhist_p, procs_p, p_id, time_p, action, addr) AND reachable(hist, mem, memhist, procs, time) IMPLIES readValuesCorrect(hist_p, memhist_p, procs_p) reachable: LEMMA rho(hist, mem, memhist, procs, time, hist_p, mem_p, memhist_p, procs_p, p_id, time_p, action, addr) AND reachable(hist, mem, memhist, procs, time) IMPLIES reachable(hist_p, mem_p, memhist_p, procs_p, time_p) END propsPrf $$$propsPrf.prf (|propsPrf| (|ltIsStrict| "" (GRIND) (("" (APPLY-EXTENSIONALITY 7 :HIDE? T) NIL NIL)) NIL) (|nextExists| "" (SKOSIMP*) (("" (NEW-SPLIT-IF) (("1" (EXPAND "next") (("1" (NEW-SPLIT-IF) (("1" (CLEAN-UP) (("1" (CASE "exists (myset : setof[posnat]): myset = {(index : posnat)| index <= size(hist!1) AND lt(h!1, timestamp(lst(hist!1)(index))) }") (("1" (SKOSIMP*) (("1" (CASE "exists (small : posnat) : member(small, myset!1) and forall (ind : posnat) : member (ind, myset!1) implies small <= ind") (("1" (SKOSIMP*) (("1" (INST + "small!1") (("1" (SIMP) (("1" (EXPAND "member") (("1" (REPLACE*) (("1" (SIMP) (("1" (SIMP) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (HIDE 2) (("2" (CASE "not member(index!1, myset!1)") (("1" (EXPAND "member") (("1" (REPLACE*) (("1" (SIMP) NIL NIL)) NIL)) NIL) ("2" (CASE "forall (upper : posnat): (forall (ind : posnat): member(ind, myset!1) and ind <= upper implies EXISTS (small: posnat): member(small, myset!1) AND (FORALL (ind: posnat): member(ind, myset!1) IMPLIES small <= ind))") (("1" (INST - "index!1") (("1" (INST - "index!1") (("1" (SIMP) NIL NIL)) NIL)) NIL) ("2" (INDUCT "upper") (("1" (SIMP) NIL NIL) ("2" (SIMP) NIL NIL) ("3" (SKOSIMP*) (("3" (SIMP) (("3" (CASE "j!1 = 0") (("1" (INST + 1) (("1" (SIMP) NIL NIL)) NIL) ("2" (SIMP) (("2" (INST + "ind!1") (("2" (SIMP) (("2" (SKOSIMP*) (("2" (INST -1 "ind!2") (("2" (SIMP) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (INST + "({index: posnat | index <= size(hist!1) AND lt(h!1, timestamp(lst(hist!1)(index)))})") NIL NIL)) NIL)) NIL)) NIL)) NIL) ("2" (EXPAND "next") (("2" (NEW-SPLIT-IF) (("2" (SKOSIMP*) (("2" (INST? +) (("2" (SIMP) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|thetaReachable| "" (EXPAND "theta") (("" (EXPAND "reachable") (("" (SKOSIMP*) (("" (APPLY (THEN (SPLIT +) (LAZYGRIND))) NIL NIL)) NIL)) NIL)) NIL) (|queuesNonNeg| "" (EXP-RHO) (("" (REVEAL "queuesNonNeg") (("" (INST? "queuesNonNeg" :WHERE +) (("" (SPLIT-RHO-ALL) NIL NIL)) NIL)) NIL)) NIL) (|localTimeEarlier| "" (EXP-RHO :HIDE? T) (("" (REVEAL "localTimeEarlier" "queuesNonNeg" "inQmatchHistP") (("" (INST? "localTimeEarlier" :WHERE + :IF-MATCH BEST) (("" (INST? "queuesNonNeg" :WHERE + :IF-MATCH BEST) (("" (SPSI) (("1" (SPLIT-RHO-ALL) (("1" (INST? "localTimeEarlier") (("1" (SIMP) NIL NIL)) NIL)) NIL) ("2" (SKOSIMP*) (("2" (CASE "time!1 = t(procs!1(p_id!2))") (("1" (SIMP) (("1" (INSTBEST "localTimeEarlier") (("1" (SPLIT-RHO-ALL) NIL NIL)) NIL)) NIL) ("2" (SIMP) (("2" (CLEAN-UP) (("2" (SKOSIMP*) (("2" (LABEL "time" 1) (("2" (SPLIT-RHO-ALL) (("2" (INST "inQmatchHistP" "p_id!2" "qPoint2!1") (("2" (REPLACE*) (("2" (SIMP) (("2" (REVEAL "QtimeInc") (("2" (INST -1 "p_id!2" "head(inQ(procs!1(p_id!2)))" "qPoint2!1") (("2" (SIMP) (("2" (REVEAL "inQmatchHistP") (("2" (INST? - :WHERE 1) (("2" (REPLACE*) (("2" (SIMP) (("2" (SPSI "QtimeInc") (("2" (INST -1 "qPoint2!1") (("2" (SIMP) (("2" (SIMP) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("3" (CASE "time!1 = t(procs!1(p_id!2))") (("1" (SIMP) (("1" (SPLIT-RHO-ALL) (("1" (INST "toProve" "tail(inQ(procs!1(p_id!2)))") (("1" (SIMP) (("1" (SIMP) NIL NIL)) NIL)) NIL) ("2" (INST? "inQmatchHistP") (("2" (INST "localTimeEarlier" "head(inQ(procs!1(p_id!2)))") (("2" (SIMP) NIL NIL)) NIL)) NIL)) NIL)) NIL) ("2" (SIMP) (("2" (CLEAN-UP) (("2" (SKOSIMP*) (("2" (INST-CP -1 "qPoint2!1") (("2" (SPLIT-RHO-ALL) (("2" (REVEAL "inQmatchHistT") (("2" (INST -1 "p_id!2" "2 + t(procs!1(p_id!2))") (("2" (SIMP) (("2" (SKOSIMP*) (("2" (INST "toProve" "qPoint!1") (("2" (SIMP) (("2" (REPLACE*) (("2" (SIMP) (("2" (REVEAL "inQmatchHistT") (("2" (INST -1 "t(procs!1(p_id!2)) + 1") (("2" (SIMP) (("2" (SKOSIMP*) (("2" (REVEAL "QtimeInc") (("2" (INST -1 "p_id!1" "qPoint!1" "qPoint!2") (("2" (SIMP) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|cacheEqualMemhist| "" (EXP-RHO :HIDE? T) (("" (REVEAL "cacheEqualMemhist" "localTimeEarlier") (("" (INST? "cacheEqualMemhist" :WHERE +) (("" (INST "cacheEqualMemhist" "a!1") (("" (INST "localTimeEarlier" "p_id!2") (("" (SPLIT-RHO) (("1" (REPLACE*) (("1" (SIMP) (("1" (SPLIT-ALL) NIL NIL)) NIL)) NIL) ("2" (REPLACE*) (("2" (SIMP) (("2" (SPLIT-ALL) NIL NIL)) NIL)) NIL) ("3" (REPLACE*) (("3" (SIMP) (("3" (SPLIT-ALL) NIL NIL)) NIL)) NIL) ("4" (REPLACE*) (("4" (SIMP) (("4" (SPLIT-ALL) NIL NIL)) NIL)) NIL) ("5" (REPLACE*) (("5" (SIMP) NIL NIL)) NIL) ("6" (REVEAL "queuesMatchProg") (("6" (INST? "queuesMatchProg" :WHERE "toProve") (("6" (SIMP) (("6" (INST "queuesMatchProg" "head(inQ(procs!1(p_id!2)))") (("6" (SIMP) (("6" (REPLACE*) (("6" (NEW-SPLIT-IF) (("6" (REVEAL "queuesNonNeg") (("6" (INST?) (("6" (SIMP) (("6" (REVEAL "inQmatchHistP") (("6" (INST? :WHERE +) (("6" (REVEAL "inQmatchHistT") (("6" (INST -1 "p_id!2" "t(procs!1(p_id!2)) + 1") (("6" (REVEAL "QtimeInc") (("6" (CASE "not t(QE(inQ(procs!1(p_id!2)))(head(inQ(procs!1(p_id!2))))) = t(procs!1(p_id!2))") (("1" (SIMP) (("1" (CASE "time!1 = t(procs!1(p_id!2))") (("1" (SIMP) NIL NIL) ("2" (SIMP) (("2" (SKOSIMP*) (("2" (INST -1 "p_id!2" "head(inQ(procs!1(p_id!2)))" "qPoint!1") (("2" (SIMP) (("2" (CASE "qPoint!1 > head(inQ(procs!1(p_id!2))) ") (("1" (SIMP) (("1" (SIMP) (("1" (INST "QtimeInc" "qPoint!1") (("1" (SIMP) NIL NIL)) NIL)) NIL)) NIL) ("2" (SIMP) (("2" (SPSI "toProve") (("2" (CLEAN-UP) (("2" (REVEAL "memhistCorrect") (("2" (INST? :WHERE "toProve") (("2" (NEW-SPLIT-IF) (("2" (NEW-SPLIT-IF) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (SIMP) (("2" (SIMP) (("2" (CLEAN-UP) (("2" (NEW-SPLIT-IF) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|queuesMatchProg| "" (EXP-RHO) (("" (REVEAL "queuesMatchProg" "inQmatchHistP") (("" (INST? "queuesMatchProg" :WHERE +) (("" (APPLY (THEN (SPLIT +) (SKOSIMP*))) (("1" (INST? "queuesMatchProg") (("1" (SPLIT-RHO) (("1" (REPLACE*) (("1" (SIMP) (("1" (SPLIT-ALL) NIL NIL)) NIL)) NIL) ("2" (REPLACE*) (("2" (SIMP) (("2" (SPLIT-ALL) NIL NIL)) NIL)) NIL) ("3" (REPLACE*) (("3" (SIMP) (("3" (SPLIT-ALL) NIL NIL)) NIL)) NIL) ("4" (REPLACE*) (("4" (SIMP) (("4" (SPLIT-ALL) NIL NIL)) NIL)) NIL) ("5" (REPLACE*) (("5" (SIMP) (("5" (NEW-SPLIT-IF) (("1" (REVEAL "queuesMatchProg") (("1" (INST -2 "p_id!1") (("1" (FLATTEN) (("1" (INST -3 "head(outQ(procs!1(p_id!1)))") (("1" (REVEAL "queuesNonNeg") (("1" (INST "queuesNonNeg" "p_id!1") (("1" (SIMP) (("1" (SIMP) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (SIMP) (("2" (NEW-SPLIT-IF) (("2" (INST? "inQmatchHistP") (("2" (SIMP) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("6" (REPLACE*) (("6" (SIMP) (("6" (SPLIT-ALL) NIL NIL)) NIL)) NIL) ("7" (REPLACE*) (("7" (SIMP) NIL NIL)) NIL)) NIL)) NIL) ("2" (INST? "queuesMatchProg") (("2" (INST? "queuesMatchProg") (("2" (SPLIT-RHO-ALL) (("2" (EXPAND "canWrite") (("2" (PROPAX) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|QtimeInc| "" (EXP-RHO :HIDE? T) (("" (REVEAL "QtimeInc") (("" (INST? "QtimeInc" :WHERE "toProve") (("" (INST "QtimeInc" "qPoint!1" "qPoint2!1") (("" (SPSI) (("1" (SPLIT-RHO-ALL) (("1" (REVEAL "inQmatchHistP") (("1" (INST? "inQmatchHistP") (("1" (SIMP) NIL NIL)) NIL)) NIL) ("2" (REVEAL "inQmatchHistP") (("2" (INST? "inQmatchHistP") (("2" (SIMP) NIL NIL)) NIL)) NIL)) NIL) ("2" (SKOSIMP*) (("2" (CASE "(qPoint!1 < tail(inQ(procs!1(p_id!2))) AND qPoint!1 >= head(inQ(procs!1(p_id!2)))) AND qPoint2!1 < tail(inQ(procs!1(p_id!2))) AND qPoint2!1 >= head(inQ(procs!1(p_id!2)))") (("1" (SIMP) (("1" (CASE " t(QE(inQ(procs!1(p_id!2)))(qPoint2!1)) = t(QE(inQ(procs!1(p_id!2)))(qPoint!1))") (("1" (SIMP) (("1" (INST "QtimeInc" "point!1") (("1" (SPLIT-RHO-ALL) NIL NIL)) NIL)) NIL) ("2" (SPLIT-RHO-ALL) NIL NIL)) NIL)) NIL) ("2" (SIMP) (("2" (REPLACE*) (("2" (CLEAN-UP) (("2" (SPLIT-RHO-ALL) (("1" (REVEAL "inQmatchHistP") (("1" (INST? "inQmatchHistP") (("1" (SIMP) (("1" (REPLACE*) (("1" (SIMP) (("1" (REVEAL "QtimeInc") (("1" (CLEAN-UP) (("1" (INST -1 "qPoint!1" "point!1") (("1" (SIMP) (("1" (INST?) (("1" (SIMP) (("1" (INST?) (("1" (SIMP) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (REVEAL "inQmatchHistP") (("2" (INST? "inQmatchHistP") (("2" (SIMP) NIL NIL)) NIL)) NIL) ("3" (REVEAL "inQmatchHistP") (("3" (INST? "inQmatchHistP") (("3" (SIMP) (("3" (SPSI -) (("3" (REVEAL "QtimeInc") (("3" (CLEAN-UP) (("3" (INST -1 "qPoint!1" "point!1") (("3" (SIMP) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("3" (CASE "(qPoint!1 < tail(inQ(procs!1(p_id!2))) AND qPoint!1 >= head(inQ(procs!1(p_id!2)))) AND qPoint2!1 < tail(inQ(procs!1(p_id!2))) AND qPoint2!1 >= head(inQ(procs!1(p_id!2)))") (("1" (SIMP) (("1" (CASE "t(QE(inQ(procs!1(p_id!2)))(qPoint2!1)) = t(QE(inQ(procs!1(p_id!2)))(qPoint!1))") (("1" (SIMP) (("1" (SPLIT-RHO-ALL) NIL NIL)) NIL) ("2" (REPLACE*) (("2" (SIMP) (("2" (SKOSIMP*) (("2" (INST? :WHERE "QtimeInc") (("2" (SIMP) (("2" (SPLIT-RHO-ALL) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (REPLACE*) (("2" (CLEAN-UP) (("2" (SPLIT-RHO-ALL) (("1" (REVEAL "inQmatchHistT") (("1" (INST? "inQmatchHistT") (("1" (INST "inQmatchHistT" "time!1") (("1" (SIMP) (("1" (REVEAL "localTimeEarlier") (("1" (INST? "localTimeEarlier") (("1" (SIMP) (("1" (REVEAL "inQmatchHistP") (("1" (INST? "inQmatchHistP") (("1" (SIMP) (("1" (CASE "time!1 = 0") (("1" (SIMP) NIL NIL) ("2" (SIMP) (("2" (REVEAL "inQmatchHistT") (("2" (INST -1 "t(QE(inQ(procs!1(p_id!2)))(qPoint!1)) + 1") (("2" (SIMP) (("2" (SKOSIMP*) (("2" (INST "toProve" "qPoint!2") (("2" (SIMP) (("2" (REPLACE*) (("2" (SIMP) (("2" (REVEAL "QtimeInc") (("2" (CLEAN-UP) (("2" (INST -1 "qPoint!2" "qPoint!1") (("2" (SIMP) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (INST "toProve" "qPoint2!1") (("2" (SIMP) (("2" (SIMP) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|memhistCorrect| "" (EXP-RHO :HIDE? T) (("" (REVEAL "memhistCorrect") (("" (SPSI) (("1" (SPLIT-RHO-ALL) NIL NIL) ("2" (SKOSIMP*) (("2" (INST "memhistCorrect" "t!1") (("2" (SPLIT-RHO) (("1" (LABEL "hist" -4) (("1" (HIDE "hist") (("1" (REPLACE*) (("1" (HIDE "rho") (("1" (SPSI) (("1" (SKOSIMP*) (("1" (INST-CP 1 "index!1") (("1" (INST 1 "index!1 + 1") (("1" (REVEAL "hist") (("1" (REPLACE*) (("1" (HIDE "hist") (("1" (SIMP) (("1" (NEW-SPLIT-IF) (("1" (NEW-SPLIT-IF) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (REPLACE*) (("2" (SIMP) NIL NIL)) NIL) ("3" (REPLACE*) (("3" (SIMP) NIL NIL)) NIL) ("4" (REPLACE*) (("4" (SIMP) NIL NIL)) NIL) ("5" (LABEL "hist" -5) (("5" (HIDE "hist") (("5" (REPLACE*) (("5" (SIMP) (("5" (HIDE "rho") (("5" (SPSI) (("1" (NEW-SPLIT-IF) (("1" (CLEAN-UP) (("1" (REVEAL "queuesMatchProg") (("1" (INST?) (("1" (SIMP) (("1" (INSTBEST) (("1" (INST?) (("1" (REVEAL "queuesNonNeg") (("1" (INST?) (("1" (SIMP) (("1" (REPLACE*) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (CASE "t!1 = time!1") (("1" (SIMP) (("1" (CLEAN-UP) (("1" (INST + "size(hist!1) + 1") (("1" (REVEAL "hist") (("1" (REPLACE*) (("1" (SIMP) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (SIMP) (("2" (SKOSIMP*) (("2" (INST + "index!1") (("2" (REVEAL "hist") (("2" (REPLACE*) (("2" (SIMP) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("6" (REPLACE*) (("6" (SIMP) NIL NIL)) NIL) ("7" (REPLACE*) (("7" (SIMP) NIL NIL)) NIL)) NIL)) NIL)) NIL) ("3" (SPLIT-RHO-ALL) NIL NIL)) NIL)) NIL)) NIL) (|inQmatchHist| "" (EXP-RHO :HIDE? T) (("" (APPLY (THEN (SPSI) (SKOSIMP*))) (("1" (REVEAL "inQmatchHistP") (("1" (INST "inQmatchHistP" "p_id!2" "qPoint!1") (("1" (SPLIT-RHO) (("1" (LABEL "hist" -4) (("1" (HIDE "hist") (("1" (REPLACE*) (("1" (SIMP) (("1" (NEW-SPLIT-IF) (("1" (HIDE "rho") (("1" (REPLACE*) (("1" (SIMP) (("1" (SKOSIMP*) (("1" (SIMP) (("1" (INST-CP + "index!1") (("1" (INST + "index!1 + 1") (("1" (REVEAL "hist") (("1" (REPLACE*) (("1" (SIMP) (("1" (HIDE "hist") (("1" (SPLIT-ALL) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (REPLACE*) (("2" (SIMP) (("2" (SIMP) (("2" (SKOSIMP*) (("2" (REVEAL "hist") (("2" (INST-CP + "index!1") (("2" (INST + "index!1 + 1") (("2" (SPLIT-RHO-ALL) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (REPLACE*) (("2" (SIMP) (("2" (SPLIT-ALL) NIL NIL)) NIL)) NIL) ("3" (REPLACE*) (("3" (SIMP) (("3" (SPLIT-ALL) (("3" (REVEAL "localTimeEarlier") (("3" (INST? "localTimeEarlier") (("3" (SIMP) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("4" (REPLACE*) (("4" (SIMP) (("4" (SPLIT-ALL) NIL NIL)) NIL)) NIL) ("5" (REPLACE*) (("5" (SIMP) (("5" (SPLIT-ALL) (("1" (CLEAN-UP) (("1" (REVEAL "localTimeEarlier") (("1" (INST? "localTimeEarlier") (("1" (SIMP) (("1" (INST + "1 + size(hist!1)") (("1" (SIMP) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (INST + "index!1") (("2" (SIMP) NIL NIL)) NIL)) NIL)) NIL)) NIL) ("6" (REPLACE*) (("6" (SIMP) (("6" (SPLIT-ALL) (("6" (REVEAL "inQmatchHistP") (("6" (INST? :WHERE "toProve") (("6" (HIDE "rho") (("6" (REPLACE*) (("6" (SIMP) (("6" (REVEAL "QtimeInc") (("6" (INST "QtimeInc" "p_id!2" "head(inQ(procs!1(p_id!2)))" "qPoint!1") (("6" (SIMP) (("6" (SPSI "QtimeInc") (("6" (INST -1 "qPoint!1") (("6" (SIMP) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("7" (REPLACE*) (("7" (SIMP) NIL NIL)) NIL)) NIL)) NIL)) NIL) ("2" (SPLIT-ALL) (("2" (REVEAL "inQmatchHistT") (("2" (SIMP) (("2" (INST "inQmatchHistT" "p_id!2" "t!1") (("2" (SIMP) (("2" (CASE "t!1 <= time!1 AND t!1 > t(procs!1(p_id!2)) ") (("1" (SIMP) (("1" (SKOSIMP*) (("1" (INST "toProve" "qPoint!1") (("1" (SPLIT-RHO-ALL) (("1" (HIDE "rho") (("1" (REVEAL "inQmatchHistT") (("1" (INST -1 "1 + t(procs!1(p_id!2))") (("1" (SIMP) (("1" (SKOSIMP*) (("1" (REVEAL "QtimeInc") (("1" (INST "QtimeInc" "p_id!2" "qPoint!1" "qPoint!2") (("1" (SIMP) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (SPLIT-RHO-ALL) (("1" (INST "toProve" "tail(inQ(procs!1(p_id!2)))") (("1" (REVEAL "queuesNonNeg") (("1" (INST? "queuesNonNeg" :WHERE "toProve") (("1" (SIMP) (("1" (SIMP) NIL NIL)) NIL)) NIL)) NIL)) NIL) ("2" (CLEAN-UP) (("2" (HIDE "rho") (("2" (INST + "tail(inQ(procs!1(p_id!2)))") (("2" (SIMP) (("2" (REVEAL "queuesNonNeg") (("2" (INST?) (("2" (SIMP) (("2" (SIMP) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|outQpcInc| "" (EXP-RHO :HIDE? T) (("" (REVEAL "outQpcInc") (("" (INST? "outQpcInc" :WHERE +) (("" (INST "outQpcInc" "qPoint!1") (("" (CASE "not (pc(QE(outQ(procs_p!1(p_id!2)))(qPoint!1)) < pc(procs_p!1(p_id!2)))") (("1" (HIDE 2) (("1" (SPLIT-RHO-ALL) NIL NIL)) NIL) ("2" (CASE " qPoint!1 < tail(outQ(procs!1(p_id!2))) AND qPoint!1 >= head(outQ(procs!1(p_id!2)))") (("1" (SPSI) (("1" (SKOSIMP*) (("1" (INST? "outQpcInc" :WHERE +) (("1" (APPLY (THEN (SPLIT-RHO) (REPLACE*) (HIDE "rho") (SIMP) (NEW-SPLIT-IF) (SPSI))) (("1" (NEW-SPLIT-IF) NIL NIL)) NIL)) NIL)) NIL) ("2" (SKOSIMP*) (("2" (INST? "outQpcInc") (("2" (INST "outQpcInc" "pc!1") (("2" (CASE "pc!1 > pc(QE(outQ(procs!1(p_id!2)))(qPoint!1)) AND pc!1 < pc(procs!1(p_id!2))") (("1" (SIMP) (("1" (SKOSIMP*) (("1" (INST "toProve" "qPoint2!1") (("1" (SPLIT-RHO-ALL) (("1" (REVEAL "outQpcInc") (("1" (INST -2 "qPoint2!1") (("1" (SIMP) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (REPLACE*) (("2" (SIMP) (("2" (CLEAN-UP) (("2" (SPLIT-RHO-ALL) (("1" (EXPAND "canRead") (("1" (PROPAX) NIL NIL)) NIL) ("2" (INST 1 "tail(outQ(procs!1(p_id!2)))") (("2" (SIMP) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (HIDE "toProve") (("2" (EXPAND "canRead") (("2" (REVEAL "queuesNonNeg") (("2" (INST? "queuesNonNeg" :WHERE +) (("2" (LABEL "toSplit" -2) (("2" (APPLY (THEN (SPLIT-RHO) (REPLACE*) (SIMP) (NEW-SPLIT-IF "toSplit"))) (("2" (REVEAL 1) (("2" (REPLACE*) (("2" (SIMP) (("2" (HIDE "rho") (("2" (REVEAL "outQpcInc") (("2" (CLEAN-UP) (("2" (APPLY (THEN (SPSI) (SKOSIMP*) (SIMP))) (("2" (NEW-SPLIT-IF -) (("2" (INST? "outQpcInc") (("2" (SIMP) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|histComplete| "" (EXP-RHO :HIDE? T) (("" (APPLY (THEN (SPSI) (SKOSIMP*) (SIMP))) (("1" (REVEAL "histCompleteR") (("1" (INST -1 "index!1") (("1" (APPLY (THEN (SPLIT-RHO) (REPLACE*) (SIMP))) (("1" (HIDE "rho") (("1" (INTRONEXT) (("1" (CASE "index!1 = 1 + size(hist!1)") (("1" (SIMP) (("1" (CLEAN-UP) (("1" (NEW-SPLIT-IF) (("1" (NEW-SPLIT-IF) (("1" (SKOSIMP*) (("1" (EXPAND "oc") (("1" (REVEAL "histCompleteNumRead") (("1" (INST - "p_id!1") (("1" (FLATTEN) (("1" (INST - "r2!1 -1") (("1" (EXPAND "oc") (("1" (SIMP) (("1" (SKOSIMP*) (("1" (INST + "index!2") (("1" (SIMP) NIL NIL)) NIL)) NIL)) NIL)) NIL) ("2" (SIMP) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (SPSI) (("1" (SKOSIMP*) (("1" (REVEAL "histCompleteR") (("1" (CLEAN-UP) (("1" (INST?) (("1" (SIMP) (("1" (NEW-SPLIT-IF -) (("1" (INST - "index2!1") (("1" (SIMP) NIL NIL)) NIL) ("2" (NEW-SPLIT-IF -) (("2" (CASE "index2!1 > 1") (("1" (INST - "index2!1 - 1") (("1" (SIMP) NIL NIL)) NIL) ("2" (SIMP) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (SKOSIMP*) (("2" (EXPAND "oc") (("2" (REVEAL "histCompleteR") (("2" (INST - "size(hist!1)") (("2" (CLEAN-UP) (("2" (SIMP) (("2" (INST?) (("2" (SIMP) (("2" (EXPAND "oc") (("2" (SKOSIMP*) (("2" (INST + "index!2") (("2" (NEW-SPLIT-IF) (("2" (REVEAL 1) (("2" (INST + "index!2 + 1") (("2" (SIMP) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (SIMP) (("2" (NEW-SPLIT-IF) (("1" (SPSI) (("1" (SKOSIMP*) (("1" (INST-CP - "index2!1") (("1" (SIMP) (("1" (NEW-SPLIT-IF -) (("1" (NEW-SPLIT-IF -) (("1" (INST "histCompleteR" "index2!1 - 1") (("1" (SIMP) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (SKOSIMP*) (("2" (EXPAND "oc") (("2" (INST - "r2!1") (("2" (SIMP) (("2" (SKOSIMP*) (("2" (INST + "index!2 + 1") (("2" (REVEAL 1) (("2" (INST + "index!2") (("2" (NEW-SPLIT-IF) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (SPSI) (("1" (SKOSIMP*) (("1" (EXPAND "oc") (("1" (REVEAL "histCompleteNumRead") (("1" (INST - "p_id!1") (("1" (FLATTEN) (("1" (INST - "r2!1 - 1") (("1" (EXPAND "oc") (("1" (SIMP) (("1" (SKOSIMP*) (("1" (INST-CP + "index!2") (("1" (INST + "index!2 + 1") (("1" (NEW-SPLIT-IF) (("1" (NEW-SPLIT-IF) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (SIMP) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (SPSI) (("1" (SKOSIMP*) (("1" (REVEAL "histCompleteR") (("1" (INST - "index!1 - 1") (("1" (SIMP) (("1" (NEW-SPLIT-IF -) (("1" (INST - "index2!1") (("1" (SIMP) NIL NIL)) NIL) ("2" (NEW-SPLIT-IF -) (("2" (INST - "index2!1 - 1") (("2" (SIMP) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (SKOSIMP*) (("2" (REVEAL "histCompleteJ") (("2" (INST - "index!1 - 1") (("2" (SIMP) (("2" (EXPAND "oc") (("2" (INST? -) (("2" (SIMP) (("2" (SKOSIMP*) (("2" (INST + "index!2") (("2" (SIMP) (("2" (NEW-SPLIT-IF) (("2" (REVEAL 1) (("2" (INST 1 "index!2 + 1") (("2" (SIMP) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (INST + " next(hist!1, (# t := t(procs!1(p_id!1)), r := 1 + numRead(procs!1(p_id!1)), id := p_id!1 #))") NIL NIL)) NIL)) NIL) ("2" (HIDE "rho") (("2" (CASE "index!1 = 1 + size(hist!1)") (("1" (NEW-SPLIT-IF) (("1" (SKOSIMP*) (("1" (NEW-SPLIT-IF -) (("1" (REVEAL "histMatchTime") (("1" (INST?) (("1" (SIMP) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (SIMP) (("2" (SPSI) (("1" (SKOSIMP*) (("1" (INST? -) (("1" (SIMP) (("1" (NEW-SPLIT-IF -) (("1" (REVEAL "histMatchTime") (("1" (INST?) (("1" (SIMP) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (SKOSIMP*) (("2" (INST? -) (("2" (EXPAND "oc") (("2" (SIMP) (("2" (SKOSIMP*) (("2" (INST + "index!2") (("2" (NEW-SPLIT-IF) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (REVEAL "histCompleteNumRead") (("2" (INST - "id!1") (("2" (SPSI) (("1" (SKOSIMP*) (("1" (INST - "r2!1") (("1" (SPLIT-RHO-ALL) (("1" (HIDE "rho") (("1" (CASE "exists (next: posnat) : next(hist!1, (# t := t(procs!1(id!1)), r := 1 + numRead(procs!1(id!1)), id := id!1 #)) = next") (("1" (SKOSIMP*) (("1" (EXPAND "oc") (("1" (LEMMA "nextSize") (("1" (INST?) (("1" (CASE "r2!1 = numRead(procs!1(id!1))") (("1" (INST + "next!1") (("1" (EXPAND "timestamp") (("1" (REPLACE*) (("1" (NEW-SPLIT-IF -) NIL NIL)) NIL)) NIL)) NIL) ("2" (EXPAND "timestamp") (("2" (SIMP) (("2" (SKOSIMP*) (("2" (INST-CP + "index!1") (("2" (INST + "index!1 + 1") (("2" (SPLIT-ALL) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (INST + "next(hist!1, (# t := t(procs!1(id!1)), r := 1 + numRead(procs!1(id!1)), id := id!1 #))") NIL NIL)) NIL)) NIL) ("2" (EXPAND "oc") (("2" (SKOSIMP*) (("2" (INST-CP + "index!1") (("2" (INST + "index!1 + 1") (("2" (EXPAND "timestamp") (("2" (SPLIT-ALL) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("3" (HIDE "rho") (("3" (EXPAND "oc") (("3" (SKOSIMP*) (("3" (INST-CP + "index!1") (("3" (INST + "index!1 + 1") (("3" (EXPAND "timestamp") (("3" (SPLIT-ALL) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (APPLY (THEN (SPLIT-RHO) (REPLACE*) (SIMP) (NEW-SPLIT-IF))) (("1" (HIDE "rho") (("1" (EXPAND "oc") (("1" (INTRONEXT) (("1" (REVEAL "histMatchTimeE") (("1" (INST - "procs!1(id!1)`t") (("1" (REVEAL "localTimeEarlier") (("1" (INST?) (("1" (SIMP) (("1" (SKOSIMP*) (("1" (INST + "id(lst(hist!1)(index!1))") (("1" (INST-CP + "index!1") (("1" (INST + "index!1 + 1") (("1" (EXPAND "timestamp") (("1" (SPLIT-ALL) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (INST + "next(hist!1, (# t := t(procs!1(id!1)), r := 1 + numRead(procs!1(id!1)), id := id!1 #))") NIL NIL)) NIL)) NIL)) NIL) ("2" (HIDE "rho") (("2" (EXPAND "oc") (("2" (SKOSIMP*) (("2" (INST + "id2!1") (("2" (INST-CP + "index!1") (("2" (INST + "index!1 + 1") (("2" (EXPAND "timestamp") (("2" (SPLIT-RHO-ALL) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("3" (SKOSIMP*) (("3" (INST? +) (("3" (EXPAND "oc") (("3" (SKOSIMP*) (("3" (INST + "index!1") (("3" (SIMP) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("4" (REDUCE-ALL) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|histMatchPC| "" (EXP-RHO) (("" (APPLY (THEN (SPSI) (SKOSIMP*))) (("1" (RERUN ("1" (REVEAL "histCompletePC") (INST? -) (SPSI) (("1" (APPLY (THEN (SPLIT-RHO) (REPLACE*) (SIMP))) (("1" (LABEL "canRead" -2) (EXPAND "canRead") (SIMP) (HIDE "rho") (INTRONEXT) (("1" (CASE " index!1 = 1 + size(hist!1)") (("1" (SIMP) (CLEAN-UP) (NEW-SPLIT-IF) (SPSI) (REVEAL "histCompletePC") (INST - "size(hist!1)") (CLEAN-UP) (NEW-SPLIT-IF) (NEW-SPLIT-IF)) ("2" (SIMP) (NEW-SPLIT-IF) (("1" (SPLIT-ALL)) ("2" (SPSI) (REVEAL "histCompletePC") (INST - "index!1 - 1") (SPLIT-ALL)))))) ("2" (INST + " next(hist!1, (# t := t(procs!1(p_id!1)), r := 1 + numRead(procs!1(p_id!1)), id := p_id!1 #))")))) ("2" (SPLIT-ALL)) ("3" (SPLIT-ALL)) ("4" (SPLIT-ALL)) ("5" (CASE "index!1 = 1 + size(hist!1)") (("1" (SIMP) (CLEAN-UP) (REVEAL "queuesNonNeg") (INST?) (SIMP) (HIDE "rho") (REVEAL "outQpcInc") (INST?) (SIMP) (NEW-SPLIT-IF) (INST?) (SIMP)) ("2" (SIMP) (REVEAL "queuesNonNeg") (INST?) (SIMP) (REVEAL "outQpcInc") (INST?) (NEW-SPLIT-IF) (("1" (NEW-SPLIT-IF) (INST? -) (SIMP)) ("2" (HIDE "rho") (REVEAL "outQpcInc") (INST -2 "lst(hist!1)(index!1)`id" "outQ(procs!1(lst(hist!1)(index!1)`id))`head") (NEW-SPLIT-IF)))))) ("6" (SPLIT-ALL)))) ("2" (SKOSIMP*) (APPLY (THEN (SPLIT-RHO) (REPLACE*) (SIMP))) (("1" (LABEL "canRead" -2) (HIDE "rho") (INTRONEXT) (("1" (CASE "index!1 = 1 + size(hist!1)") (("1" (SIMP) (REPLACE*) (CLEAN-UP) (CASE "next!1 = 1 + size(hist!1)") (("1" (REPLACE*) (SIMP) (NEW-SPLIT-IF) (REVEAL "histMatchPC") (INST - "index2!1") (SIMP) (CLEAN-UP) (NEW-SPLIT-IF -) (REVEAL "queuesNonNeg") (INST?) (EXPAND "canRead") (PROPAX)) ("2" (SIMP) (NEW-SPLIT-IF) (("1" (REVEAL "histCompletePC") (INST - "size(hist!1)") (SIMP) (CLEAN-UP) (INST - "index2!1") (SIMP)) ("2" (NEW-SPLIT-IF) (("1" (REVEAL "histCompletePC") (INST - "size(hist!1)") (CLEAN-UP) (SIMP) (NEW-SPLIT-IF -) (("1" (EXPAND "canRead") (PROPAX)) ("2" (CASE "next!1 = size(hist!1)") (("1" (REPLACE -1) (EXPAND "lt") (EXPAND "timestamp") (REVEAL "histMatchTime") (INST?) (SIMP) (NEW-SPLIT-IF -) (SKOSIMP*) (EXPAND "canRead") (FLATTEN) (INST? "canRead") (SIMP)) ("2" (REVEAL "histLt") (INST - "next!1" "size(hist!1)") (SIMP) (LEMLTSTRICT) (INST "trans" "(# t := t(procs!1(p_id!1)), r := 1 + numRead(procs!1(p_id!1)), id := p_id!1 #)" "timestamp(lst(hist!1)(next!1))" "timestamp(lst(hist!1)(size(hist!1)))") (SIMP) (EXPAND "timestamp") (EXPAND "lt") (REVEAL "histMatchTime") (INST?) (SIMP) (NEW-SPLIT-IF -) (SKOSIMP*) (EXPAND "canRead") (FLATTEN) (INST? "canRead") (SIMP)))))) ("2" (REVEAL "histMatchPC") (INST - "size(hist!1)") (SIMP) (INST? -) (SIMP) (SPSI)))))))) ("2" (SIMP) (INST - "index2!1") (NEW-SPLIT-IF) (("1" (NEW-SPLIT-IF) (EXPAND "canRead") (NEW-SPLIT-IF) (("1" (REVEAL "histMatchPC") (INST -2 "index2!1") (SIMP)) ("2" (REVEAL "histMatchPC") (INST -2 "index!1 - 1") (SIMP) (INST? -) (INST? -) (SIMP)))) ("2" (EXPAND "canRead") (NEW-SPLIT-IF) (("1" (NEW-SPLIT-IF) (REVEAL "histMatchPC") (INST? -) (SIMP)) ("2" (NEW-SPLIT-IF) (("1" (NEW-SPLIT-IF) (APPLY (THEN (CASE "next!1 < index2!1") (SIMP))) (REVEAL "histMatchTime") (SIMP) (INST -1 "index2!1 - 1") (SIMP) (NEW-SPLIT-IF -) (("1" (SKOSIMP*) (INST? "canRead") (SIMP)) ("2" (LEMLTSTRICT) (INST "trans" "timestamp(lst(hist!1)(index2!1 - 1))" "(# t := t(procs!1(p_id!1)), r := 1 + numRead(procs!1(p_id!1)), id := p_id!1 #)" "timestamp(lst(hist!1)(next!1))") (REVEAL "histLt") (INST - "next!1" "index2!1 - 1") (SIMP) (INST? "linear" :WHERE -1) (SIMP) (EXPAND "timestamp") (SPSI "histLt") (("1" (EXPAND "lt") (SIMP)) ("2" (CLEAN-UP) (APPLY (THEN (CASE "index2!1 = next!1 + 1") (REPLACE -1) (SIMP))) (HIDE "ltIsStrict") (EXPAND "lt") (SIMP)))))) ("2" (REVEAL "histMatchPC") (INST -2 "index!1 - 1") (SIMP) (NEW-SPLIT-IF) (("1" (APPLY (THEN (CASE "index!1 > next!1") (SIMP))) (HIDE 2 3 4) (CASE "index!1 - 1 = next!1") (("1" (REVEAL "histMatchTime") (INST?) (SIMP) (EXPAND "timestamp") (EXPAND "lt") (NEW-SPLIT-IF -) (SKOSIMP*) (INST? "canRead") (SIMP)) ("2" (LEMLTSTRICT) (INST "trans" "(# t := t(procs!1(p_id!1)), r := 1 + numRead(procs!1(p_id!1)), id := p_id!1 #)" "timestamp(lst(hist!1)(next!1))" "timestamp(lst(hist!1)(index!1 -1))") (REVEAL "histLt") (INST - "next!1" "index!1 - 1") (SIMP) (EXPAND "timestamp") (SIMP) (REVEAL "histMatchTime") (INST -1 "index!1 - 1") (SIMP) (NEW-SPLIT-IF -) (("1" (SKOSIMP*) (INST? "canRead") (SIMP)) ("2" (EXPAND "lt") (SIMP)))))) ("2" (INST? -) (INST? -) (SPSI)))))))))))) ("2" (INST + "next(hist!1, (# t := t(procs!1(p_id!1)), r := 1 + numRead(procs!1(p_id!1)), id := p_id!1 #))")))) ("2" (INST?) (SIMP)) ("3" (INST?) (SIMP)) ("4" (INST?) (SIMP)) ("5" (HIDE "rho") (LABEL "id" -2) (HIDE "id") (REVEAL "id") (NEW-SPLIT-IF) (("1" (REVEAL "id") (SIMP) (NEW-SPLIT-IF "toProve") (REDUCE-ALL) (REPLACE "id" :DIR RL) (REVEAL "rho") (REVEAL "queuesNonNeg") (INST?) (SIMP)) ("2" (REVEAL "id") (SIMP) (NEW-SPLIT-IF) (("1" (REVEAL "histMatchPC") (INST?) (REVEAL "queuesNonNeg") (INST?) (REVEAL "rho") (SIMP)) ("2" (NEW-SPLIT-IF -) (("1" (INST?) (SPSI)) ("2" (INST?) (SPSI)))))))) ("6" (INST?) (SIMP)) ("7" (INST?) (SIMP)))) ("3" (SKOSIMP*) (APPLY (THEN (SPLIT-RHO) (REPLACE*) (SIMP) (SKOSIMP*))) (("1" (LABEL "canRead" -2) (HIDE "rho") (INTRONEXT) (("1" (APPLY (THEN (CASE "index!1 = 1 + size(hist!1)") (SIMP))) (("1" (CLEAN-UP) (REVEAL "histMatchPCe") (INST? -) (INST - "pc!1") (EXPAND "canRead") (SIMP) (NEW-SPLIT-IF) (HIDE "canRead") (SPLIT-ALL) (("1" (INST? + :WHERE "histMatchPCe") (SIMP)) ("2" (HIDE "nextSize") (REVEAL "histMatchPC") (INST - "size(hist!1)") (SIMP) (INST?) (INST "histMatchPC" "pc!1") (SIMP) (CLEAN-UP) (SKOSIMP*) (INST-CP + "index2!1") (INST + "index2!1 + 1") (SPLIT-ALL)))) ("2" (INST? "histMatchPC") (NEW-SPLIT-IF -) (("1" (INST? "histMatchPC") (SIMP) (SKOSIMP*) (INST? +) (SIMP)) ("2" (NEW-SPLIT-IF -) (("1" (REVEAL "histMatchPCe") (INST -1 "p_id!1" "pc!1") (EXPAND "canRead") (SIMP) (SKOSIMP*) (INST-CP + "index!2") (CASE "index!2 < next!1") (("1" (SIMP)) ("2" (SIMP) (CLEAN-UP) (HIDE 4) (REVEAL "histMatchTime") (INST - "index!2") (SIMP) (SPSI -) (("1" (SKOSIMP*) (INST "canRead" "qPoint!1") (SIMP)) ("2" (REPLACE*) (HIDE "histMatchPC" "canRead") (CASE "index!2 = next!1") (("1" (EXPAND "timestamp") (EXPAND "lt") (SIMP) (SIMP)) ("2" (REVEAL "histLt") (INST - "next!1" "index!2") (SIMP) (LEMLTSTRICT) (INST? "linear" :WHERE "histLt") (SIMP) (INST "trans" "(# t := t(lst(hist!1)(index!2)), r := r(lst(hist!1)(index!2)), id := id(lst(hist!1)(index!2)) #)" "(# t := t(procs!1(p_id!1)), r := 1 + numRead(procs!1(p_id!1)), id := p_id!1 #)" "timestamp(lst(hist!1)(next!1))") (EXPAND "timestamp") (SIMP) (EXPAND "lt" "trans") (SIMP)))))))) ("2" (REVEAL "histMatchPC") (HIDE -1) (INST -1 "index!1 - 1") (SIMP) (INST?) (INST - "pc!1") (SIMP) (SKOSIMP*) (INST-CP + "index2!1") (INST + "index2!1 + 1") (SPLIT-ALL)))))))) ("2" (INST + " next(hist!1, (# t := t(procs!1(p_id!1)), r := 1 + numRead(procs!1(p_id!1)), id := p_id!1 #))")))) ("2" (HIDE "rho") (INST? -) (INST? -) (SIMP)) ("3" (HIDE "rho") (INST? -) (INST? -) (SIMP)) ("4" (HIDE "rho") (INST? -) (INST? -) (SIMP)) ("5" (HIDE "rho") (CASE "index!1 = 1 + size(hist!1)") (("1" (REPLACE*) (SIMP) (CLEAN-UP) (REVEAL "histMatchPCe") (INST?) (REVEAL "rho") (REVEAL "queuesNonNeg") (INST?) (SIMP) (HIDE "rho") (INST?) (SIMP) (SKOSIMP*) (INST? :WHERE "histMatchPCe") (SIMP)) ("2" (SIMP) (INST? -) (INST? -) (SIMP) (SKOSIMP*) (INST + "index2!1") (SIMP)))) ("6" (HIDE "rho") (INST? -) (INST? -) (SIMP)) ("7" (HIDE "rho") (INST? -) (INST? -) (SIMP))))))) NIL NIL) ("2" (HIDE "rho") (("2" (REVEAL "histMatchPCe") (("2" (INST - "id!1" "pc!1") (("2" (REVEAL "queuesNonNeg") (("2" (INST?) (("2" (REVEAL "rho") (("2" (APPLY (THEN (SPLIT-RHO) (REPLACE*) (SIMP) (SKOSIMP*))) (("1" (RERUN ("1" (LABEL "canRead" -2) (HIDE "rho") (INTRONEXT) (("1" (CASE "id!1 = p_id!1") (("1" (EXPAND "canRead") (SIMP) (CASE " pc!1 = pc(procs!1(id!1))") (("1" (INST + "next!1") (SIMP)) ("2" (SIMP) (SKOSIMP*) (INST-CP + "index!1") (INST + "index!1 + 1") (SIMP) (SPLIT-ALL)))) ("2" (CASE " pc!1 < IF head(outQ(procs!1(id!1))) < tail(outQ(procs!1(id!1))) THEN pc(QE(outQ(procs!1(id!1)))(head(outQ(procs!1(id!1))))) ELSE pc(procs!1(id!1)) ENDIF") (("1" (SPSI "histMatchPCe") (SKOSIMP*) (INST-CP + "index!1") (INST + "index!1 + 1") (SPLIT-ALL)) ("2" (NEW-SPLIT-IF -)))))) ("2" (INST + "next(hist!1, (# t := t(procs!1(p_id!1)), r := 1 + numRead(procs!1(p_id!1)), id := p_id!1 #))"))))) NIL NIL) ("2" (RERUN ("2" (HIDE "rho") (SPLIT-ALL -))) NIL NIL) ("3" (RERUN ("3" (HIDE "rho") (SPLIT-ALL -))) NIL NIL) ("4" (RERUN ("4" (HIDE "rho") (SPLIT-ALL -))) NIL NIL) ("5" (CASE "id!1 = p_id!1") (("1" (SIMP) (("1" (HIDE "rho") (("1" (CASE "pc!1 < pc(QE(outQ(procs!1(id!1)))(head(outQ(procs!1(id!1)))))") (("1" (SIMP) (("1" (SKOSIMP*) (("1" (INST-CP + "index!1") (("1" (INST + "index!1 + 1") (("1" (SPLIT-ALL) NIL NIL)) NIL)) NIL)) NIL)) NIL) ("2" (INST + "1 + size(hist!1)") (("2" (NEW-SPLIT-IF) (("2" (REVEAL "outQpcInc") (("2" (INST?) (("2" (SIMP) (("2" (CLEAN-UP) (("2" (NEW-SPLIT-IF "toProve") (("1" (CASE "outQ(procs!1(p_id!1))`QE(1 + head(outQ(procs!1(p_id!1))))`pc = pc(QE(outQ(procs!1(p_id!1)))(head(outQ(procs!1(p_id!1))))) + 1") (("1" (SIMP) NIL NIL) ("2" (INST?) (("2" (INST - " pc(QE(outQ(procs!1(p_id!1)))(head(outQ(procs!1(p_id!1))))) + 1") (("2" (SIMP) (("2" (REVEAL "outQpcInc") (("2" (HIDE -1 -2 -4) (("2" (INST -1 "1 + head(outQ(procs!1(p_id!1)))") (("2" (SIMP) (("2" (SIMP) (("2" (SKOSIMP*) (("2" (INST - "qPoint2!1") (("2" (SIMP) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (INST -4 "pc(QE(outQ(procs!1(p_id!1)))(head(outQ(procs!1(p_id!1))))) + 1") (("2" (SIMP) (("2" (SKOSIMP*) (("2" (INST - "qPoint2!1") (("2" (SIMP) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (RERUN ("2" (HIDE "rho") (SIMP) (SPSI -) (SKOSIMP*) (INST-CP + "index!1") (INST + "index!1 + 1") (SPLIT-ALL))) NIL NIL)) NIL) ("6" (RERUN ("6" (HIDE "rho") (SPLIT-ALL -))) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|histMatchTime| "" (EXP-RHO) (("" (APPLY (THEN (SPSI) (SKOSIMP*) (SIMP))) (("1" (REVEAL "histMatchTime") (("1" (INST?) (("1" (SPLIT-RHO) (("1" (LABEL "canRead" -2) (("1" (LABEL "hist" -4) (("1" (CASE "exists (next : posnat) : next(hist!1, (# t := t(procs!1(p_id!1)), r := 1 + numRead(procs!1(p_id!1)), id := p_id!1 #)) = next") (("1" (SKOSIMP*) (("1" (HIDE "hist") (("1" (REPLACE*) (("1" (HIDE "rho") (("1" (REVEAL "hist") (("1" (REPLACE*) (("1" (HIDE -1) (("1" (CASE "index!1 <= size(hist!1)") (("1" (SIMP) (("1" (LIFT-IF +) (("1" (SPSI) (("1" (SPSI) (("1" (NEW-SPLIT-IF -) NIL NIL) ("2" (NEW-SPLIT-IF) NIL NIL)) NIL) ("2" (NEW-SPLIT-IF) (("1" (CASE "index!1 = 1") (("1" (REVEAL "firstExists") (("1" (SIMP) (("1" (APPLY (THEN (CASE "next!1 = 1") (SIMP))) (("1" (REPLACE -4 :DIR RL) (("1" (LEMMA "nextSize") (("1" (INST?) (("1" (SIMP) (("1" (EXPAND "timestamp") (("1" (EXPAND "lt") (("1" (PROPAX) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (LEMMA "nextSize") (("2" (INST?) (("1" (SIMP) (("1" (REPLACE -5) (("1" (HIDE 2) (("1" (LEMLTSTRICT) (("1" (INST -2 "timestamp(lst(hist!1)(index!1 - 1))" "(# t := t(procs!1(lst(hist!1)(index!1 - 1)`id)), r := 1 + numRead(procs!1(lst(hist!1)(index!1 - 1)`id)), id := lst(hist!1)(index!1 - 1)`id #)" "timestamp(lst(hist!1)(next!1))") (("1" (SIMP) (("1" (CASE "not lt(timestamp(lst(hist!1)(index!1 - 1)), (# t := t(procs!1(lst(hist!1)(index!1 - 1)`id)), r := 1 + numRead(procs!1(lst(hist!1)(index!1 - 1)`id)), id := lst(hist!1)(index!1 - 1)`id #))") (("1" (EXPAND "timestamp" +) (("1" (EXPAND "lt" +) (("1" (SIMP) (("1" (REVEAL "histMatchTime") (("1" (INST -1 "index!1 - 1") (("1" (SIMP) (("1" (SPSI -) (("1" (SKOSIMP*) (("1" (EXPAND "canRead") (("1" (FLATTEN) (("1" (INST? "canRead") (("1" (SIMP) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (SIMP) (("2" (REVEAL "histLt") (("2" (INST -1 "next!1" "index!1 - 1") (("2" (INST? "ltIsStrict" :WHERE "ltIsStrict") (("2" (SIMP) (("2" (EXPAND "timestamp" +) (("2" (SIMP) (("2" (APPLY (THEN (CASE "index!1 = next!1") (SIMP))) (("2" (REVEAL 1) (("2" (SIMP) (("2" (REVEAL "localTimeEarlier") (("2" (INST?) (("2" (SIMP) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (SIMP) NIL NIL)) NIL)) NIL)) NIL) ("2" (REVEAL "localTimeEarlier") (("2" (INST?) (("2" (SIMP) (("2" (SPSI) (("2" (REVEAL "histMatchTime") (("2" (INST?) (("2" (SIMP) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (LIFT-IF) (("2" (NEW-SPLIT-IF) (("1" (NEW-SPLIT-IF -) (("1" (HIDE 1) (("1" (LEMMA "nextSize") (("1" (INST?) (("1" (SIMP) NIL NIL)) NIL)) NIL)) NIL) ("2" (NEW-SPLIT-IF -) (("2" (APPLY (THEN (CASE "index!1 = 1 + size(hist!1)") (SIMP))) (("2" (REPLACE*) (("2" (REVEAL "histMatchTime") (("2" (INST - "size(hist!1)") (("2" (SIMP) (("2" (NEW-SPLIT-IF) (("2" (NEW-SPLIT-IF) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (APPLY (THEN (CASE "index!1 = 1 + size(hist!1)") (SIMP))) (("2" (REPLACE*) (("2" (LEMMA "nextSize") (("2" (INST?) (("2" (REPLACE*) (("2" (SIMP) (("2" (NEW-SPLIT-IF) (("2" (NEW-SPLIT-IF) (("1" (REVEAL "localTimeEarlier") (("1" (INST?) (("1" (SIMP) NIL NIL)) NIL)) NIL) ("2" (REVEAL "histMatchTime") (("2" (INST?) (("2" (SPLIT-ALL) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (INST + " next(hist!1, (# t := t(procs!1(p_id!1)), r := 1 + numRead(procs!1(p_id!1)), id := p_id!1 #))") NIL NIL)) NIL)) NIL)) NIL) ("2" (REPLACE*) (("2" (SIMP) (("2" (SPLIT-ALL) NIL NIL)) NIL)) NIL) ("3" (REPLACE*) (("3" (SIMP) (("3" (HIDE "rho") (("3" (SPLIT-ALL) (("3" (INST? +) (("3" (SIMP) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("4" (REPLACE*) (("4" (HIDE "rho") (("4" (SPLIT-ALL) NIL NIL)) NIL)) NIL) ("5" (REPLACE*) (("5" (SIMP) (("5" (HIDE "rho") (("5" (LIFT-IF +) (("5" (SPSI) (("1" (CLEAN-UP) (("1" (REVEAL "localTimeEarlier") (("1" (INST?) (("1" (SIMP) (("1" (INST + "(tail(inQ(procs!1(p_id!1))))") (("1" (SIMP) (("1" (REVEAL "queuesNonNeg") (("1" (INST?) (("1" (SIMP) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (SIMP) (("2" (NEW-SPLIT-IF) (("2" (SKOSIMP*) (("2" (INST?) (("2" (SIMP) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("6" (REPLACE*) (("6" (HIDE "rho") (("6" (SPLIT-ALL) (("1" (INST? +) (("1" (SIMP) NIL NIL)) NIL) ("2" (INST-CP + "qPoint!1") (("2" (SIMP) (("2" (CLEAN-UP) (("2" (APPLY (THEN (CASE "head(inQ(procs!1(lst(hist!1)(index!1)`id))) = qPoint!1") (SIMP))) (("2" (REPLACE*) (("2" (REVEAL "inQmatchHistT") (("2" (INST?) (("2" (INST - "1 + t(procs!1(lst(hist!1)(index!1)`id))") (("2" (SIMP) (("2" (SKOSIMP*) (("2" (REVEAL "QtimeInc") (("2" (INST?) (("2" (INST -1 "qPoint!1") (("2" (SIMP) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("7" (REPLACE*) (("7" (SIMP) NIL NIL)) NIL)) NIL)) NIL)) NIL) ("2" (REVEAL "histMatchTimeE") (("2" (INST?) (("2" (APPLY (THEN (SPLIT-RHO) (REPLACE*) (SIMP) (SKOSIMP*))) (("1" (HIDE "rho") (("1" (CASE "exists (next : posnat) : next(hist!1, (# t := t(procs!1(p_id!1)), r := 1 + numRead(procs!1(p_id!1)), id := p_id!1 #)) = next") (("1" (SKOSIMP*) (("1" (REPLACE*) (("1" (INST-CP 1 "index!1") (("1" (INST 1 "index!1 + 1") (("1" (SPLIT-ALL) NIL NIL)) NIL)) NIL)) NIL)) NIL) ("2" (INST + "next(hist!1, (# t := t(procs!1(p_id!1)), r := 1 + numRead(procs!1(p_id!1)), id := p_id!1 #))") NIL NIL)) NIL)) NIL) ("2" (HIDE "rho") (("2" (CASE "t!1 = 1 + time!1") (("1" (INST + "1 + size(hist!1)") (("1" (SIMP) NIL NIL)) NIL) ("2" (SIMP) (("2" (SKOSIMP*) (("2" (INST + "index!1") (("2" (SIMP) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|histJ0write| "" (EXP-RHO :HIDE? T) (("" (REVEAL "histJ0write") (("" (INST - "index!1") (("" (APPLY (THEN (SPLIT-RHO) (REPLACE*) (SIMP))) (("1" (LABEL "canRead" -2) (("1" (HIDE "rho") (("1" (CASE "exists (next : posnat): next(hist!1, (# t := t(procs!1(p_id!1)), r := 1 + numRead(procs!1(p_id!1)), id := p_id!1 #)) = next") (("1" (SKOSIMP*) (("1" (REPLACE*) (("1" (LEMMA "nextSize") (("1" (INST?) (("1" (EXPAND "canRead") (("1" (SPLIT-ALL) (("1" (REVEAL "histJ0write") (("1" (INST?) (("1" (SIMP) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (INST + " next(hist!1, (# t := t(procs!1(p_id!1)), r := 1 + numRead(procs!1(p_id!1)), id := p_id!1 #))") NIL NIL)) NIL)) NIL)) NIL) ("2" (SPSI) NIL NIL) ("3" (SPSI) NIL NIL) ("4" (SPSI) NIL NIL) ("5" (HIDE "rho") (("5" (NEW-SPLIT-IF) (("5" (REVEAL "queuesMatchProg") (("5" (INST?) (("5" (FLATTEN) (("5" (INSTBEST) (("5" (INSTBEST) (("5" (SIMP) (("5" (REVEAL "queuesNonNeg") (("5" (INST?) (("5" (SIMP) (("5" (SIMP) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("6" (SPSI) NIL NIL) ("7" (SPSI) NIL NIL)) NIL)) NIL)) NIL)) NIL) (|histLt| "" (EXP-RHO) (("" (REVEAL "histLt") (("" (INST?) (("" (APPLY (THEN (SPLIT-RHO) (REPLACE*) (SIMP))) (("1" (LABEL "canRead" -2) (("1" (HIDE "rho") (("1" (CASE "exists (next : posnat): next(hist!1, (# t := t(procs!1(p_id!1)), r := 1 + numRead(procs!1(p_id!1)), id := p_id!1 #)) = next") (("1" (SKOSIMP*) (("1" (REPLACE*) (("1" (LEMMA "nextSize") (("1" (INST?) (("1" (EXPAND "canRead") (("1" (NEW-SPLIT-IF) (("1" (NEW-SPLIT-IF) (("1" (NEW-SPLIT-IF) (("1" (REVEAL "histMatchTime") (("1" (INST?) (("1" (SPSI) (("1" (HIDE "histMatchTime") (("1" (SPSI -) (("1" (CLEAN-UP) (("1" (LEMMA "nextExists") (("1" (INST?) (("1" (INST?) (("1" (NEW-SPLIT-IF -) (("1" (EXPAND "timestamp") (("1" (INST?) (("1" (SIMP) (("1" (LEMLTSTRICT) (("1" (INST? :WHERE +) (("1" (SIMP) (("1" (SPSI -) (("1" (HIDE "canRead") (("1" (CLEAN-UP) (("1" (REVEAL "histMatchTime") (("1" (SIMP) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (INST - "index!1") (("2" (SIMP) (("2" (LEMLTSTRICT) (("2" (INST? :WHERE +) (("2" (EXPAND "timestamp") (("2" (SIMP) (("2" (SPSI -) (("2" (REVEAL "histMatchTime") (("2" (SIMP) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (REVEAL "histLt") (("2" (INST?) (("2" (SIMP) NIL NIL)) NIL)) NIL)) NIL)) NIL) ("2" (SPSI) (("1" (CASE "index2!1 - 1 = next!1") (("1" (REPLACE*) (("1" (EXPAND "timestamp") (("1" (SPSI) (("1" (EXPAND "lt") (("1" (PROPAX) NIL NIL)) NIL)) NIL)) NIL)) NIL) ("2" (REVEAL "histMatchTime") (("2" (INST?) (("2" (SPSI) (("2" (LEMLTSTRICT) (("2" (INST? :WHERE +) (("2" (SIMP) (("2" (CLEAN-UP) (("2" (SPSI -) (("2" (INST - "(# t := lst(hist!1)(index2!1 - 1)`t, r := lst(hist!1)(index2!1 - 1)`r, id := lst(hist!1)(index2!1 - 1)`id #)" "(# t := t(procs!1(p_id!1)), r := 1 + numRead(procs!1(p_id!1)), id := p_id!1 #)" "timestamp(lst(hist!1)(next!1))") (("2" (SIMP) (("2" (SPSI -) (("2" (REVEAL "histLt") (("2" (INST - "next!1" "index2!1 - 1") (("2" (SIMP) (("2" (REVEAL "linear") (("2" (INST? :WHERE -) (("2" (EXPAND "timestamp") (("2" (SIMP) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (REVEAL "histLt") (("2" (INST?) (("2" (SIMP) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (INST + "next(hist!1, (# t := t(procs!1(p_id!1)), r := 1 + numRead(procs!1(p_id!1)), id := p_id!1 #))") NIL NIL)) NIL)) NIL)) NIL) ("2" (HIDE "rho") (("2" (NEW-SPLIT-IF) (("2" (CLEAN-UP) (("2" (REVEAL "histMatchTime") (("2" (INST?) (("2" (SIMP) (("2" (SPSI) (("2" (EXPAND "lt") (("2" (PROPAX) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|firstExists| "" (EXP-RHO :HIDE? T) (("" (REVEAL "firstExists") (("" (APPLY (THEN (SPLIT-RHO) (REPLACE*) (SIMP))) (("1" (HIDE "rho") (("1" (INTRONEXT) (("1" (NEW-SPLIT-IF) (("1" (CASE "size(hist!1) = 0") (("1" (SIMP) (("1" (REVEAL "histMatchTimeE") (("1" (INST - "t(procs!1(p_id!1))") (("1" (SIMP) (("1" (REVEAL "localTimeEarlier") (("1" (INST?) (("1" (SIMP) (("1" (CLEAN-UP) (("1" (REVEAL "histCompleteNumRead") (("1" (INST - "p_id!1") (("1" (FLATTEN) (("1" (INST - "0") (("1" (EXPAND "oc") (("1" (PROPAX) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (SIMP) (("2" (EXPAND "lt") (("2" (EXPAND "timestamp") (("2" (GROUND) (("2" (APPLY (THEN (CASE "next!1 = 1") (REPLACE*) (SIMP))) (("2" (REVEAL "histCompleteNumRead") (("2" (INST?) (("2" (FLATTEN) (("2" (INST - "0") (("2" (EXPAND "oc") (("2" (SKOSIMP*) (("2" (REVEAL "histLt") (("2" (INST - "1" "index!1") (("2" (SIMP) (("2" (EXPAND "timestamp") (("2" (EXPAND "lt") (("2" (SIMP) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (INST + "next(hist!1, (# t := t(procs!1(p_id!1)), r := 1 + numRead(procs!1(p_id!1)), id := p_id!1 #))") NIL NIL)) NIL)) NIL) ("2" (HIDE "rho") (("2" (NEW-SPLIT-IF) (("2" (REVEAL "histMatchTimeE") (("2" (INST - "1") (("2" (SIMP) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|readValuesCorrect| "" (EXP-RHO :HIDE? T) (("" (REVEAL "readValuesCorrect") (("" (INST -1 "id!1" "pc!1") (("" (CASE "action!1 = read") (("1" (SIMP) (("1" (LABEL "canRead" -3) (("1" (REPLACE*) (("1" (HIDE "rho") (("1" (INTRONEXT) (("1" (NEW-SPLIT-IF) (("1" (NEW-SPLIT-IF) (("1" (EXPAND "canRead") (("1" (SIMP) (("1" (REVEAL "cacheEqualMemhist") (("1" (INST? -) (("1" (SIMP) (("1" (INST? +) (("1" (NEW-SPLIT-IF) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (NEW-SPLIT-IF) (("1" (SKOSIMP*) (("1" (INST-CP + "index!1") (("1" (INST + "index!1 + 1") (("1" (SPLIT-ALL) NIL NIL)) NIL)) NIL)) NIL) ("2" (REDUCE-ALL) NIL NIL)) NIL)) NIL) ("2" (NEW-SPLIT-IF) (("2" (SKOSIMP*) (("2" (INST-CP + "index!1") (("2" (INST + "index!1 + 1") (("2" (SPLIT-ALL) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (INST + "next(hist!1, (# t := t(procs!1(p_id!1)), r := 1 + numRead(procs!1(p_id!1)), id := p_id!1 #))") NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (CASE "action!1 = memWrite") (("1" (SIMP) (("1" (REPLACE*) (("1" (HIDE "rho") (("1" (NEW-SPLIT-IF) (("1" (SKOSIMP*) (("1" (INST + "index!1") (("1" (SIMP) (("1" (NEW-SPLIT-IF) (("1" (REVEAL "histCompleteTstime") (("1" (INST?) (("1" (SIMP) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (CASE "pc!1 < pc(procs_p!1(id!1)) AND op(instlist(id!1, pc!1)) = READ and pc!1 < pc(procs!1(id!1)) AND op(instlist(id!1, pc!1)) = READ") (("1" (SIMP) (("1" (SKOSIMP*) (("1" (INST + "index!1") (("1" (SPLIT-RHO-ALL) NIL NIL)) NIL)) NIL)) NIL) ("2" (EXPAND "canWrite") (("2" (SPLIT-RHO-ALL) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|reachable| "" (SKOSIMP*) (("" (EXPAND "reachable" +) (("" (LEMMA "memhistCorrect") (("" (LEMMA "cacheEqualMemhist") (("" (LEMMA "queuesNonNeg") (("" (LEMMA "inQmatchHist") (("" (INST?) (("" (INST?) (("" (INST?) (("" (INST?) (("" (SIMP) (("" (LEMMA "localTimeEarlier") (("" (LEMMA "QtimeInc") (("" (LEMMA "queuesMatchProg") (("" (LEMMA "outQpcInc") (("" (INST?) (("" (INST?) (("" (INST?) (("" (INST?) (("" (SIMP) (("" (LEMMA "histComplete") (("" (LEMMA "histMatchPC") (("" (LEMMA "histMatchTime") (("" (LEMMA "histLt") (("" (INST?) (("" (INST?) (("" (INST?) (("" (INST?) (("" (SIMP) (("" (LEMMA "histJ0write") (("" (LEMMA "firstExists") (("" (LEMMA "readValuesCorrect") (("" (INST?) (("" (INST?) (("" (INST?) (("" (SIMP) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL))