%Patch files loaded: patch2 version 1.2.2.98 $$$sporadic_tasks.pvs %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Sporadic tasks % % - tasks are in [0..nbtask-1] % % - prio(i): priority of task i % % - jobs are pairs (i, n) where i is a task, n is nat % % - prio of a job = prio of its task % % % % C(i): max length of jobs of task i % % T(i): min delay between two successive jobs of i % % D(i): dealine for each job of i % % % % B(p): upper bound on blocking time for jobs of % % priority >= p % % % % dispatch(j): start of job j % % prog(j): program for job j % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% sporadic_tasks [ nbtasks: posnat, (IMPORTING programs, tasks_and_jobs[nbtasks]) prio: [task -> priority], C, T, D: [task -> posnat], B: [priority -> nat], dispatch: [job -> nat], prog: [job -> prog] ]: THEORY BEGIN ASSUMING i: VAR task % below(nbtask) n, m: VAR nat p: VAR priority j: VAR job % [task, nat] s: VAR semaphore prio(i, n): priority = prio(i) good_dispatch: ASSUMPTION dispatch(i, n) + T(i) <= dispatch(i, n + 1) bound_length: ASSUMPTION length(prog(i, n)) <= C(i) blocking: ASSUMPTION prio(j) < p IMPLIES max_cs(prog(j), p) <= B(p) good_ceiling: ASSUMPTION member(s, resources(prog(j))) IMPLIES prio(j) <= ceil(s) good_programs: ASSUMPTION well_behaved(prog(j)) IMPORTING fsets_sum cpu_usage: ASSUMPTION sum(fullset[task], lambda i: C(i)/T(i)) < 1 topprio_is_used: ASSUMPTION EXISTS i: prio(i) = maxprio - 1 ENDASSUMING IMPORTING traces[job, prio, dispatch, prog], ceiling_equations, schedules3 u: VAR trace t, t1, t2: VAR nat %----------------------------------------- % Properties of dispatch, blocking, etc. %----------------------------------------- dispatch_delay: LEMMA dispatch(i, n + m) - dispatch(i, m) >= n * T(i) increasing_dispatch: LEMMA n < m IMPLIES dispatch(i, n) + T(i) <= dispatch(i, m) blocking_bound: LEMMA blocking(u, p, t) <= B(p) process_time_bound: LEMMA process_time(sch(u), t1, t2, j) <= C(j`1) finished_prop: LEMMA process_time(sch(u), t1, t2, j) = C(j`1) IMPLIES finished(u, j, t2) %---------------------------------------------------------------- % Set of jobs of priority >= p AND dispatched between t1 and t2 %----------------------------------------------------------------- K(p, t1, t2): set[job] = { j | prio(j) >= p AND t1 <= dispatch(j) AND dispatch(j) < t2 } L(i, t1, t2): set[job] = { j | j`1 = i AND t1 <= dispatch(j) AND dispatch(j) < t2 } A(p): set[task] = { i | prio(i) >= p } partition_K: LEMMA partition(K(p, t1, t2))(A(p), lambda i: L(i, t1, t2)) A_nonempty: JUDGEMENT A(p) HAS_TYPE non_empty_finite_set[task] %------------------------------- % The sets L and K are finite %------------------------------- injection_prop: LEMMA t1 <= t2 AND n = ceiling((t2 - t1) / T(i)) IMPLIES EXISTS (h: [(L(i, t1, t2)) -> below(n)]): injective?(h) L_finite: JUDGEMENT L(i, t1, t2) HAS_TYPE finite_set[job] card_L: LEMMA t1 <= t2 IMPLIES card(L(i, t1, t2)) <= ceiling((t2 - t1)/ T(i)) K_finite: JUDGEMENT K(p, t1, t2) HAS_TYPE finite_set[job] bound_L: LEMMA L(i, t1, t2)(j) IMPLIES process_time(sch(u), t1, t2, j) <= C(i) finished_L: LEMMA L(i, t1, t2)(j) AND process_time(sch(u), t1, t2, j) = C(i) IMPLIES finished(u, j, t2) process_time_L: LEMMA t1 <= t2 IMPLIES process_time(sch(u), t1, t2, L(i, t1, t2)) <= C(i) * ceiling((t2 - t1)/ T(i)) max_process_time_L: LEMMA t1 <= t2 AND member(j, L(i, t1, t2)) AND process_time(sch(u), t1, t2, L(i, t1, t2)) = C(i) * ceiling((t2 - t1)/ T(i)) IMPLIES finished(u, j, t2) process_time_K: LEMMA t1 <= t2 IMPLIES process_time(sch(u), t1, t2, K(p, t1, t2)) <= sum(A(p), lambda i: C(i) * ceiling((t2 - t1)/T(i))) max_process_time_K: LEMMA t1 < t2 AND member(j, K(p, t1, t2)) AND process_time(sch(u), t1, t2, K(p, t1, t2)) = sum(A(p), lambda i: C(i) * ceiling((t2 - t1)/T(i))) IMPLIES finished(u, j, t2) %-------------------------------------------------------------- % Quiet time: time t such that all jobs of priority >= p % started before t are finished at t %--------------------------------------------------------------- quiet(u, p, t): bool = FORALL j: dispatch(j) < t AND prio(j) >= p IMPLIES finished(u, j, t) not_busy_quiet: LEMMA not busy(u, p, t) IMPLIES quiet(u, p, t) quiet_step: LEMMA quiet(u, p, t) AND not busy(u, p, t) IMPLIES quiet(u, p, t+1) zero_is_quiet: LEMMA quiet(u, p, 0) busy_interval: LEMMA quiet(u, p, t1) AND t1 <= t2 IMPLIES process_time(sch(u), t1, t2, K(p, t1, t2)) = process_time(sch(u), t1, t2, K(p)) busy_interval2: LEMMA quiet(u, p, t1) AND t1 <= t2 IMPLIES process_time(sch(u), t1, t2, K(p)) <= sum(A(p), lambda i: C(i) * ceiling((t2 - t1)/T(i))) %----------------------------------------------------------------- % - M(p): smallest solution of the equation % B_p + sum_{prio(i) <= p} C_i * ceiling(x / T_i) = x %---------------------------------------------------------------- x: VAR posreal d: VAR posnat bound(x, p): bool = sum(A(p), lambda i: C(i) * ceiling(x / T(i))) + B(p) = x partial_cpu_usage: LEMMA sum(A(p), lambda i: C(i)/T(i)) < 1 smallest_bound: LEMMA EXISTS d: bound(d, p) AND (FORALL x: bound(x, p) IMPLIES d <= x) M(p): { d | bound(d, p) AND FORALL x: bound(x, p) IMPLIES d <= x } solution_prop: LEMMA sum(A(p), lambda i: C(i) * ceiling(M(p)/T(i))) = M(p) - B(p) %---------------- % Busy periods %---------------- busy_period(u, p, t1, t2): bool = t1 < t2 AND busy(u, p, t1) AND quiet(u, p, t1) AND quiet(u, p, t2) AND FORALL t: t1 < t AND t < t2 IMPLIES not quiet(u, p, t) busy_period_prop: LEMMA busy_period(u, p, t1, t2) AND t1 <= t AND t < t2 IMPLIES busy(u, p, t) %---------------------------------------- % Bound on the length of busy periods %---------------------------------------- critical_interval: PROPOSITION quiet(u, p, t1) IMPLIES EXISTS t2: t1 < t2 AND t2 <= t1 + M(p) AND quiet(u, p, t2) delay_to_quiet_time: LEMMA FORALL t: EXISTS t2: quiet(u, p, t2) AND t < t2 AND t2 <= t + M(p) busy_period_length: LEMMA busy_period(u, p, t1, t2) IMPLIES t2 - t1 <= M(p) job_in_busy_period: LEMMA prio(j) = p IMPLIES EXISTS t1, t2: t1 <= dispatch(j) AND dispatch(j) < t2 AND busy_period(u, p, t1, t2) %--------------------------- % First termination bound %--------------------------- termination1: PROPOSITION prio(j) = p IMPLIES finished(u, j, dispatch(j) + M(p)) %------------------------------------------------------ % First schedulability criterion: M(prio(i)) <= D(i) %------------------------------------------------------ deadline(j): nat = dispatch(j) + D(j`1) schedulability1: PROPOSITION (FORALL i: M(prio(i)) <= D(i)) IMPLIES (FORALL u, j: finished(u, j, deadline(j))) %------------------------------------------------------ % Schedulability criterion in the more standard case % - one task per priority % - deadline before period %------------------------------------------------------ l, l1, l2: VAR task M: VAR posnat H(i): set[task] = { l | prio(l) > prio(i) } J(i): set[task] = { l | prio(l) = prio(i) } B(i): nat = B(prio(i)) schedulability_criterion: PROPOSITION (FORALL l1, l2: prio(l1) = prio(l2) IMPLIES l1 = l2) AND (FORALL i: D(i) <= T(i)) AND (FORALL i: EXISTS M: sum(H(i), lambda l: C(l) * ceiling(M / T(l))) + B(i) + C(i) = M AND M <= D(i)) IMPLIES (FORALL u, j: finished(u, j, deadline(j))) END sporadic_tasks $$$sporadic_tasks.prf (|sporadic_tasks| (|IMP_traces_TCC1| "" (LEMMA "good_ceiling") (("" (PROPAX) NIL NIL)) NIL) (|IMP_traces_TCC2| "" (LEMMA "good_programs") (("" (PROPAX) NIL NIL)) NIL) (|dispatch_delay| "" (SKOLEM + ("i!1" "m!1" _)) (("" (INDUCT-AND-SIMPLIFY "n") (("" (USE "good_dispatch") (("" (ASSERT) NIL NIL)) NIL)) NIL)) NIL) (|increasing_dispatch| "" (SKOSIMP) (("" (USE "dispatch_delay" ("m" "n!1" "n" "m!1 - n!1")) (("1" (USE "both_sides_times_pos_le1" ("pz" "T(i!1)" "x" "n!1 + 1" "y" "m!1")) (("1" (ASSERT) NIL NIL)) NIL) ("2" (ASSERT) NIL NIL)) NIL)) NIL) (|blocking_bound| "" (SKOLEM!) (("" (EXPAND "blocking") (("" (AUTO-REWRITE "blocking" "blocker_prio2") (("" (SMASH) NIL NIL)) NIL)) NIL)) NIL) (|process_time_bound| "" (SKOLEM!) (("" (CASE "t1!1 <= t2!1") (("1" (REWRITE "process_time2") (("1" (USE "bound_length" ("n" "j!1`2")) (("1" (ASSERT) NIL NIL)) NIL)) NIL) ("2" (AUTO-REWRITE "process_time" "sum") (("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL) (|finished_prop| "" (SKOSIMP) (("" (CASE "t1!1 <= t2!1") (("1" (REWRITE "process_time2") (("1" (REWRITE "finished_equiv") (("1" (USE "bound_length" ("n" "j!1`2")) (("1" (ASSERT) NIL NIL)) NIL)) NIL)) NIL) ("2" (AUTO-REWRITE "process_time" "sum") (("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL) (|partition_K| "" (GRIND) (("" (APPLY-EXTENSIONALITY :HIDE? T) (("" (REDUCE) NIL NIL)) NIL)) NIL) (|A_nonempty| "" (SKOLEM!) (("" (LEMMA "topprio_is_used") (("" (GRIND :IF-MATCH NIL) (("" (INST?) (("" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL) (|injection_prop| "" (SKOSIMP) (("" (INST + "lambda (j: (L(i!1, t1!1, t2!1))): floor((dispatch(j) - t1!1)/T(i!1))") (("1" (GRIND) (("1" (APPLY-EXTENSIONALITY :HIDE? T) (("1" (DELETE -2 -3 -5 -6 -7 -8) (("1" (AUTO-REWRITE "div_simp") (("1" (USE "increasing_dispatch" ("n" "x1!1`2" "m" "x2!1`2")) (("1" (USE "increasing_dispatch" ("n" "x2!1`2" "m" "x1!1`2")) (("1" (CASE-REPLACE "(i!1, x1!1`2) = x1!1") (("1" (CASE-REPLACE "(i!1, x2!1`2) = x2!1") (("1" (DELETE -1 -2) (("1" (GROUND) (("1" (USE "both_sides_div_pos_le1" ("pz" "T(i!1)" "x" "T(i!1) + dispatch(x2!1)" "y" "dispatch(x1!1)")) (("1" (REWRITE "div_distributes" -1 :DIR RL) (("1" (ASSERT) NIL NIL)) NIL)) NIL) ("2" (USE "both_sides_div_pos_le1" ("pz" "T(i!1)" "x" "T(i!1) + dispatch(x1!1)" "y" "dispatch(x2!1)")) (("2" (REWRITE "div_distributes" -1 :DIR RL) (("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL) ("2" (ASSERT) NIL NIL)) NIL) ("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (SKOLEM-TYPEPRED) (("2" (EXPAND "L") (("2" (GROUND) (("1" (USE "pos_div_ge" ("x" "dispatch(j!1) - t1!1")) (("1" (ASSERT) NIL NIL)) NIL) ("2" (USE "both_sides_div_pos_lt1" ("pz" "T(i!1)" "x" "dispatch(j!1) - t1!1" "y" "t2!1 - t1!1")) (("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|L_finite| "" (SKOLEM!) (("" (CASE "t1!1 <= t2!1") (("1" (ASSERT) (("1" (EXPAND "is_finite") (("1" (NAME "n!1" "ceiling((t2!1 - t1!1) / T(i!1))") (("1" (USE "pos_div_ge") (("1" (ASSERT) (("1" (USE "injection_prop" ("n" "n!1")) (("1" (ASSERT) (("1" (SKOLEM!) (("1" (INST + "n!1" "h!1") NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (ASSERT) (("2" (CASE-REPLACE "L(i!1, t1!1, t2!1) = emptyset") (("1" (ASSERT) NIL NIL) ("2" (DELETE 3) (("2" (AUTO-REWRITE "L" "emptyset") (("2" (APPLY-EXTENSIONALITY :HIDE? T) (("2" (REDUCE) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|card_L| "" (SKOSIMP) (("" (ASSERT) (("" (REWRITE "card_def") (("" (NAME-REPLACE "n!1" "ceiling((t2!1 - t1!1) / T(i!1))" :HIDE? NIL) (("" (USE "pos_div_ge") (("" (ASSERT) (("" (REWRITE "Card_injection") (("" (USE "injection_prop" ("n" "n!1")) (("" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|K_finite| "" (SKOLEM!) (("" (USE "partition_K") (("" (EXPAND "partition") (("" (GROUND) (("" (REPLACE*) (("" (REWRITE "union_is_finite") NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|bound_L| "" (EXPAND "L") (("" (SKOSIMP) (("" (REPLACE -1 + RL) (("" (REWRITE "process_time_bound") NIL NIL)) NIL)) NIL)) NIL) (|finished_L| "" (EXPAND "L") (("" (SKOSIMP) (("" (REPLACE -1 - RL) (("" (FORWARD-CHAIN "finished_prop") NIL NIL)) NIL)) NIL)) NIL) (|process_time_L| "" (SKOSIMP) (("" (ASSERT) (("" (REWRITE "process_time_finite_set") (("" (USE "sum_bound[job]" ("N" "C(i!1)")) (("" (AUTO-REWRITE "bound_L" "card_L") (("" (GROUND) (("" (USE "both_sides_times_pos_le2" ("x" "card(L(i!1, t1!1, t2!1))" "y" "ceiling((t2!1 - t1!1) / T(i!1))" "pz" "C(i!1)")) (("" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|max_process_time_L| "" (SKOSIMP) (("" (REWRITE "process_time_finite_set") (("" (AUTO-REWRITE "bound_L" "member") (("" (CASE-REPLACE "ceiling((t2!1 - t1!1) / T(i!1)) = card(L(i!1, t1!1, t2!1))") (("1" (DELETE -1) (("1" (USE "sum_max_bound[job]" ("N" "C(i!1)")) (("1" (GROUND) (("1" (INST?) (("1" (FORWARD-CHAIN "finished_L") NIL NIL)) NIL)) NIL)) NIL)) NIL) ("2" (DELETE -2 2) (("2" (USE "sum_bound[job]" ("N" "C(i!1)")) (("2" (GROUND) (("2" (USE "both_sides_times_pos_lt2" ("pz" "C(i!1)" "x" "card(L(i!1, t1!1, t2!1))" "y" "ceiling((t2!1 - t1!1) / T(i!1))")) (("2" (ASSERT) (("2" (USE "card_L") (("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|process_time_K| (:NEW-GROUND? T) "" (SKOSIMP) (("" (USE "partition_K") (("" (USE "process_time_partition[task, job]") (("" (GROUND) (("" (REPLACE*) (("" (DELETE -1 -2) (("" (AUTO-REWRITE "process_time_L") (("" (REWRITE "sum_le") NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|max_process_time_K| "" (SKOSIMP) (("" (USE "partition_K") (("" (USE "process_time_partition[task, job]") (("" (GROUND) (("" (REPLACE*) (("" (DELETE -1 -2) (("" (USE "equal_sum_le[task]") (("" (AUTO-REWRITE "process_time_L" "A" "K" "L" "member" "prio") (("" (GROUND) (("" (DELETE -4) (("" (REDUCE :IF-MATCH NIL) (("" (INST - "j!1`1") (("" (USE "max_process_time_L") (("" (GROUND) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|not_busy_quiet| "" (SKOSIMP) (("" (AUTO-REWRITE "busy" "quiet" "ready_equiv" "finished_equiv") (("" (REDUCE) NIL NIL)) NIL)) NIL) (|quiet_step| "" (EXPAND "quiet") (("" (SKOSIMP*) (("" (INST?) (("" (GROUND) (("1" (USE "finished_stable" ("t2" "1+t!1")) (("1" (ASSERT) NIL NIL)) NIL) ("2" (EXPAND "busy") (("2" (INST?) (("2" (USE "ready_at_dispatch") (("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|zero_is_quiet| "" (SKOLEM!) (("" (GRIND) NIL NIL)) NIL) (|busy_interval| "" (SKOSIMP) (("" (USE "process_time_partition3" ("E" "K(p!1)" "E1" "{ j | prio(j) >= p!1 AND dispatch(j) < t1!1 }" "E2" "K(p!1, t1!1, t2!1)" "E3" "{ j | prio(j) >= p!1 AND t2!1 <= dispatch(j) }")) (("" (GROUND) (("1" (CASE "process_time(sch(u!1), t1!1, t2!1, {j: job | prio(j) >= p!1 AND dispatch(j) < t1!1}) = 0 AND process_time(sch(u!1), t1!1, t2!1, {j: job | prio(j) >= p!1 AND t2!1 <= dispatch(j)}) = 0") (("1" (GROUND) NIL NIL) ("2" (DELETE -1 2) (("2" (GROUND) (("1" (AUTO-REWRITE "active_prop" "finished_equiv" "ready_equiv") (("1" (REWRITE "zero_process_time") (("1" (SKOSIMP) (("1" (FORWARD-CHAIN "active_ready") (("1" (EXPAND "quiet") (("1" (INST?) (("1" (ASSERT) (("1" (ASSERT) (("1" (USE "pc_increasing" ("t1" "t1!1" "t2" "t!1")) (("1" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (AUTO-REWRITE "active_prop" "ready_equiv") (("2" (REWRITE "zero_process_time") (("2" (SKOSIMP) (("2" (FORWARD-CHAIN "active_ready") (("2" (ASSERT) (("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (DELETE -1 -2 2) (("2" (GRIND) (("2" (APPLY-EXTENSIONALITY :HIDE? T) (("2" (SMASH) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|busy_interval2| "" (SKOSIMP) (("" (REWRITE "busy_interval" :DIR RL) (("" (REWRITE "process_time_K") NIL NIL)) NIL)) NIL) (|partial_cpu_usage| "" (SKOLEM!) (("" (LEMMA "cpu_usage") (("" (USE "sum_subset[task]" ("A" "A(p!1)" "B" "fullset[task]")) (("" (ASSERT) (("" (DELETE -1 2) (("" (GRIND :EXCLUDE ("A")) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|smallest_bound| "" (SKOLEM!) (("" (EXPAND "bound") (("" (USE "partial_cpu_usage") (("" (USE "smallest_int_solution[task]" ("B1" "B(p!1)")) (("" (ASSERT) (("" (EXPAND* "G" "F") NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (M_TCC1 "" (INST + "lambda p: epsilon! d: bound(d, p) AND (FORALL (x: posreal): bound(x, p) IMPLIES d <= x)") (("" (SKOLEM!) (("" (USE "epsilon_ax[posnat]") (("" (AUTO-REWRITE "smallest_bound") (("" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL) (|solution_prop| "" (SKOLEM!) (("" (TYPEPRED "M(p!1)") (("" (DELETE -3) (("" (EXPAND "bound") (("" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL) (|busy_period_prop| "" (EXPAND "busy_period") (("" (SKOSIMP) (("" (FORWARD-CHAIN "not_busy_quiet") (("" (INST?) (("" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL) (|critical_interval| "" (SKOSIMP) (("" (CASE "busy(u!1, p!1, t1!1, t1!1+M(p!1))") (("1" (AUTO-REWRITE "solution_prop") (("1" (USE "busy_time2") (("1" (USE "busy_interval2") (("1" (ASSERT) (("1" (USE "blocking_bound") (("1" (INST + "M(p!1) + t1!1") (("1" (ASSERT) (("1" (EXPAND "quiet") (("1" (SKOSIMP) (("1" (AUTO-REWRITE "member" "K" "busy_interval") (("1" (USE "max_process_time_K" ("t1" "t1!1" "t2" "M(p!1) + t1!1")) (("1" (GROUND) (("1" (ASSERT) (("1" (INST?) (("1" (ASSERT) (("1" (USE "finished_stable" ("t1" "t1!1" "t2" "M(p!1) + t1!1")) (("1" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (CASE "busy(u!1, p!1, t1!1)") (("1" (ASSERT) (("1" (EXPAND "busy" +) (("1" (SKOSIMP) (("1" (INST + "t!1") (("1" (ASSERT) (("1" (AUTO-REWRITE "not_busy_quiet") (("1" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (DELETE 2) (("2" (INST + "t1!1+1") (("2" (GROUND) (("2" (FORWARD-CHAIN "quiet_step") (("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|delay_to_quiet_time| "" (SKOSIMP) (("" (USE "wf_nat") (("" (EXPAND "well_founded?") (("" (INST - "{ n | EXISTS t: t + n = t!1 AND quiet(u!1, p!1, t) }") (("" (GROUND) (("1" (SKOSIMP* :PREDS? T) (("1" (ASSERT) (("1" (FORWARD-CHAIN "critical_interval") (("1" (SKOSIMP) (("1" (INST + "t2!1") (("1" (GROUND) (("1" (INST - "t!1 - t2!1") (("1" (ASSERT) NIL NIL) ("2" (INST?) (("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (AUTO-REWRITE "zero_is_quiet") (("2" (INST + "t!1") (("2" (INST + "0") (("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|busy_period_length| "" (EXPAND "busy_period") (("" (SKOSIMP) (("" (FORWARD-CHAIN "critical_interval") (("" (SKOSIMP) (("" (INST?) (("" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|job_in_busy_period| "" (SKOSIMP) (("" (LEMMA "wf_nat") (("" (EXPAND "well_founded?") (("" (INST-CP - "{ n | EXISTS t: t = dispatch(j!1) - n AND quiet(u!1, p!1, t) }") (("" (REDUCE :IF-MATCH NIL) (("1" (DELETE -1) (("1" (INST - "{ t | dispatch(j!1) < t AND quiet(u!1, p!1, t) }") (("1" (REDUCE :IF-MATCH NIL) (("1" (INST + "t!1" "y!2") (("1" (ASSERT) (("1" (EXPAND "busy_period") (("1" (GROUND) (("1" (CASE-REPLACE "t!1 = dispatch(j!1)") (("1" (EXPAND "busy") (("1" (INST?) (("1" (AUTO-REWRITE "ready_at_dispatch") (("1" (ASSERT) NIL NIL)) NIL)) NIL)) NIL) ("2" (REPLACE -3 - RL) (("2" (FORWARD-CHAIN "quiet_step") (("2" (ASSERT) (("2" (INST -7 "y!1 - 1") (("1" (ASSERT) NIL NIL) ("2" (INST + "1+t!1") (("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (SKOSIMP) (("2" (CASE "t!2 <= dispatch(j!1)") (("1" (ASSERT) (("1" (INST -10 "dispatch(j!1) - t!2") (("1" (ASSERT) NIL NIL) ("2" (INST? +) (("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL) ("2" (ASSERT) (("2" (INST - "t!2") NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (DELETE -1 -2 -3 -4 2) (("2" (USE "delay_to_quiet_time" ("t" "dispatch(j!1)")) (("2" (REDUCE :INSTANTIATOR INST!) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (DELETE -1 -2 2) (("2" (AUTO-REWRITE "zero_is_quiet") (("2" (INST + "dispatch(j!1)") (("2" (INST + "0") (("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|termination1| "" (SKOSIMP) (("" (USE "delay_to_quiet_time") (("" (SKOSIMP) (("" (EXPAND "quiet") (("" (INST?) (("" (ASSERT) (("" (USE "finished_stable" ("t2" "M(p!1) + dispatch(j!1)")) (("" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|schedulability1| "" (SKOSIMP*) (("" (INST - "j!1`1") (("" (USE "termination1") (("" (ASSERT) (("" (AUTO-REWRITE "prio") (("" (ASSERT) (("" (USE "finished_stable" ("t2" "deadline(j!1)")) (("" (AUTO-REWRITE "deadline") (("" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|schedulability_criterion| "" (SKOSIMP) (("" (REWRITE "schedulability1") (("" (DELETE 2) (("" (SKOLEM!) (("" (INST? -3) (("" (SKOSIMP) (("" (CASE "bound(M!1, prio(i!1))") (("1" (DELETE -2 -3 -4) (("1" (TYPEPRED "M(prio(i!1))") (("1" (INST - "M!1") (("1" (ASSERT) NIL NIL)) NIL)) NIL)) NIL) ("2" (DELETE 2) (("2" (EXPAND* "B" "bound") (("2" (CASE-REPLACE "A(prio(i!1)) = add(i!1, H(i!1))") (("1" (AUTO-REWRITE "sum_add" "member" "H" "div_simp") (("1" (ASSERT) (("1" (CASE-REPLACE "ceiling(M!1 / T(i!1)) = 1") (("1" (ASSERT) NIL NIL) ("2" (DELETE -1 -2 -4 2) (("2" (INST?) (("2" (USE "both_sides_div_pos_le1" ("pz" "T(i!1)" "x" "M!1" "y" "T(i!1)")) (("2" (ASSERT) (("2" (TYPEPRED "ceiling(M!1 / T(i!1))") (("2" (ASSERT :FLUSH? T) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (DELETE -2 -3 -4 2) (("2" (APPLY-EXTENSIONALITY :HIDE? T) (("2" (GRIND) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) $$$indexed_partitions.pvs indexed_partitions [T, U: TYPE ] : THEORY BEGIN A, B, C: VAR set[T] X, Y, Z: VAR set[U] F: VAR [T -> set[U]] a, b, c: VAR T x, y, z: VAR U %-------------------------------------------------------- % Union and intersection of a family F(a) for a in A %-------------------------------------------------------- union(A, F): set[U] = { x | EXISTS (a: (A)): F(a)(x) } inter(A, F): set[U] = { x | FORALL (a: (A)): F(a)(x) } union_upper_bound: LEMMA FORALL (a: (A)): subset?(F(a), union(A, F)) inter_lower_bound: LEMMA FORALL (a: (A)): subset?(inter(A, F), F(a)) union_least_upper_bound: LEMMA subset?(union(A, F), X) IFF FORALL (a: (A)): subset?(F(a), X) inter_least_upper_bound: LEMMA subset?(X, inter(A, F)) IFF FORALL (a: (A)): subset?(X, F(a)) union_emptyset: LEMMA union(emptyset, F) = emptyset union_empty: LEMMA empty?(A) IMPLIES empty?(union(A, F)) inter_emptyset: LEMMA inter(emptyset, F) = fullset %---------------------------------------- % Finiteness of union and intersection %---------------------------------------- IMPORTING finite_sets@finite_sets_inductions G: VAR [T -> finite_set[U]] D: VAR finite_set[T] E: VAR (nonempty?[T]) finite_inter: LEMMA (EXISTS (a: (A)): is_finite(F(a))) IMPLIES is_finite(inter(A, F)) inter_is_finite: JUDGEMENT inter(E, G) HAS_TYPE finite_set[U] union_is_finite: JUDGEMENT union(D, G) HAS_TYPE finite_set[U] %-------------- % Partitions %-------------- partition(X)(A, F): bool = X = union(A, F) AND FORALL (a, b: (A)): a = b OR disjoint?(F(a), F(b)) END indexed_partitions $$$indexed_partitions.prf (|indexed_partitions| (|union_upper_bound| "" (GRIND) NIL NIL) (|inter_lower_bound| "" (GRIND) NIL NIL) (|union_least_upper_bound| "" (GRIND) NIL NIL) (|inter_least_upper_bound| "" (GRIND) NIL NIL) (|union_emptyset| "" (SKOLEM!) (("" (APPLY-EXTENSIONALITY :HIDE? T) (("" (GRIND) NIL NIL)) NIL)) NIL) (|union_empty| "" (GRIND) NIL NIL) (|inter_emptyset| "" (SKOLEM!) (("" (APPLY-EXTENSIONALITY :HIDE? T) (("" (GRIND) NIL NIL)) NIL)) NIL) (|finite_inter| "" (SKOSIMP*) (("" (USE "inter_lower_bound") (("" (FORWARD-CHAIN "finite_subset") NIL NIL)) NIL)) NIL) (|inter_is_finite| "" (SKOLEM-TYPEPRED) (("" (REWRITE "finite_inter") (("" (DELETE 2) (("" (GRIND) NIL NIL)) NIL)) NIL)) NIL) (|union_is_finite| "" (SKOLEM + (_ "G!1")) (("" (AUTO-REWRITE "nonempty?" "union_emptyset" "finite_union[U]") (("" (INDUCT "D" :NAME "finite_set_induction_rest[T]") (("1" (ASSERT) NIL NIL) ("2" (SKOSIMP) (("2" (CASE-REPLACE "union(SS!1, G!1) = union(G!1(choose(SS!1)), union(rest(SS!1), G!1))") (("1" (ASSERT) NIL NIL) ("2" (DELETE -1 2) (("2" (AUTO-REWRITE "union" "rest" "remove" "member") (("2" (APPLY-EXTENSIONALITY :HIDE? T) (("2" (REDUCE) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) $$$sum_indexed_partitions.pvs sum_indexed_partitions [T, U: TYPE] : THEORY BEGIN IMPORTING indexed_partitions, sum_sequences, fsets_sum F: VAR [T -> set[U]] A: VAR finite_set[T] X: VAR set[U] u: VAR [nat -> U] i: VAR T t1, t2: VAR nat sum_partition: LEMMA partition(X)(A, F) IMPLIES sum(u, t1, t2, X) = sum(A, lambda i: sum(u, t1, t2, F(i))) END sum_indexed_partitions $$$sum_indexed_partitions.prf (|sum_indexed_partitions| (|sum_partition_TCC1| "" (ASSUMING-TCC) NIL NIL) (|sum_partition_TCC2| "" (ASSUMING-TCC) NIL NIL) (|sum_partition| "" (SKOLEM + (_ "F!1" _ "t1!1" "t2!1" "u!1")) (("" (AUTO-REWRITE "sum_emptyset" "sum" "partition" "nonempty?" "union_emptyset" "union_upper_bound") (("" (INDUCT "A" :NAME "finite_set_induction_rest[T]") (("1" (REDUCE) (("1" (REWRITE "sum_emptyset[T, real, 0, +]") NIL NIL)) NIL) ("2" (SKOSIMP*) (("2" (INST - "difference(X!1, F!1(choose(SS!1)))") (("2" (GROUND) (("1" (REWRITE "sum_diff_subset") (("1" (ASSERT) NIL NIL) ("2" (DELETE -1 2) (("2" (GRIND :EXCLUDE ("choose")) NIL NIL)) NIL)) NIL) ("2" (DELETE 2) (("2" (GROUND) (("1" (APPLY-EXTENSIONALITY :HIDE? T) (("1" (GRIND :EXCLUDE "choose") NIL NIL)) NIL) ("2" (AUTO-REWRITE "rest" "remove" "member") (("2" (REDUCE) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) $$$schedules2.pvs schedules2 [ index, job: TYPE ]: THEORY BEGIN IMPORTING schedules, sum_indexed_partitions sch: VAR schedule[job] t1, t2: VAR nat E: VAR set[job] A: VAR finite_set[index] F: VAR [index -> set[job]] i: VAR index process_time_partition: LEMMA partition(E)(A, F) IMPLIES process_time(sch, t1, t2, E) = sum(A, lambda i: process_time(sch, t1, t2, F(i))) END schedules2 $$$schedules2.prf (|schedules2| (|process_time_partition_TCC1| "" (ASSUMING-TCC) NIL NIL) (|process_time_partition_TCC2| "" (ASSUMING-TCC) NIL NIL) (|process_time_partition| "" (SKOSIMP) (("" (EXPAND "process_time") (("" (REWRITE "sum_partition") (("" (DELETE 2) (("" (GRIND) (("" (DELETE -) (("" (APPLY-EXTENSIONALITY :HIDE? T) (("" (REDUCE) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) $$$schedules3.pvs schedules3 [job: TYPE] : THEORY BEGIN IMPORTING schedules2 sch: VAR schedule[job] t1, t2: VAR nat A: VAR finite_set[job] j: VAR job process_time_finite_set: LEMMA process_time(sch, t1, t2, A) = sum(A, lambda j: process_time(sch, t1, t2, j)) END schedules3 $$$schedules3.prf (|schedules3| (|process_time_finite_set_TCC1| "" (ASSUMING-TCC) NIL NIL) (|process_time_finite_set_TCC2| "" (ASSUMING-TCC) NIL NIL) (|process_time_finite_set| "" (SKOLEM!) (("" (EXPAND "process_time" 1 2) (("" (REWRITE "process_time_partition") (("" (DELETE 2) (("" (GRIND) (("" (APPLY-EXTENSIONALITY :HIDE? T) (("" (REDUCE) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) $$$fsets_minmax.pvs %--------------------------------------------------- % Minimum/Maximum of a function over a finite set %--------------------------------------------------- fsets_minmax [T:TYPE] : THEORY BEGIN IMPORTING finite_sets@finite_sets, finite_sets@finite_sets_inductions S: VAR finite_set[T] A, B: VAR non_empty_finite_set[T] t: VAR T f, g: VAR [T -> real] x, y: VAR real %--------------------------------------- % x is the minimum of f(t) for t in S %-------------------------------------- minimum(S, f, x): bool = (EXISTS (t: (S)): x = f(t)) AND (FORALL (t: (S)): x <= f(t)) unique_minimum: LEMMA minimum(S, f, x) AND minimum(S, f, y) IMPLIES x = y minimum_exists: LEMMA EXISTS x: minimum(A, f, x) min(A, f): { x | minimum(A, f, x) } min_prop1: LEMMA FORALL (t: (A)): min(A, f) <= f(t) min_prop2: LEMMA EXISTS (t: (A)): min(A, f) = f(t) min_def: LEMMA min(A, f) = x IFF (EXISTS (t: (A)): x = f(t)) AND (FORALL (t: (A)): x <= f(t)) min_nnreal: JUDGEMENT min(A, (f: [T -> nonneg_real])) HAS_TYPE nonneg_real min_npreal: JUDGEMENT min(A, (f: [T -> nonpos_real])) HAS_TYPE nonpos_real min_posreal: JUDGEMENT min(A, (f: [T -> posreal])) HAS_TYPE posreal min_negreal: JUDGEMENT min(A, (f: [T -> negreal])) HAS_TYPE negreal min_rat: JUDGEMENT min(A, (f: [T -> rat])) HAS_TYPE rat min_nnrat: JUDGEMENT min(A, (f: [T -> nonneg_rat])) HAS_TYPE nonneg_rat min_nprat: JUDGEMENT min(A, (f: [T -> nonpos_rat])) HAS_TYPE nonpos_rat min_posrat: JUDGEMENT min(A, (f: [T -> posrat])) HAS_TYPE posrat min_negrat: JUDGEMENT min(A, (f: [T -> negrat])) HAS_TYPE negrat min_int: JUDGEMENT min(A, (f: [T -> int])) HAS_TYPE int min_nat: JUDGEMENT min(A, (f: [T -> nat])) HAS_TYPE nat min_npint: JUDGEMENT min(A, (f: [T -> nonpos_int])) HAS_TYPE nonpos_int min_posnat: JUDGEMENT min(A, (f: [T -> posnat])) HAS_TYPE posnat min_negint: JUDGEMENT min(A, (f: [T -> negint])) HAS_TYPE negint %--------------------------------------- % x is the maximum of f(t) for t in S %-------------------------------------- maximum(S, f, x): bool = (EXISTS (t: (S)): x = f(t)) AND (FORALL (t: (S)): f(t) <= x) unique_maximum: LEMMA maximum(S, f, x) AND maximum(S, f, y) IMPLIES x = y maximum_exists: LEMMA EXISTS x: maximum(A, f, x) max(A, f): { x | maximum(A, f, x) } max_prop1: LEMMA FORALL (t: (A)): f(t) <= max(A, f) max_prop2: LEMMA EXISTS (t: (A)): max(A, f) = f(t) max_def: LEMMA max(A, f) = x IFF (EXISTS (t: (A)): x = f(t)) AND (FORALL (t: (A)): f(t) <= x) max_nnreal: JUDGEMENT max(A, (f: [T -> nonneg_real])) HAS_TYPE nonneg_real max_npreal: JUDGEMENT max(A, (f: [T -> nonpos_real])) HAS_TYPE nonpos_real max_posreal: JUDGEMENT max(A, (f: [T -> posreal])) HAS_TYPE posreal max_negreal: JUDGEMENT max(A, (f: [T -> negreal])) HAS_TYPE negreal max_rat: JUDGEMENT max(A, (f: [T -> rat])) HAS_TYPE rat max_nnrat: JUDGEMENT max(A, (f: [T -> nonneg_rat])) HAS_TYPE nonneg_rat max_nprat: JUDGEMENT max(A, (f: [T -> nonpos_rat])) HAS_TYPE nonpos_rat max_posrat: JUDGEMENT max(A, (f: [T -> posrat])) HAS_TYPE posrat max_negrat: JUDGEMENT max(A, (f: [T -> negrat])) HAS_TYPE negrat max_int: JUDGEMENT max(A, (f: [T -> int])) HAS_TYPE int max_nat: JUDGEMENT max(A, (f: [T -> nat])) HAS_TYPE nat max_npint: JUDGEMENT max(A, (f: [T -> nonpos_int])) HAS_TYPE nonpos_int max_posnat: JUDGEMENT max(A, (f: [T -> posnat])) HAS_TYPE posnat max_negint: JUDGEMENT max(A, (f: [T -> negint])) HAS_TYPE negint END fsets_minmax $$$fsets_minmax.prf (|fsets_minmax| (|unique_minimum| "" (SKOLEM!) (("" (GRIND :IF-MATCH NIL) (("" (INST - "t!2") (("" (INST - "t!1") (("" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL) (|minimum_exists| "" (SKOLEM + (_ "f!1")) (("" (INDUCT "A" :NAME "nonempty_finite_set_induct[T]") (("1" (SKOLEM!) (("1" (INST + "f!1(e!1)") (("1" (GRIND) NIL NIL)) NIL)) NIL) ("2" (SKOSIMP*) (("2" (INST + "min(x!1, f!1(e!1))") (("2" (GRIND :IF-MATCH NIL) (("1" (INST? :IF-MATCH ALL) (("1" (ASSERT) NIL NIL)) NIL) ("2" (INST?) NIL NIL) ("3" (INST? + :IF-MATCH ALL) NIL NIL) ("4" (INST? + :IF-MATCH ALL) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|min_TCC1| "" (INST + "lambda A, f: epsilon! x: minimum(A, f, x)") (("" (SKOLEM!) (("" (USE "epsilon_ax[real]") (("" (AUTO-REWRITE "minimum_exists") (("" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL) (|min_prop1| "" (SKOLEM!) (("" (TYPEPRED "min(A!1, f!1)") (("" (GRIND) NIL NIL)) NIL)) NIL) (|min_prop2| "" (SKOLEM!) (("" (TYPEPRED "min(A!1, f!1)") (("" (GRIND) NIL NIL)) NIL)) NIL) (|min_def| "" (SKOLEM!) (("" (REWRITE "minimum" :DIR RL) (("" (GROUND) (("" (TYPEPRED "min(A!1, f!1)") (("" (USE "unique_minimum") (("" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|min_nnreal| "" (SKOLEM!) (("" (USE "min_prop2") (("" (REDUCE) NIL NIL)) NIL)) NIL) (|min_npreal| "" (SKOLEM!) (("" (USE "min_prop2") (("" (REDUCE) NIL))))) (|min_posreal| "" (SKOLEM!) (("" (USE "min_prop2") (("" (REDUCE) NIL))))) (|min_negreal| "" (SKOLEM!) (("" (USE "min_prop2") (("" (REDUCE) NIL))))) (|min_rat| "" (SKOLEM!) (("" (USE "min_prop2") (("" (REDUCE) NIL))))) (|min_nnrat| "" (SKOLEM!) (("" (USE "min_prop2") (("" (REDUCE) NIL))))) (|min_nprat| "" (SKOLEM!) (("" (USE "min_prop2") (("" (REDUCE) NIL))))) (|min_posrat| "" (SKOLEM!) (("" (USE "min_prop2") (("" (REDUCE) NIL))))) (|min_negrat| "" (SKOLEM!) (("" (USE "min_prop2") (("" (REDUCE) NIL))))) (|min_int| "" (SKOLEM!) (("" (USE "min_prop2") (("" (REDUCE) NIL))))) (|min_nat| "" (SKOLEM!) (("" (USE "min_prop2") (("" (REDUCE) NIL))))) (|min_npint| "" (SKOLEM!) (("" (USE "min_prop2") (("" (REDUCE) NIL))))) (|min_posnat| "" (SKOLEM!) (("" (USE "min_prop2") (("" (REDUCE) NIL))))) (|min_negint| "" (SKOLEM!) (("" (USE "min_prop2") (("" (REDUCE) NIL))))) (|unique_maximum| "" (SKOLEM!) (("" (GRIND :IF-MATCH NIL) (("" (INST - "t!2") (("" (INST - "t!1") (("" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL) (|maximum_exists| "" (SKOLEM + (_ "f!1")) (("" (INDUCT "A" :NAME "nonempty_finite_set_induct[T]") (("1" (SKOLEM!) (("1" (INST + "f!1(e!1)") (("1" (GRIND) NIL NIL)) NIL)) NIL) ("2" (SKOSIMP*) (("2" (INST + "max(x!1, f!1(e!1))") (("2" (GRIND :IF-MATCH NIL) (("1" (INST? :IF-MATCH ALL) (("1" (ASSERT) NIL NIL)) NIL) ("2" (INST?) NIL NIL) ("3" (INST? + :IF-MATCH ALL) NIL NIL) ("4" (INST? + :IF-MATCH ALL) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|max_TCC1| "" (INST + "lambda A, f: epsilon! x: maximum(A, f, x)") (("" (AUTO-REWRITE "maximum_exists") (("" (SKOLEM!) (("" (USE "epsilon_ax[real]") (("" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL) (|max_prop1| "" (SKOLEM!) (("" (TYPEPRED "max(A!1, f!1)") (("" (GRIND) NIL NIL)) NIL)) NIL) (|max_prop2| "" (SKOLEM!) (("" (TYPEPRED "max(A!1, f!1)") (("" (GRIND) NIL NIL)) NIL)) NIL) (|max_def| "" (SKOLEM!) (("" (REWRITE "maximum" :DIR RL) (("" (GROUND) (("" (TYPEPRED "max(A!1, f!1)") (("" (USE "unique_maximum") (("" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|max_nnreal| "" (SKOLEM!) (("" (USE "max_prop2") (("" (REDUCE) NIL))))) (|max_npreal| "" (SKOLEM!) (("" (USE "max_prop2") (("" (REDUCE) NIL))))) (|max_posreal| "" (SKOLEM!) (("" (USE "max_prop2") (("" (REDUCE) NIL))))) (|max_negreal| "" (SKOLEM!) (("" (USE "max_prop2") (("" (REDUCE) NIL))))) (|max_rat| "" (SKOLEM!) (("" (USE "max_prop2") (("" (REDUCE) NIL))))) (|max_nnrat| "" (SKOLEM!) (("" (USE "max_prop2") (("" (REDUCE) NIL))))) (|max_nprat| "" (SKOLEM!) (("" (USE "max_prop2") (("" (REDUCE) NIL))))) (|max_posrat| "" (SKOLEM!) (("" (USE "max_prop2") (("" (REDUCE) NIL))))) (|max_negrat| "" (SKOLEM!) (("" (USE "max_prop2") (("" (REDUCE) NIL))))) (|max_int| "" (SKOLEM!) (("" (USE "max_prop2") (("" (REDUCE) NIL))))) (|max_nat| "" (SKOLEM!) (("" (USE "max_prop2") (("" (REDUCE) NIL))))) (|max_npint| "" (SKOLEM!) (("" (USE "max_prop2") (("" (REDUCE) NIL))))) (|max_posnat| "" (SKOLEM!) (("" (USE "max_prop2") (("" (REDUCE) NIL))))) (|max_negint| "" (SKOLEM!) (("" (USE "max_prop2") (("" (REDUCE) NIL)))))) $$$ceiling_equations.pvs %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Equations of the form % % % % Sum C_i * ceiling(x/T_i) + B = x % % % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% ceiling_equations[U: TYPE] : THEORY BEGIN IMPORTING fsets_sum[U], fsets_minmax[U] %% IMPORTING fsets_sum, fsets_minmax sould work but judgements are not visible i: VAR U A: VAR finite_set[U] E: VAR non_empty_finite_set[U] C, T: VAR [U -> posreal] B: VAR nonneg_real x, y: VAR nonneg_real c, z, w: VAR posreal n, m: VAR nat %---------------------------------- % F(C, T, x): a term in the sum %---------------------------------- F(C, T, x)(i): nonneg_real = C(i) * ceiling(x / T(i)) low_F1: LEMMA x * (C(i) / T(i)) <= F(C, T, x)(i) low_F2: LEMMA C(i) <= F(C, T, z)(i) high_F: LEMMA F(C, T, x)(i) < C(i) + x * (C(i) / T(i)) increasing_F: LEMMA x <= y IMPLIES F(C, T, x)(i) <= F(C, T, y)(i) increasing_F2: LEMMA x <= y IMPLIES F(C, T, x)(i) = F(C, T, y)(i) OR F(C, T, x)(i) + C(i) <= F(C, T, y)(i) F_zero: LEMMA F(C, T, 0)(i) = 0 F_posreal: JUDGEMENT F(C, T, z) HAS_TYPE [U -> posreal] %------------------------------------- % G(A, C, T, x): the sum for i in A %------------------------------------- G(A, C, T, x): nonneg_real = sum(A, F(C, T, x)) low_G1: LEMMA x * sum(A, lambda i: C(i)/T(i)) <= G(A, C, T, x) low_G2: LEMMA sum(A, C) <= G(A, C, T, z) high_G1: LEMMA G(A, C, T, x) <= x * sum(A, lambda i: C(i)/T(i)) + sum(A, C) high_G2: LEMMA not empty?(A) IMPLIES G(A, C, T, x) < x * sum(A, lambda i: C(i)/T(i)) + sum(A, C) increasing_G: LEMMA x <= y IMPLIES G(A, C, T, x) <= G(A, C, T, y) increasing_G2: LEMMA x <= y IMPLIES G(A, C, T, x) = G(A, C, T, y) OR (EXISTS i: A(i) AND G(A, C, T, x) + C(i) <= G(A, C, T, y)) G_zero: LEMMA G(A, C, T, 0) = 0 G_empty: LEMMA empty?(A) IMPLIES G(A, C, T, x) = 0 G_posreal: JUDGEMENT G(E, C, T, z) HAS_TYPE posreal %--------------------------------- % u(0) = B + sum(E, C) % u(n+1) = B + G(E, C, T, u(n)) %--------------------------------- u(E, B, C, T)(n): RECURSIVE posreal = IF n=0 THEN B + sum(E, C) ELSE B + G(E, C, T, u(E, B, C, T)(n - 1)) ENDIF MEASURE n increasing_u1: LEMMA u(E, B, C, T)(n) <= u(E, B, C, T)(n + 1) increasing_u2: LEMMA u(E, B, C, T)(n) = u(E, B, C, T)(n+1) OR EXISTS i: E(i) AND u(E, B, C, T)(n) + C(i) <= u(E, B, C, T)(n + 1) increasing_u3: LEMMA n <= m IMPLIES u(E, B, C, T)(n) <= u(E, B, C, T)(m) fixed_point: LEMMA (EXISTS n: u(E, B, C, T)(n + 1) = u(E, B, C, T)(n)) OR (EXISTS c: FORALL n: u(E, B, C, T)(n) >= n * c + B + sum(E, C)) least_fixed_point: LEMMA B + G(E, C, T, z) = z IMPLIES FORALL n: u(E, B, C, T)(n) <= z fixed_point_prop: LEMMA z < u(E, B, C, T)(n) IMPLIES z < B + G(E, C, T, z) %-------------------------- % Existence of solutions %-------------------------- upper_bound1: LEMMA sum(E, lambda i: C(i)/T(i)) < 1 IMPLIES EXISTS z: G(E, C, T, z) + B <= z upper_bound2: LEMMA sum(E, lambda i: C(i)/T(i)) < 1 IMPLIES EXISTS z: FORALL n: u(E, B, C, T)(n) <= z fixed_point_exists: LEMMA sum(E, lambda i: C(i)/T(i)) < 1 IMPLIES EXISTS n: u(E, B, C, T)(n + 1) = u(E, B, C, T)(n) %-------------------- % Main results %-------------------- solution_exists: LEMMA sum(E, lambda i: C(i)/T(i)) < 1 IMPLIES EXISTS z: G(E, C, T, z) + B = z smallest_solution: LEMMA sum(E, lambda i: C(i)/T(i)) < 1 IMPLIES EXISTS z: G(E, C, T, z) + B = z AND FORALL w: G(E, C, T, w) + B = w IMPLIES z <= w smallest_solution2: LEMMA sum(E, lambda i: C(i)/T(i)) < 1 IMPLIES EXISTS z: G(E, C, T, z) + B = z AND (FORALL w: G(E, C, T, w) + B <= w IMPLIES z <= w) %--------------------------------------------------- % Case when C(i) and T(i) are posnat and B is nat %--------------------------------------------------- C1, T1: VAR [U -> posnat] B1: VAR nat q: VAR posnat integer_solution: LEMMA sum(E, lambda i: C1(i)/T1(i)) < 1 IMPLIES EXISTS q: G(E, C1, T1, q) + B1 = q smallest_int_solution: LEMMA sum(E, lambda i: C1(i)/T1(i)) < 1 IMPLIES EXISTS q: G(E, C1, T1, q) + B1 = q AND FORALL w: G(E, C1, T1, w) + B1 = w IMPLIES q <= w smallest_int_solution2: LEMMA sum(E, lambda i: C1(i)/T1(i)) < 1 IMPLIES EXISTS q: G(E, C1, T1, q) + B1 = q AND (FORALL w: G(E, C1, T1, w) + B1 <= w IMPLIES q <= w) END ceiling_equations $$$ceiling_equations.prf (|ceiling_equations| (|low_F1| "" (EXPAND "F") (("" (SKOLEM!) (("" (USE "both_sides_times_pos_le1" ("pz" "C!1(i!1)" "x" "x!1/T!1(i!1)" "y" "ceiling(x!1 / T!1(i!1))")) (("" (ASSERT) NIL NIL)) NIL)) NIL)) NIL) (|low_F2| "" (EXPAND "F") (("" (SKOLEM!) (("" (USE "both_sides_times_pos_le2" ("pz" "C!1(i!1)" "x" "1" "y" "ceiling(z!1 / T!1(i!1))")) (("" (ASSERT) NIL NIL)) NIL)) NIL)) NIL) (|high_F| "" (EXPAND "F") (("" (SKOLEM!) (("" (USE "both_sides_times_pos_lt1" ("pz" "C!1(i!1)" "x" "ceiling(x!1/T!1(i!1))" "y" "1 + x!1 / T!1(i!1)")) (("" (ASSERT) NIL NIL)) NIL)) NIL)) NIL) (|increasing_F| "" (EXPAND "F") (("" (SKOSIMP) (("" (REWRITE "both_sides_times_pos_le2") (("" (USE "both_sides_div_pos_le1" ("y" "y!1")) (("" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL) (|increasing_F2| "" (EXPAND "F") (("" (SKOSIMP) (("" (REWRITE "both_sides_times2") (("" (USE "both_sides_times_pos_le2" ("pz" "C!1(i!1)" "x" "1 + ceiling(x!1 / T!1(i!1))" "y" "ceiling(y!1 / T!1(i!1))")) (("" (USE "both_sides_div_pos_le1" ("y" "y!1")) (("" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|F_zero| "" (GRIND) NIL NIL) (|F_posreal| "" (EXPAND "F") (("" (SKOLEM!) (("" (REWRITE "pos_times_gt") (("" (ASSERT) NIL NIL)) NIL)) NIL)) NIL) (|low_G1| "" (EXPAND "G") (("" (SKOLEM!) (("" (AUTO-REWRITE "low_F1" "sum_mult") (("" (USE "sum_le" ("f" "lambda i: x!1 * (C!1(i) / T!1(i))" "g" "F(C!1, T!1, x!1)")) (("" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL) (|low_G2| "" (SKOLEM!) (("" (EXPAND "G") (("" (REWRITE "sum_le") (("" (SKOLEM!) (("" (REWRITE "low_F2") NIL NIL)) NIL)) NIL)) NIL)) NIL) (|high_G1| "" (EXPAND "G") (("" (SKOLEM!) (("" (AUTO-REWRITE "sum_mult") (("" (USE "sum_le" ("f" "F(C!1, T!1, x!1)" "g" "lambda i: x!1 * (C!1(i) / T!1(i)) + C!1(i)")) (("" (GROUND) (("1" (REWRITE "sum_distributive" :DIR RL) NIL NIL) ("2" (SKOLEM!) (("2" (USE "high_F") (("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|high_G2| "" (EXPAND "G") (("" (SKOSIMP) (("" (ASSERT) (("" (AUTO-REWRITE "sum_mult" "high_F") (("" (USE "sum_lt" ("f" "F(C!1, T!1, x!1)" "g" "lambda i: C!1(i) + x!1 * (C!1(i) / T!1(i))")) (("" (ASSERT) (("" (REWRITE "sum_distributive" :DIR RL) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|increasing_G| "" (AUTO-REWRITE "G" "sum_le" "increasing_F") (("" (REDUCE) NIL NIL)) NIL) (|increasing_G2| "" (SKOSIMP) (("" (EXPAND "G") (("" (REWRITE "sum_f_g") (("" (DELETE 2) (("" (SKOLEM!) (("" (USE "increasing_F2") (("" (GROUND) (("" (INST?) (("" (ASSERT) (("" (USE "sum_update" ("f" "F(C!1, T!1, x!1)" "t" "x!2" "c" "C!1(x!2) + F(C!1, T!1, x!1)(x!2)")) (("" (ASSERT) (("" (USE "sum_le" ("f" "F(C!1, T!1, x!1) WITH [(x!2) := F(C!1, T!1, x!1)(x!2) + C!1(x!2)]" "g" "F(C!1, T!1, y!1)")) (("" (GROUND) (("" (DELETE -1 2 3) (("" (AUTO-REWRITE "increasing_F") (("" (REDUCE) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|G_zero| "" (EXPAND "G") (("" (SKOLEM!) (("" (REWRITE "sum_zero") (("" (SKOLEM!) (("" (REWRITE "F_zero") NIL NIL)) NIL)) NIL)) NIL)) NIL) (|G_empty| "" (EXPAND "G") (("" (SKOSIMP) (("" (REWRITE "emptyset_is_empty?") (("" (REPLACE*) (("" (REWRITE "sum_emptyset") NIL NIL)) NIL)) NIL)) NIL)) NIL) (|G_posreal| "" (SKOLEM!) (("" (EXPAND "G") (("" (ASSERT) NIL NIL)) NIL)) NIL) (|u_TCC1| "" (SUBTYPE-TCC) NIL NIL) (|u_TCC2| "" (TERMINATION-TCC) NIL NIL) (|increasing_u1| "" (INDUCT-AND-REWRITE "n" 1 "u") (("1" (USE "low_G2") (("1" (ASSERT) NIL NIL)) NIL) ("2" (USE "increasing_G" ("x" "u(E!1, B!1, C!1, T!1)(j!1)" "y" "G(E!1, C!1, T!1, u(E!1, B!1, C!1, T!1)(j!1)) + B!1")) (("2" (ASSERT) NIL NIL)) NIL)) NIL) (|increasing_u2| "" (SKOSIMP) (("" (AUTO-REWRITE "u") (("" (CASE-REPLACE "n!1 = 0") (("1" (ASSERT) (("1" (CASE "EXISTS c: c <= sum(E!1, C!1) AND G(E!1, C!1, T!1, c) = sum(E!1, C!1)") (("1" (SKOSIMP) (("1" (USE "increasing_G2" ("x" "c!1" "y" "sum(E!1, C!1) + B!1")) (("1" (REDUCE) NIL NIL)) NIL)) NIL) ("2" (DELETE -1 2 3) (("2" (INST + "min(sum(E!1, C!1), min(E!1, T!1))") (("2" (AUTO-REWRITE "G" "F" "div_simp") (("2" (GROUND) (("2" (REWRITE "sum_f_g") (("2" (DELETE 2) (("2" (SKOLEM!) (("2" (CASE-REPLACE "ceiling(min(sum(E!1, C!1), min(E!1, T!1)) / T!1(x!1)) = 1") (("1" (ASSERT) NIL NIL) ("2" (DELETE 2) (("2" (USE "min_prop1" ("A" "E!1" "f" "T!1")) (("2" (USE "both_sides_div_pos_le1" ("x" "min(sum(E!1, C!1), min(E!1, T!1))" "y" "T!1(x!1)" "pz" "T!1(x!1)")) (("2" (ASSERT) (("2" (TYPEPRED "ceiling(min(sum(E!1, C!1), min(E!1, T!1)) / T!1(x!1))") (("2" (ASSERT :FLUSH? T) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (ASSERT) (("2" (USE "increasing_G2" ("x" "u(E!1, B!1, C!1, T!1)(n!1 - 1)" "y" "u(E!1, B!1, C!1, T!1)(n!1)")) (("2" (REWRITE "increasing_u1") (("2" (REDUCE) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|increasing_u3| "" (SKOSIMP) (("" (CASE "FORALL n: u(E!1, B!1, C!1, T!1)(n!1) <= u(E!1, B!1, C!1, T!1)(n!1 + n)") (("1" (ASSERT) (("1" (INST - "m!1 - n!1") (("1" (ASSERT) NIL NIL)) NIL)) NIL) ("2" (DELETE -1 2) (("2" (INDUCT "n") (("1" (ASSERT) NIL NIL) ("2" (SKOSIMP) (("2" (USE "increasing_u1" ("n" "n!1 + j!1")) (("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|fixed_point| "" (SKOSIMP) (("" (ASSERT) (("" (INST 2 "min(E!1, C!1)") (("" (INDUCT "n" 2) (("1" (AUTO-REWRITE "u") (("1" (ASSERT) NIL NIL)) NIL) ("2" (SKOSIMP) (("2" (USE "increasing_u2") (("2" (GROUND) (("1" (INST?) (("1" (ASSERT) NIL NIL)) NIL) ("2" (SKOSIMP) (("2" (USE "min_prop1") (("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|least_fixed_point| "" (SKOSIMP) (("" (INDUCT-AND-REWRITE "n" 1 "u") (("1" (USE "low_G2") (("1" (ASSERT) NIL NIL)) NIL) ("2" (USE "increasing_G" ("y" "z!1")) (("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL) (|fixed_point_prop| "" (SKOLEM + ("B!1" "C!1" "E!1" "T!1" _ "z!1")) (("" (INDUCT-AND-REWRITE "n" 1 "u") (("1" (USE "low_G2") (("1" (ASSERT) NIL NIL)) NIL) ("2" (USE "increasing_G" ("x" "u(E!1, B!1, C!1, T!1)(j!1)" "y" "z!1")) (("2" (GROUND) NIL NIL)) NIL)) NIL)) NIL) (|upper_bound1| "" (SKOSIMP) (("" (CASE "EXISTS x: x * sum(E!1, lambda i: C!1(i)/T!1(i)) + sum(E!1, C!1) + B!1 = x") (("1" (SKOLEM!) (("1" (ASSERT) (("1" (INST + "x!1") (("1" (USE "high_G1") (("1" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL) ("2" (DELETE 2) (("2" (NAME-REPLACE "a!1" "sum(E!1, LAMBDA (i: U): C!1(i) / T!1(i))") (("2" (ASSERT) (("2" (INST + "(sum(E!1, C!1) + B!1) / (1 - a!1)") (("1" (USE "div_cancel2" ("x" "sum(E!1, C!1) + B!1" "n0z" "1 - a!1")) (("1" (ASSERT) NIL NIL)) NIL) ("2" (REWRITE "pos_div_ge") (("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|upper_bound2| "" (SKOSIMP) (("" (USE "upper_bound1" ("B" "B!1")) (("" (ASSERT) (("" (SKOLEM!) (("" (INST?) (("" (INDUCT-AND-REWRITE "n" 1 "u") (("1" (USE "low_G2") (("1" (ASSERT) NIL NIL)) NIL) ("2" (USE "increasing_G" ("y" "z!1")) (("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|fixed_point_exists| "" (SKOSIMP) (("" (USE "fixed_point") (("" (GROUND) (("" (USE "upper_bound2") (("" (ASSERT) (("" (SKOSIMP*) (("" (DELETE -3 1) (("" (CASE "EXISTS n: (z!1 - B!1)/c!1 < n") (("1" (SKOLEM!) (("1" (REWRITE "div_mult_pos_lt1") (("1" (INST - "n!1") (("1" (INST - "n!1") (("1" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL) ("2" (DELETE -) (("2" (LEMMA "axiom_of_archimedes" ("x" "(z!1 - B!1) / c!1")) (("2" (SKOLEM!) (("2" (CASE "i!1 < 0") (("1" (INST + "0") (("1" (ASSERT) NIL NIL)) NIL) ("2" (ASSERT) (("2" (INST?) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|solution_exists| "" (SKOSIMP) (("" (USE "fixed_point_exists" ("B" "B!1")) (("" (AUTO-REWRITE "u") (("" (ASSERT) (("" (SKOLEM!) (("" (ASSERT) (("" (INST?) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|smallest_solution| "" (SKOSIMP) (("" (USE "fixed_point_exists" ("B" "B!1")) (("" (AUTO-REWRITE "u") (("" (ASSERT) (("" (SKOLEM!) (("" (INST?) (("" (GROUND) (("" (SKOSIMP) (("" (USE "least_fixed_point") (("" (ASSERT) (("" (INST?) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|smallest_solution2| "" (SKOSIMP) (("" (USE "fixed_point_exists" ("B" "B!1")) (("" (AUTO-REWRITE "u") (("" (ASSERT) (("" (SKOLEM!) (("" (INST?) (("" (GROUND) (("" (SKOSIMP) (("" (USE "fixed_point_prop" ("z" "w!1" "n" "n!1")) (("" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|integer_solution| "" (SKOSIMP) (("" (USE "solution_exists" ("B" "B1!1")) (("" (ASSERT) (("" (SKOLEM!) (("" (INST?) (("" (EXPAND "G") (("" (EXPAND "F") (("" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|smallest_int_solution| "" (SKOSIMP) (("" (USE "smallest_solution" ("B" "B1!1")) (("" (ASSERT) (("" (SKOSIMP) (("" (INST? +) (("1" (GROUND) NIL NIL) ("2" (EXPAND* "G" "F") (("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|smallest_int_solution2| "" (SKOSIMP) (("" (USE "smallest_solution2" ("B" "B1!1")) (("" (ASSERT) (("" (SKOSIMP) (("" (INST? +) (("1" (GROUND) NIL NIL) ("2" (EXPAND* "G" "F") (("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) $$$sum_partitions.pvs sum_partitions [ T: TYPE] : THEORY BEGIN IMPORTING sum_sequences[T] A, B, C, D, X: VAR set[T] u: VAR [nat -> T] t, t1, t2, n: VAR nat partition2(X)(A, B): bool = disjoint?(A, B) AND X = union(A, B) partition3(X)(A, B, C): bool = disjoint?(A, B) AND partition2(X)(union(A, B), C) partition4(X)(A, B, C, D): bool= disjoint?(A, B) AND disjoint?(C, D) AND partition2(X)(union(A, B), union(C, D)) sum_partition2: LEMMA partition2(X)(A, B) IMPLIES sum(u, t1, t2, X) = sum(u, t1, t2, A) + sum(u, t1, t2, B) sum_partition3: LEMMA partition3(X)(A, B, C) IMPLIES sum(u, t1, t2, X) = sum(u, t1, t2, A) + sum(u, t1, t2, B) + sum(u, t1, t2, C) sum_partition4: LEMMA partition4(X)(A, B, C, D) IMPLIES sum(u, t1, t2, X) = sum(u, t1, t2, A) + sum(u, t1, t2, B) + sum(u, t1, t2, C) + sum(u, t1, t2, D) END sum_partitions $$$sum_partitions.prf (|sum_partitions| (|sum_partition2| "" (AUTO-REWRITE "partition2" "sum_disj_union") (("" (REDUCE) NIL NIL)) NIL) (|sum_partition3| "" (AUTO-REWRITE "partition3" "partition2" "sum_disj_union") (("" (REDUCE) NIL NIL)) NIL) (|sum_partition4| "" (AUTO-REWRITE "partition4" "partition2" "sum_disj_union") (("" (REDUCE) NIL NIL)) NIL)) $$$sum_sequences.pvs sum_sequences [ T: TYPE] : THEORY BEGIN u, u1, u2: VAR [nat -> T] t, t1, t2, t3, n: VAR nat E, E1, E2: VAR set[T] %------------------------------------------------------------------------ % sum(u, t1, t2, E) = card { t | t1 <= t < t2 AND u(t) belongs to E } %------------------------------------------------------------------------ sum(u, t1, t2, E): RECURSIVE nat = IF t2 <= t1 THEN 0 ELSIF E(u(t2-1)) THEN 1 + sum(u, t1, t2-1, E) ELSE sum(u, t1, t2-1, E) ENDIF MEASURE max(t2 - t1, 0) %% Auxiliary lemmas for inductive proofs sum_init: LEMMA sum(u, t, t, E) = 0 sum_step: LEMMA sum(u, t, t + n + 1, E) = IF E(u(t + n)) THEN 1 + sum(u, t, t + n, E) ELSE sum(u, t, t + n, E) ENDIF %----------------------- % Bounds & splitting %----------------------- max_sum: LEMMA t1 <= t2 IMPLIES sum(u, t1, t2, E) <= t2 - t1 sum_zero: LEMMA sum(u, t1, t2, E) = 0 IFF FORALL t: t1 <= t AND t < t2 IMPLIES not E(u(t)) sum_full: LEMMA sum(u, t1, t2, E) = t2 - t1 IFF t1 <= t2 AND FORALL t: t1 <= t AND t < t2 IMPLIES E(u(t)) sum_split: LEMMA t1 <= t AND t <= t2 IMPLIES sum(u, t1, t, E) + sum(u, t, t2, E) = sum(u, t1, t2, E) sum_increasing: LEMMA t1 <= t2 AND t2 <= t3 IMPLIES sum(u, t1, t2, E) <= sum(u, t1, t3, E) equal_sums: LEMMA (FORALL (t | t1 <= t AND t < t2): E(u1(t)) IFF E(u2(t))) IMPLIES sum(u1, t1, t2, E) = sum(u2, t1, t2, E) %------------------------- % sum for various sets %------------------------- sum_emptyset: LEMMA sum(u, t1, t2, emptyset) = 0 sum_fullset: LEMMA t1 <= t2 IMPLIES sum(u, t1, t2, fullset) = t2 - t1 sum_disj_union: LEMMA disjoint?(E1, E2) IMPLIES sum(u, t1, t2, union(E1, E2)) = sum(u, t1, t2, E1) + sum(u, t1, t2, E2) sum_diff_subset: LEMMA subset?(E1, E2) IMPLIES sum(u, t1, t2, difference(E2, E1)) = sum(u, t1, t2, E2) - sum(u, t1, t2, E1) sum_union_inter: LEMMA sum(u, t1, t2, union(E1, E2)) + sum(u, t1, t2, intersection(E1, E2)) = sum(u, t1, t2, E1) + sum(u, t1, t2, E2) sum_complement: LEMMA t1 <= t2 IMPLIES sum(u, t1, t2, complement(E)) = t2 - t1 - sum(u, t1, t2, E) sum_subset: LEMMA subset?(E1, E2) IMPLIES sum(u, t1, t2, E1) <= sum(u, t1, t2, E2) sum_union1: LEMMA sum(u, t1, t2, E1) <= sum(u, t1, t2, union(E1, E2)) sum_union2: LEMMA sum(u, t1, t2, E2) <= sum(u, t1, t2, union(E1, E2)) sum_inter1: LEMMA sum(u, t1, t2, intersection(E1, E2)) <= sum(u, t1, t2, E1) sum_inter2: LEMMA sum(u, t1, t2, intersection(E1, E2)) <= sum(u, t1, t2, E2) END sum_sequences $$$sum_sequences.prf (|sum_sequences| (|sum_TCC1| "" (SUBTYPE-TCC) NIL NIL) (|sum_TCC2| "" (SUBTYPE-TCC) NIL NIL) (|sum_TCC3| "" (TERMINATION-TCC) NIL NIL) (|sum_TCC4| "" (SUBTYPE-TCC) NIL NIL) (|sum_init| "" (GRIND) NIL NIL) (|sum_step| "" (GRIND) NIL NIL) (|max_sum| "" (SKOSIMP) (("" (ASSERT) (("" (CASE "FORALL n: sum(u!1, t1!1, t1!1+n, E!1) <= n") (("1" (INST - "t2!1 - t1!1") (("1" (ASSERT) NIL NIL)) NIL) ("2" (DELETE -1 2) (("2" (INDUCT-AND-SIMPLIFY "n" 1 :DEFS NIL :REWRITES ("sum_init" ("sum_step"))) NIL NIL)) NIL)) NIL)) NIL)) NIL) (|sum_zero| "" (SKOLEM!) (("" (CASE "t2!1 < t1!1") (("1" (GRIND) NIL NIL) ("2" (ASSERT) (("2" (CASE "FORALL n: sum(u!1, t1!1, t1!1 + n, E!1) = 0 IFF (FORALL t: t lift[job]] sch, sch1, sch2: VAR schedule t, t1, t2, t3: VAR nat j, k: VAR job E, E1, E2, E3, E4: VAR set[job] x: VAR lift[job] %------------------------------------------------------------------------- % active(sch, j, t): j is the job active at time t in sch % idle(sch, t): no job is active at time t % % process_time(sch, t1, t2, E): time allocated to a job of E in [t1, t2[ % = card { u | t1 <= u < t2 AND active_job at time u belongs to E } % % idle_time(sch, t1, t2): idle time in [t1, t2[ % = card { u | t1 <= u < t2 AND no job is active at time u } %------------------------------------------------------------------------- active(sch, j, t): bool = sch(t) = up(j) idle(sch, t): bool = sch(t) = bottom idle_time(sch, t1, t2): nat = sum(sch, t1, t2, bottom?) process_time(sch, t1, t2, E): nat = sum(sch, t1, t2, { x | up?(x) AND E(down(x)) }) %--------------- % Properties %--------------- unique_active: LEMMA active(sch, j, t) AND active(sch, k, t) IMPLIES j = k idle_equiv: LEMMA idle(sch, t) IFF NOT EXISTS j: active(sch, j, t) total_cpu: LEMMA t1 <= t2 IMPLIES process_time(sch, t1, t2, fullset) + idle_time(sch, t1, t2) = t2 - t1 max_idle_time: LEMMA t1 <= t2 IMPLIES idle_time(sch, t1, t2) <= t2 - t1 zero_idle_time: LEMMA idle_time(sch, t1, t2) = 0 IFF FORALL t: t1 <= t AND t < t2 IMPLIES not idle(sch, t) idle_interval: LEMMA idle_time(sch, t1, t2) = t2 - t1 IFF t1 <= t2 AND FORALL t: t1 <= t AND t < t2 IMPLIES idle(sch, t) split_idle_time: LEMMA t1 <= t2 AND t2 <= t3 IMPLIES idle_time(sch, t1, t2) + idle_time(sch, t2, t3) = idle_time(sch, t1, t3) increasing_idle_time: LEMMA t1 <= t2 AND t2 <= t3 IMPLIES idle_time(sch, t1, t2) <= idle_time(sch, t1, t3) equal_idle_time: LEMMA (FORALL t: t1 <= t AND t < t2 IMPLIES (idle(sch1, t) IFF idle(sch2, t))) IMPLIES idle_time(sch1, t1, t2) = idle_time(sch2, t1, t2) %------------------------------ % Properties of process_time %------------------------------ max_process_time: LEMMA t1 <= t2 IMPLIES process_time(sch, t1, t2, E) <= t2 - t1 zero_process_time: LEMMA process_time(sch, t1, t2, E) = 0 IFF FORALL t, j: t1 <= t AND t < t2 AND active(sch, j, t) IMPLIES not E(j) busy_interval: LEMMA process_time(sch, t1, t2, E) = t2 - t1 IFF t1 <= t2 AND FORALL t: t1 <= t AND t < t2 IMPLIES EXISTS j: active(sch, j, t) AND E(j) split_process_time: LEMMA t1 <= t2 AND t2 <= t3 IMPLIES process_time(sch, t1, t2, E) + process_time(sch, t2, t3, E) = process_time(sch, t1, t3, E) increasing_process_time: LEMMA t1 <= t2 AND t2 <= t3 IMPLIES process_time(sch, t1, t2, E) <= process_time(sch, t1, t3, E) equal_process_time: LEMMA (FORALL t, j: t1 <= t AND t < t2 AND E(j) IMPLIES (active(sch1, j, t) IFF active(sch2, j, t))) IMPLIES process_time(sch1, t1, t2, E) = process_time(sch2, t1, t2, E) %----------------------------------------- % Process time for various sets of jobs %----------------------------------------- process_time_emptyset: LEMMA process_time(sch, t1, t2, emptyset) = 0 process_time_subset: LEMMA subset?(E1, E2) IMPLIES process_time(sch, t1, t2, E1) <= process_time(sch, t1, t2, E2) process_time_partition2: LEMMA partition2(E)(E1, E2) IMPLIES process_time(sch, t1, t2, E) = process_time(sch, t1, t2, E1) + process_time(sch, t1, t2, E2) process_time_partition3: LEMMA partition3(E)(E1, E2, E3) IMPLIES process_time(sch, t1, t2, E) = process_time(sch, t1, t2, E1) + process_time(sch, t1, t2, E2) + process_time(sch, t1, t2, E3) process_time_partition4: LEMMA partition4(E)(E1, E2, E3, E4) IMPLIES process_time(sch, t1, t2, E) = process_time(sch, t1, t2, E1) + process_time(sch, t1, t2, E2) + process_time(sch, t1, t2, E3) + process_time(sch, t1, t2, E4) %-------------------------------------- % Abbreviations for sums from 0 to t % and for sums over singleton sets %-------------------------------------- process_time(sch, t, E): nat = process_time(sch, 0, t, E) process_time(sch, t1, t2, j): nat = process_time(sch, t1, t2, singleton(j)) process_time(sch, t, j): nat = process_time(sch, t, singleton(j)) idle_time(sch, t): nat = idle_time(sch, 0, t) total_cpu2: LEMMA process_time(sch, t, fullset) + idle_time(sch, t) = t process_time_equiv1: LEMMA t1 <= t2 IMPLIES process_time(sch, t1, t2, E) = process_time(sch, t2, E) - process_time(sch, t1, E) process_time_equiv2: LEMMA t1 <= t2 IMPLIES process_time(sch, t1, t2, j) = process_time(sch, t2, j) - process_time(sch, t1, j) idle_time_equiv: LEMMA t1 <= t2 IMPLIES idle_time(sch, t1, t2) = idle_time(sch, t2) - idle_time(sch, t1) %----------------------------------------- % Next value of process_time(sch, t, j) %----------------------------------------- process_time_init: LEMMA process_time(sch, 0, j) = 0 process_time_step: LEMMA process_time(sch, t+1, j) = IF active(sch, j, t) THEN 1 + process_time(sch, t, j) ELSE process_time(sch, t, j) ENDIF process_time_init2: LEMMA process_time(sch, t, t, j) = 0 process_time_step2: LEMMA t1 <= t2 IMPLIES process_time(sch, t1, t2 +1, j) = IF active(sch, j, t2) THEN 1 + process_time(sch, t1, t2, j) ELSE process_time(sch, t1, t2, j) ENDIF %-------------------------------------------------- % Schedule constructed from act(j, t) predicate %-------------------------------------------------- act: VAR { p: [job, nat -> bool] | FORALL j, k, t: p(j, t) AND p(k, t) => j = k } sched(act): schedule = lambda t: IF EXISTS j: act(j, t) THEN up(epsilon! j: act(j, t)) ELSE bottom ENDIF schedule_from_act1: LEMMA active(sched(act), j, t) IFF act(j, t) schedule_from_act2: LEMMA idle(sched(act), t) IFF NOT EXISTS j: act(j, t) END schedules $$$schedules.prf (|schedules| (|unique_active| "" (EXPAND "active") (("" (SKOSIMP) (("" (ASSERT) (("" (CASE "down(up(j!1)) = k!1") (("1" (ASSERT) NIL NIL) ("2" (REPLACE*) (("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|idle_equiv| "" (GRIND) (("" (INST + "down(sch!1(t!1))") (("" (REWRITE "lift_up_eta[job]") NIL NIL)) NIL)) NIL) (|total_cpu| "" (EXPAND* "process_time" "idle_time" "fullset") (("" (SKOSIMP) (("" (CASE-REPLACE "{ x | up?(x) } = complement(bottom?)") (("1" (REWRITE "sum_complement") (("1" (ASSERT) NIL NIL)) NIL) ("2" (DELETE 2) (("2" (AUTO-REWRITE "complement" "member") (("2" (APPLY-EXTENSIONALITY :HIDE? T) (("2" (SMASH) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|max_idle_time| "" (EXPAND "idle_time") (("" (SKOSIMP) (("" (REWRITE "max_sum") NIL NIL)) NIL)) NIL) (|zero_idle_time| "" (EXPAND* "idle_time" "idle") (("" (SKOLEM!) (("" (REWRITE "sum_zero") (("" (APPLY (THEN (SMASH) (SKOSIMP) (INST?) (ASSERT))) NIL NIL)) NIL)) NIL)) NIL) (|idle_interval| "" (EXPAND* "idle_time" "idle") (("" (SKOLEM!) (("" (REWRITE "sum_full") (("" (APPLY (THEN (SMASH) (SKOSIMP) (INST?) (ASSERT))) NIL NIL)) NIL)) NIL)) NIL) (|split_idle_time| "" (EXPAND "idle_time") (("" (SKOSIMP) (("" (REWRITE "sum_split") NIL NIL)) NIL)) NIL) (|increasing_idle_time| "" (EXPAND "idle_time") (("" (SKOSIMP) (("" (REWRITE "sum_increasing") NIL NIL)) NIL)) NIL) (|equal_idle_time| "" (EXPAND* "idle_time" "idle") (("" (SKOSIMP) (("" (REWRITE "equal_sums") (("" (APPLY (THEN (SKOSIMP) (INST?) (SMASH))) NIL NIL)) NIL)) NIL)) NIL) (|max_process_time| "" (EXPAND "process_time") (("" (SKOSIMP) (("" (REWRITE "max_sum") NIL NIL)) NIL)) NIL) (|zero_process_time| "" (EXPAND* "process_time" "active") (("" (SKOLEM!) (("" (REWRITE "sum_zero") (("" (AUTO-REWRITE "lift_up_eta") (("" (APPLY (THEN (REDUCE :IF-MATCH NIL) (REDUCE))) NIL NIL)) NIL)) NIL)) NIL)) NIL) (|busy_interval| "" (EXPAND* "process_time" "active") (("" (SKOLEM!) (("" (REWRITE "sum_full") (("" (AUTO-REWRITE "lift_up_eta") (("" (APPLY (THEN (REDUCE :IF-MATCH NIL) (REDUCE))) NIL NIL)) NIL)) NIL)) NIL)) NIL) (|split_process_time| "" (EXPAND "process_time") (("" (SKOSIMP) (("" (REWRITE "sum_split") NIL NIL)) NIL)) NIL) (|increasing_process_time| "" (EXPAND "process_time") (("" (SKOSIMP) (("" (REWRITE "sum_increasing") NIL NIL)) NIL)) NIL) (|equal_process_time| "" (EXPAND* "process_time" "active") (("" (SKOSIMP) (("" (REWRITE "equal_sums") (("" (AUTO-REWRITE "lift_up_eta") (("" (DELETE 2) (("" (APPLY (THEN (REDUCE :IF-MATCH NIL) (REDUCE :POLARITY? T))) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|process_time_emptyset| "" (SKOLEM!) (("" (AUTO-REWRITE "emptyset" "sum_emptyset" "process_time") (("" (ASSERT) (("" (CASE-REPLACE "{ x | FALSE } = emptyset") (("1" (ASSERT) NIL NIL) ("2" (EXPAND "emptyset") (("2" (PROPAX) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|process_time_subset| "" (EXPAND "process_time") (("" (SKOSIMP) (("" (REWRITE "sum_subset") (("" (DELETE 2) (("" (GRIND :REWRITES ("some_or_none_some_eta")) NIL NIL)) NIL)) NIL)) NIL)) NIL) (|process_time_partition2| "" (SKOSIMP) (("" (EXPAND "process_time") (("" (REWRITE "sum_partition2") (("" (DELETE 2) (("" (GRIND) (("" (APPLY-EXTENSIONALITY :HIDE? T) (("" (REDUCE) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|process_time_partition3| "" (SKOSIMP) (("" (EXPAND "process_time") (("" (REWRITE "sum_partition3") (("" (DELETE 2) (("" (GRIND) (("" (APPLY-EXTENSIONALITY :HIDE? T) (("" (REDUCE) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|process_time_partition4| "" (SKOSIMP) (("" (EXPAND "process_time") (("" (REWRITE "sum_partition4") (("" (DELETE 2) (("" (GRIND) (("" (APPLY-EXTENSIONALITY :HIDE? T) (("" (REDUCE) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|total_cpu2| "" (EXPAND* "process_time" "idle_time") (("" (SKOSIMP) (("" (USE "total_cpu") (("" (ASSERT) NIL NIL)) NIL)) NIL)) NIL) (|process_time_equiv1| "" (EXPAND "process_time" 1 2) (("" (EXPAND "process_time" 1 3) (("" (SKOSIMP) (("" (USE "split_process_time" ("t1" "0" "t2" "t1!1" "t3" "t2!1")) (("" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL) (|process_time_equiv2| "" (EXPAND "process_time") (("" (SKOSIMP) (("" (REWRITE "process_time_equiv1") NIL NIL)) NIL)) NIL) (|idle_time_equiv| "" (EXPAND "idle_time" 1 2) (("" (EXPAND "idle_time" 1 3) (("" (SKOSIMP) (("" (USE "split_idle_time" ("t1" "0")) (("" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL) (|process_time_init| "" (GRIND) NIL NIL) (|process_time_step| "" (GRIND) (("" (APPLY-EXTENSIONALITY :HIDE? T) NIL NIL)) NIL) (|process_time_init2| "" (GRIND) NIL NIL) (|process_time_step2| "" (GRIND) (("" (APPLY-EXTENSIONALITY :HIDE? T) NIL NIL)) NIL) (|sched_TCC1| "" (EXISTENCE-TCC) NIL NIL) (|schedule_from_act1| "" (SKOLEM-TYPEPRED) (("" (EXPAND* "sched" "active") (("" (CASE "EXISTS j: true") (("1" (SMASH) (("1" (USE "epsilon_ax[job]") (("1" (GROUND) (("1" (CASE "down(up(epsilon! (j: job): act!1(j, t!1))) = j!1") (("1" (ASSERT) NIL NIL) ("2" (REPLACE*) (("2" (ASSERT) NIL NIL)) NIL) ("3" (PROPAX) NIL NIL)) NIL)) NIL)) NIL) ("2" (USE "epsilon_ax[job]") (("2" (GROUND) (("2" (INST - "j!1" "epsilon! j: act!1(j, t!1)" "t!1") (("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL) ("3" (INST? +) NIL NIL)) NIL) ("2" (INST + "j!1") NIL NIL)) NIL)) NIL)) NIL) (|schedule_from_act2| "" (EXPAND* "idle" "sched") (("" (SKOLEM!) (("" (SMASH) NIL NIL)) NIL)) NIL)) $$$precedence.pvs %%%%%%%%%%%%%%%%%%%%%%%%%% % order between jobs % %%%%%%%%%%%%%%%%%%%%%%%%%% precedence [ (IMPORTING basic_types) job: TYPE, prio: [job -> priority], dispatch: [job -> nat] ] : THEORY BEGIN j, k: VAR job A: VAR (nonempty?[job]) precedes(j, k): bool = prio(j) > prio(k) OR prio(j) = prio(k) AND dispatch(j) <= dispatch(k) topjob_exists: LEMMA EXISTS (j: (A)): FORALL (k: (A)): precedes(j, k) top(A): { j | A(j) AND FORALL (k: (A)): precedes(j, k) } topjob_maxprio: LEMMA FORALL (k: (A)): prio(k) <= prio(top(A)) topjob_dispatch: LEMMA FORALL (k: (A)): prio(k) = prio(top(A)) IMPLIES dispatch(top(A)) <= dispatch(k) END precedence $$$precedence.prf (|precedence| (|topjob_exists| "" (LEMMA "wf_nat") (("" (EXPAND "well_founded?") (("" (SKOSIMP*) (("" (INST-CP - "{ n:nat | EXISTS j: A!1(j) AND prio(j) = maxprio - n }") (("" (GROUND) (("1" (SKOSIMP* :PREDS? T) (("1" (INST -4 "{ t:nat | EXISTS j: A!1(j) AND prio(j) = maxprio - y!1 AND dispatch(j) = t }") (("1" (GROUND) (("1" (SKOSIMP* :PREDS? T) (("1" (EXPAND "precedes") (("1" (INST + "j!2") (("1" (SKOSIMP) (("1" (ASSERT) (("1" (CASE "prio(j!2) = prio(k!1)") (("1" (ASSERT) (("1" (INST - "dispatch(k!1)") (("1" (ASSERT) NIL NIL) ("2" (INST + "k!1") (("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL) ("2" (DELETE 3) (("2" (INST -7 "maxprio - prio(k!1)") (("1" (ASSERT) NIL NIL) ("2" (ASSERT) (("2" (INST + "k!1") (("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (INST + "dispatch(j!1)") (("2" (DELETE 2) (("2" (INST?) (("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (DELETE -1 2) (("2" (TYPEPRED "A!1") (("2" (GRIND :IF-MATCH NIL) (("2" (INST + "maxprio - prio(x!1)") (("1" (INST?) (("1" (ASSERT) NIL NIL)) NIL) ("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|top_TCC1| "" (INST + "lambda A: epsilon! (j: (A)): FORALL (k: (A)): precedes(j, k)") (("1" (SKOLEM!) (("1" (USE "epsilon_ax[(A!1)]") (("1" (GROUND) (("1" (REWRITE "topjob_exists") NIL NIL)) NIL) ("2" (DELETE 2) (("2" (TYPEPRED "A!1") (("2" (GRIND) NIL NIL)) NIL)) NIL)) NIL)) NIL) ("2" (GRIND) NIL NIL)) NIL) (|topjob_maxprio| "" (SKOLEM!) (("" (TYPEPRED "top(A!1)") (("" (GRIND) NIL NIL)) NIL)) NIL) (|topjob_dispatch| "" (SKOLEM!) (("" (TYPEPRED "top(A!1)") (("" (GRIND) NIL NIL)) NIL)) NIL)) $$$priority_ceiling.pvs %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Priority ceiling scheduler % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% priority_ceiling [ (IMPORTING programs) job: TYPE, prio: [job -> priority], dispatch: [job -> nat], prog: [job -> prog] ] : THEORY BEGIN ASSUMING j: VAR job s: VAR semaphore good_ceiling: ASSUMPTION member(s, resources(prog(j))) IMPLIES prio(j) <= ceil(s) good_programs: ASSUMPTION well_behaved(prog(j)) ENDASSUMING j1, j2, k: VAR job p: VAR priority n, m, t, t1, t2: VAR nat cmd: VAR command IMPORTING precedence[job, prio, dispatch] %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Resource management state: % % - for each job j: % % alloc(j) = set of semaphores held by j % % request(j) = set of semaphores j is waiting for % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% rsrc_state: TYPE = [# alloc, request: [job -> rsrc_set] #] r, r1, r2: VAR rsrc_state %------------------------------------------------------------------ % Blocking rules: % - a blocker of j is a job that owns an s of ceiling >= prio(j) % - j is blocked if it has pending requests and blockers %------------------------------------------------------------------ blk(r, j): set[job] = { k | k /= j AND EXISTS s: member(s, r`alloc(k)) AND ceil(s) >= prio(j) } blocked(r, j): bool = not empty?(blk(r, j)) AND not empty?(r`request(j)) %--------------------------------------------------- % Allocation request: P(s) by j % - allocates s to j if j has no blocker % - otherwise s is recorded as a pending request % (and j becomes blocked) %--------------------------------------------------- alloc_step(r, j, s): rsrc_state = IF empty?(blk(r, j)) THEN r WITH [ `alloc(j) := add(s, r`alloc(j)) ] ELSE r WITH [ `request(j) := add(s, r`request(j)) ] ENDIF %------------------------------------------------- % Release request: V(s) by j % - removes s from alloc(j) % (no effect if j does not own s) %------------------------------------------------- release_step(r, j, s): rsrc_state = r WITH [ `alloc(j) := remove(s, r`alloc(j)) ] %--------------------------------------------- % Wakeup(r, j): grant j's pending requests %--------------------------------------------- wakeup(r, j): rsrc_state = r WITH [ `alloc(j) := union(r`alloc(j), r`request(j)), `request(j) := emptyset ] %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Scheduler state: % % - rsrc: resource state % % - for each job j: % % pc(j) = program counter for job j % % - time: global time counter % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% sch_state: TYPE = [# rsrc: rsrc_state, pc: [j:job -> pc(prog(j))], time: nat #] q, q1, q2: VAR sch_state %-------------------------------------------------------------------- % Selection of active job in state q: % - finished(q, j): job j is completed % - ready(q, j) : j is ready to execute % - topjob(q, j) : j has highest precedence among the ready jobs % - eligible(q, j): j can be active in state q % ==> either j is a topjob and is not blocked % or j is blocking a topjob k %-------------------------------------------------------------------- finished(q, j): bool = complete(prog(j), q`pc(j)) ready(q, j): bool = dispatch(j) <= q`time AND not finished(q, j) topjob(q, j): bool = ready(q, j) AND (FORALL k: ready(q, k) IMPLIES precedes(j, k)) eligible(q, j): bool = topjob(q, j) AND not blocked(q`rsrc, j) OR (EXISTS k: topjob(q, k) AND blocked(q`rsrc, k) AND member(j, blk(q`rsrc, k))) %--------------------------------------------------- % Execution of a step by job j (requires j ready) % - update rsrc state % - increment j's pc % - increment time counter %--------------------------------------------------- run_step(r, j, cmd): rsrc_state = CASES cmd OF P(s): alloc_step(wakeup(r, j), j, s), V(s): release_step(wakeup(r, j), j, s), Step: wakeup(r, j) ENDCASES step(q, (j | ready(q, j))): sch_state = (# rsrc := run_step(q`rsrc, j, cmd(prog(j), q`pc(j))), pc := q`pc WITH [(j) := q`pc(j) + 1], time := q`time +1 #) %----------------------------- % idle_step: no job active %----------------------------- idle(q): bool = not EXISTS j: eligible(q, j) idle_step(q): sch_state = q WITH [time := q`time + 1] %------------------------------ % Existence of eligible jobs %------------------------------ topjob_maxprio: LEMMA topjob(q, j) AND ready(q, k) IMPLIES prio(k) <= prio(j) topjob_dispatch: LEMMA topjob(q, j) AND ready(q, k) AND prio(k) = prio(j) IMPLIES dispatch(j) <= dispatch(k) topjob_exists: LEMMA (EXISTS j: ready(q, j)) IMPLIES (EXISTS j: topjob(q, j)) eligible_exists: LEMMA (EXISTS j: ready(q, j)) IMPLIES (EXISTS j: eligible(q, j)) %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Invariant for type correctness % % ensures that eligible jobs are ready % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% P(q): bool = (FORALL j: union(q`rsrc`alloc(j), q`rsrc`request(j)) = needs(prog(j), q`pc(j))) AND (FORALL j: q`time <= dispatch(j) IMPLIES q`pc(j) = 0) %------------------- % Invariance of P %------------------- alloc_P: LEMMA union(alloc_step(r, j, s)`alloc(k), alloc_step(r, j, s)`request(k)) = IF j=k THEN add(s, union(r`alloc(k), r`request(k))) ELSE union(r`alloc(k), r`request(k)) ENDIF wakeup_P: LEMMA union(wakeup(r, j)`alloc(k), wakeup(r, j)`request(k)) = union(r`alloc(k), r`request(k)) release_P: LEMMA union(release_step(r, j, s)`alloc(k), release_step(r, j, s)`request(k)) = IF j=k THEN union(remove(s, r`alloc(k)), r`request(k)) ELSE union(r`alloc(k), r`request(k)) ENDIF step_P: LEMMA P(q) AND ready(q, j) IMPLIES P(step(q, j)) idle_P: LEMMA P(q) IMPLIES P(idle_step(q)) %%%%%%%%%%%%%%%%%%%%%%%%%%%% % Good states: satisfy P % %%%%%%%%%%%%%%%%%%%%%%%%%%%% good_state: NONEMPTY_TYPE = (P) g, g1, g2: VAR good_state %---------------------------------------------------- % Any job eligible in a good state is ready %---------------------------------------------------- good_prop: LEMMA needs(prog(j), g`pc(j)) = union(g`rsrc`alloc(j), g`rsrc`request(j)) alloc_not_ready: LEMMA not ready(g, j) IMPLIES empty?(g`rsrc`alloc(j)) alloc_before_dispatch: LEMMA g`time <= dispatch(j) IMPLIES empty?(g`rsrc`alloc(j)) request_not_ready: LEMMA not ready(g, j) IMPLIES empty?(g`rsrc`request(j)) request_before_dispatch: LEMMA g`time <= dispatch(j) IMPLIES empty?(g`rsrc`request(j)) eligible_ready: LEMMA eligible(g, j) IMPLIES ready(g, j) %------------------------------------------- % Ceiling of allocated/requested resource % is higher than job priority %------------------------------------------- alloc_prop1: LEMMA subset?(g`rsrc`alloc(j), resources(prog(j))) ceiling_prop1: LEMMA member(s, g`rsrc`alloc(j)) IMPLIES prio(j) <= ceil(s) alloc_prop2: LEMMA subset?(g`rsrc`request(j), resources(prog(j))) ceiling_prop2: LEMMA member(s, g`rsrc`request(j)) IMPLIES prio(j) <= ceil(s) idle_equiv: LEMMA idle(g) IFF not EXISTS j: ready(g, j) prio_blocker: LEMMA topjob(g, j) AND member(k, blk(g`rsrc, j1)) IMPLIES prio(k) <= prio(j) dispatch_blocker: LEMMA topjob(g, j) AND member(k, blk(g`rsrc, j1)) AND prio(k) = prio(j) IMPLIES dispatch(j) <= dispatch(k) %%%%%%%%%%%%%%%%%%%%%%%%%% % Transition system % %%%%%%%%%%%%%%%%%%%%%%%%%% %------------------ % initial state %------------------ init_rsrc: rsrc_state = (# alloc := lambda j: emptyset, request := lambda j: emptyset #) init_sch: good_state = (# rsrc := init_rsrc, pc := lambda j: 0, time := 0 #) %------------------------ % transition relation %------------------------ T(g1, g2): bool = (idle(g1) AND g2 = idle_step(g1)) OR (EXISTS j: eligible(g1, j) AND g2 = step(g1, j)) %------------------------------------------------------ % - transitions increment time % - jobs ready after a transition were ready before % unless they've just been dispatched %------------------------------------------------------ time_step: LEMMA T(g1, g2) IMPLIES g2`time = 1 + g1`time readiness_step: LEMMA T(g1, g2) AND ready(g2, j) AND dispatch(j) <= g1`time IMPLIES ready(g1, j) %%%%%%%%%%%%%%%%%%%%% % Main Invariants % %%%%%%%%%%%%%%%%%%%%% P2(r): bool = FORALL j, k, s: member(s, r`alloc(j)) AND prio(j) <= prio(k) AND prio(k) <= ceil(s) AND j /= k IMPLIES empty?(r`alloc(k)) P3(r): bool = FORALL j, s: member(s, r`alloc(j)) IMPLIES prio(j) <= ceil(s) Q(g): bool = FORALL j, k: ready(g, j) AND prio(k) <= prio(j) AND dispatch(j) < dispatch(k) IMPLIES empty?(g`rsrc`alloc(k)) %------------------- % Invariance of Q %------------------- init_Q: LEMMA Q(init_sch) step_Q: LEMMA Q(g1) AND T(g1, g2) IMPLIES Q(g2) %------------------------- % Induction step for P2 %------------------------- alloc_P2: LEMMA P3(r) AND P2(r) IMPLIES P2(alloc_step(r, j, s)) wakeup_P2: LEMMA P3(r) AND P2(r) AND not blocked(r, j) IMPLIES P2(wakeup(r, j)) release_P2: LEMMA P2(r) IMPLIES P2(release_step(r, j, s)) %--------------------------------- % Auxiliary results: % - blocking is intransitive % - P3 holds in good states % - eligible job is not blocked %--------------------------------- intransitive_blocking: LEMMA P2(r) AND member(j1, blk(r, k)) AND prio(j2) <= prio(k) IMPLIES NOT member(j2, blk(r, j1)) invar_P2_aux: LEMMA P3(g`rsrc) invar_P2_aux2: LEMMA P3(wakeup(g`rsrc, j)) step_P2_aux: LEMMA P2(g`rsrc) AND eligible(g, j) IMPLIES not blocked(g`rsrc, j) %-------------------- % Invariance of P2 %-------------------- init_P2: LEMMA P2(init_rsrc) step_P2: LEMMA P2(g1`rsrc) AND T(g1, g2) IMPLIES P2(g2`rsrc) %%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Consequences of P2 and Q % %%%%%%%%%%%%%%%%%%%%%%%%%%%%% %-------------------- % Mutual exclusion %--------------------- mutual_exclusion: LEMMA P2(r) AND P3(r) AND j /= k IMPLIES disjoint?(r`alloc(j), r`alloc(k)) %------------------------------------------------------------- % Job of lower priority than j that can run when j is ready %------------------------------------------------------------- blockers(r, j): set[job] = { k | member(k, blk(r, j)) AND prio(k) < prio(j) } unique_blocker: LEMMA P2(r) AND member(j1, blockers(r, k)) AND member(j2, blockers(r, k)) IMPLIES j1 = j2 blockers_in_cs: LEMMA member(k, blockers(g`rsrc, j)) IMPLIES cs(prog(k), g`pc(k), prio(j)) eligible_prio: LEMMA Q(g) AND ready(g, j) AND eligible(g, k) IMPLIES precedes(k, j) OR member(k, blockers(g`rsrc, j)) blockers_step: LEMMA Q(g1) AND ready(g1, j) AND T(g1, g2) IMPLIES subset?(blockers(g2`rsrc, j), blockers(g1`rsrc, j)) %---------------------------------------------------------------------------- % blockers(r, p): jobs of priority

= p %---------------------------------------------------------------------------- blockers(r, p): set[job] = { k | prio(k) < p AND EXISTS s: member(s, r`alloc(k)) AND ceil(s) >= p } unique_blocker2: LEMMA P2(r) AND member(j1, blockers(r, p)) AND member(j2, blockers(r, p)) IMPLIES j1 = j2 blockers_in_cs2: LEMMA member(k, blockers(g`rsrc, p)) IMPLIES cs(prog(k), g`pc(k), p) eligible_prio2: LEMMA (EXISTS j: prio(j) >= p AND ready(g, j)) AND eligible(g, k) IMPLIES prio(k) >= p OR member(k, blockers(g`rsrc, p)) blockers_step2: LEMMA (EXISTS j: prio(j) >= p AND ready(g1, j)) AND T(g1, g2) IMPLIES subset?(blockers(g2`rsrc, p), blockers(g1`rsrc, p)) END priority_ceiling $$$priority_ceiling.prf (|priority_ceiling| (|step_TCC1| "" (SUBTYPE-TCC) NIL NIL) (|step_TCC2| "" (SUBTYPE-TCC) NIL NIL) (|topjob_maxprio| "" (GRIND :EXCLUDE "ready") NIL NIL) (|topjob_dispatch| "" (GRIND :EXCLUDE "ready") NIL NIL) (|topjob_exists| "" (SKOSIMP) (("" (USE "precedence[job,prio,dispatch].topjob_exists" ("A" "{ j | ready(q!1, j) }")) (("1" (DELETE -2) (("1" (GRIND :DEFS NIL :REWRITES ("topjob") :POLARITY? T) NIL NIL)) NIL) ("2" (DELETE 2) (("2" (GRIND :EXCLUDE ("ready")) NIL NIL)) NIL)) NIL)) NIL) (|eligible_exists| "" (SKOSIMP) (("" (FORWARD-CHAIN "topjob_exists") (("" (DELETE -2) (("" (SKOLEM!) (("" (CASE "blocked(q!1`rsrc, j!1)") (("1" (ASSERT) (("1" (EXPAND* "blocked" "empty?") (("1" (SKOSIMP*) (("1" (INST + "x!1") (("1" (EXPAND "eligible") (("1" (FLATTEN) (("1" (INST?) (("1" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (ASSERT) (("2" (INST?) (("2" (EXPAND "eligible") (("2" (PROPAX) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|alloc_P| "" (SKOLEM!) (("" (APPLY-EXTENSIONALITY :HIDE? T) (("" (GRIND) NIL NIL)) NIL)) NIL) (|wakeup_P| "" (SKOLEM!) (("" (APPLY-EXTENSIONALITY :HIDE? T) (("" (GRIND) NIL NIL)) NIL)) NIL) (|release_P| "" (SKOLEM!) (("" (APPLY-EXTENSIONALITY :HIDE? T) (("" (GRIND) NIL NIL)) NIL)) NIL) (|step_P| "" (EXPAND "P") (("" (SKOSIMP) (("" (SPLIT) (("1" (DELETE -2) (("1" (AUTO-REWRITE "alloc_P" "wakeup_P" "release_P" "needs" ("step" "run_step")) (("1" (SKOSIMP) (("1" (INST - "j!2") (("1" (SMASH) (("1" (REPLACE*) (("1" (REPLACE -3 + RL) (("1" (DELETE -1 -2 -3 1) (("1" (APPLY-EXTENSIONALITY :HIDE? T) (("1" (GRIND) NIL NIL) ("2" (GRIND) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (DELETE -1) (("2" (GRIND :EXCLUDE ("finished" "run_step") :IF-MATCH NIL) (("2" (INST?) (("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|idle_P| "" (GRIND :EXCLUDE ("union" "needs")) NIL NIL) (|good_state_TCC1| "" (INST + "(# rsrc:= (# alloc:= lambda j: emptyset, request:= lambda j: emptyset #), pc:= lambda j: 0, time := 0 #)") (("1" (GRIND) (("1" (APPLY-EXTENSIONALITY :HIDE? T) NIL NIL)) NIL) ("2" (SKOLEM!) (("2" (ASSERT) NIL NIL)) NIL)) NIL) (|good_prop| "" (AUTO-REWRITE "P") (("" (REDUCE) NIL NIL)) NIL) (|alloc_not_ready| "" (GRIND :IF-MATCH NIL) (("1" (INST?) (("1" (USE "good_programs") (("1" (EXPAND "well_behaved") (("1" (REPLACE*) (("1" (REPLACE -2 - RL) (("1" (DELETE -2 -3 -4) (("1" (REDUCE) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (INST?) (("2" (INST?) (("2" (ASSERT) (("2" (REPLACE*) (("2" (ASSERT) (("2" (REWRITE "emptyset_is_empty?" :DIR RL) (("2" (DELETE -2 1) (("2" (REDUCE) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|alloc_before_dispatch| "" (GRIND) (("" (REWRITE "emptyset_is_empty?[semaphore]" :DIR RL) (("" (INST?) (("" (ASSERT) NIL NIL)) NIL)) NIL)) NIL) (|request_not_ready| "" (GRIND :IF-MATCH NIL) (("1" (INST?) (("1" (USE "good_programs") (("1" (EXPAND "well_behaved") (("1" (REPLACE*) (("1" (REPLACE -2 - RL) (("1" (DELETE -2 -3 -4) (("1" (REDUCE) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (INST?) (("2" (INST?) (("2" (ASSERT) (("2" (REPLACE*) (("2" (ASSERT) (("2" (REWRITE "emptyset_is_empty?" :DIR RL) (("2" (DELETE -2 1) (("2" (REDUCE) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|request_before_dispatch| "" (GRIND) (("" (REWRITE "emptyset_is_empty?[semaphore]" :DIR RL) (("" (INST?) (("" (ASSERT) NIL NIL)) NIL)) NIL)) NIL) (|eligible_ready| "" (EXPAND "eligible") (("" (REDUCE) (("1" (FORWARD-CHAIN "alloc_not_ready") (("1" (DELETE -2 -3 -4 1) (("1" (GRIND) NIL NIL)) NIL)) NIL) ("2" (EXPAND "topjob") (("2" (PROPAX) NIL NIL)) NIL)) NIL)) NIL) (|alloc_prop1| "" (SKOSIMP :PREDS? T) (("" (EXPAND "P") (("" (GROUND) (("" (INST?) (("" (USE "rsrc_needs4") (("" (REPLACE -2 - RL) (("" (DELETE -2 -3) (("" (GRIND :EXCLUDE ("resources")) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|ceiling_prop1| "" (SKOSIMP) (("" (REWRITE "good_ceiling") (("" (USE "alloc_prop1") (("" (GRIND :EXCLUDE "resources") NIL NIL)) NIL)) NIL)) NIL) (|alloc_prop2| "" (SKOSIMP :PREDS? T) (("" (EXPAND "P") (("" (GROUND) (("" (INST?) (("" (USE "rsrc_needs4") (("" (REPLACE -2 - RL) (("" (DELETE -2 -3) (("" (GRIND :EXCLUDE ("resources")) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|ceiling_prop2| "" (SKOSIMP) (("" (REWRITE "good_ceiling") (("" (USE "alloc_prop2") (("" (GRIND :EXCLUDE "resources") NIL NIL)) NIL)) NIL)) NIL) (|idle_equiv| "" (EXPAND "idle") (("" (SKOLEM!) (("" (GROUND) (("1" (REWRITE "eligible_exists") NIL NIL) ("2" (SKOLEM!) (("2" (INST?) (("2" (USE "eligible_ready") (("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|prio_blocker| "" (SKOSIMP) (("" (USE "topjob_maxprio") (("" (ASSERT) (("" (FORWARD-CHAIN "alloc_not_ready") (("" (DELETE -2 1 2) (("" (GRIND) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|dispatch_blocker| "" (SKOSIMP) (("" (USE "topjob_dispatch") (("" (ASSERT) (("" (FORWARD-CHAIN "alloc_not_ready") (("" (DELETE -2 -4 1 2) (("" (GRIND) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|init_sch_TCC1| "" (SUBTYPE-TCC) NIL NIL) (|init_sch_TCC2| "" (GRIND) (("" (APPLY-EXTENSIONALITY :HIDE? T) NIL NIL)) NIL) (T_TCC1 "" (SKOSIMP*) (("" (DELETE 1) (("" (FORWARD-CHAIN "eligible_ready") NIL NIL)) NIL)) NIL) (|time_step| "" (GRIND :EXCLUDE ("eligible" "run_step")) NIL NIL) (|readiness_step| "" (SKOSIMP) (("" (EXPAND "T") (("" (REDUCE) (("1" (EXPAND* "idle_step" "ready" "finished") NIL NIL) ("2" (CASE-REPLACE "j!1 = j!2") (("1" (FORWARD-CHAIN "eligible_ready") NIL NIL) ("2" (ASSERT) (("2" (EXPAND* "step" "ready" "finished" "complete") NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|init_Q| "" (GRIND) NIL NIL) (|step_Q| "" (EXPAND "Q") (("" (SKOSIMP*) (("" (USE "readiness_step" ("g1" "g1!1" "g2" "g2!1")) (("" (GROUND) (("1" (INST?) (("1" (ASSERT) (("1" (AUTO-REWRITE "idle_equiv" "T") (("1" (REDUCE) (("1" (DELETE -4 -5) (("1" (CASE-REPLACE "j!2 = k!1") (("1" (ASSERT) (("1" (DELETE +) (("1" (EXPAND "eligible") (("1" (REDUCE) (("1" (DELETE -1 -2 -4 -5 -7 -8) (("1" (GRIND) NIL NIL)) NIL) ("2" (EXPAND* "topjob" "precedes") (("2" (GROUND) (("2" (INST - "j!1") (("2" (GROUND) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (GRIND :EXCLUDE ("eligible")) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (FORWARD-CHAIN "time_step") (("2" (REWRITE "alloc_not_ready") (("2" (EXPAND "ready") (("2" (PROPAX) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|alloc_P2| "" (GRIND :IF-MATCH NIL :EXCLUDE "empty?") (("1" (DELETE -2) (("1" (EXPAND "empty?") (("1" (SKOLEM!) (("1" (INST - "k!1" "x!1") (("1" (INST - "k!1") (("1" (REDUCE) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (INST - "j!2" "k!1" "s!2") (("2" (ASSERT) NIL NIL)) NIL) ("3" (DELETE -1 -2 3) (("3" (EXPAND "empty?") (("3" (INST - "j!2") (("3" (REDUCE) NIL NIL)) NIL)) NIL)) NIL) ("4" (INST - "j!2" "k!1" "s!2") (("4" (ASSERT) NIL NIL)) NIL)) NIL) (|wakeup_P2| "" (GRIND :IF-MATCH NIL :EXCLUDE "empty?") (("1" (INST - "j!2" "k!1" "s!1") (("1" (ASSERT) NIL NIL)) NIL) ("2" (DELETE -2 -4 -5 -7) (("2" (EXPAND "empty?") (("2" (SKOLEM!) (("2" (INST - "k!1" "x!1") (("2" (INST - "k!1") (("2" (REDUCE) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("3" (DELETE -1 -2 3) (("3" (EXPAND "empty?") (("3" (INST - "j!2") (("3" (REDUCE) NIL NIL)) NIL)) NIL)) NIL) ("4" (INST - "j!2" "k!1" "s!1") (("4" (ASSERT) NIL NIL)) NIL) ("5" (INST - "j!2" "k!1" "s!1") (("5" (ASSERT) NIL NIL)) NIL) ("6" (DELETE -1 -2 -4 -6 -7 1 2) (("6" (EXPAND "empty?") (("6" (REDUCE) NIL NIL)) NIL)) NIL) ("7" (INST - "j!2" "k!1" "s!1") (("7" (ASSERT) (("7" (DELETE -1 -4 -5 -6 -7 1 2) (("7" (EXPAND "empty?") (("7" (REDUCE) NIL NIL)) NIL)) NIL)) NIL)) NIL) ("8" (INST - "j!2" "k!1" "s!1") (("8" (ASSERT) NIL NIL)) NIL)) NIL) (|release_P2| "" (GRIND :IF-MATCH NIL :EXCLUDE ("empty?")) (("1" (INST - "j!2" "k!1" "s!2") (("1" (ASSERT) NIL NIL)) NIL) ("2" (INST - "j!2" "k!1" "s!2") (("2" (ASSERT) (("2" (DELETE -2 -3 -4 -5 1 2) (("2" (EXPAND "empty?") (("2" (SKOLEM!) (("2" (ASSERT) (("2" (INST?) (("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("3" (INST - "j!2" "k!1" "s!2") (("3" (ASSERT) NIL NIL)) NIL)) NIL) (|intransitive_blocking| "" (GRIND :IF-MATCH NIL) (("" (CASE "prio(j1!1) <= prio(j2!1)") (("1" (INST - "j1!1" "j2!1" "s!1") (("1" (ASSERT) (("1" (INST?) NIL NIL)) NIL)) NIL) ("2" (INST - "j2!1" "j1!1" "s!2") (("2" (ASSERT) (("2" (INST?) NIL NIL)) NIL)) NIL)) NIL)) NIL) (|invar_P2_aux| "" (EXPAND "P3") (("" (SKOSIMP*) (("" (FORWARD-CHAIN "ceiling_prop1") NIL NIL)) NIL)) NIL) (|invar_P2_aux2| "" (SKOLEM-TYPEPRED) (("" (USE "invar_P2_aux" ("g" "g!1 WITH [rsrc := wakeup(g!1`rsrc, j!1)]")) (("" (DELETE 2) (("" (EXPAND "P") (("" (GROUND) (("" (DELETE -2) (("" (AUTO-REWRITE "wakeup_P") (("" (REDUCE) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|step_P2_aux| "" (EXPAND "eligible") (("" (REDUCE) (("" (DELETE -4) (("" (EXPAND* "blocked" "empty?") (("" (REDUCE) (("" (USE "intransitive_blocking" ("j1" "j!1")) (("" (ASSERT) (("" (DELETE -4) (("" (FORWARD-CHAIN "prio_blocker") NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|init_P2| "" (GRIND) NIL NIL) (|step_P2| "" (AUTO-REWRITE "idle_step" "alloc_P2" "wakeup_P2" "release_P2" "step_P2_aux" "invar_P2_aux" "invar_P2_aux2" ("step" "run_step" "T")) (("" (REDUCE) NIL NIL)) NIL) (|mutual_exclusion| "" (GRIND :IF-MATCH NIL) (("" (INST? -2 :IF-MATCH ALL) (("" (ASSERT) (("" (INST-CP - "j!1" "k!1" "x!1") (("" (INST - "k!1" "j!1" "x!1") (("" (REDUCE) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|unique_blocker| "" (GRIND :IF-MATCH NIL) (("" (CASE "prio(j1!1) <= prio(j2!1)") (("1" (INST - "j1!1" "j2!1" "s!1") (("1" (ASSERT) (("1" (INST?) NIL NIL)) NIL)) NIL) ("2" (INST - "j2!1" "j1!1" "s!2") (("2" (ASSERT) (("2" (INST?) NIL NIL)) NIL)) NIL)) NIL)) NIL) (|blockers_in_cs| "" (SKOSIMP) (("" (GRIND :EXCLUDE ("needs") :REWRITES ("good_prop")) NIL NIL)) NIL) (|eligible_prio| "" (SKOSIMP) (("" (CASE "topjob(g!1, k!1)") (("1" (ASSERT) (("1" (EXPAND* "topjob" "precedes") (("1" (FLATTEN) (("1" (INST?) (("1" (GROUND) NIL NIL)) NIL)) NIL)) NIL)) NIL) ("2" (ASSERT) (("2" (EXPAND "eligible") (("2" (SKOSIMP) (("2" (DELETE 1) (("2" (CASE "prio(j!1) = prio(k!1)") (("1" (ASSERT) (("1" (EXPAND "Q") (("1" (INST - "j!1" "k!1") (("1" (ASSERT) (("1" (EXPAND "precedes") (("1" (DELETE -1 -3 -4 -5 2) (("1" (GRIND) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (FORWARD-CHAIN "topjob_maxprio") (("2" (DELETE -2 -3 -4 -5) (("2" (GRIND) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|blockers_step| "" (SKOSIMP) (("" (EXPAND* "T" "subset?") (("" (REDUCE) (("1" (EXPAND "idle_step") (("1" (PROPAX) NIL NIL)) NIL) ("2" (DELETE -4) (("2" (CASE-REPLACE "j!2 = x!1") (("1" (CASE "prio(j!1) <= prio(x!1)") (("1" (ASSERT) (("1" (DELETE -2 -3 -4 -5 1) (("1" (GRIND :EXCLUDE ("blk" "step")) NIL NIL)) NIL)) NIL) ("2" (FORWARD-CHAIN "eligible_prio") (("2" (EXPAND "precedes") (("2" (GROUND) NIL NIL)) NIL)) NIL)) NIL) ("2" (FORWARD-CHAIN "eligible_ready") (("2" (ASSERT) (("2" (DELETE -1 -2 -3 -4) (("2" (EXPAND* "member" "blockers") (("2" (GROUND) (("2" (DELETE -2) (("2" (GRIND) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|unique_blocker2| "" (GRIND :IF-MATCH NIL) (("" (CASE "prio(j1!1) <= prio(j2!1)") (("1" (INST - "j1!1" "j2!1" "s!1") (("1" (ASSERT) (("1" (INST?) NIL NIL)) NIL)) NIL) ("2" (INST - "j2!1" "j1!1" "s!2") (("2" (ASSERT) (("2" (INST?) NIL NIL)) NIL)) NIL)) NIL)) NIL) (|blockers_in_cs2| "" (SKOSIMP) (("" (GRIND :EXCLUDE ("needs") :REWRITES ("good_prop")) NIL NIL)) NIL) (|eligible_prio2| "" (SKOSIMP*) (("" (GRIND :EXCLUDE ("blocked")) NIL NIL)) NIL) (|blockers_step2| "" (SKOSIMP) (("" (EXPAND* "T" "subset?" "idle_step") (("" (REDUCE) (("" (DELETE -4) (("" (CASE-REPLACE "j!2 = x!1") (("1" (USE "eligible_prio2") (("1" (GROUND) (("1" (DELETE -2 -3 -4 -5 1) (("1" (GRIND :EXCLUDE ("step")) NIL NIL)) NIL)) NIL)) NIL) ("2" (FORWARD-CHAIN "eligible_ready") (("2" (ASSERT) (("2" (DELETE -1 -2 -3 -4) (("2" (GRIND) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) $$$traces.pvs %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Traces for priority ceiling protocol % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% traces [ (IMPORTING programs) job: TYPE, prio: [job -> priority], dispatch: [job -> nat], prog: [job -> prog] ] : THEORY BEGIN ASSUMING j: VAR job s: VAR semaphore good_ceiling: ASSUMPTION member(s, resources(prog(j))) IMPLIES prio(j) <= ceil(s) good_programs: ASSUMPTION well_behaved(prog(j)) ENDASSUMING IMPORTING priority_ceiling[job, prio, dispatch, prog] j1, j2, k: VAR job p: VAR priority n, m, t, t1, t2: VAR nat g, g1, g2: VAR good_state %%%%%%%%%%%%%%% % Traces % %%%%%%%%%%%%%%% %----------------------- % Existence of traces %----------------------- next_state_exists: LEMMA EXISTS g2: T(g1, g2) tr(t): RECURSIVE good_state = IF t=0 THEN init_sch ELSE epsilon! g: T(tr(t-1), g) ENDIF MEASURE t %---------- % traces %---------- trace: NONEMPTY_TYPE = { w: [nat -> good_state] | w(0) = init_sch AND FORALL t: T(w(t), w(t+1)) } CONTAINING tr tr_is_a_trace: JUDGEMENT tr HAS_TYPE trace u, v: VAR trace init_trace: LEMMA u(0) = init_sch step_trace: LEMMA T(u(t), u(t+1)) %------------------- % Main invariants %------------------- invariance_P2: PROPOSITION FORALL t: P2(u(t)`rsrc) invariance_Q: PROPOSITION FORALL t: Q(u(t)) time_invariant: PROPOSITION FORALL t: u(t)`time = t %------------- % Clean up %------------- pc(u, j, t): pc(prog(j)) = u(t)`pc(j) finished(u, j, t): bool = finished(u(t), j) ready(u, j, t): bool = ready(u(t), j) active(u, j, t): bool = eligible(u(t), j) AND u(t+1) = step(u(t), j) blockers(u, j, t): set[job] = blockers(u(t)`rsrc, j) blockers(u, p, t): set[job] = blockers(u(t)`rsrc, p) busy(u, p, t): bool = EXISTS j: prio(j) >= p AND ready(u, j, t) busy(u, p, t1, t2): bool = FORALL t: t1 <= t AND t <= t2 IMPLIES busy(u, p, t) %------------------------------------ % Results from priority_ceiling %------------------------------------ pc_init: LEMMA pc(u, j, 0) = 0 pc_step: LEMMA pc(u, j, t+1) = IF active(u, j, t) THEN pc(u, j, t) + 1 ELSE pc(u, j, t) ENDIF pc_increasing: LEMMA t1 <= t2 IMPLIES pc(u, j, t1) <= pc(u, j, t2) pc_before_dispatch: LEMMA t <= dispatch(j) IMPLIES pc(u, j, t) = 0 active_ready: LEMMA active(u, j, t) IMPLIES ready(u, j, t) active_unique: LEMMA active(u, j, t) AND active(u, k, t) IMPLIES j = k ready_after_dispatch: LEMMA ready(u, j, t) IMPLIES dispatch(j) <= t ready_equiv: LEMMA ready(u, j, t) IFF dispatch(j) <= t AND pc(u, j, t) < length(prog(j)) ready_at_dispatch: LEMMA ready(u, j, dispatch(j)) finished_equiv: LEMMA finished(u, j, t) IFF pc(u, j, t) = length(prog(j)) finished_stable: LEMMA t1 <= t2 AND finished(u, j, t1) IMPLIES finished(u, j, t2) readiness: LEMMA (EXISTS j: ready(u, j, t)) IMPLIES (EXISTS j: active(u, j, t)) readiness_step2: LEMMA ready(u, j, t+1) AND dispatch(j) <= t IMPLIES ready(u, j, t) readiness_interval: LEMMA ready(u, j, t1) AND dispatch(j) <= t AND t <= t1 IMPLIES ready(u, j, t) active_prio: LEMMA active(u, k, t) AND ready(u, j, t) IMPLIES precedes(k, j) OR member(k, blockers(u, j, t)) active_prio2: LEMMA busy(u, p, t) AND active(u, k, t) IMPLIES prio(k) >= p OR member(k, blockers(u, p, t)) single_blocker: LEMMA member(j1, blockers(u, k, t)) AND member(j2, blockers(u, k, t)) IMPLIES j1 = j2 single_blocker2: LEMMA member(j1, blockers(u, p, t)) AND member(j2, blockers(u, p, t)) IMPLIES j1 = j2 blocker_in_cs: LEMMA member(j, blockers(u, k, t)) IMPLIES cs(prog(j), pc(u, j, t), prio(k)) blocker_in_cs2: LEMMA member(k, blockers(u, p, t)) IMPLIES cs(prog(k), pc(u, k, t), p) blocker_step: LEMMA ready(u, j, t) IMPLIES subset?(blockers(u, j, t+1), blockers(u, j, t)) blocker_step2: LEMMA busy(u, p, t) IMPLIES subset?(blockers(u, p, t+1), blockers(u, p, t)) %%%%%%%%%%%%%%%%%%%%%%%%%%% % Scheduling analysis % %%%%%%%%%%%%%%%%%%%%%%%%%%% IMPORTING schedules[job] %----------------------------- % schedule given by trace u %----------------------------- sch(u): schedule = sched(lambda j, t: active(u, j, t)) active_prop: LEMMA active(sch(u), j, t) IFF active(u, j, t) process_time1: LEMMA process_time(sch(u), t, j) = pc(u, j, t) process_time2: LEMMA t1 <= t2 IMPLIES process_time(sch(u), t1, t2, j) = pc(u, j, t2) - pc(u, j, t1) process_time_max: LEMMA process_time(sch(u), t, j) <= length(prog(j)) process_time_before_dispatch: LEMMA t <= dispatch(j) IMPLIES process_time(sch(u), t, j) = 0 process_time_at_dispatch: LEMMA process_time(sch(u), dispatch(j), j) = 0 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Blocking time for a job j % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %------------------------------------------------------- % the blocker of j is determined at j's dispatch time %------------------------------------------------------- blocker(u, j): set[job] = blockers(u, j, dispatch(j)) blockers_at_dispatch: LEMMA ready(u, j, t) IMPLIES subset?(blockers(u, j, t), blocker(u, j)) active_priority: LEMMA ready(u, j, t) AND active(u, k, t) IMPLIES precedes(k, j) OR member(k, blocker(u, j)) blockers_in_critical_section: LEMMA ready(u, j, t) AND member(k, blocker(u, j)) AND t1=dispatch(j) IMPLIES pc(u, k, t) = pc(u, k, t1) OR critical_section(prog(k), pc(u, k, t1), pc(u, k, t), prio(j)) blockers_dispatch: LEMMA member(k, blocker(u, j)) IMPLIES dispatch(k) < dispatch(j) %------------------ % Blocking for j %------------------ the_blocker(u, (j | not empty?(blocker(u, j)))): job = choose(blocker(u, j)) blocker_def: LEMMA empty?(blocker(u, j)) OR blocker(u, j) = singleton(the_blocker(u, j)) blocker_prio: LEMMA not empty?(blocker(u, j)) IMPLIES prio(the_blocker(u, j)) < prio(j) blocker_prop: LEMMA not empty?(blocker(u, j)) IMPLIES j /= the_blocker(u, j) blocking(u, j): nat = IF empty?(blocker(u, j)) THEN 0 ELSE max_cs(prog(the_blocker(u, j)), prio(j)) ENDIF blocking_time: LEMMA ready(u, j, t2) AND t1=dispatch(j) IMPLIES process_time(sch(u), t1, t2, blocker(u, j)) <= blocking(u, j) %--------------------------------------------------------------------------- % schedulable(u, j, t): j can fit in the interval [dispatch(j), t] %--------------------------------------------------------------------------- H(j): set[job] = { k | k /= j AND precedes(k, j) } schedulable(u, j, t): bool = process_time(sch(u), dispatch(j), t, H(j)) + blocking(u, j) + length(prog(j)) <= t - dispatch(j) process_time_ready_job: LEMMA ready(u, j, t2) AND t1 = dispatch(j) IMPLIES process_time(sch(u), t1, t2, j) = (t2 - t1) - process_time(sch(u), t1, t2, H(j)) - process_time(sch(u), t1, t2, blocker(u, j)) schedulable_prop: LEMMA schedulable(u, j, t) IMPLIES finished(u, j, t) %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Blocking for the set of jobs of priority >= p % % in a busy interval [t1, t2] % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% K(p): set[job] = { j | prio(j) >= p } %---------------------------------------------------------- % The blocker is determined at the start of the interval %---------------------------------------------------------- blockers_busy: LEMMA busy(u, p, t1, t2) AND t1 <= t AND t <= t2 IMPLIES subset?(blockers(u, p, t), blockers(u, p, t1)) active_priority2: LEMMA busy(u, p, t1, t2) AND t1 <= t AND t <= t2 AND active(u, j, t) IMPLIES prio(j) >= p OR member(j, blockers(u, p, t1)) blocker_in_critical_section2: LEMMA busy(u, p, t1, t2) AND member(k, blockers(u, p, t1)) AND t1 <= t AND t <= t2 IMPLIES pc(u, k, t) = pc(u, k, t1) OR critical_section(prog(k), pc(u, k, t1), pc(u, k, t), p) blocker_dispatch2: LEMMA member(k, blockers(u, p, t1)) IMPLIES dispatch(k) < t1 %--------------------- % Blocking for K(p) %--------------------- the_blocker(u, p, (t | not empty?(blockers(u, p, t)))): job = choose(blockers(u, p, t)) blocker_def2: LEMMA empty?(blockers(u, p, t)) OR blockers(u, p, t) = singleton(the_blocker(u, p, t)) blocker_prio2: LEMMA not empty?(blockers(u, p, t)) IMPLIES prio(the_blocker(u, p, t)) < p blocking(u, p, t): nat = IF empty?(blockers(u, p, t)) THEN 0 ELSE max_cs(prog(the_blocker(u, p, t)), p) ENDIF blocking_time2: LEMMA busy(u, p, t1, t2) IMPLIES process_time(sch(u), t1, t2, blockers(u, p, t1)) <= blocking(u, p, t1) %----------------------------------------------------- % Process time allocated to K(p) in a busy interval %----------------------------------------------------- process_time_busy_interval: LEMMA busy(u, p, t1, t2) AND t1 <= t2 IMPLIES process_time(sch(u), t1, t2, K(p)) = t2 - t1 - process_time(sch(u), t1, t2, blockers(u, p, t1)) busy_time2: LEMMA busy(u, p, t1, t2) AND t1 <= t2 IMPLIES process_time(sch(u), t1, t2, K(p)) >= t2 - t1 - blocking(u, p, t1) %----------------------------------------------------------------- % Relation between blocker of j and blocker of K(p) in [t1, t2] %----------------------------------------------------------------- blockers_prop: LEMMA busy(u, p, t1, t2) AND t1 <= dispatch(j) AND dispatch(j) <= t2 AND prio(j) = p IMPLIES subset?(blocker(u, j), blockers(u, p, t1)) blocking_prop: LEMMA busy(u, p, t1, t2) AND t1 <= dispatch(j) AND dispatch(j) <= t2 AND prio(j) = p IMPLIES blocking(u, j) = 0 OR blocking(u, j) = blocking(u, p, t1) END traces $$$traces.prf (|traces| (|IMP_priority_ceiling_TCC1| "" (LEMMA "good_ceiling") (("" (PROPAX) NIL NIL)) NIL) (|IMP_priority_ceiling_TCC2| "" (LEMMA "good_programs") (("" (PROPAX) NIL NIL)) NIL) (|next_state_exists| "" (AUTO-REWRITE "T" "idle_P" "step_P" "eligible_ready") (("" (SKOLEM!) (("" (CASE "idle(g1!1)") (("1" (INST + "idle_step(g1!1)") (("1" (ASSERT) NIL NIL)) NIL) ("2" (ASSERT) (("2" (EXPAND "idle") (("2" (SKOLEM!) (("2" (ASSERT) (("2" (INST + "step(g1!1, j!1)") (("2" (INST?) (("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|tr_TCC1| "" (SUBTYPE-TCC) NIL NIL) (|tr_TCC2| "" (TERMINATION-TCC) NIL NIL) (|trace_TCC1| "" (AUTO-REWRITE "tr") (("" (GROUND) (("" (SKOLEM!) (("" (USE "epsilon_ax[good_state]") (("" (ASSERT) (("" (REWRITE "next_state_exists") NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|tr_is_a_trace| "" (LEMMA "trace_TCC1") (("" (PROPAX) NIL NIL)) NIL) (|init_trace| "" (REDUCE) NIL NIL) (|step_trace| "" (REDUCE :POLARITY? T) NIL NIL) (|invariance_P2| "" (AUTO-REWRITE "init_sch" "init_P2") (("" (SKOLEM + ("u!1" _)) (("" (INDUCT "t") (("1" (ASSERT) (("1" (REWRITE "init_trace") (("1" (ASSERT) NIL NIL)) NIL)) NIL) ("2" (SKOSIMP) (("2" (USE* "step_trace" "step_P2") (("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|invariance_Q| "" (SKOLEM + ("u!1" _)) (("" (AUTO-REWRITE "init_Q" "init_trace") (("" (INDUCT "t") (("1" (ASSERT) (("1" (REWRITE "init_trace") (("1" (ASSERT) NIL NIL)) NIL)) NIL) ("2" (SKOSIMP) (("2" (USE* "step_trace" "step_Q") (("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|time_invariant| "" (AUTO-REWRITE "init_sch") (("" (INDUCT "t") (("1" (SKOLEM!) (("1" (REWRITE "init_trace") (("1" (ASSERT) NIL NIL)) NIL)) NIL) ("2" (SKOSIMP*) (("2" (INST?) (("2" (USE "step_trace") (("2" (GRIND :EXCLUDE ("idle" "eligible" "run_step")) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|active_TCC1| "" (SKOSIMP) (("" (FORWARD-CHAIN "eligible_ready") NIL NIL)) NIL) (|pc_init| "" (GRIND :EXCLUDE ("T")) NIL NIL) (|pc_step| "" (SKOLEM!) (("" (SMASH) (("1" (AUTO-REWRITE "pc" "step" "active") (("1" (REDUCE) NIL NIL)) NIL) ("2" (EXPAND "active") (("2" (USE "step_trace") (("2" (EXPAND "T") (("2" (AUTO-REWRITE "pc" "idle_step" "step") (("2" (REDUCE) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|pc_increasing| "" (SKOLEM + ("j!1" "t1!1" _ "u!1")) (("" (INDUCT-AND-REWRITE "t2" 1 "pc_init" "pc_step") (("1" (CASE-REPLACE "t1!1 = 0") (("1" (ASSERT) NIL NIL) ("2" (ASSERT) NIL NIL)) NIL) ("2" (CASE "active(u!1, j!1, j!2)") (("1" (ASSERT) NIL NIL) ("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL) (|pc_before_dispatch| "" (AUTO-REWRITE "pc" "P" "time_invariant") (("" (SKOSIMP) (("" (TYPEPRED "u!1(t!1)") (("" (REDUCE) NIL NIL)) NIL)) NIL)) NIL) (|active_ready| "" (EXPAND* "active" "ready") (("" (SKOSIMP) (("" (FORWARD-CHAIN "eligible_ready") NIL NIL)) NIL)) NIL) (|active_unique| "" (EXPAND "active") (("" (SKOSIMP) (("" (FORWARD-CHAIN "eligible_ready") (("" (ASSERT) (("" (AUTO-REWRITE "step") (("" (CASE "step(u!1(t!1), j!1)`pc(j!1) = u!1(t!1)`pc(j!1)") (("1" (ASSERT) NIL NIL) ("2" (REPLACE*) (("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|ready_after_dispatch| "" (AUTO-REWRITE "time_invariant" "ready") (("" (SKOSIMP) (("" (ASSERT) (("" (ASSERT) NIL NIL)) NIL)) NIL)) NIL) (|ready_equiv| "" (SKOLEM!) (("" (GRIND :REWRITES ("time_invariant")) NIL NIL)) NIL) (|ready_at_dispatch| "" (SKOLEM!) (("" (AUTO-REWRITE "ready_equiv" "pc_before_dispatch") (("" (ASSERT) NIL NIL)) NIL)) NIL) (|finished_equiv| "" (SKOLEM!) (("" (GRIND) NIL NIL)) NIL) (|finished_stable| "" (AUTO-REWRITE "finished_equiv") (("" (SKOSIMP) (("" (ASSERT) (("" (USE "pc_increasing" ("t2" "t2!1")) (("" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL) (|readiness| "" (SKOSIMP) (("" (EXPAND* "ready" "active") (("" (AUTO-REWRITE "idle") (("" (FORWARD-CHAIN "eligible_exists") (("" (USE "step_trace") (("" (EXPAND "T") (("" (GROUND) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|readiness_step2| "" (AUTO-REWRITE "step_trace" "time_invariant") (("" (EXPAND "ready") (("" (SKOSIMP) (("" (USE "readiness_step" ("g1" "u!1(t!1)")) (("" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL) (|readiness_interval| "" (EXPAND* "ready" "ready" "finished" "complete") (("" (AUTO-REWRITE "time_invariant" "pc") (("" (SKOSIMP) (("" (ASSERT) (("" (DELETE -1 -2) (("" (USE "pc_increasing") (("" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|active_prio| "" (EXPAND* "active" "ready" "blockers") (("" (SKOSIMP) (("" (USE "invariance_Q") (("" (FORWARD-CHAIN "eligible_prio") NIL NIL)) NIL)) NIL)) NIL) (|active_prio2| "" (EXPAND* "busy" "blockers" "active" "ready") (("" (SKOSIMP) (("" (FORWARD-CHAIN "eligible_prio2") NIL NIL)) NIL)) NIL) (|single_blocker| "" (EXPAND "blockers") (("" (SKOSIMP) (("" (AUTO-REWRITE "invariance_P2") (("" (USE "unique_blocker") (("" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL) (|single_blocker2| "" (AUTO-REWRITE "invariance_P2" "blockers") (("" (SKOSIMP) (("" (ASSERT) (("" (USE "unique_blocker2") (("" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL) (|blocker_in_cs| "" (EXPAND* "blockers" "pc") (("" (SKOSIMP) (("" (REWRITE "blockers_in_cs") NIL NIL)) NIL)) NIL) (|blocker_in_cs2| "" (AUTO-REWRITE "pc" "blockers" "time_invariant") (("" (SKOSIMP) (("" (ASSERT) (("" (FORWARD-CHAIN "blockers_in_cs2") NIL NIL)) NIL)) NIL)) NIL) (|blocker_step| "" (AUTO-REWRITE "step_trace" "invariance_Q") (("" (EXPAND* "ready" "blockers") (("" (SKOSIMP) (("" (REWRITE "blockers_step") NIL NIL)) NIL)) NIL)) NIL) (|blocker_step2| "" (EXPAND* "busy" "blockers" "ready") (("" (AUTO-REWRITE "step_trace") (("" (SKOSIMP) (("" (REWRITE "blockers_step2") NIL NIL)) NIL)) NIL)) NIL) (|sch_TCC1| "" (SKOSIMP*) (("" (USE "active_unique") (("" (ASSERT) NIL NIL)) NIL)) NIL) (|active_prop| "" (AUTO-REWRITE "sch_TCC1") (("" (SKOLEM!) (("" (EXPAND "sch") (("" (REWRITE "schedule_from_act1") NIL NIL)) NIL)) NIL)) NIL) (|process_time1| "" (INDUCT-AND-REWRITE "t" 1 "pc_init" "pc_step" ("process_time_init" "process_time_step") "active_prop") NIL NIL) (|process_time2| "" (AUTO-REWRITE "process_time_equiv2" "process_time1") (("" (REDUCE) NIL NIL)) NIL) (|process_time_max| "" (AUTO-REWRITE "process_time1" "pc") (("" (REDUCE) NIL NIL)) NIL) (|process_time_before_dispatch| "" (INDUCT-AND-REWRITE "t" 1 "process_time1" "pc_init" ("pc_step")) (("" (FORWARD-CHAIN "active_ready") (("" (FORWARD-CHAIN "ready_after_dispatch") (("" (ASSERT) NIL NIL)) NIL)) NIL)) NIL) (|process_time_at_dispatch| "" (SKOLEM!) (("" (REWRITE "process_time_before_dispatch") NIL NIL)) NIL) (|blockers_at_dispatch| "" (SKOSIMP) (("" (CASE "FORALL n: ready(u!1, j!1, n + dispatch(j!1)) IMPLIES subset?(blockers(u!1, j!1, n + dispatch(j!1)), blockers(u!1, j!1, dispatch(j!1)))") (("1" (FORWARD-CHAIN "ready_after_dispatch") (("1" (EXPAND "blocker") (("1" (ASSERT) (("1" (INST - "t!1 - dispatch(j!1)") (("1" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL) ("2" (DELETE -1 2) (("2" (AUTO-REWRITE-THEORY "sets[job]") (("2" (INDUCT "n") (("1" (REDUCE) NIL NIL) ("2" (SKOSIMP) (("2" (USE "readiness_step2") (("2" (ASSERT) (("2" (FORWARD-CHAIN "blocker_step") (("2" (ASSERT) (("2" (APPLY (THEN (SKOSIMP) (INST?) (INST?) (ASSERT))) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|active_priority| "" (SKOSIMP) (("" (FORWARD-CHAIN "active_prio") (("" (FORWARD-CHAIN "blockers_at_dispatch") (("" (APPLY (THEN (EXPAND "subset?") (INST?) (ASSERT))) NIL NIL)) NIL)) NIL)) NIL) (|blockers_in_critical_section| "" (SKOSIMP) (("" (CASE "FORALL n: ready(u!1, j!1, t1!1 + n) IMPLIES pc(u!1, k!1, t1!1 + n) = pc(u!1, k!1, t1!1) OR critical_section(prog(k!1), pc(u!1, k!1, t1!1), pc(u!1, k!1, t1!1 + n), prio(j!1))") (("1" (FORWARD-CHAIN "ready_after_dispatch") (("1" (ASSERT) (("1" (INST - "t!1 - t1!1") (("1" (ASSERT) NIL NIL)) NIL)) NIL)) NIL) ("2" (DELETE -1 2 3) (("2" (INDUCT "n") (("1" (GROUND) NIL NIL) ("2" (SKOSIMP) (("2" (CASE "ready(u!1, j!1, t1!1+j!2)") (("1" (ASSERT) (("1" (AUTO-REWRITE "pc_step") (("1" (CASE "active(u!1, k!1, j!2 + t1!1)") (("1" (ASSERT) (("1" (FORWARD-CHAIN "active_prio") (("1" (DELETE -2 -3 -4 -5 -7 1 2) (("1" (GRIND :EXCLUDE ("blk")) NIL NIL)) NIL) ("2" (FORWARD-CHAIN "blocker_in_cs") (("2" (DELETE -2 -3 -4 -6 -7 -8) (("2" (EXPAND "critical_section") (("2" (REDUCE :IF-MATCH NIL) (("2" (INST? :POLARITY? T) (("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL) ("2" (DELETE -1 -3 2 3) (("2" (USE "readiness_step2") (("2" (GROUND) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|blockers_dispatch| "" (AUTO-REWRITE "initially_not_cs2" "time_invariant") (("" (SKOSIMP) (("" (EXPAND "blocker") (("" (FORWARD-CHAIN "blocker_in_cs") (("" (EXPAND "pc") (("" (TYPEPRED "u!1(dispatch(j!1))") (("" (EXPAND "P") (("" (REDUCE) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|the_blocker_TCC1| "" (EXPAND "nonempty?") (("" (PROPAX) NIL NIL)) NIL) (|blocker_def| "" (SKOSIMP) (("" (AUTO-REWRITE "member" "singleton" "the_blocker" "nonempty?") (("" (APPLY-EXTENSIONALITY 2 :HIDE? T) (("" (SMASH) (("" (USE "single_blocker" ("t" "dispatch(j!1)")) (("" (REWRITE "blocker" :DIR RL) (("" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|blocker_prio| "" (SKOSIMP) (("" (AUTO-REWRITE "nonempty?" "the_blocker") (("" (ASSERT) (("" (TYPEPRED "choose(blocker(u!1, j!1))") (("" (AUTO-REWRITE "blocker" "blockers") (("" (ASSERT) (("" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|blocker_prop| "" (SKOSIMP) (("" (FORWARD-CHAIN "blocker_prio") (("" (ASSERT) NIL NIL)) NIL)) NIL) (|blocking_time| "" (EXPAND "blocking") (("" (SKOSIMP) (("" (USE "blocker_def") (("" (SMASH) (("1" (REWRITE "emptyset_is_empty?") (("1" (REPLACE*) (("1" (REWRITE "process_time_emptyset") (("1" (ASSERT) NIL NIL)) NIL)) NIL)) NIL) ("2" (REPLACE*) (("2" (REWRITE "process_time" :DIR RL) (("2" (FORWARD-CHAIN "ready_after_dispatch") (("2" (ASSERT) (("2" (REWRITE "process_time2") (("2" (USE "blockers_in_critical_section" ("k" "the_blocker(u!1, j!1)" "t" "t2!1" "t1" "t1!1")) (("2" (GROUND) (("1" (FORWARD-CHAIN "max_cs2") (("1" (ASSERT) NIL NIL)) NIL) ("2" (EXPAND* "member" "the_blocker") NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|process_time_ready_job| "" (SKOSIMP) (("" (FORWARD-CHAIN "ready_after_dispatch") (("" (ASSERT) (("" (AUTO-REWRITE "active_prop" "idle_equiv") (("" (EXPAND "process_time" 1 1) (("" (REPLACE -3 - RL) (("" (USE "total_cpu") (("" (ASSERT) (("" (CASE-REPLACE "idle_time(sch(u!1), t1!1, t2!1) = 0") (("1" (DELETE -1) (("1" (ASSERT) (("1" (USE "process_time_partition4" ("E" "fullset[job]" "E1" "singleton(j!1)" "E2" "H(j!1)" "E3" "blocker(u!1, j!1)" "E4" "{ k | not blocker(u!1, j!1)(k) AND not precedes(k, j!1) }")) (("1" (GROUND) (("1" (CASE-REPLACE "process_time(sch(u!1), t1!1, t2!1, {k: job | NOT blocker(u!1, j!1)(k) AND NOT precedes(k, j!1)}) = 0") (("1" (ASSERT) NIL NIL) ("2" (DELETE -1 -2 2) (("2" (REWRITE "zero_process_time") (("2" (SKOSIMP) (("2" (USE "readiness_interval" ("t" "t!1" "t1" "t2!1")) (("2" (ASSERT) (("2" (FORWARD-CHAIN "active_priority") (("2" (EXPAND "member") (("2" (PROPAX) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (DELETE -1 -2 -3 -4 2) (("2" (GRIND :EXCLUDE ("blk")) (("2" (APPLY-EXTENSIONALITY :HIDE? T) (("2" (SMASH) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (DELETE -1 2) (("2" (REWRITE "zero_idle_time") (("2" (SKOSIMP) (("2" (USE "readiness" ("t" "t!1")) (("2" (GROUND) (("2" (USE "readiness_interval" ("t" "t!1" "t1" "t2!1")) (("2" (ASSERT) (("2" (INST?) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|schedulable_prop| "" (SKOSIMP) (("" (EXPAND "schedulable") (("" (ASSERT) (("" (CASE "ready(u!1, j!1, t!1)") (("1" (ASSERT) (("1" (USE* "process_time_ready_job" "blocking_time") (("1" (ASSERT) (("1" (AUTO-REWRITE "process_time_equiv2" "process_time_at_dispatch" "ready_equiv" "process_time1") (("1" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL) ("2" (DELETE -) (("2" (AUTO-REWRITE "ready_equiv" "finished" "complete" "pc") (("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|blockers_busy| "" (SKOSIMP) (("" (CASE "FORALL n: t1!1 + n <= t2!1 IMPLIES subset?(blockers(u!1, p!1, t1!1+n), blockers(u!1, p!1, t1!1))") (("1" (ASSERT) (("1" (INST - "t!1 - t1!1") (("1" (ASSERT) NIL NIL)) NIL)) NIL) ("2" (DELETE -2 -3 2) (("2" (INDUCT "n") (("1" (GROUND) (("1" (GRIND :EXCLUDE ("blockers" "busy")) NIL NIL)) NIL) ("2" (SKOSIMP) (("2" (ASSERT) (("2" (EXPAND "busy") (("2" (INST - "t1!1 + j!1") (("2" (ASSERT) (("2" (FORWARD-CHAIN "blocker_step2") (("2" (DELETE -3 -4) (("2" (GRIND :EXCLUDE ("blockers")) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|active_priority2| "" (SKOSIMP) (("" (FORWARD-CHAIN "blockers_busy") (("" (EXPAND "busy") (("" (INST?) (("" (ASSERT) (("" (FORWARD-CHAIN "active_prio2") (("" (DELETE -3 -4 -5 -6 1) (("" (GRIND :EXCLUDE ("blockers")) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|blocker_in_critical_section2| "" (SKOSIMP) (("" (ASSERT) (("" (CASE "FORALL n: t1!1 + n <= t2!1 IMPLIES pc(u!1, k!1, t1!1 + n) = pc(u!1, k!1, t1!1) OR critical_section(prog(k!1), pc(u!1, k!1, t1!1), pc(u!1, k!1, t1!1+n), p!1)") (("1" (INST - "t!1 - t1!1") (("1" (ASSERT) NIL NIL)) NIL) ("2" (DELETE 2 3) (("2" (INDUCT "n") (("1" (GROUND) NIL NIL) ("2" (SKOSIMP) (("2" (ASSERT) (("2" (AUTO-REWRITE "pc_step") (("2" (CASE "active(u!1, k!1, j!1 + t1!1)") (("1" (ASSERT) (("1" (DELETE 1) (("1" (EXPAND "busy") (("1" (INST - "t1!1 + j!1") (("1" (ASSERT) (("1" (FORWARD-CHAIN "active_prio2") (("1" (DELETE -2 -3 -4 -5 -7 -8 1) (("1" (GRIND) NIL NIL)) NIL) ("2" (FORWARD-CHAIN "blocker_in_cs2") (("2" (DELETE -2 -3 -5 -6 -7 -8 -9) (("2" (EXPAND "critical_section") (("2" (GROUND) (("1" (SKOSIMP) (("1" (ASSERT) NIL NIL)) NIL) ("2" (SKOSIMP) (("2" (INST?) (("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|blocker_dispatch2| "" (AUTO-REWRITE "initially_not_cs2" "time_invariant") (("" (SKOSIMP) (("" (EXPAND "blockers") (("" (FORWARD-CHAIN "blockers_in_cs2") (("" (TYPEPRED "u!1(t1!1)") (("" (EXPAND "P") (("" (REDUCE) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|the_blocker_TCC2| "" (SUBTYPE-TCC) NIL NIL) (|blocker_def2| "" (SKOSIMP) (("" (ASSERT) (("" (AUTO-REWRITE "singleton" "member" "nonempty?" "the_blocker") (("" (APPLY-EXTENSIONALITY :HIDE? T) (("" (SMASH) (("" (USE "single_blocker2" ("j1" "x!1" "j2" "the_blocker(u!1, p!1, t!1)")) (("" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|blocker_prio2| "" (SKOSIMP) (("" (AUTO-REWRITE "nonempty?" "the_blocker") (("" (ASSERT) (("" (TYPEPRED "choose(blockers(u!1, p!1, t!1))") (("" (AUTO-REWRITE "blockers") (("" (ASSERT) (("" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|blocking_time2| "" (SKOLEM!) (("" (EXPAND "blocking") (("" (SMASH) (("1" (REWRITE "emptyset_is_empty?") (("1" (REPLACE*) (("1" (REWRITE "process_time_emptyset") (("1" (ASSERT) NIL NIL)) NIL)) NIL)) NIL) ("2" (CASE "t1!1 <= t2!1") (("1" (USE "blocker_def2") (("1" (REDUCE) (("1" (REWRITE "process_time" :DIR RL) (("1" (REWRITE "process_time2") (("1" (USE "blocker_in_critical_section2") (("1" (GROUND) (("1" (FORWARD-CHAIN "max_cs2") NIL NIL) ("2" (EXPAND* "the_blocker" "member") NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (AUTO-REWRITE "process_time" "sum") (("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|process_time_busy_interval| "" (SKOSIMP) (("" (USE "total_cpu") (("" (AUTO-REWRITE "active_prop" "idle_equiv") (("" (ASSERT) (("" (CASE-REPLACE "idle_time(sch(u!1), t1!1, t2!1) = 0") (("1" (DELETE -1) (("1" (ASSERT) (("1" (USE "process_time_partition3" ("E" "fullset[job]" "E1" "K(p!1)" "E2" "blockers(u!1, p!1, t1!1)" "E3" "{ k | prio(k) < p!1 AND not member(k, blockers(u!1, p!1, t1!1)) }")) (("1" (GROUND) (("1" (CASE-REPLACE "process_time(sch(u!1), t1!1, t2!1, {k: job | prio(k) < p!1 AND NOT member(k, blockers(u!1, p!1, t1!1))}) = 0") (("1" (ASSERT) NIL NIL) ("2" (DELETE -1 -2 2) (("2" (REWRITE "zero_process_time") (("2" (SKOSIMP) (("2" (USE "active_priority2" ("j" "j!1")) (("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (DELETE -1 -2 -3 2) (("2" (GRIND) (("2" (APPLY-EXTENSIONALITY :HIDE? T) (("2" (SMASH) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (DELETE -1 2) (("2" (REWRITE "zero_idle_time") (("2" (SKOSIMP) (("2" (REWRITE "readiness") (("2" (AUTO-REWRITE "busy") (("2" (REDUCE) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|busy_time2| "" (SKOSIMP) (("" (FORWARD-CHAIN "process_time_busy_interval") (("" (FORWARD-CHAIN "blocking_time2") (("" (ASSERT) NIL NIL)) NIL)) NIL)) NIL) (|blockers_prop| "" (SKOSIMP) (("" (CASE "subset?(blocker(u!1, j!1), blockers(u!1, p!1, dispatch(j!1)))") (("1" (FORWARD-CHAIN "blockers_busy") (("1" (DELETE -3 -4 -5 -6) (("1" (GRIND :EXCLUDE ("blocker" "blockers") :IF-MATCH NIL) (("1" (INST?) (("1" (INST?) (("1" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (DELETE -1 -2 -3 2) (("2" (GRIND) NIL NIL)) NIL)) NIL)) NIL) (|blocking_prop| "" (SKOSIMP) (("" (FORWARD-CHAIN "blockers_prop") (("" (EXPAND "blocking") (("" (SMASH) (("1" (DELETE -2 -3 -4 -5 2) (("1" (APPLY (THEN (GRIND :EXCLUDE ("blocker" "blockers") :IF-MATCH NIL) (INST?) (INST?) (ASSERT))) NIL NIL)) NIL) ("2" (USE* "blocker_def" "blocker_def2") (("2" (GROUND) (("1" (DELETE -1 -4 -5 -6 -7 2 3) (("1" (GRIND :IF-MATCH NIL :EXCLUDE ("blockers" "blocker")) (("1" (INST? :POLARITY? T) (("1" (INST?) (("1" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL) ("2" (REPLACE*) (("2" (DELETE -1 -2 -4 -5 -6 -7 1 2) (("2" (AUTO-REWRITE-THEORY "sets[job]") (("2" (REDUCE :IF-MATCH NIL) (("2" (INST - "the_blocker(u!1, j!1)") (("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) $$$fsets_sum.pvs %------------------------------------------------------------------------ % Finite sum over real-valued functions % (reworked from Ricky Butler's version in finite set lib) %------------------------------------------------------------------------ fsets_sum[T: TYPE]: THEORY BEGIN %% IMPORTING finite_sets@finite_sets_sum[T,real,0,+] IMPORTING finite_sets@finite_sets, finite_sets@finite_sets_inductions S, A, B: VAR finite_set[T] E: VAR non_empty_finite_set[T] t, x, x1, x2: VAR T c, N: VAR real f, g: VAR function[T -> real] %% Things below and up to sum_distributive have been %% copied from finite_set@finite_sets_sum. %% %% Shouldn't need to do that but there was a problem with %% judgements otherwise. Bug in PVS: I can't reverse the %% change? (7/19/99) %% %% Fixed by Sam (9/1/99) but still things do not work so well %% (auto-rewrite in proof of sum_indexed_partitions.sum_partition) %% %------------------------------------ % Definition and basic properties %------------------------------------ sum(S, f) : RECURSIVE real = IF (empty?(S)) THEN 0 ELSE f(choose(S)) + sum(rest(S),f) ENDIF MEASURE card(S) sum_emptyset : THEOREM sum(emptyset, f) = 0 sum_singleton : THEOREM sum(singleton(x), f) = f(x) sum_x : THEOREM FORALL (x: (S)): sum(S, f) = f(x) + sum(remove(x, S), f) sum_x1_x2 : THEOREM FORALL (x1, x2: (S)): f(x1) + sum(remove(x1, S), f) = f(x2) + sum(remove(x2, S), f) sum_add : THEOREM sum(add(x, S),f) = IF S(x) THEN sum(S, f) ELSE sum(S, f) + f(x) ENDIF sum_remove : THEOREM sum(remove(x, S),f) = IF S(x) THEN sum(S, f) - f(x) ELSE sum(S, f) ENDIF sum_rest : THEOREM NOT empty?(S) IMPLIES f(choose(S)) + sum(rest(S),f) = sum(S,f) sum_disj_union: THEOREM disjoint?(A, B) IMPLIES sum(union(A, B), f) = sum(A, f) + sum(B, f) sum_diff_subset: THEOREM subset?(A, B) IMPLIES sum(difference(B, A), f) = sum(B, f) - sum(A, f) sum_union : THEOREM sum(union(A, B), f) + sum(intersection(A, B),f ) = sum(A, f) + sum(B, f) sum_diff_intersection: THEOREM sum(A, f) = sum(difference(A, B), f) + sum(intersection(A, B), f) sum_f_g : THEOREM (FORALL (x: (S)): f(x) = g(x)) IMPLIES sum(S, f) = sum(S, g) sum_particular : THEOREM sum(S, f WITH [x := c]) = IF S(x) THEN sum(S, f) + c - f(x) ELSE sum(S, f) ENDIF sum_distributive: THEOREM sum(A, f) + sum(A, g) = sum(A, LAMBDA x: f(x) + g(x)) %--------------------------- % Sum for a few functions %--------------------------- sum_const : THEOREM sum(S, (LAMBDA t: c)) = c*card(S) sum_mult : THEOREM sum(S,(LAMBDA t: c*f(t))) = c*sum(S,f) sum_1_is_card: THEOREM sum(S,(LAMBDA t: 1)) = card(S) sum_update : THEOREM sum(S, f WITH [(t) := c]) = IF S(t) THEN sum(S, f) - f(t) + c ELSE sum(S, f) ENDIF %------------------------------------------------------ % Ordering properties for two sums over the same set %------------------------------------------------------ sum_le : THEOREM (FORALL (t: (S)): f(t) <= g(t)) IMPLIES sum(S, f) <= sum(S, g) sum_ge : THEOREM (FORALL (t: (S)): f(t) >= g(t)) IMPLIES sum(S, f) >= sum(S, g) sum_lt : THEOREM (FORALL (t: (E)): f(t) < g(t)) IMPLIES sum(E, f) < sum(E, g) sum_gt : THEOREM (FORALL (t: (E)): f(t) > g(t)) IMPLIES sum(E, f) > sum(E, g) %------------------------------------------------ % Bounds on sum derived from bounds of f on S %------------------------------------------------ sum_bound : THEOREM (FORALL (t: (S)): f(t) <= N) IMPLIES sum(S,f) <= N*card(S) sum_bound2 : THEOREM (FORALL (t: (S)): f(t) >= N) IMPLIES sum(S,f) >= N*card(S) sum_bound3 : THEOREM (FORALL (t: (E)): f(t) < N) IMPLIES sum(E,f) < N*card(E) sum_bound4 : THEOREM (FORALL (t: (E)): f(t) > N) IMPLIES sum(E,f) > N*card(E) %--------------------- % Sign of sum(S, f) %--------------------- sum_nonneg : LEMMA (FORALL (t: (S)): f(t) >= 0) IMPLIES sum(S,f) >= 0 sum_nonpos : LEMMA (FORALL (t: (S)): f(t) <= 0) IMPLIES sum(S,f) <= 0 sum_pos : LEMMA (FORALL (t: (S)): f(t) >= 0) AND (EXISTS (t: (S)): f(t) > 0) IMPLIES sum(S, f) > 0 sum_pos2 : LEMMA (FORALL (t: (E)): f(t) > 0) IMPLIES sum(E,f) > 0 sum_neg : LEMMA (FORALL (t: (S)): f(t) <= 0) AND (EXISTS (t: (S)): f(t) < 0) IMPLIES sum(S, f) < 0 sum_neg2 : LEMMA (FORALL (t: (E)): f(t) < 0) IMPLIES sum(E,f) < 0 sum_zero : LEMMA (FORALL (t: (S)): f(t) = 0) IMPLIES sum(S, f) = 0 %----------------------- % Closure properties %----------------------- U: VAR set[real] sum_closure1: LEMMA (FORALL (a, b: (U)): U(a+b)) AND (FORALL (t: (E)): U(f(t))) IMPLIES U(sum(E, f)) sum_closure2: LEMMA U(0) AND (FORALL (a, b: (U)): U(a+b)) AND (FORALL (t: (S)): U(f(t))) IMPLIES U(sum(S, f)) %--------------- % Judgements %--------------- nnf: VAR [T -> nonneg_real] npf: VAR [T -> nonpos_real] pf: VAR [T -> posreal] nf: VAR [T -> negreal] sum_nnreal_is_nnreal: JUDGEMENT sum(S, nnf) HAS_TYPE nonneg_real sum_npreal_is_npreal: JUDGEMENT sum(S, npf) HAS_TYPE nonpos_real sum_posreal_is_posreal: JUDGEMENT sum(E, pf) HAS_TYPE posreal sum_negreal_is_negreal: JUDGEMENT sum(E, nf) HAS_TYPE negreal u: VAR [T -> rat] nnu: VAR [T -> nonneg_rat] npu: VAR [T -> nonpos_rat] pu: VAR [T -> posrat] nu: VAR [T -> negrat] sum_rat_is_rat: JUDGEMENT sum(S, u) HAS_TYPE rat sum_nnrat_is_nnrat: JUDGEMENT sum(S, nnu) HAS_TYPE nonneg_rat sum_nprat_is_nprat: JUDGEMENT sum(S, npu) HAS_TYPE nonpos_rat sum_posrat_is_posrat: JUDGEMENT sum(E, pu) HAS_TYPE posrat sum_negrat_is_negrat: JUDGEMENT sum(E, nu) HAS_TYPE negrat v: VAR [T -> int] npv: VAR [T -> nonpos_int] nv: VAR [T -> negint] sum_int_is_int: JUDGEMENT sum(S, v) HAS_TYPE int sum_npint_is_npint: JUDGEMENT sum(S, npv) HAS_TYPE nonpos_int sum_negint_is_negint: JUDGEMENT sum(E, nv) HAS_TYPE negint w: VAR [T -> nat] pw: VAR [T -> posnat] sum_nat_is_nat: JUDGEMENT sum(S, w) HAS_TYPE nat sum_posnat_is_posnat: JUDGEMENT sum(E, pw) HAS_TYPE posnat %------------------------------------------------------- % Properties of f derived from the value of Sum(S, f) %------------------------------------------------------- sum_max_bound : THEOREM sum(S,f) = N * card(S) AND (FORALL (t: (S)): f(t) <= N) IMPLIES (FORALL (t: (S)): f(t) = N) sum_min_bound : THEOREM sum(S,f) = N * card(S) AND (FORALL (t: (S)): f(t) >= N) IMPLIES (FORALL (t: (S)): f(t) = N) sum_0_non_neg : THEOREM sum(S,f) = 0 AND (FORALL (t: (S)): f(t) >= 0) IMPLIES (FORALL (t: (S)): f(t) = 0) sum_0_non_pos : THEOREM sum(S,f) = 0 AND (FORALL (t: (S)): f(t) <= 0) IMPLIES (FORALL (t: (S)): f(t) = 0) equal_sum_le : THEOREM sum(S, f) = sum(S, g) AND (FORALL (t: (S)): f(t) <= g(t)) IMPLIES (FORALL (t: (S)): f(t) = g(t)) equal_sum_ge : THEOREM sum(S, f) = sum(S, g) AND (FORALL (t: (S)): f(t) >= g(t)) IMPLIES (FORALL (t: (S)): f(t) = g(t)) h, h1, h2: VAR function[T -> nonneg_real] sum_0_non_neg2 : COROLLARY sum(S, h) = 0 IMPLIES (FORALL (t : (S)) : h(t) = 0) k, k1, k2: VAR function[T -> nonpos_real] sum_0_non_pos2 : COROLLARY sum(S, k) = 0 IMPLIES (FORALL (t : (S)) : k(t) = 0) %-------------------------------------------------- % Some relations between Sum(A, f) AND Sum(B, f) % when A is a subset of B %-------------------------------------------------- sum_subset: THEOREM subset?(A, B) IMPLIES sum(A, h) <= sum(B, h) sum_subset2: THEOREM subset?(A, B) IMPLIES sum(A, k) >= sum(B, k) sum_order_sub: THEOREM subset?(A, B) AND (FORALL (t:T): h1(t) <= h2(t)) IMPLIES sum(A, h1) <= sum(B, h2) sum_order_sub2: THEOREM subset?(A, B) AND (FORALL (t:T): k1(t) >= k2(t)) IMPLIES sum(A, k1) >= sum(B, k2) sum_subset3: THEOREM subset?(A, B) AND (FORALL (t: (B)): A(t) OR f(t) = 0) IMPLIES sum(A, f) = sum(B, f) END fsets_sum $$$fsets_sum.prf (|fsets_sum| (|sum_TCC1| "" (GRIND) NIL NIL) (|sum_TCC2| "" (AUTO-REWRITE "nonempty?" "card_rest") (("" (SKOSIMP) (("" (ASSERT) NIL NIL)) NIL)) NIL) (|sum_TCC3| "" (TERMINATION-TCC)) (|sum_emptyset| "" (GRIND) NIL NIL) (|sum_singleton_TCC1| "" (SUBTYPE-TCC)) (|sum_singleton| "" (AUTO-REWRITE "singleton" "sum_emptyset" "nonempty?") (("" (SKOLEM!) (("" (EXPAND "sum") (("" (CASE "empty?(singleton(x!1))") (("1" (DELETE +) (("1" (GRIND) NIL NIL)) NIL) ("2" (ASSERT) (("2" (TYPEPRED "choose(singleton(x!1))") (("2" (CASE-REPLACE "rest(singleton(x!1)) = emptyset") (("1" (REDUCE) NIL NIL) ("2" (DELETE 3) (("2" (APPLY-EXTENSIONALITY :HIDE? T) (("2" (GRIND :EXCLUDE ("empty?" "choose")) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|sum_x_TCC1| "" (SUBTYPE-TCC)) (|sum_x| "" (SKOLEM + (_ "f!1" _)) (("" (AUTO-REWRITE "sum" "nonempty?" "emptyset" "card_rest" "card_remove") (("" (INDUCT "S" :NAME "finite_set_induction_gen[T]") (("" (SKOSIMP) (("" (SKOLEM-TYPEPRED) (("" (CASE "empty?(S!1)") (("1" (DELETE -3 1) (("1" (GRIND) NIL NIL)) NIL) ("2" (ASSERT) (("2" (CASE "rest(S!1)(x!1)") (("1" (INST-CP - "rest(S!1)") (("1" (INST - "remove(x!1, S!1)") (("1" (ASSERT) (("1" (INST - "choose(S!1)") (("1" (INST - "x!1") (("1" (CASE-REPLACE "remove(x!1, rest(S!1)) = remove(choose(S!1), remove(x!1, S!1))") (("1" (ASSERT) NIL NIL) ("2" (DELETE -3 -4 2 3) (("2" (AUTO-REWRITE "remove" "rest" "member") (("2" (APPLY-EXTENSIONALITY :HIDE? T) (("2" (SMASH) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (DELETE -3 2 3) (("2" (AUTO-REWRITE "remove" "rest" "member") (("2" (REDUCE) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (DELETE -2) (("2" (AUTO-REWRITE "rest" "member" "remove") (("2" (REDUCE) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|sum_x1_x2_TCC1| "" (SUBTYPE-TCC)) (|sum_x1_x2| "" (SKOLEM!) (("" (REWRITE "sum_x" :DIR RL) (("" (REWRITE "sum_x" :DIR RL) NIL NIL)) NIL)) NIL) (|sum_add_TCC1| "" (SUBTYPE-TCC)) (|sum_add| "" (SKOLEM!) (("" (SMASH) (("1" (CASE-REPLACE "add(x!1, S!1) = S!1") (("1" (DELETE 2) (("1" (AUTO-REWRITE "add" "member") (("1" (APPLY-EXTENSIONALITY :HIDE? T) (("1" (SMASH) NIL NIL)) NIL)) NIL)) NIL)) NIL) ("2" (AUTO-REWRITE "add") (("2" (USE "sum_x" ("S" "add(x!1, S!1)")) (("2" (CASE-REPLACE "remove(x!1, add(x!1, S!1)) = S!1") (("2" (DELETE -1 3) (("2" (AUTO-REWRITE "remove" "add" "member") (("2" (APPLY-EXTENSIONALITY :HIDE? T) (("2" (SMASH) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|sum_remove_TCC1| "" (SUBTYPE-TCC)) (|sum_remove| "" (SKOLEM!) (("" (SMASH) (("1" (USE "sum_x") (("1" (ASSERT) NIL NIL)) NIL) ("2" (CASE-REPLACE "remove(x!1, S!1) = S!1") (("2" (DELETE 3) (("2" (AUTO-REWRITE-DEFS) (("2" (APPLY-EXTENSIONALITY :HIDE? T) (("2" (SMASH) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|sum_rest| "" (AUTO-REWRITE "sum") (("" (REDUCE) NIL NIL)) NIL) (|sum_disj_union_TCC1| "" (SUBTYPE-TCC)) (|sum_disj_union| "" (AUTO-REWRITE "sum_add" "sum_emptyset" "union" "member" "disjoint?" "intersection" "add" "empty?" "emptyset") (("" (SKOLEM + ("A!1" _ "f!1")) (("" (INDUCT "B" :NAME "finite_set_ind_modified[T]") (("1" (GROUND) (("1" (CASE-REPLACE "union(A!1, emptyset[T]) = A!1") (("1" (DELETE -1 2) (("1" (APPLY-EXTENSIONALITY :HIDE? T) NIL NIL)) NIL)) NIL)) NIL) ("2" (SKOSIMP) (("2" (GROUND) (("1" (INST - "e!1") (("1" (CASE-REPLACE "union(A!1, add(e!1, S!1)) = add(e!1, union(A!1, S!1))") (("1" (ASSERT) (("1" (ASSERT) NIL NIL)) NIL) ("2" (DELETE -1 3 4) (("2" (APPLY-EXTENSIONALITY :HIDE? T) (("2" (SMASH) NIL NIL)) NIL)) NIL)) NIL)) NIL) ("2" (SKOSIMP) (("2" (INST?) (("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|sum_diff_subset_TCC1| "" (SUBTYPE-TCC)) (|sum_diff_subset| "" (SKOSIMP) (("" (USE "sum_disj_union" ("A" "A!1" "B" "difference(B!1, A!1)")) (("" (GROUND) (("1" (CASE-REPLACE "union(A!1, difference(B!1, A!1)) = B!1") (("1" (ASSERT) NIL NIL) ("2" (DELETE -1 2) (("2" (AUTO-REWRITE-DEFS) (("2" (APPLY-EXTENSIONALITY :HIDE? T) (("2" (REDUCE) NIL NIL)) NIL)) NIL)) NIL)) NIL) ("2" (DELETE 2) (("2" (GRIND) NIL NIL)) NIL)) NIL)) NIL)) NIL) (|sum_union_TCC1| "" (SUBTYPE-TCC)) (|sum_union_TCC2| "" (SUBTYPE-TCC)) (|sum_union| "" (SKOLEM!) (("" (USE "sum_diff_subset" ("A" "A!1" "B" "union(A!1, B!1)")) (("" (GROUND) (("1" (USE "sum_diff_subset" ("A" "intersection(A!1, B!1)" "B" "B!1")) (("1" (GROUND) (("1" (CASE-REPLACE "difference(union(A!1, B!1), A!1) = difference(B!1, intersection(A!1, B!1))") (("1" (ASSERT) NIL NIL) ("2" (DELETE -1 -2 2) (("2" (APPLY-EXTENSIONALITY :HIDE? T) (("2" (GRIND) NIL NIL)) NIL)) NIL)) NIL) ("2" (DELETE -1 2) (("2" (GRIND) NIL NIL)) NIL)) NIL)) NIL) ("2" (DELETE 2) (("2" (GRIND) NIL NIL)) NIL)) NIL)) NIL)) NIL) (|sum_diff_intersection_TCC1| "" (SUBTYPE-TCC)) (|sum_diff_intersection| "" (SKOLEM!) (("" (REWRITE "sum_disj_union" :DIR RL) (("1" (CASE-REPLACE "union(difference(A!1, B!1), intersection(A!1, B!1)) = A!1") (("1" (DELETE 2) (("1" (APPLY-EXTENSIONALITY :HIDE? T) (("1" (GRIND) NIL NIL)) NIL)) NIL)) NIL) ("2" (DELETE 2) (("2" (GRIND) NIL NIL)) NIL)) NIL)) NIL) (|sum_f_g| "" (SKOLEM + (_ "f!1" "g!1")) (("" (AUTO-REWRITE "sum" "sum_emptyset" "nonempty?") (("" (INDUCT "S" :NAME "finite_set_induction_rest[T]") (("1" (SKOSIMP) (("1" (ASSERT) NIL NIL)) NIL) ("2" (SKOSIMP) (("2" (GROUND) (("1" (INST?) (("1" (ASSERT) NIL NIL)) NIL) ("2" (DELETE 2) (("2" (GRIND :EXCLUDE ("choose")) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|sum_particular| "" (SKOLEM!) (("" (SMASH) (("1" (USE "sum_remove" ("f" "f!1")) (("1" (USE "sum_remove" ("f" "f!1 WITH [x!1 := c!1]")) (("1" (ASSERT) (("1" (USE "sum_f_g" ("g" "f!1")) (("1" (GROUND) (("1" (DELETE -1 -2 2) (("1" (GRIND) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (REWRITE "sum_f_g") NIL NIL)) NIL)) NIL) (|sum_distributive| "" (SKOLEM + (_ "f!1" "g!1")) (("" (AUTO-REWRITE "sum" "sum_emptyset" "nonempty?") (("" (INDUCT "A" :NAME "finite_set_induction_rest[T]") (("1" (ASSERT) NIL NIL) ("2" (SKOSIMP) (("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL) (|sum_const| "" (INDUCT-AND-SIMPLIFY "S" :NAME "finite_set_induction_rest[T]" :DEFS NIL :REWRITES ("sum" "sum_emptyset" "card_emptyset" "card_rest")) NIL NIL) (|sum_mult| "" (INDUCT-AND-SIMPLIFY "S" :NAME "finite_set_induction_rest[T]" :DEFS NIL :REWRITES ("sum" "sum_emptyset")) NIL NIL) (|sum_1_is_card| "" (SKOLEM!) (("" (REWRITE "sum_const") (("" (ASSERT) NIL NIL)) NIL)) NIL) (|sum_update| "" (SKOLEM!) (("" (SMASH) (("1" (AUTO-REWRITE "member") (("1" (USE "sum_remove") (("1" (USE "sum_remove" ("f" "f!1 WITH [(t!1) := c!1]")) (("1" (ASSERT) (("1" (CASE "sum(remove(t!1, S!1), f!1) = sum(remove(t!1, S!1), f!1 WITH [(t!1) := c!1])") (("1" (ASSERT) NIL NIL) ("2" (REWRITE "sum_f_g") (("2" (DELETE -1 -2 2 3) (("2" (GRIND) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (REWRITE "sum_f_g") NIL NIL)) NIL)) NIL) (|sum_le| "" (INDUCT-AND-SIMPLIFY "S" :NAME "finite_set_induction_rest[T]" :DEFS NIL :REWRITES ("sum" "sum_emptyset" "nonempty?") :IF-MATCH NIL) (("" (INST - "f!1" "g!1") (("" (GROUND) (("1" (INST?) (("1" (ASSERT) NIL NIL)) NIL) ("2" (DELETE 2) (("2" (AUTO-REWRITE "rest" "remove" "member") (("2" (REDUCE) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|sum_ge| "" (SKOSIMP) (("" (USE "sum_le" ("f" "g!1" "g" "f!1")) (("" (REDUCE) NIL NIL)) NIL)) NIL) (|sum_lt| "" (INDUCT-AND-SIMPLIFY "E" :NAME "nonempty_finite_set_induct[T]" :DEFS NIL :REWRITES ("sum_singleton" "sum_add") :THEORIES ("sets[T]") :IF-MATCH NIL) (("1" (INST?) NIL NIL) ("2" (INST - "f!1" "g!1") (("2" (GROUND) (("1" (INST?) (("1" (ASSERT) NIL NIL)) NIL) ("2" (DELETE 2 3) (("2" (REDUCE) NIL NIL)) NIL)) NIL)) NIL)) NIL) (|sum_gt| "" (SKOSIMP) (("" (USE "sum_lt" ("f" "g!1" "g" "f!1")) (("" (REDUCE) NIL NIL)) NIL)) NIL) (|sum_bound| "" (SKOLEM + ("N!1" _ "f!1")) (("" (INDUCT-AND-SIMPLIFY "S" :NAME "finite_set_induction_rest[T]" :DEFS NIL :REWRITES ("sum" "card_emptyset" "card_rest" "sum_emptyset" "nonempty?")) (("" (TYPEPRED "t!1") (("" (AUTO-REWRITE-THEORY "sets[T]") (("" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL) (|sum_bound2| "" (SKOLEM + ("N!1" _ "f!1")) (("" (INDUCT-AND-SIMPLIFY "S" :NAME "finite_set_induction_rest[T]" :DEFS NIL :REWRITES ("sum" "card_emptyset" "card_rest" "sum_emptyset" "nonempty?")) (("" (TYPEPRED "t!1") (("" (AUTO-REWRITE-THEORY "sets[T]") (("" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL) (|sum_bound3| "" (AUTO-REWRITE "sum_singleton" "card_singleton" "sum_add" "card_add") (("" (AUTO-REWRITE-THEORY "sets[T]") (("" (INDUCT-AND-SIMPLIFY "E" :NAME "nonempty_finite_set_induct[T]" :DEFS NIL) NIL NIL)) NIL)) NIL) (|sum_bound4| "" (INDUCT-AND-SIMPLIFY "E" :NAME "nonempty_finite_set_induct[T]" :DEFS NIL :REWRITES ("sum_singleton" "card_singleton" "sum_add" "card_add") :THEORIES "sets[T]") NIL NIL) (|sum_nonneg| "" (SKOSIMP) (("" (FORWARD-CHAIN "sum_bound2") (("" (ASSERT) NIL NIL)) NIL)) NIL) (|sum_nonpos| "" (SKOSIMP) (("" (FORWARD-CHAIN "sum_bound") (("" (ASSERT) NIL NIL)) NIL)) NIL) (|sum_pos| "" (SKOSIMP*) (("" (AUTO-REWRITE "remove" "member") (("" (USE "sum_nonneg" ("S" "remove(t!1, S!1)")) (("" (GROUND) (("1" (USE "sum_remove") (("1" (ASSERT) NIL NIL)) NIL) ("2" (DELETE -2 2) (("2" (REDUCE) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|sum_pos2| "" (SKOSIMP) (("" (FORWARD-CHAIN "sum_bound4") (("" (ASSERT) NIL NIL)) NIL)) NIL) (|sum_neg| "" (SKOSIMP*) (("" (AUTO-REWRITE "remove" "member") (("" (USE "sum_nonpos" ("S" "remove(t!1, S!1)")) (("" (GROUND) (("1" (USE "sum_remove") (("1" (ASSERT) NIL NIL)) NIL) ("2" (DELETE -2 2) (("2" (REDUCE) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|sum_neg2| "" (SKOSIMP) (("" (FORWARD-CHAIN "sum_bound3") (("" (ASSERT) NIL NIL)) NIL)) NIL) (|sum_zero| "" (SKOSIMP) (("" (USE* "sum_nonneg" "sum_nonpos") (("" (APPLY (REPEAT (THEN (SPLIT) (SKOLEM!) (INST?) (ASSERT)))) NIL NIL)) NIL)) NIL) (|sum_closure1| "" (SKOLEM + (_ "U!1" "f!1")) (("" (INDUCT-AND-SIMPLIFY "E" :NAME "nonempty_finite_set_induct[T]" :REWRITES ("sum_add" "sum_singleton") :EXCLUDE ("sum") :THEORIES ("sets[T]")) (("" (INST? -2) NIL NIL)) NIL)) NIL) (|sum_closure2| "" (SKOLEM + (_ "U!1" "f!1")) (("" (AUTO-REWRITE "sum" "sum_emptyset" "rest" "remove" "member" "nonempty?") (("" (INDUCT "S" :NAME "finite_set_induction_rest[T]") (("1" (REDUCE) NIL NIL) ("2" (REDUCE) NIL NIL)) NIL)) NIL)) NIL) (|sum_nnreal_is_nnreal| "" (SKOLEM!) (("" (REWRITE "sum_nonneg") (("" (SKOLEM!) (("" (ASSERT) NIL NIL)) NIL)) NIL)) NIL) (|sum_npreal_is_npreal| "" (SKOLEM!) (("" (REWRITE "sum_nonpos") (("" (SKOLEM!) (("" (ASSERT) NIL NIL)) NIL)) NIL)) NIL) (|sum_posreal_is_posreal| "" (SKOLEM!) (("" (REWRITE "sum_pos2") (("" (SKOLEM!) (("" (ASSERT) NIL NIL)) NIL)) NIL)) NIL) (|sum_negreal_is_negreal| "" (SKOLEM!) (("" (REWRITE "sum_neg2") (("" (SKOLEM!) (("" (ASSERT) NIL NIL)) NIL)) NIL)) NIL) (|sum_rat_is_rat| "" (SKOLEM!) (("" (REWRITE "sum_closure2") NIL NIL)) NIL) (|sum_nnrat_is_nnrat| "" (SKOLEM!) (("" (ASSERT) NIL NIL)) NIL) (|sum_nprat_is_nprat| "" (SKOLEM!) (("" (REWRITE "sum_npreal_is_npreal") NIL NIL)) NIL) (|sum_posrat_is_posrat| "" (SUBTYPE-TCC) NIL NIL) (|sum_negrat_is_negrat| "" (SKOLEM!) (("" (REWRITE "sum_negreal_is_negreal") NIL NIL)) NIL) (|sum_int_is_int| "" (AUTO-REWRITE-THEORY "integers") (("" (INDUCT-AND-SIMPLIFY "S" 1 "finite_set_induction_rest[T]" :DEFS NIL :REWRITES ("sum_emptyset" "sum")) NIL NIL)) NIL) (|sum_npint_is_npint| "" (SKOLEM!) (("" (REWRITE "sum_npreal_is_npreal") NIL NIL)) NIL) (|sum_negint_is_negint| "" (SKOLEM!) (("" (REWRITE "sum_negreal_is_negreal") NIL NIL)) NIL) (|sum_nat_is_nat| "" (SKOLEM!) (("" (REWRITE "sum_nnreal_is_nnreal") NIL NIL)) NIL) (|sum_posnat_is_posnat| "" (AUTO-REWRITE-DEFS :EXPLICIT? T) (("" (ASSERT) (("" (SKOLEM-TYPEPRED) (("" (ASSERT) NIL NIL)) NIL)) NIL)) NIL) (|sum_max_bound| "" (SKOSIMP) (("" (SKOLEM!) (("" (AUTO-REWRITE "card_remove" "member") (("" (USE "sum_bound" ("S" "remove(t!1, S!1)" "N" "N!1")) (("" (GROUND) (("1" (USE "sum_remove") (("1" (ASSERT) (("1" (INST?) (("1" (ASSERT) NIL NIL)) NIL)) NIL)) NIL) ("2" (DELETE -1 2) (("2" (AUTO-REWRITE "remove") (("2" (REDUCE) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|sum_min_bound| "" (SKOSIMP) (("" (SKOLEM!) (("" (AUTO-REWRITE "card_remove" "member") (("" (USE "sum_bound2" ("S" "remove(t!1, S!1)" "N" "N!1")) (("" (GROUND) (("1" (USE "sum_remove") (("1" (ASSERT) (("1" (INST?) (("1" (ASSERT) NIL NIL)) NIL)) NIL)) NIL) ("2" (DELETE -1 2) (("2" (AUTO-REWRITE "remove") (("2" (REDUCE) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|sum_0_non_neg| "" (SKOSIMP) (("" (USE "sum_min_bound") (("" (GROUND) NIL NIL)) NIL)) NIL) (|sum_0_non_pos| "" (SKOSIMP) (("" (USE "sum_max_bound") (("" (GROUND) NIL NIL)) NIL)) NIL) (|equal_sum_le| "" (SKOSIMP*) (("" (ASSERT) (("" (USE "sum_le" ("S" "remove(t!1, S!1)" "f" "f!1" "g" "g!1")) (("" (GROUND) (("1" (AUTO-REWRITE "member") (("1" (USE "sum_remove" ("f" "f!1")) (("1" (USE "sum_remove" ("f" "g!1")) (("1" (ASSERT) (("1" (INST?) (("1" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (DELETE -1 2) (("2" (AUTO-REWRITE "remove" "member") (("2" (REDUCE) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|equal_sum_ge| "" (SKOSIMP) (("" (USE "equal_sum_le" ("f" "g!1" "g" "f!1")) (("" (REDUCE) NIL NIL)) NIL)) NIL) (|sum_0_non_neg2| "" (SKOSIMP) (("" (USE "sum_0_non_neg") (("" (GROUND) (("" (SKOLEM!) (("" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL) (|sum_0_non_pos2| "" (SKOSIMP) (("" (USE "sum_0_non_pos") (("" (GROUND) (("" (SKOLEM!) (("" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL) (|sum_subset| "" (SKOSIMP) (("" (USE "sum_diff_subset" ("A" "A!1" "B" "B!1")) (("" (ASSERT) (("" (USE "sum_nonneg" ("S" "difference(B!1, A!1)")) (("" (GROUND) NIL NIL)) NIL)) NIL)) NIL)) NIL) (|sum_subset2| "" (SKOSIMP) (("" (USE "sum_diff_subset" ("A" "A!1" "B" "B!1")) (("" (ASSERT) (("" (USE "sum_nonpos" ("S" "difference(B!1, A!1)")) (("" (GROUND) NIL NIL)) NIL)) NIL)) NIL)) NIL) (|sum_order_sub| "" (SKOSIMP) (("" (USE "sum_subset" ("h" "h1!1")) (("" (ASSERT) (("" (USE "sum_le" ("S" "B!1" "f" "h1!1" "g" "h2!1")) (("" (GROUND) (("" (DELETE -1 -2 2) (("" (REDUCE) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|sum_order_sub2| "" (SKOSIMP) (("" (USE "sum_subset2" ("k" "k1!1")) (("" (ASSERT) (("" (USE "sum_ge" ("S" "B!1" "f" "k1!1" "g" "k2!1")) (("" (GROUND) (("" (SKOLEM!) (("" (INST?) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|sum_subset3| "" (SKOSIMP) (("" (USE "sum_diff_subset" ("f" "f!1" "A" "A!1" "B" "B!1")) (("" (ASSERT) (("" (USE "sum_zero" ("S" "difference(B!1, A!1)")) (("" (GROUND) (("" (DELETE -1 -2 2) (("" (GRIND) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) $$$tasks_and_jobs.pvs tasks_and_jobs [ n: posnat ] : THEORY BEGIN task: NONEMPTY_TYPE = below(n) job: NONEMPTY_TYPE = [task, nat] set_of_tasks: JUDGEMENT set[task] SUBTYPE_OF finite_set[task] END tasks_and_jobs $$$tasks_and_jobs.prf (|tasks_and_jobs| (|task_TCC1| "" (INST + "0") (("" (ASSERT) NIL NIL)) NIL) (|set_of_tasks| "" (GRIND :IF-MATCH NIL) (("" (INST + "n" "lambda (i: (x!1)): i") (("" (SKOSIMP) (("" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) $$$max_bounded.pvs max_bounded[T: TYPE FROM nat] : THEORY BEGIN x, y: VAR nat E: VAR set[T] %------------------------- % Bound and bounded set %------------------------- bound(E, x): bool = FORALL (y: (E)): y <= x sup(E, x): bool = bound(E, x) AND FORALL y: bound(E, y) IMPLIES x <= y sup_unique: LEMMA sup(E, x) AND sup(E, y) IMPLIES x = y bounded?(E): bool = EXISTS x: bound(E, x) bounded_set: TYPE = { E | bounded?(E) } F, F1, F2: VAR bounded_set sup_exists: LEMMA EXISTS x: sup(F, x) sup_empty: LEMMA empty?(F) IMPLIES sup(F, 0) sup_nonempty: LEMMA not empty?(F) IMPLIES EXISTS (x: (F)): sup(F, x) %------------------------------------ % Maximum element of a bounded set %------------------------------------ A, B: VAR { F | not empty?(F) } bounded_union1: JUDGEMENT union(F1, F2) HAS_TYPE bounded_set bounded_union2: JUDGEMENT union(A, B) HAS_TYPE { F | not empty?(F) } bounded_inter1: JUDGEMENT intersection(F, E) HAS_TYPE bounded_set bounded_inter2: JUDGEMENT intersection(E, F) HAS_TYPE bounded_set max(A): { (x:(A)) | sup(A, x) } max_prop1: LEMMA FORALL (y: (A)): y <= max(A) max_prop2: LEMMA max(A) <= x IFF FORALL (y: (A)): y <= x max_subset: LEMMA subset?(A, B) IMPLIES max(A) <= max(B) max_union: LEMMA max(union(A, B)) = max(max(A), max(B)) max_intersection1: LEMMA not empty?(intersection(A, E)) IMPLIES max(intersection(A, E)) <= max(A) max_intersection2: LEMMA not empty?(intersection(E, B)) IMPLIES max(intersection(E, B)) <= max(B) END max_bounded $$$max_bounded.prf (|max_bounded| (|sup_unique| "" (EXPAND "sup") (("" (REDUCE :IF-MATCH ALL) NIL NIL)) NIL) (|sup_exists| "" (LEMMA "wf_nat") (("" (GRIND :IF-MATCH NIL :EXCLUDE ("bound")) (("" (DELETE -1) (("" (INST - "{ n: nat | bound(F!1, n) }") (("" (GROUND) (("" (SKOSIMP* :PREDS? T) (("" (INST? +) (("" (ASSERT) (("" (SKOSIMP) (("" (ASSERT) (("" (INST - "y!2") (("" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|sup_empty| "" (GRIND) NIL NIL) (|sup_nonempty| "" (SKOSIMP) (("" (USE "sup_exists") (("" (SKOLEM!) (("" (INST?) (("" (EXPAND* "empty?" "member" "sup" "bound") (("" (SKOLEM!) (("" (FLATTEN) (("" (ASSERT) (("" (INST -2 "x!1 - 1") (("1" (ASSERT) (("1" (SKOLEM!) (("1" (INST - "y!1") (("1" (ASSERT) NIL NIL)) NIL)) NIL)) NIL) ("2" (INST - "x!2") (("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|bounded_union1| "" (GRIND :IF-MATCH NIL) (("" (INST + "max(x!1, x!2)") (("" (REDUCE :IF-MATCH NIL) (("1" (INST?) (("1" (ASSERT) NIL NIL)) NIL) ("2" (INST? -6) (("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL) (|bounded_union2| "" (GRIND :EXCLUDE ("bounded?")) NIL NIL) (|bounded_inter1| "" (GRIND :IF-MATCH NIL) (("" (INST + "x!1") (("" (REDUCE :INSTANTIATOR INST!) NIL NIL)) NIL)) NIL) (|bounded_inter2| "" (GRIND :IF-MATCH NIL) (("" (INST + "x!1") (("" (REDUCE :INSTANTIATOR INST!) NIL NIL)) NIL)) NIL) (|max_TCC1| "" (INST + "lambda A: epsilon! (x: (A)): sup(A, x)") (("1" (SKOLEM-TYPEPRED) (("1" (USE "epsilon_ax[(A!1)]") (("1" (GROUND) (("1" (REWRITE "sup_nonempty") NIL NIL)) NIL) ("2" (DELETE -1 3) (("2" (GRIND) NIL NIL)) NIL)) NIL)) NIL) ("2" (SKOLEM-TYPEPRED) (("2" (DELETE -) (("2" (GRIND) NIL NIL)) NIL)) NIL)) NIL) (|max_prop1| "" (SKOLEM!) (("" (TYPEPRED "max(A!1)") (("" (GRIND) NIL NIL)) NIL)) NIL) (|max_prop2| "" (SKOLEM!) (("" (TYPEPRED "max(A!1)") (("" (EXPAND* "sup" "bound") (("" (GROUND) (("1" (SKOLEM!) (("1" (INST - "y!1") (("1" (ASSERT) NIL NIL)) NIL)) NIL) ("2" (INST? -5) (("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|max_subset| "" (SKOSIMP) (("" (REWRITE "max_prop2") (("" (GRIND :IF-MATCH NIL) (("" (INST?) (("" (ASSERT) (("" (USE "max_prop1" ("A" "B!1" "y" "y!1")) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|max_union| "" (SKOLEM!) (("" (CASE "max(max(A!1), max(B!1)) <= max(union(A!1, B!1))") (("1" (ASSERT) (("1" (USE "max_prop2" ("A" "union(A!1, B!1)" "x" "max(max(A!1), max(B!1))")) (("1" (GROUND) (("1" (DELETE -1 2 3) (("1" (GRIND :EXCLUDE "max") (("1" (USE "max_prop1" ("A" "A!1" "y" "y!1")) (("1" (ASSERT) NIL NIL)) NIL) ("2" (USE "max_prop1" ("A" "B!1" "y" "y!1")) (("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (DELETE 2) (("2" (EXPAND "max") (("2" (LIFT-IF) (("2" (GROUND) (("1" (REWRITE "max_subset") (("1" (DELETE -1 2) (("1" (GRIND) NIL NIL)) NIL)) NIL) ("2" (REWRITE "max_subset") (("2" (DELETE 2 3) (("2" (GRIND) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|max_intersection1| "" (SKOSIMP) (("" (ASSERT) (("" (REWRITE "max_subset") (("" (DELETE 2 3) (("" (GRIND) NIL NIL)) NIL)) NIL)) NIL)) NIL) (|max_intersection2| "" (SKOSIMP) (("" (ASSERT) (("" (REWRITE "max_subset") (("" (DELETE 2 3) (("" (GRIND) NIL NIL)) NIL)) NIL)) NIL)) NIL)) $$$command_adt.pvs %%% ADT file generated from command command_adt: THEORY BEGIN IMPORTING basic_types command: TYPE P?, V?, step?: [command -> boolean] P: [semaphore -> (P?)] request: [(P?) -> semaphore] V: [semaphore -> (V?)] sem: [(V?) -> semaphore] Step: (step?) ord(x: command): upto(2) = CASES x OF P(P1_var): 0, V(V1_var): 1, Step: 2 ENDCASES command_P_extensionality: AXIOM FORALL (P?_var: (P?), (P?_var2: (P?))): request(P?_var) = request(P?_var2) IMPLIES P?_var = P?_var2; command_P_eta: AXIOM FORALL (P?_var: (P?)): P(request(P?_var)) = P?_var; command_V_extensionality: AXIOM FORALL (V?_var: (V?), (V?_var2: (V?))): sem(V?_var) = sem(V?_var2) IMPLIES V?_var = V?_var2; command_V_eta: AXIOM FORALL (V?_var: (V?)): V(sem(V?_var)) = V?_var; command_Step_extensionality: AXIOM FORALL (step?_var: (step?), (step?_var2: (step?))): step?_var = step?_var2; command_request_P: AXIOM FORALL (P1_var: semaphore): request(P(P1_var)) = P1_var; command_sem_V: AXIOM FORALL (V1_var: semaphore): sem(V(V1_var)) = V1_var; command_inclusive: AXIOM FORALL (command_var: command): P?(command_var) OR V?(command_var) OR step?(command_var); command_induction: AXIOM FORALL (p: [command -> boolean]): (FORALL (P1_var: semaphore): p(P(P1_var))) AND (FORALL (V1_var: semaphore): p(V(V1_var))) AND p(Step) IMPLIES (FORALL (command_var: command): p(command_var)); subterm(x, y: command): boolean = x = y; <<(x, y: command): boolean = FALSE; command_well_founded: AXIOM well_founded?[command](<<); reduce_nat(P?_fun, V?_fun: [semaphore -> nat], (step?_fun: nat)): [command -> nat] = LAMBDA (command_adtvar: command): CASES command_adtvar OF P(P1_var): P?_fun(P1_var), V(V1_var): V?_fun(V1_var), Step: step?_fun ENDCASES; REDUCE_nat(P?_fun, V?_fun: [[semaphore, command] -> nat], (step?_fun: [command -> nat])): [command -> nat] = LAMBDA (command_adtvar: command): CASES command_adtvar OF P(P1_var): P?_fun(P1_var, command_adtvar), V(V1_var): V?_fun(V1_var, command_adtvar), Step: step?_fun(command_adtvar) ENDCASES; reduce_ordinal(P?_fun, V?_fun: [semaphore -> ordinal], (step?_fun: ordinal)): [command -> ordinal] = LAMBDA (command_adtvar: command): CASES command_adtvar OF P(P1_var): P?_fun(P1_var), V(V1_var): V?_fun(V1_var), Step: step?_fun ENDCASES; REDUCE_ordinal(P?_fun, V?_fun: [[semaphore, command] -> ordinal], (step?_fun: [command -> ordinal])): [command -> ordinal] = LAMBDA (command_adtvar: command): CASES command_adtvar OF P(P1_var): P?_fun(P1_var, command_adtvar), V(V1_var): V?_fun(V1_var, command_adtvar), Step: step?_fun(command_adtvar) ENDCASES; END command_adt command_adt_reduce[range: TYPE]: THEORY BEGIN IMPORTING basic_types IMPORTING command_adt reduce(P?_fun, V?_fun: [semaphore -> range], (step?_fun: range)): [command -> range] = LAMBDA (command_adtvar: command): CASES command_adtvar OF P(P1_var): P?_fun(P1_var), V(V1_var): V?_fun(V1_var), Step: step?_fun ENDCASES; REDUCE(P?_fun, V?_fun: [[semaphore, command] -> range], (step?_fun: [command -> range])): [command -> range] = LAMBDA (command_adtvar: command): CASES command_adtvar OF P(P1_var): P?_fun(P1_var, command_adtvar), V(V1_var): V?_fun(V1_var, command_adtvar), Step: step?_fun(command_adtvar) ENDCASES; END command_adt_reduce $$$basic_types.pvs basic_types : THEORY BEGIN %-------------------- % Priority of jobs %-------------------- maxprio: posnat priority: NONEMPTY_TYPE = below(maxprio) %-------------------------- % Semaphores and ceiling %-------------------------- semaphore: NONEMPTY_TYPE ceil: [semaphore -> priority] rsrc_set: TYPE = set[semaphore] END basic_types $$$basic_types.prf (|basic_types| (|priority_TCC1| "" (INST + "0") (("" (ASSERT) NIL)))) $$$command.pvs %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % commands available to jobs % % P(S): request to lock S % % V(S): request to unlock S % % Step: any other command % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% command : DATATYPE BEGIN IMPORTING basic_types P(request: semaphore): P? V(sem: semaphore): V? Step: step? END command $$$programs.pvs %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Programs: finite sequences of commands % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% programs : THEORY BEGIN IMPORTING command, max_bounded prog: TYPE = [# length: posnat, clist: [below(length) -> command] #] p: VAR prog s: VAR semaphore n: VAR priority %-------------------------------------------- % pc(p): type of index for program counter %-------------------------------------------- pc(p): NONEMPTY_TYPE = upto(length(p)) %-------------------------------------------------- % complete(p, i): index i points to the end of p % cmd(p, i): command for step i of p %-------------------------------------------------- complete(p, (i: pc(p))): bool = i = length(p) cmd(p, (i: below(length(p)))): command = clist(p)(i) %--------------------------------------------------- % Resources needed by p to perform step i = % all the resources acquired in steps [0..i-1] % and not released %--------------------------------------------------- needs(p, (i: pc(p))): RECURSIVE rsrc_set = IF i=0 THEN emptyset ELSE CASES cmd(p, i-1) OF P(s): add(s, needs(p, i-1)), V(s): remove(s, needs(p, i-1)), Step: needs(p, i-1) ENDCASES ENDIF MEASURE i %------------------------------------------------- % Resources used by p: % resources(p, i) = resources used in [0..i-1] % resources(p) = all resources used by p %------------------------------------------------- resources(p, (i: pc(p))): RECURSIVE rsrc_set = IF i=0 THEN emptyset ELSE CASES cmd(p, i-1) OF P(s): add(s, resources(p, i-1)), V(s): resources(p, i-1), Step: resources(p, i-1) ENDCASES ENDIF MEASURE i resources(p): rsrc_set = resources(p, length(p)) %----------------------------------------- % Relations between needs and resources %----------------------------------------- rsrc_needs1: LEMMA FORALL (i: pc(p)): subset?(needs(p, i), resources(p, i)) rsrc_needs2: LEMMA FORALL (i, j: pc(p)): i <= j IMPLIES subset?(resources(p, i), resources(p, j)) rsrc_needs3: LEMMA FORALL (i: pc(p)): subset?(resources(p, i), resources(p)) rsrc_needs4: LEMMA FORALL (i: pc(p)): subset?(needs(p, i), resources(p)) rsrc_equiv1: LEMMA FORALL (i: pc(p)): resources(p, i) = { s | EXISTS (j: pc(p) | j <= i): member(s, needs(p, j)) } rsrc_equiv2: LEMMA resources(p) = { s | EXISTS (j: pc(p)): member(s, needs(p, j)) } rsrc_equiv3: LEMMA member(s, resources(p)) IFF EXISTS (j: below(length(p))): cmd(p, j) = P(s) %%%%%%%%%%%%%%%%%%%%%%%%%% % Critical Sections % %%%%%%%%%%%%%%%%%%%%%%%%%% %------------------------------------------------------------------- % well_behaved(p): p releases all its resources on termination % cs(p, i): step i is within a critical section of p % cs(p, i, n): step i is within a critical section of level n % (i.e. between P(s) and V(s) where s has ceiling >= n) %------------------------------------------------------------------- well_behaved(p): bool = empty?(needs(p, length(p))) good_prog: TYPE = (well_behaved) cs(p, (i: pc(p))): bool = not empty?(needs(p, i)) cs(p, (i: pc(p)), n): bool = EXISTS s: member(s, needs(p, i)) AND ceil(s) >= n cs_level1: LEMMA FORALL (i: pc(p)): cs(p, i, n) IMPLIES cs(p, i) cs_level2: LEMMA FORALL (i: pc(p)): cs(p, i) IFF EXISTS n: cs(p, i, n) well_behaved1: LEMMA well_behaved(p) IFF not cs(p, length(p)) initially_not_cs1: LEMMA NOT cs(p, 0) initially_not_cs2: LEMMA NOT cs(p, 0, n) cs_exists1: LEMMA (EXISTS (i: pc(p)): cs(p, i)) IFF not empty?(resources(p)) cs_exists2: LEMMA (EXISTS (i: pc(p)): cs(p, i, n)) IFF EXISTS s: member(s, resources(p)) AND ceil(s) >= n %----------------------------------------------------------------------- % critical_section(p, i, j): p[i]...p[j-1] is a critical section % critical_section(p, i, j, n): same thing but at level n %----------------------------------------------------------------------- critical_section(p, (i, j: pc(p))): bool = i < j AND FORALL (k: pc(p)): i <= k AND k < j IMPLIES cs(p, k) critical_section(p, (i, j: pc(p)), n): bool = i < j AND FORALL (k: pc(p)): i <= k AND k < j IMPLIES cs(p, k, n) critical_section1: LEMMA FORALL (i, j: pc(p)): critical_section(p, i, j, n) IMPLIES critical_section(p, i, j) subsection1: LEMMA FORALL (i, j, k, l: pc(p)): critical_section(p, i, j) AND i <= k AND k < l AND l <= j IMPLIES critical_section(p, k, l) subsection2: LEMMA FORALL (i, j, k, l: pc(p)): critical_section(p, i, j, n) AND i <= k AND k < l AND l <= j IMPLIES critical_section(p, k, l, n) max_critical_section_length: LEMMA FORALL (i, j: pc(p)): critical_section(p, i, j) IMPLIES j - i < length(p) %------------------------------------------- % length of the longest critical sections %------------------------------------------- len_cs(p): bounded_set[pc(p)] = { a: pc(p) | EXISTS (i, j: pc(p)): critical_section(p, i, j) AND a = j-i } max_cs(p): pc(p) = IF empty?(len_cs(p)) THEN 0 ELSE max(len_cs(p)) ENDIF len_cs(p, n): bounded_set[pc(p)] = { a: pc(p) | EXISTS (i, j: pc(p)): critical_section(p, i, j, n) AND a = j-i } max_cs(p, n): pc(p) = IF empty?(len_cs(p, n)) THEN 0 ELSE max(len_cs(p, n)) ENDIF len_section_level: LEMMA subset?(len_cs(p, n), len_cs(p)) max_section_level: LEMMA max_cs(p, n) <= max_cs(p) max_cs1: LEMMA FORALL (i, j: pc(p)): critical_section(p, i, j) IMPLIES j - i <= max_cs(p) max_cs2: LEMMA FORALL (i, j: pc(p)): critical_section(p, i, j, n) IMPLIES j - i <= max_cs(p, n) no_critical_section: LEMMA well_behaved(p) IMPLIES (max_cs(p) = 0 IFF empty?(resources(p))) max_cs3: LEMMA max_cs(p) <= length(p) - 1 no_critical_section_lev: LEMMA well_behaved(p) IMPLIES (max_cs(p, n) = 0 IFF (FORALL s: member(s, resources(p)) IMPLIES ceil(s) < n)) max_cs4: LEMMA max_cs(p, n) <= length(p) - 1 END programs $$$programs.prf (|programs| (|needs_TCC1| "" (SUBTYPE-TCC) NIL NIL) (|needs_TCC2| "" (SUBTYPE-TCC) NIL NIL) (|needs_TCC3| "" (TERMINATION-TCC) NIL NIL) (|needs_TCC4| "" (SUBTYPE-TCC) NIL NIL) (|needs_TCC5| "" (TERMINATION-TCC) NIL NIL) (|needs_TCC6| "" (SUBTYPE-TCC) NIL NIL) (|needs_TCC7| "" (TERMINATION-TCC) NIL NIL) (|resources_TCC1| "" (SUBTYPE-TCC) NIL NIL) (|rsrc_needs1| "" (SKOLEM + ("p!1" _)) (("" (INDUCT-AND-SIMPLIFY "i") NIL NIL)) NIL) (|rsrc_needs2| "" (SKOLEM + ("p!1" "i!1" _)) (("" (INDUCT-AND-SIMPLIFY "j") NIL NIL)) NIL) (|rsrc_needs3| "" (SKOLEM!) (("" (EXPAND "resources" 1 2) (("" (REWRITE "rsrc_needs2") NIL NIL)) NIL)) NIL) (|rsrc_needs4| "" (SKOLEM!) (("" (USE* "rsrc_needs1" "rsrc_needs3") (("" (AUTO-REWRITE "subset?" "member") (("" (REDUCE) NIL NIL)) NIL)) NIL)) NIL) (|rsrc_equiv1| "" (SKOLEM + ("p!1" _)) (("" (INDUCT-AND-SIMPLIFY "i" :IF-MATCH NIL) (("1" (APPLY-EXTENSIONALITY :HIDE? T) NIL NIL) ("2" (REPLACE*) (("2" (DELETE -2) (("2" (APPLY-EXTENSIONALITY :HIDE? T) (("2" (REDUCE :IF-MATCH NIL) (("1" (INST + "1 + jt!1") (("1" (ASSERT) NIL NIL)) NIL) ("2" (INST?) NIL NIL) ("3" (CASE-REPLACE "j!1 = 1 + jt!1") (("1" (ASSERT) (("1" (INST?) NIL NIL)) NIL) ("2" (ASSERT) (("2" (INST?) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("3" (DELETE -1) (("3" (APPLY-EXTENSIONALITY 2 :HIDE? T) (("3" (REDUCE :IF-MATCH NIL) (("1" (INST?) NIL NIL) ("2" (CASE-REPLACE "j!1 = jt!1 + 1") (("1" (SMASH) (("1" (INST?) NIL NIL) ("2" (INST?) NIL NIL)) NIL) ("2" (ASSERT) (("2" (INST?) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|rsrc_equiv2| "" (SKOLEM!) (("" (EXPAND "resources") (("" (REWRITE "rsrc_equiv1") (("" (APPLY-EXTENSIONALITY :HIDE? T) (("" (REDUCE) NIL NIL)) NIL)) NIL)) NIL)) NIL) (|rsrc_equiv3| "" (EXPAND "resources") (("" (SKOLEM!) (("" (CASE "FORALL (i: pc(p!1)): member(s!1, resources(p!1, i)) IFF EXISTS (j: pc(p!1)): j < i AND cmd(p!1, j) = P(s!1)") (("1" (INST?) (("1" (REPLACE*) (("1" (DELETE -) (("1" (APPLY (THEN (PROP) (SKOSIMP) (INST?) (ASSERT))) NIL NIL)) NIL)) NIL)) NIL) ("2" (DELETE 2) (("2" (APPLY (THEN (INDUCT-AND-SIMPLIFY$ "i" :IF-MATCH NIL) (REPEAT* (INST?)) (ASSERT))) (("1" (DELETE 2) (("1" (APPLY-EXTENSIONALITY 2) NIL NIL)) NIL) ("2" (CASE-REPLACE "j!1 = jt!1") (("1" (REPLACE*) (("1" (ASSERT) NIL NIL)) NIL) ("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL) ("3" (SKOSIMP) (("3" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL) (|cs_level1| "" (GRIND) NIL NIL) (|cs_level2| "" (GRIND :EXCLUDE "resources" :IF-MATCH NIL) (("1" (INST?) NIL NIL) ("2" (INST + "ceil(x!1)") (("2" (INST + "x!1") (("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL) (|well_behaved1| "" (GRIND :EXCLUDE ("empty?" "resources")) NIL NIL) (|initially_not_cs1_TCC1| "" (SUBTYPE-TCC) NIL NIL) (|initially_not_cs1| "" (GRIND) NIL NIL) (|initially_not_cs2| "" (GRIND) NIL NIL) (|cs_exists1| "" (SKOLEM!) (("" (REWRITE "rsrc_equiv2") (("" (GRIND :EXCLUDE ("needs")) NIL NIL)) NIL)) NIL) (|cs_exists2| "" (SKOLEM!) (("" (REWRITE "rsrc_equiv2") (("" (GRIND :EXCLUDE ("needs") :IF-MATCH NIL) (("1" (INST?) (("1" (ASSERT) (("1" (INST?) NIL NIL)) NIL)) NIL) ("2" (INST?) (("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL) (|critical_section1| "" (AUTO-REWRITE "critical_section_lev" "critical_section" "cs_level2") (("" (REDUCE :IF-MATCH NIL) (("" (INST - "k!1") (("" (INST? +) (("" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL) (|subsection1| "" (APPLY (THEN (EXPAND "critical_section") (REPEAT* (THEN (SKOSIMP) (ASSERT))) (INST?) (ASSERT))) NIL NIL) (|subsection2| "" (APPLY (THEN (EXPAND "critical_section") (REPEAT* (THEN (SKOSIMP) (ASSERT))) (INST?) (ASSERT))) NIL NIL) (|max_critical_section_length| "" (EXPAND "critical_section") (("" (SKOSIMP) (("" (ASSERT) (("" (INST - "i!1") (("" (ASSERT) (("" (USE "initially_not_cs1") (("" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|len_cs_TCC1| "" (GRIND :EXCLUDE "critical_section" :IF-MATCH NIL) (("" (INST + "length(p!1)") (("" (SKOLEM!) (("" (ASSERT) NIL NIL)) NIL)) NIL)) NIL) (|len_cs_TCC2| "" (EXPAND* "bounded?" "bound") (("" (SKOLEM!) (("" (INST + "length(p!1)") (("" (SKOLEM!) (("" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL) (|len_section_level| "" (GRIND :EXCLUDE ("critical_section" "critical_section_lev") :IF-MATCH NIL) (("" (FORWARD-CHAIN "critical_section1") (("" (INST?) (("" (ASSERT) NIL NIL)) NIL)) NIL)) NIL) (|max_section_level| "" (SKOLEM!) (("" (USE "len_section_level") (("" (EXPAND "max_cs") (("" (SMASH) (("1" (DELETE 2) (("1" (APPLY (THEN (GRIND :EXCLUDE ("len_cs") :IF-MATCH NIL) (INST?) (INST?) (ASSERT))) NIL NIL)) NIL) ("2" (REWRITE "max_subset") NIL NIL)) NIL)) NIL)) NIL)) NIL) (|max_cs1| "" (SKOSIMP) (("" (EXPAND "max_cs") (("" (SMASH) (("1" (GRIND :EXCLUDE ("critical_section") :IF-MATCH NIL) (("1" (INST - "j!1 - i!1") (("1" (INST?) (("1" (ASSERT) NIL NIL)) NIL)) NIL)) NIL) ("2" (REWRITE "max_prop1") (("2" (DELETE 2 3) (("2" (FORWARD-CHAIN "max_critical_section_length") (("2" (ASSERT) (("2" (EXPAND "len_cs") (("2" (INST?) (("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|max_cs2| "" (SKOSIMP) (("" (EXPAND "max_cs") (("" (SMASH) (("1" (GRIND :EXCLUDE ("critical_section") :IF-MATCH NIL) (("1" (INST - "j!1 - i!1") (("1" (INST?) (("1" (ASSERT) NIL NIL)) NIL)) NIL)) NIL) ("2" (REWRITE "max_prop1") (("2" (DELETE 2 3) (("2" (FORWARD-CHAIN "critical_section1") (("2" (FORWARD-CHAIN "max_critical_section_length") (("2" (ASSERT) (("2" (EXPAND "len_cs") (("2" (INST?) (("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|no_critical_section| "" (SKOSIMP) (("" (EXPAND "max_cs") (("" (REWRITE "well_behaved1") (("" (USE "cs_exists1") (("" (CASE "empty?(len_cs(p!1))") (("1" (SMASH) (("1" (DELETE -3 1) (("1" (GRIND :EXCLUDE ("cs") :IF-MATCH NIL) (("1" (INST - "1") (("1" (INST + "i!1" "i!1+1") (("1" (REDUCE) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (SMASH) (("1" (CASE "1 <= max(len_cs(p!1))") (("1" (ASSERT) NIL NIL) ("2" (SKOLEM!) (("2" (AUTO-REWRITE "len_cs" "critical_section") (("2" (REWRITE "max_prop1") (("2" (INST + "i!1" "i!1 + 1") (("2" (REDUCE) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (DELETE -1 4) (("2" (GRIND :EXCLUDE ("cs") :IF-MATCH NIL) (("2" (INST + "i!1") (("2" (INST? -) (("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|max_cs3| "" (SKOSIMP) (("" (EXPAND "max_cs") (("" (SMASH) (("" (REWRITE "max_prop2") (("" (SKOLEM-TYPEPRED) (("" (EXPAND "len_cs" -) (("" (SKOSIMP) (("" (FORWARD-CHAIN "max_critical_section_length") (("" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|no_critical_section_lev| "" (SKOSIMP) (("" (REWRITE "well_behaved1") (("" (USE "cs_level1") (("" (ASSERT) (("" (DELETE 2) (("" (EXPAND "max_cs") (("" (CASE "empty?(len_cs(p!1, n!1))") (("1" (SMASH) (("1" (USE "cs_exists2") (("1" (GROUND) (("1" (DELETE -2 -4 2) (("1" (GRIND :EXCLUDE ("cs") :IF-MATCH NIL) (("1" (INST - "1") (("1" (INST + "i!1" "i!1+1") (("1" (REDUCE) NIL NIL)) NIL)) NIL)) NIL)) NIL) ("2" (DELETE -1 -2 2 3) (("2" (REDUCE) NIL NIL)) NIL)) NIL)) NIL)) NIL) ("2" (SMASH) (("1" (USE "cs_exists2") (("1" (GROUND) (("1" (DELETE -2 3) (("1" (CASE "1 <= max(len_cs(p!1, n!1))") (("1" (ASSERT) NIL NIL) ("2" (AUTO-REWRITE "len_cs" "critical_section") (("2" (REWRITE "max_prop1") (("2" (SKOLEM!) (("2" (ASSERT) (("2" (INST + "i!1" "i!1+1") (("2" (REDUCE) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (DELETE -1 2 3 4) (("2" (REDUCE) NIL NIL)) NIL)) NIL)) NIL) ("2" (USE "cs_exists2") (("2" (GROUND) (("1" (DELETE -1 1 2 3) (("1" (REDUCE) NIL NIL)) NIL) ("2" (DELETE -1 1 5) (("2" (GRIND :EXCLUDE ("cs") :IF-MATCH NIL) (("2" (INST + "i!1") (("2" (INST - "i!1") (("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|max_cs4| "" (SKOSIMP) (("" (EXPAND "max_cs") (("" (SMASH) (("" (REWRITE "max_prop2") (("" (SKOLEM-TYPEPRED) (("" (EXPAND "len_cs" -) (("" (SKOSIMP) (("" (FORWARD-CHAIN "critical_section1") (("" (FORWARD-CHAIN "max_critical_section_length") (("" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL))