PVS Bug 696
Synopsis: prover loops
Severity: serious
Priority: medium
Responsible: owre
State: open
Class: sw-bug
Arrival-Date: Wed Jul 31 11:45:00 2002
Originator: Bruno Dutertre
Organization: sdl.sri.com
Release: PVS 2.4
Environment:
System:
Architecture:
Description:
This is a multi-part message in MIME format.
--------------030807020401080701020807
Content-Type: text/plain; charset=us-ascii; format=flowed
Content-Transfer-Encoding: 7bit
Sam, Shankar,
In the proof of process_time_ready_job, there is a
(split) after (use "process_time_partition4" ...).
This used to be (ground) rather than (split), but if
you use (ground) with PVS3.0, the prover loops.
Bruno
--------------030807020401080701020807
Content-Type: text/plain;
name="traces.dmp"
Content-Transfer-Encoding: 7bit
Content-Disposition: inline;
filename="traces.dmp"
$$$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))
%% Stuff for DASC talk
alloc(u, j, t): rsrc_set = u(t)`rsrc`alloc(j)
mutual_exclusion: LEMMA
j /= k IMPLIES disjoint?(alloc(u, j, t), alloc(u, k, 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)), pr
io(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(blocke
rs(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
(good_ceiling 0
(good_ceiling-1 nil 3237060222 nil nil nil nil nil nil nil shostak))
(good_programs 0
(good_programs-1 nil 3237060222 nil nil nil nil nil nil nil shostak))
(IMP_priority_ceiling_TCC1 0
(IMP_priority_ceiling_TCC1-1 nil 3237060221 nil
("" (lemma "good_ceiling") (("" (propax) nil nil)) nil)
proved-complete ((good_ceiling formula-decl nil traces nil)) nil nil
nil nil))
(IMP_priority_ceiling_TCC2 0
(IMP_priority_ceiling_TCC2-1 nil 3237060221 nil
("" (lemma "good_programs") (("" (propax) nil nil)) nil)
proved-complete ((good_programs formula-decl nil traces nil)) nil
nil nil nil))
(next_state_exists 0
(next_state_exists-1 nil 3237060221 nil
("" (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?) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
proved-complete
((good_state nonempty-type-eq-decl nil priority_ceiling nil)
(P const-decl "bool" priority_ceiling nil)
(idle const-decl "bool" priority_ceiling nil)
(sch_state type-eq-decl nil priority_ceiling nil)
(rsrc_state type-eq-decl nil priority_ceiling nil)
(dispatch formal-const-decl "[job -> nat]" traces nil)
(prio formal-const-decl "[job -> priority]" traces nil)
(priority nonempty-type-eq-decl nil basic_types nil)
(maxprio const-decl "posnat" basic_types nil)
(> const-decl "bool" reals nil)
(nonneg_int nonempty-type-eq-decl nil integers nil)
(< const-decl "bool" reals nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(>= const-decl "bool" reals nil)
(bool nonempty-type-eq-decl nil booleans nil)
(int nonempty-type-eq-decl nil integers nil)
(integer_pred const-decl "[rational -> boolean]" integers nil)
(rational nonempty-type-from-decl nil rationals nil)
(rational_pred const-decl "[real -> boolean]" rationals nil)
(real nonempty-type-from-decl nil reals nil)
(real_pred const-decl "[number -> boolean]" reals nil)
(boolean nonempty-type-decl nil booleans nil)
(number nonempty-type-decl nil numbers nil)
(prog formal-const-decl
"[job -> prog]"
traces nil)
(prog type-eq-decl
nil
programs nil)
(command type-decl nil command_adt nil)
(below type-eq-decl nil naturalnumbers nil)
(posnat nonempty-type-eq-decl nil integers nil)
(pc nonempty-type-eq-decl nil programs nil)
(job formal-type-decl nil traces nil)
(T const-decl "bool" priority_ceiling nil)
(idle_step const-decl "sch_state" priority_ceiling nil)
(idle_P formula-decl nil priority_ceiling nil)
(step const-decl "sch_state" priority_ceiling nil)
(ready const-decl "bool" priority_ceiling nil)
(eligible_ready formula-decl nil priority_ceiling nil)
(step_P formula-decl nil priority_ceiling nil))
nil nil nil nil))
(tr_TCC1 0
(tr_TCC1-1 nil 3237060221 nil ("" (subtype-tcc) nil nil)
proved-complete
((nat nonempty-type-eq-decl nil naturalnumbers nil)
(int nonempty-type-eq-decl nil integers nil)
(integer_pred const-decl "[rational -> boolean]" integers nil)
(rational nonempty-type-from-decl nil rationals nil)
(rational_pred const-decl "[real -> boolean]" rationals nil)
(>= const-decl "bool" reals nil)
(real nonempty-type-from-decl nil reals nil)
(real_pred const-decl "[number -> boolean]" reals nil)
(number nonempty-type-decl nil numbers nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil))
nil nil nil nil))
(tr_TCC2 0
(tr_TCC2-1 nil 3237060221 nil ("" (termination-tcc) nil nil)
proved-complete nil nil nil nil nil))
(trace_TCC1 0
(trace_TCC1-1 nil 3237060221 nil
("" (auto-rewrite "tr")
(("" (ground)
(("" (skolem!)
(("" (use "epsilon_ax[good_state]")
(("" (assert) (("" (rewrite "next_state_exists") nil nil))
nil))
nil))
nil))
nil))
nil)
proved-complete
((next_state_exists formula-decl nil traces nil)
(pred type-eq-decl nil defined_types nil)
(T const-decl "bool" priority_ceiling nil)
(good_state nonempty-type-eq-decl nil priority_ceiling nil)
(P const-decl "bool" priority_ceiling nil)
(sch_state type-eq-decl nil priority_ceiling nil)
(rsrc_state type-eq-decl nil priority_ceiling nil)
(dispatch formal-const-decl "[job -> nat]" traces nil)
(prio formal-const-decl "[job -> priority]" traces nil)
(priority nonempty-type-eq-decl nil basic_types nil)
(maxprio const-decl "posnat" basic_types nil)
(> const-decl "bool" reals nil)
(nonneg_int nonempty-type-eq-decl nil integers nil)
(< const-decl "bool" reals nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(>= const-decl "bool" reals nil)
(bool nonempty-type-eq-decl nil booleans nil)
(int nonempty-type-eq-decl nil integers nil)
(integer_pred const-decl "[rational -> boolean]" integers nil)
(rational nonempty-type-from-decl nil rationals nil)
(rational_pred const-decl "[real -> boolean]" rationals nil)
(real nonempty-type-from-decl nil reals nil)
(real_pred const-decl "[number -> boolean]" reals nil)
(boolean nonempty-type-decl nil booleans nil)
(number nonempty-type-decl nil numbers nil)
(prog formal-const-decl
"[job -> prog]"
traces nil)
(prog type-eq-decl
nil
programs nil)
(command type-decl nil command_adt nil)
(below type-eq-decl nil naturalnumbers nil)
(posnat nonempty-type-eq-decl nil integers nil)
(pc nonempty-type-eq-decl nil programs nil)
(job formal-type-decl nil traces nil)
(epsilon_ax formula-decl nil epsilons nil)
(tr def-decl "good_state" traces nil))
nil nil nil nil))
(tr_is_a_trace 0
(tr_is_a_trace-1 nil 3237060221 nil
("" (lemma "trace_TCC1") (("" (propax) nil nil)) nil)
proved-complete ((trace_TCC1 subtype-tcc nil traces nil)) nil nil
nil nil))
(init_trace 0
(init_trace-1 nil 3237060221 nil ("" (reduce) nil nil)
proved-complete nil nil nil nil nil))
(step_trace 0
(step_trace-1 nil 3237060221 nil ("" (reduce :polarity? t) nil nil)
proved-complete
((boolean nonempty-type-decl nil booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(number nonempty-type-decl nil numbers nil)
(real_pred const-decl "[number -> boolean]" reals nil)
(real nonempty-type-from-decl nil reals nil)
(>= const-decl "bool" reals nil)
(rational_pred const-decl "[real -> boolean]" rationals nil)
(rational nonempty-type-from-decl nil rationals nil)
(integer_pred const-decl "[rational -> boolean]" integers nil)
(int nonempty-type-eq-decl nil integers nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(job formal-type-decl nil traces nil)
(pc nonempty-type-eq-decl nil programs nil)
(posnat nonempty-type-eq-decl nil integers nil)
(below type-eq-decl nil naturalnumbers nil)
(command type-decl nil command_adt nil)
(prog type-eq-decl
nil
programs nil)
(prog formal-const-decl
"[job -> prog]"
traces nil)
(< const-decl "bool" reals nil)
(nonneg_int nonempty-type-eq-decl nil integers nil)
(> const-decl "bool" reals nil)
(maxprio const-decl "posnat" basic_types nil)
(priority nonempty-type-eq-decl nil basic_types nil)
(prio formal-const-decl "[job -> priority]" traces nil)
(dispatch formal-const-decl "[job -> nat]" traces nil)
(rsrc_state type-eq-decl nil priority_ceiling nil)
(sch_state type-eq-decl nil priority_ceiling nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(P const-decl "bool" priority_ceiling nil)
(good_state nonempty-type-eq-decl nil priority_ceiling nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(init_sch const-decl "good_state" priority_ceiling nil)
(T const-decl "bool" priority_ceiling nil)
(+ const-decl "[real, real -> real]" reals nil)
(trace nonempty-type-eq-decl nil traces nil))
nil nil nil nil))
(invariance_P2 0
(invariance_P2-1 nil 3237060221 nil
("" (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)
proved-complete
((number nonempty-type-decl nil numbers nil)
(boolean nonempty-type-decl nil booleans nil)
(real_pred const-decl "[number -> boolean]" reals nil)
(real nonempty-type-from-decl nil reals nil)
(rational_pred const-decl "[real -> boolean]" rationals nil)
(rational nonempty-type-from-decl nil rationals nil)
(integer_pred const-decl "[rational -> boolean]" integers nil)
(int nonempty-type-eq-decl nil integers nil)
(bool nonempty-type-eq-decl nil booleans nil)
(>= const-decl "bool" reals nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(pred type-eq-decl nil defined_types nil)
(job formal-type-decl nil traces nil)
(rsrc_set type-eq-decl nil basic_types nil)
(< const-decl "bool" reals nil)
(nonneg_int nonempty-type-eq-decl nil integers nil)
(> const-decl "bool" reals nil)
(posnat nonempty-type-eq-decl nil integers nil)
(maxprio const-decl "posnat" basic_types nil)
(priority nonempty-type-eq-decl nil basic_types nil)
(prio formal-const-decl "[job -> priority]" traces nil)
(dispatch formal-const-decl "[job -> nat]" traces nil)
(below type-eq-decl nil naturalnumbers nil)
(command type-decl nil command_adt nil)
(prog type-eq-decl
nil
programs nil)
(prog formal-const-decl
"[job -> prog]"
traces nil)
(rsrc_state type-eq-decl nil priority_ceiling nil)
(P2 const-decl "bool" priority_ceiling nil)
(pc nonempty-type-eq-decl nil programs nil)
(sch_state type-eq-decl nil priority_ceiling nil)
(P const-decl "bool" priority_ceiling nil)
(good_state nonempty-type-eq-decl nil priority_ceiling nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(init_sch const-decl "good_state" priority_ceiling nil)
(T const-decl "bool" priority_ceiling nil)
(+ const-decl "[real, real -> real]" reals nil)
(trace nonempty-type-eq-decl nil traces nil)
(nat_induction formula-decl nil naturalnumbers nil)
(init_trace formula-decl nil traces nil)
(init_P2 formula-decl nil priority_ceiling nil)
(step_trace formula-decl nil traces nil)
(step_P2 formula-decl nil priority_ceiling nil))
nil nil nil nil))
(invariance_Q 0
(invariance_Q-1 nil 3237060221 nil
("" (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)
proved-complete
((number nonempty-type-decl nil numbers nil)
(boolean nonempty-type-decl nil booleans nil)
(real_pred const-decl "[number -> boolean]" reals nil)
(real nonempty-type-from-decl nil reals nil)
(rational_pred const-decl "[real -> boolean]" rationals nil)
(rational nonempty-type-from-decl nil rationals nil)
(integer_pred const-decl "[rational -> boolean]" integers nil)
(int nonempty-type-eq-decl nil integers nil)
(bool nonempty-type-eq-decl nil booleans nil)
(>= const-decl "bool" reals nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(pred type-eq-decl nil defined_types nil)
(job formal-type-decl nil traces nil)
(pc nonempty-type-eq-decl nil programs nil)
(posnat nonempty-type-eq-decl nil integers nil)
(below type-eq-decl nil naturalnumbers nil)
(command type-decl nil command_adt nil)
(prog type-eq-decl
nil
programs nil)
(prog formal-const-decl
"[job -> prog]"
traces nil)
(< const-decl "bool" reals nil)
(nonneg_int nonempty-type-eq-decl nil integers nil)
(> const-decl "bool" reals nil)
(maxprio const-decl "posnat" basic_types nil)
(priority nonempty-type-eq-decl nil basic_types nil)
(prio formal-const-decl "[job -> priority]" traces nil)
(dispatch formal-const-decl "[job -> nat]" traces nil)
(rsrc_state type-eq-decl nil priority_ceiling nil)
(sch_state type-eq-decl nil priority_ceiling nil)
(P const-decl "bool" priority_ceiling nil)
(good_state nonempty-type-eq-decl nil priority_ceiling nil)
(Q const-decl "bool" priority_ceiling nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(init_sch const-decl "good_state" priority_ceiling nil)
(T const-decl "bool" priority_ceiling nil)
(+ const-decl "[real, real -> real]" reals nil)
(trace nonempty-type-eq-decl nil traces nil)
(nat_induction formula-decl nil naturalnumbers nil)
(init_trace formula-decl nil traces nil)
(init_Q formula-decl nil priority_ceiling nil)
(step_trace formula-decl nil traces nil)
(step_Q formula-decl nil priority_ceiling nil))
nil nil nil nil))
(time_invariant 0
(time_invariant-1 nil 3237060221 nil
("" (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)
proved-complete
((step_trace formula-decl nil traces nil)
(idle_step const-decl "sch_state" priority_ceiling nil)
(cmd const-decl "command" programs nil)
(step const-decl "sch_state" priority_ceiling nil)
(init_trace formula-decl nil traces nil)
(nat_induction formula-decl nil naturalnumbers nil)
(trace nonempty-type-eq-decl nil traces nil)
(+ const-decl "[real, real -> real]" reals nil)
(T const-decl "bool" priority_ceiling nil)
(init_sch const-decl "good_state" priority_ceiling nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(good_state nonempty-type-eq-decl nil priority_ceiling nil)
(P const-decl "bool" priority_ceiling nil)
(sch_state type-eq-decl nil priority_ceiling nil)
(rsrc_state type-eq-decl nil priority_ceiling nil)
(dispatch formal-const-decl "[job -> nat]" traces nil)
(prio formal-const-decl "[job -> priority]" traces nil)
(priority nonempty-type-eq-decl nil basic_types nil)
(maxprio const-decl "posnat" basic_types nil)
(> const-decl "bool" reals nil)
(nonneg_int nonempty-type-eq-decl nil integers nil)
(< const-decl "bool" reals nil)
(prog formal-const-decl
"[job -> prog]"
traces nil)
(prog type-eq-decl
nil
programs nil)
(command type-decl nil command_adt nil)
(below type-eq-decl nil naturalnumbers nil)
(posnat nonempty-type-eq-decl nil integers nil)
(pc nonempty-type-eq-decl nil programs nil)
(job formal-type-decl nil traces nil)
(pred type-eq-decl nil defined_types nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(>= const-decl "bool" reals nil)
(bool nonempty-type-eq-decl nil booleans nil)
(int nonempty-type-eq-decl nil integers nil)
(integer_pred const-decl "[rational -> boolean]" integers nil)
(rational nonempty-type-from-decl nil rationals nil)
(rational_pred const-decl "[real -> boolean]" rationals nil)
(real nonempty-type-from-decl nil reals nil)
(real_pred const-decl "[number -> boolean]" reals nil)
(boolean nonempty-type-decl nil booleans nil)
(number nonempty-type-decl nil numbers nil))
nil nil nil nil))
(active_TCC1 0
(active_TCC1-1 nil 3237060221 nil
("" (skosimp) (("" (forward-chain "eligible_ready") nil nil)) nil)
proved-complete
((prog formal-const-decl
"[job -> prog]"
traces nil)
(prog type-eq-decl
nil
programs nil)
(command type-decl nil command_adt nil)
(below type-eq-decl nil naturalnumbers nil)
(dispatch formal-const-decl "[job -> nat]" traces nil)
(prio formal-const-decl "[job -> priority]" traces nil)
(priority nonempty-type-eq-decl nil basic_types nil)
(maxprio const-decl "posnat" basic_types nil)
(posnat nonempty-type-eq-decl nil integers nil)
(> const-decl "bool" reals nil)
(nonneg_int nonempty-type-eq-decl nil integers nil)
(< const-decl "bool" reals nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(>= const-decl "bool" reals nil)
(bool nonempty-type-eq-decl nil booleans nil)
(int nonempty-type-eq-decl nil integers nil)
(integer_pred const-decl "[rational -> boolean]" integers nil)
(rational nonempty-type-from-decl nil rationals nil)
(rational_pred const-decl "[real -> boolean]" rationals nil)
(real nonempty-type-from-decl nil reals nil)
(real_pred const-decl "[number -> boolean]" reals nil)
(boolean nonempty-type-decl nil booleans nil)
(number nonempty-type-decl nil numbers nil)
(job formal-type-decl nil traces nil)
(trace nonempty-type-eq-decl nil traces nil)
(+ const-decl "[real, real -> real]" reals nil)
(T const-decl "bool" priority_ceiling nil)
(init_sch const-decl "good_state" priority_ceiling nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(good_state nonempty-type-eq-decl nil priority_ceiling nil)
(P const-decl "bool" priority_ceiling nil)
(sch_state type-eq-decl nil priority_ceiling nil)
(rsrc_state type-eq-decl nil priority_ceiling nil)
(pc nonempty-type-eq-decl nil programs nil)
(eligible_ready formula-decl nil priority_ceiling nil))
nil nil nil nil))
(pc_init 0
(pc_init-1 nil 3237060221 nil ("" (grind :exclude ("T")) nil nil)
proved-complete
((boolean nonempty-type-decl nil booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(job formal-type-decl nil traces nil)
(pc nonempty-type-eq-decl nil programs nil)
(posnat nonempty-type-eq-decl nil integers nil)
(below type-eq-decl nil naturalnumbers nil)
(command type-decl nil command_adt nil)
(prog type-eq-decl
nil
programs nil)
(prog formal-const-decl
"[job -> prog]"
traces nil)
(number nonempty-type-decl nil numbers nil)
(real_pred const-decl "[number -> boolean]" reals nil)
(real nonempty-type-from-decl nil reals nil)
(rational_pred const-decl "[real -> boolean]" rationals nil)
(rational nonempty-type-from-decl nil rationals nil)
(integer_pred const-decl "[rational -> boolean]" integers nil)
(int nonempty-type-eq-decl nil integers nil)
(>= const-decl "bool" reals nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(< const-decl "bool" reals nil)
(nonneg_int nonempty-type-eq-decl nil integers nil)
(> const-decl "bool" reals nil)
(maxprio const-decl "posnat" basic_types nil)
(priority nonempty-type-eq-decl nil basic_types nil)
(prio formal-const-decl "[job -> priority]" traces nil)
(dispatch formal-const-decl "[job -> nat]" traces nil)
(rsrc_state type-eq-decl nil priority_ceiling nil)
(sch_state type-eq-decl nil priority_ceiling nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(P const-decl "bool" priority_ceiling nil)
(good_state nonempty-type-eq-decl nil priority_ceiling nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(init_sch const-decl "good_state" priority_ceiling nil)
(T const-decl "bool" priority_ceiling nil)
(+ const-decl "[real, real -> real]" reals nil)
(trace nonempty-type-eq-decl nil traces nil)
(init_rsrc const-decl "rsrc_state" priority_ceiling nil)
(pc const-decl "pc(prog(j))" traces nil))
nil nil nil nil))
(pc_step 0
(pc_step-1 nil 3237060221 nil
("" (skolem!)
(("" (smash)
(("1" (auto-rewrite "pc" "step" "active")
(("1" (reduce) nil nil)) nil)
("2" (expand "active")
(("2" (use "step_trace" ("t" "t!1"))
(("2" (expand "T")
(("2" (auto-rewrite "pc" "idle_step" "step")
(("2" (reduce) nil nil)) nil))
nil))
nil))
nil))
nil))
nil)
proved-complete
((idle_step const-decl "sch_state" priority_ceiling nil)
(pc nonempty-type-eq-decl nil programs nil)
(rsrc_state type-eq-decl nil priority_ceiling nil)
(sch_state type-eq-decl nil priority_ceiling nil)
(P const-decl "bool" priority_ceiling nil)
(good_state nonempty-type-eq-decl nil priority_ceiling nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(init_sch const-decl "good_state" priority_ceiling nil)
(T const-decl "bool" priority_ceiling nil)
(+ const-decl "[real, real -> real]" reals nil)
(trace nonempty-type-eq-decl nil traces nil)
(step_trace formula-decl nil traces nil)
(pc const-decl "pc(prog(j))" traces nil)
(active const-decl "bool" traces nil)
(step const-decl "sch_state" priority_ceiling nil)
(job formal-type-decl nil traces nil)
(number nonempty-type-decl nil numbers nil)
(boolean nonempty-type-decl nil booleans nil)
(real_pred const-decl "[number -> boolean]" reals nil)
(real nonempty-type-from-decl nil reals nil)
(rational_pred const-decl "[real -> boolean]" rationals nil)
(rational nonempty-type-from-decl nil rationals nil)
(integer_pred const-decl "[rational -> boolean]" integers nil)
(int nonempty-type-eq-decl nil integers nil)
(bool nonempty-type-eq-decl nil booleans nil)
(>= const-decl "bool" reals nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(< const-decl "bool" reals nil)
(nonneg_int nonempty-type-eq-decl nil integers nil)
(> const-decl "bool" reals nil)
(posnat nonempty-type-eq-decl nil integers nil)
(maxprio const-decl "posnat" basic_types nil)
(priority nonempty-type-eq-decl nil basic_types nil)
(prio formal-const-decl "[job -> priority]" traces nil)
(dispatch formal-const-decl "[job -> nat]" traces nil)
(below type-eq-decl nil naturalnumbers nil)
(command type-decl nil command_adt nil)
(prog type-eq-decl
nil
programs nil)
(prog formal-const-decl
"[job -> prog]"
traces nil))
nil nil nil nil))
(pc_increasing 0
(pc_increasing-1 nil 3237060221 nil
("" (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)
proved-complete
((active const-decl "bool" traces nil)
(pc_step formula-decl nil traces nil)
(pc_init formula-decl nil traces nil)
(number nonempty-type-decl nil numbers nil)
(boolean nonempty-type-decl nil booleans nil)
(real_pred const-decl "[number -> boolean]" reals nil)
(real nonempty-type-from-decl nil reals nil)
(rational_pred const-decl "[real -> boolean]" rationals nil)
(rational nonempty-type-from-decl nil rationals nil)
(integer_pred const-decl "[rational -> boolean]" integers nil)
(int nonempty-type-eq-decl nil integers nil)
(bool nonempty-type-eq-decl nil booleans nil)
(>= const-decl "bool" reals nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(pred type-eq-decl nil defined_types nil)
(IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
(<= const-decl "bool" reals nil)
(job formal-type-decl nil traces nil)
(pc nonempty-type-eq-decl nil programs nil)
(posnat nonempty-type-eq-decl nil integers nil)
(below type-eq-decl nil naturalnumbers nil)
(command type-decl nil command_adt nil)
(prog type-eq-decl
nil
programs nil)
(prog formal-const-decl
"[job -> prog]"
traces nil)
(< const-decl "bool" reals nil)
(nonneg_int nonempty-type-eq-decl nil integers nil)
(> const-decl "bool" reals nil)
(maxprio const-decl "posnat" basic_types nil)
(priority nonempty-type-eq-decl nil basic_types nil)
(prio formal-const-decl "[job -> priority]" traces nil)
(dispatch formal-const-decl "[job -> nat]" traces nil)
(rsrc_state type-eq-decl nil priority_ceiling nil)
(sch_state type-eq-decl nil priority_ceiling nil)
(P const-decl "bool" priority_ceiling nil)
(good_state nonempty-type-eq-decl nil priority_ceiling nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(init_sch const-decl "good_state" priority_ceiling nil)
(T const-decl "bool" priority_ceiling nil)
(+ const-decl "[real, real -> real]" reals nil)
(trace nonempty-type-eq-decl nil traces nil)
(pc const-decl "pc(prog(j))" traces nil)
(nat_induction formula-decl nil naturalnumbers nil))
nil nil nil nil))
(pc_before_dispatch 0
(pc_before_dispatch-1 nil 3237060222 nil
("" (auto-rewrite "pc" "P" "time_invariant")
(("" (skosimp)
(("" (typepred "u!1(t!1)") (("" (reduce) nil nil)) nil)) nil))
nil)
proved-complete
((trace nonempty-type-eq-decl nil traces nil)
(+ const-decl "[real, real -> real]" reals nil)
(T const-decl "bool" priority_ceiling nil)
(init_sch const-decl "good_state" priority_ceiling nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(good_state nonempty-type-eq-decl nil priority_ceiling nil)
(P const-decl "bool" priority_ceiling nil)
(sch_state type-eq-decl nil priority_ceiling nil)
(rsrc_state type-eq-decl nil priority_ceiling nil)
(dispatch formal-const-decl "[job -> nat]" traces nil)
(prio formal-const-decl "[job -> priority]" traces nil)
(priority nonempty-type-eq-decl nil basic_types nil)
(maxprio const-decl "posnat" basic_types nil)
(> const-decl "bool" reals nil)
(nonneg_int nonempty-type-eq-decl nil integers nil)
(< const-decl "bool" reals nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(>= const-decl "bool" reals nil)
(int nonempty-type-eq-decl nil integers nil)
(integer_pred const-decl "[rational -> boolean]" integers nil)
(rational nonempty-type-from-decl nil rationals nil)
(rational_pred const-decl "[real -> boolean]" rationals nil)
(real nonempty-type-from-decl nil reals nil)
(real_pred const-decl "[number -> boolean]" reals nil)
(number nonempty-type-decl nil numbers nil)
(prog formal-const-decl
"[job -> prog]"
traces nil)
(prog type-eq-decl
nil
programs nil)
(command type-decl nil command_adt nil)
(below type-eq-decl nil naturalnumbers nil)
(posnat nonempty-type-eq-decl nil integers nil)
(pc nonempty-type-eq-decl nil programs nil)
(job formal-type-decl nil traces nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil)
(time_invariant formula-decl nil traces nil)
(pc const-decl "pc(prog(j))" traces nil))
nil nil nil nil))
(active_ready 0
(active_ready-1 nil 3237060222 nil
("" (expand* "active" "ready")
(("" (skosimp) (("" (forward-chain "eligible_ready") nil nil))
nil))
nil)
proved-complete
((ready const-decl "bool" traces nil)
(active const-decl "bool" traces nil)
(eligible_ready formula-decl nil priority_ceiling nil)
(pc nonempty-type-eq-decl nil programs nil)
(rsrc_state type-eq-decl nil priority_ceiling nil)
(sch_state type-eq-decl nil priority_ceiling nil)
(P const-decl "bool" priority_ceiling nil)
(good_state nonempty-type-eq-decl nil priority_ceiling nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(init_sch const-decl "good_state" priority_ceiling nil)
(T const-decl "bool" priority_ceiling nil)
(+ const-decl "[real, real -> real]" reals nil)
(trace nonempty-type-eq-decl nil traces nil)
(job formal-type-decl nil traces nil)
(number nonempty-type-decl nil numbers nil)
(boolean nonempty-type-decl nil booleans nil)
(real_pred const-decl "[number -> boolean]" reals nil)
(real nonempty-type-from-decl nil reals nil)
(rational_pred const-decl "[real -> boolean]" rationals nil)
(rational nonempty-type-from-decl nil rationals nil)
(integer_pred const-decl "[rational -> boolean]" integers nil)
(int nonempty-type-eq-decl nil integers nil)
(bool nonempty-type-eq-decl nil booleans nil)
(>= const-decl "bool" reals nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(< const-decl "bool" reals nil)
(nonneg_int nonempty-type-eq-decl nil integers nil)
(> const-decl "bool" reals nil)
(posnat nonempty-type-eq-decl nil integers nil)
(maxprio const-decl "posnat" basic_types nil)
(priority nonempty-type-eq-decl nil basic_types nil)
(prio formal-const-decl "[job -> priority]" traces nil)
(dispatch formal-const-decl "[job -> nat]" traces nil)
(below type-eq-decl nil naturalnumbers nil)
(command type-decl nil command_adt nil)
(prog type-eq-decl
nil
programs nil)
(prog formal-const-decl
"[job -> prog]"
traces nil))
nil nil nil nil))
(active_unique 0
(active_unique-1 nil 3237060222 nil
("" (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)
proved-complete
((active const-decl "bool" traces nil)
(eligible_ready formula-decl nil priority_ceiling nil)
(pc nonempty-type-eq-decl nil programs nil)
(rsrc_state type-eq-decl nil priority_ceiling nil)
(sch_state type-eq-decl nil priority_ceiling nil)
(P const-decl "bool" priority_ceiling nil)
(good_state nonempty-type-eq-decl nil priority_ceiling nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(init_sch const-decl "good_state" priority_ceiling nil)
(T const-decl "bool" priority_ceiling nil)
(+ const-decl "[real, real -> real]" reals nil)
(trace nonempty-type-eq-decl nil traces nil)
(job formal-type-decl nil traces nil)
(number nonempty-type-decl nil numbers nil)
(boolean nonempty-type-decl nil booleans nil)
(real_pred const-decl "[number -> boolean]" reals nil)
(real nonempty-type-from-decl nil reals nil)
(rational_pred const-decl "[real -> boolean]" rationals nil)
(rational nonempty-type-from-decl nil rationals nil)
(integer_pred const-decl "[rational -> boolean]" integers nil)
(int nonempty-type-eq-decl nil integers nil)
(bool nonempty-type-eq-decl nil booleans nil)
(>= const-decl "bool" reals nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(< const-decl "bool" reals nil)
(nonneg_int nonempty-type-eq-decl nil integers nil)
(> const-decl "bool" reals nil)
(posnat nonempty-type-eq-decl nil integers nil)
(maxprio const-decl "posnat" basic_types nil)
(priority nonempty-type-eq-decl nil basic_types nil)
(prio formal-const-decl "[job -> priority]" traces nil)
(dispatch formal-const-decl "[job -> nat]" traces nil)
(below type-eq-decl nil naturalnumbers nil)
(command type-decl nil command_adt nil)
(prog type-eq-decl
nil
programs nil)
(prog formal-const-decl
"[job -> prog]"
traces nil)
(ready const-decl "bool" priority_ceiling nil)
(step const-decl "sch_state" priority_ceiling nil))
nil nil nil nil))
(ready_after_dispatch 0
(ready_after_dispatch-1 nil 3237060222 nil
("" (auto-rewrite "time_invariant" "ready")
(("" (skosimp) (("" (assert) (("" (assert) nil nil)) nil)) nil))
nil)
proved-complete
((ready const-decl "bool" traces nil)
(ready const-decl "bool" priority_ceiling nil)
(job formal-type-decl nil traces nil)
(number nonempty-type-decl nil numbers nil)
(boolean nonempty-type-decl nil booleans nil)
(real_pred const-decl "[number -> boolean]" reals nil)
(real nonempty-type-from-decl nil reals nil)
(rational_pred const-decl "[real -> boolean]" rationals nil)
(rational nonempty-type-from-decl nil rationals nil)
(integer_pred const-decl "[rational -> boolean]" integers nil)
(int nonempty-type-eq-decl nil integers nil)
(bool nonempty-type-eq-decl nil booleans nil)
(>= const-decl "bool" reals nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(< const-decl "bool" reals nil)
(nonneg_int nonempty-type-eq-decl nil integers nil)
(> const-decl "bool" reals nil)
(posnat nonempty-type-eq-decl nil integers nil)
(maxprio const-decl "posnat" basic_types nil)
(priority nonempty-type-eq-decl nil basic_types nil)
(prio formal-const-decl "[job -> priority]" traces nil)
(dispatch formal-const-decl "[job -> nat]" traces nil)
(below type-eq-decl nil naturalnumbers nil)
(command type-decl nil command_adt nil)
(prog type-eq-decl
nil
programs nil)
(prog formal-const-decl
"[job -> prog]"
traces nil)
(time_invariant formula-decl nil traces nil))
nil nil nil nil))
(ready_equiv 0
(ready_equiv-1 nil 3237060222 nil
("" (skolem!) (("" (grind :rewrites ("time_invariant")) nil nil))
nil)
proved-complete
((time_invariant formula-decl nil traces nil)
(complete const-decl "bool" programs nil)
(prog formal-const-decl
"[job -> prog]"
traces nil)
(prog type-eq-decl
nil
programs nil)
(command type-decl nil command_adt nil)
(below type-eq-decl nil naturalnumbers nil)
(dispatch formal-const-decl "[job -> nat]" traces nil)
(prio formal-const-decl "[job -> priority]" traces nil)
(priority nonempty-type-eq-decl nil basic_types nil)
(maxprio const-decl "posnat" basic_types nil)
(posnat nonempty-type-eq-decl nil integers nil)
(> const-decl "bool" reals nil)
(nonneg_int nonempty-type-eq-decl nil integers nil)
(< const-decl "bool" reals nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(>= const-decl "bool" reals nil)
(bool nonempty-type-eq-decl nil booleans nil)
(int nonempty-type-eq-decl nil integers nil)
(integer_pred const-decl "[rational -> boolean]" integers nil)
(rational nonempty-type-from-decl nil rationals nil)
(rational_pred const-decl "[real -> boolean]" rationals nil)
(real nonempty-type-from-decl nil reals nil)
(real_pred const-decl "[number -> boolean]" reals nil)
(boolean nonempty-type-decl nil booleans nil)
(number nonempty-type-decl nil numbers nil)
(job formal-type-decl nil traces nil)
(finished const-decl "bool" priority_ceiling nil)
(ready const-decl "bool" priority_ceiling nil)
(ready const-decl "bool" traces nil)
(pc const-decl "pc(prog(j))" traces nil))
nil nil nil nil))
(ready_at_dispatch 0
(ready_at_dispatch-1 nil 3237060222 nil
("" (skolem!)
(("" (auto-rewrite "ready_equiv" "pc_before_dispatch")
(("" (assert) nil nil)) nil))
nil)
proved-complete
((ready_equiv formula-decl nil traces nil)
(pc_before_dispatch formula-decl nil traces nil))
nil nil nil nil))
(finished_equiv 0
(finished_equiv-1 nil 3237060222 nil
("" (skolem!) (("" (grind) nil nil)) nil) proved-complete
((pc const-decl "pc(prog(j))" traces nil)
(finished const-decl "bool" traces nil)
(finished const-decl "bool" priority_ceiling nil)
(job formal-type-decl nil traces nil)
(number nonempty-type-decl nil numbers nil)
(boolean nonempty-type-decl nil booleans nil)
(real_pred const-decl "[number -> boolean]" reals nil)
(real nonempty-type-from-decl nil reals nil)
(rational_pred const-decl "[real -> boolean]" rationals nil)
(rational nonempty-type-from-decl nil rationals nil)
(integer_pred const-decl "[rational -> boolean]" integers nil)
(int nonempty-type-eq-decl nil integers nil)
(bool nonempty-type-eq-decl nil booleans nil)
(>= const-decl "bool" reals nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(< const-decl "bool" reals nil)
(nonneg_int nonempty-type-eq-decl nil integers nil)
(> const-decl "bool" reals nil)
(posnat nonempty-type-eq-decl nil integers nil)
(maxprio const-decl "posnat" basic_types nil)
(priority nonempty-type-eq-decl nil basic_types nil)
(prio formal-const-decl "[job -> priority]" traces nil)
(dispatch formal-const-decl "[job -> nat]" traces nil)
(below type-eq-decl nil naturalnumbers nil)
(command type-decl nil command_adt nil)
(prog type-eq-decl
nil
programs nil)
(prog formal-const-decl
"[job -> prog]"
traces nil)
(complete const-decl "bool" programs nil))
nil nil nil nil))
(finished_stable 0
(finished_stable-1 nil 3237060222 nil
("" (auto-rewrite "finished_equiv")
(("" (skosimp)
(("" (assert)
(("" (use "pc_increasing" ("t2" "t2!1"))
(("" (assert) nil nil)) nil))
nil))
nil))
nil)
proved-complete
((finished_equiv formula-decl nil traces nil)
(job formal-type-decl nil traces nil)
(pc nonempty-type-eq-decl nil programs nil)
(posnat nonempty-type-eq-decl nil integers nil)
(below type-eq-decl nil naturalnumbers nil)
(command type-decl nil command_adt nil)
(prog type-eq-decl
nil
programs nil)
(prog formal-const-decl
"[job -> prog]"
traces nil)
(< const-decl "bool" reals nil)
(nonneg_int nonempty-type-eq-decl nil integers nil)
(> const-decl "bool" reals nil)
(maxprio const-decl "posnat" basic_types nil)
(priority nonempty-type-eq-decl nil basic_types nil)
(prio formal-const-decl "[job -> priority]" traces nil)
(dispatch formal-const-decl "[job -> nat]" traces nil)
(rsrc_state type-eq-decl nil priority_ceiling nil)
(sch_state type-eq-decl nil priority_ceiling nil)
(P const-decl "bool" priority_ceiling nil)
(good_state nonempty-type-eq-decl nil priority_ceiling nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(init_sch const-decl "good_state" priority_ceiling nil)
(T const-decl "bool" priority_ceiling nil)
(+ const-decl "[real, real -> real]" reals nil)
(trace nonempty-type-eq-decl nil traces nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(>= const-decl "bool" reals nil)
(bool nonempty-type-eq-decl nil booleans nil)
(int nonempty-type-eq-decl nil integers nil)
(integer_pred const-decl "[rational -> boolean]" integers nil)
(rational nonempty-type-from-decl nil rationals nil)
(rational_pred const-decl "[real -> boolean]" rationals nil)
(real nonempty-type-from-decl nil reals nil)
(real_pred const-decl "[number -> boolean]" reals nil)
(boolean nonempty-type-decl nil booleans nil)
(number nonempty-type-decl nil numbers nil)
(pc_increasing formula-decl nil traces nil))
nil nil nil nil))
(readiness 0
(readiness-1 nil 3237060222 nil
("" (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)
proved-complete
((step_trace formula-decl nil traces nil)
(idle const-decl "bool" priority_ceiling nil)
(prog formal-const-decl
"[job -> prog]"
traces nil)
(prog type-eq-decl
nil
programs nil)
(command type-decl nil command_adt nil)
(below type-eq-decl nil naturalnumbers nil)
(dispatch formal-const-decl "[job -> nat]" traces nil)
(prio formal-const-decl "[job -> priority]" traces nil)
(priority nonempty-type-eq-decl nil basic_types nil)
(maxprio const-decl "posnat" basic_types nil)
(posnat nonempty-type-eq-decl nil integers nil)
(> const-decl "bool" reals nil)
(nonneg_int nonempty-type-eq-decl nil integers nil)
(< const-decl "bool" reals nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(>= const-decl "bool" reals nil)
(bool nonempty-type-eq-decl nil booleans nil)
(int nonempty-type-eq-decl nil integers nil)
(integer_pred const-decl "[rational -> boolean]" integers nil)
(rational nonempty-type-from-decl nil rationals nil)
(rational_pred const-decl "[real -> boolean]" rationals nil)
(real nonempty-type-from-decl nil reals nil)
(real_pred const-decl "[number -> boolean]" reals nil)
(boolean nonempty-type-decl nil booleans nil)
(number nonempty-type-decl nil numbers nil)
(job formal-type-decl nil traces nil)
(trace nonempty-type-eq-decl nil traces nil)
(+ const-decl "[real, real -> real]" reals nil)
(T const-decl "bool" priority_ceiling nil)
(init_sch const-decl "good_state" priority_ceiling nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(good_state nonempty-type-eq-decl nil priority_ceiling nil)
(P const-decl "bool" priority_ceiling nil)
(sch_state type-eq-decl nil priority_ceiling nil)
(rsrc_state type-eq-decl nil priority_ceiling nil)
(pc nonempty-type-eq-decl nil programs nil)
(eligible_exists formula-decl nil priority_ceiling nil)
(ready const-decl "bool" traces nil)
(active const-decl "bool" traces nil))
nil nil nil nil))
(readiness_step2 0
(readiness_step2-1 nil 3237060222 nil
("" (auto-rewrite "step_trace" "time_invariant")
(("" (expand "ready")
(("" (skosimp)
(("" (use "readiness_step" ("g1" "u!1(t!1)"))
(("" (assert) nil nil)) nil))
nil))
nil))
nil)
proved-complete
((step_trace formula-decl nil traces nil)
(time_invariant formula-decl nil traces nil)
(prog formal-const-decl
"[job -> prog]"
traces nil)
(prog type-eq-decl
nil
programs nil)
(command type-decl nil command_adt nil)
(below type-eq-decl nil naturalnumbers nil)
(dispatch formal-const-decl "[job -> nat]" traces nil)
(prio formal-const-decl "[job -> priority]" traces nil)
(priority nonempty-type-eq-decl nil basic_types nil)
(maxprio const-decl "posnat" basic_types nil)
(posnat nonempty-type-eq-decl nil integers nil)
(> const-decl "bool" reals nil)
(nonneg_int nonempty-type-eq-decl nil integers nil)
(< const-decl "bool" reals nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(>= const-decl "bool" reals nil)
(bool nonempty-type-eq-decl nil booleans nil)
(int nonempty-type-eq-decl nil integers nil)
(integer_pred const-decl "[rational -> boolean]" integers nil)
(rational nonempty-type-from-decl nil rationals nil)
(rational_pred const-decl "[real -> boolean]" rationals nil)
(real nonempty-type-from-decl nil reals nil)
(real_pred const-decl "[number -> boolean]" reals nil)
(boolean nonempty-type-decl nil booleans nil)
(number nonempty-type-decl nil numbers nil)
(job formal-type-decl nil traces nil)
(trace nonempty-type-eq-decl nil traces nil)
(+ const-decl "[real, real -> real]" reals nil)
(T const-decl "bool" priority_ceiling nil)
(init_sch const-decl "good_state" priority_ceiling nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(good_state nonempty-type-eq-decl nil priority_ceiling nil)
(P const-decl "bool" priority_ceiling nil)
(sch_state type-eq-decl nil priority_ceiling nil)
(rsrc_state type-eq-decl nil priority_ceiling nil)
(pc nonempty-type-eq-decl nil programs nil)
(readiness_step formula-decl nil priority_ceiling nil)
(ready const-decl "bool" traces nil))
nil nil nil nil))
(readiness_interval 0
(readiness_interval-1 nil 3237060222 nil
("" (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)
proved-complete
((ready const-decl "bool" priority_ceiling nil)
(complete const-decl "bool" programs nil)
(finished const-decl "bool" priority_ceiling nil)
(ready const-decl "bool" traces nil)
(pc const-decl "pc(prog(j))" traces nil)
(pc nonempty-type-eq-decl nil programs nil)
(posnat nonempty-type-eq-decl nil integers nil)
(below type-eq-decl nil naturalnumbers nil)
(command type-decl nil command_adt nil)
(prog type-eq-decl
nil
programs nil)
(prog formal-const-decl
"[job -> prog]"
traces nil)
(< const-decl "bool" reals nil)
(nonneg_int nonempty-type-eq-decl nil integers nil)
(> const-decl "bool" reals nil)
(maxprio const-decl "posnat" basic_types nil)
(priority nonempty-type-eq-decl nil basic_types nil)
(prio formal-const-decl "[job -> priority]" traces nil)
(dispatch formal-const-decl "[job -> nat]" traces nil)
(rsrc_state type-eq-decl nil priority_ceiling nil)
(sch_state type-eq-decl nil priority_ceiling nil)
(P const-decl "bool" priority_ceiling nil)
(good_state nonempty-type-eq-decl nil priority_ceiling nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(init_sch const-decl "good_state" priority_ceiling nil)
(T const-decl "bool" priority_ceiling nil)
(+ const-decl "[real, real -> real]" reals nil)
(trace nonempty-type-eq-decl nil traces nil)
(job formal-type-decl nil traces nil)
(number nonempty-type-decl nil numbers nil)
(boolean nonempty-type-decl nil booleans nil)
(real_pred const-decl "[number -> boolean]" reals nil)
(real nonempty-type-from-decl nil reals nil)
(rational_pred const-decl "[real -> boolean]" rationals nil)
(rational nonempty-type-from-decl nil rationals nil)
(integer_pred const-decl "[rational -> boolean]" integers nil)
(int nonempty-type-eq-decl nil integers nil)
(bool nonempty-type-eq-decl nil booleans nil)
(>= const-decl "bool" reals nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(pc_increasing formula-decl nil traces nil)
(time_invariant formula-decl nil traces nil))
nil nil nil nil))
(active_prio 0
(active_prio-1 nil 3237060222 nil
("" (expand* "active" "ready" "blockers")
(("" (skosimp)
(("" (use "invariance_Q")
(("" (forward-chain "eligible_prio") nil nil)) nil))
nil))
nil)
proved-complete
((ready const-decl "bool" traces nil) nil
(active const-decl "bool" traces nil)
(invariance_Q formula-decl nil traces nil)
(trace nonempty-type-eq-decl nil traces nil)
(+ const-decl "[real, real -> real]" reals nil)
(T const-decl "bool" priority_ceiling nil)
(init_sch const-decl "good_state" priority_ceiling nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(good_state nonempty-type-eq-decl nil priority_ceiling nil)
(P const-decl "bool" priority_ceiling nil)
(sch_state type-eq-decl nil priority_ceiling nil)
(rsrc_state type-eq-decl nil priority_ceiling nil)
(dispatch formal-const-decl "[job -> nat]" traces nil)
(prio formal-const-decl "[job -> priority]" traces nil)
(priority nonempty-type-eq-decl nil basic_types nil)
(maxprio const-decl "posnat" basic_types nil)
(> const-decl "bool" reals nil)
(nonneg_int nonempty-type-eq-decl nil integers nil)
(< const-decl "bool" reals nil)
(prog formal-const-decl
"[job -> prog]"
traces nil)
(prog type-eq-decl
nil
programs nil)
(command type-decl nil command_adt nil)
(below type-eq-decl nil naturalnumbers nil)
(posnat nonempty-type-eq-decl nil integers nil)
(pc nonempty-type-eq-decl nil programs nil)
(job formal-type-decl nil traces nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(>= const-decl "bool" reals nil)
(bool nonempty-type-eq-decl nil booleans nil)
(int nonempty-type-eq-decl nil integers nil)
(integer_pred const-decl "[rational -> boolean]" integers nil)
(rational nonempty-type-from-decl nil rationals nil)
(rational_pred const-decl "[real -> boolean]" rationals nil)
(real nonempty-type-from-decl nil reals nil)
(real_pred const-decl "[number -> boolean]" reals nil)
(boolean nonempty-type-decl nil booleans nil)
(number nonempty-type-decl nil numbers nil)
(eligible_prio formula-decl nil priority_ceiling nil))
nil nil nil nil))
(active_prio2 0
(active_prio2-1 nil 3237060222 nil
("" (expand* "busy" "blockers" "active" "ready")
(("" (skosimp) (("" (forward-chain "eligible_prio2") nil nil))
nil))
nil)
proved-complete
((ready const-decl "bool" traces nil)
(active const-decl "bool" traces nil) nil
(eligible_prio2 formula-decl nil priority_ceiling nil)
(pc nonempty-type-eq-decl nil programs nil)
(rsrc_state type-eq-decl nil priority_ceiling nil)
(sch_state type-eq-decl nil priority_ceiling nil)
(P const-decl "bool" priority_ceiling nil)
(good_state nonempty-type-eq-decl nil priority_ceiling nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(init_sch const-decl "good_state" priority_ceiling nil)
(T const-decl "bool" priority_ceiling nil)
(+ const-decl "[real, real -> real]" reals nil)
(trace nonempty-type-eq-decl nil traces nil)
(job formal-type-decl nil traces nil)
(number nonempty-type-decl nil numbers nil)
(boolean nonempty-type-decl nil booleans nil)
(real_pred const-decl "[number -> boolean]" reals nil)
(real nonempty-type-from-decl nil reals nil)
(rational_pred const-decl "[real -> boolean]" rationals nil)
(rational nonempty-type-from-decl nil rationals nil)
(integer_pred const-decl "[rational -> boolean]" integers nil)
(int nonempty-type-eq-decl nil integers nil)
(bool nonempty-type-eq-decl nil booleans nil)
(>= const-decl "bool" reals nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(< const-decl "bool" reals nil)
(nonneg_int nonempty-type-eq-decl nil integers nil)
(> const-decl "bool" reals nil)
(posnat nonempty-type-eq-decl nil integers nil)
(maxprio const-decl "posnat" basic_types nil)
(priority nonempty-type-eq-decl nil basic_types nil)
(prio formal-const-decl "[job -> priority]" traces nil)
(dispatch formal-const-decl "[job -> nat]" traces nil)
(below type-eq-decl nil naturalnumbers nil)
(command type-decl nil command_adt nil)
(prog type-eq-decl
nil
programs nil)
(prog formal-const-decl
"[job -> prog]"
traces nil))
nil nil nil nil))
(single_blocker 0
(single_blocker-1 nil 3237060222 nil
("" (expand "blockers")
(("" (skosimp)
(("" (auto-rewrite "invariance_P2")
(("" (use "unique_blocker") (("" (assert) nil nil)) nil)) nil))
nil))
nil)
proved-complete
(nil (invariance_P2 formula-decl nil traces nil)
(rsrc_set type-eq-decl nil basic_types nil)
(rsrc_state type-eq-decl nil priority_ceiling nil)
(pc nonempty-type-eq-decl nil programs nil)
(sch_state type-eq-decl nil priority_ceiling nil)
(P const-decl "bool" priority_ceiling nil)
(good_state nonempty-type-eq-decl nil priority_ceiling nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(init_sch const-decl "good_state" priority_ceiling nil)
(T const-decl "bool" priority_ceiling nil)
(+ const-decl "[real, real -> real]" reals nil)
(trace nonempty-type-eq-decl nil traces nil)
(prog formal-const-decl
"[job -> prog]"
traces nil)
(prog type-eq-decl
nil
programs nil)
(command type-decl nil command_adt nil)
(below type-eq-decl nil naturalnumbers nil)
(dispatch formal-const-decl "[job -> nat]" traces nil)
(prio formal-const-decl "[job -> priority]" traces nil)
(priority nonempty-type-eq-decl nil basic_types nil)
(maxprio const-decl "posnat" basic_types nil)
(posnat nonempty-type-eq-decl nil integers nil)
(> const-decl "bool" reals nil)
(nonneg_int nonempty-type-eq-decl nil integers nil)
(< const-decl "bool" reals nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(>= const-decl "bool" reals nil)
(bool nonempty-type-eq-decl nil booleans nil)
(int nonempty-type-eq-decl nil integers nil)
(integer_pred const-decl "[rational -> boolean]" integers nil)
(rational nonempty-type-from-decl nil rationals nil)
(rational_pred const-decl "[real -> boolean]" rationals nil)
(real nonempty-type-from-decl nil reals nil)
(real_pred const-decl "[number -> boolean]" reals nil)
(boolean nonempty-type-decl nil booleans nil)
(number nonempty-type-decl nil numbers nil)
(job formal-type-decl nil traces nil)
(unique_blocker formula-decl nil priority_ceiling nil))
nil nil nil nil))
(single_blocker2 0
(single_blocker2-1 nil 3237060222 nil
("" (auto-rewrite "invariance_P2" "blockers")
(("" (skosimp)
(("" (assert)
(("" (use "unique_blocker2") (("" (assert) nil nil)) nil))
nil))
nil))
nil)
proved-complete
(nil (invariance_P2 formula-decl nil traces nil)
(rsrc_set type-eq-decl nil basic_types nil)
(rsrc_state type-eq-decl nil priority_ceiling nil)
(pc nonempty-type-eq-decl nil programs nil)
(sch_state type-eq-decl nil priority_ceiling nil)
(P const-decl "bool" priority_ceiling nil)
(good_state nonempty-type-eq-decl nil priority_ceiling nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(init_sch const-decl "good_state" priority_ceiling nil)
(T const-decl "bool" priority_ceiling nil)
(+ const-decl "[real, real -> real]" reals nil)
(trace nonempty-type-eq-decl nil traces nil)
(prog formal-const-decl
"[job -> prog]"
traces nil)
(prog type-eq-decl
nil
programs nil)
(command type-decl nil command_adt nil)
(below type-eq-decl nil naturalnumbers nil)
(dispatch formal-const-decl "[job -> nat]" traces nil)
(prio formal-const-decl "[job -> priority]" traces nil)
(priority nonempty-type-eq-decl nil basic_types nil)
(maxprio const-decl "posnat" basic_types nil)
(posnat nonempty-type-eq-decl nil integers nil)
(> const-decl "bool" reals nil)
(nonneg_int nonempty-type-eq-decl nil integers nil)
(< const-decl "bool" reals nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(>= const-decl "bool" reals nil)
(bool nonempty-type-eq-decl nil booleans nil)
(int nonempty-type-eq-decl nil integers nil)
(integer_pred const-decl "[rational -> boolean]" integers nil)
(rational nonempty-type-from-decl nil rationals nil)
(rational_pred const-decl "[real -> boolean]" rationals nil)
(real nonempty-type-from-decl nil reals nil)
(real_pred const-decl "[number -> boolean]" reals nil)
(boolean nonempty-type-decl nil booleans nil)
(number nonempty-type-decl nil numbers nil)
(job formal-type-decl nil traces nil)
(unique_blocker2 formula-decl nil priority_ceiling nil))
nil nil nil nil))
(blocker_in_cs 0
(blocker_in_cs-1 nil 3237060222 nil
("" (expand* "blockers" "pc")
(("" (skosimp) (("" (rewrite "blockers_in_cs") nil nil)) nil)) nil)
proved-complete
((pc const-decl "pc(prog(j))" traces nil) nil
(blockers_in_cs formula-decl nil priority_ceiling nil)
(pc nonempty-type-eq-decl nil programs nil)
(rsrc_state type-eq-decl nil priority_ceiling nil)
(sch_state type-eq-decl nil priority_ceiling nil)
(P const-decl "bool" priority_ceiling nil)
(good_state nonempty-type-eq-decl nil priority_ceiling nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(init_sch const-decl "good_state" priority_ceiling nil)
(T const-decl "bool" priority_ceiling nil)
(+ const-decl "[real, real -> real]" reals nil)
(trace nonempty-type-eq-decl nil traces nil)
(job formal-type-decl nil traces nil)
(number nonempty-type-decl nil numbers nil)
(boolean nonempty-type-decl nil booleans nil)
(real_pred const-decl "[number -> boolean]" reals nil)
(real nonempty-type-from-decl nil reals nil)
(rational_pred const-decl "[real -> boolean]" rationals nil)
(rational nonempty-type-from-decl nil rationals nil)
(integer_pred const-decl "[rational -> boolean]" integers nil)
(int nonempty-type-eq-decl nil integers nil)
(bool nonempty-type-eq-decl nil booleans nil)
(>= const-decl "bool" reals nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(< const-decl "bool" reals nil)
(nonneg_int nonempty-type-eq-decl nil integers nil)
(> const-decl "bool" reals nil)
(posnat nonempty-type-eq-decl nil integers nil)
(maxprio const-decl "posnat" basic_types nil)
(priority nonempty-type-eq-decl nil basic_types nil)
(prio formal-const-decl "[job -> priority]" traces nil)
(dispatch formal-const-decl "[job -> nat]" traces nil)
(below type-eq-decl nil naturalnumbers nil)
(command type-decl nil command_adt nil)
(prog type-eq-decl
nil
programs nil)
(prog formal-const-decl
"[job -> prog]"
traces nil))
nil nil nil nil))
(blocker_in_cs2 0
(blocker_in_cs2-1 nil 3237060222 nil
("" (auto-rewrite "pc" "blockers" "time_invariant")
(("" (skosimp)
(("" (assert) (("" (forward-chain "blockers_in_cs2") nil nil))
nil))
nil))
nil)
proved-complete
((pc const-decl "pc(prog(j))" traces nil) nil
(prog formal-const-decl
"[job -> prog]"
traces nil)
(prog type-eq-decl
nil
programs nil)
(command type-decl nil command_adt nil)
(below type-eq-decl nil naturalnumbers nil)
(dispatch formal-const-decl "[job -> nat]" traces nil)
(prio formal-const-decl "[job -> priority]" traces nil)
(priority nonempty-type-eq-decl nil basic_types nil)
(maxprio const-decl "posnat" basic_types nil)
(posnat nonempty-type-eq-decl nil integers nil)
(> const-decl "bool" reals nil)
(nonneg_int nonempty-type-eq-decl nil integers nil)
(< const-decl "bool" reals nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(>= const-decl "bool" reals nil)
(bool nonempty-type-eq-decl nil booleans nil)
(int nonempty-type-eq-decl nil integers nil)
(integer_pred const-decl "[rational -> boolean]" integers nil)
(rational nonempty-type-from-decl nil rationals nil)
(rational_pred const-decl "[real -> boolean]" rationals nil)
(real nonempty-type-from-decl nil reals nil)
(real_pred const-decl "[number -> boolean]" reals nil)
(boolean nonempty-type-decl nil booleans nil)
(number nonempty-type-decl nil numbers nil)
(job formal-type-decl nil traces nil)
(trace nonempty-type-eq-decl nil traces nil)
(+ const-decl "[real, real -> real]" reals nil)
(T const-decl "bool" priority_ceiling nil)
(init_sch const-decl "good_state" priority_ceiling nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(good_state nonempty-type-eq-decl nil priority_ceiling nil)
(P const-decl "bool" priority_ceiling nil)
(sch_state type-eq-decl nil priority_ceiling nil)
(rsrc_state type-eq-decl nil priority_ceiling nil)
(pc nonempty-type-eq-decl nil programs nil)
(blockers_in_cs2 formula-decl nil priority_ceiling nil))
nil nil nil nil))
(blocker_step 0
(blocker_step-1 nil 3237060222 nil
("" (auto-rewrite "step_trace" "invariance_Q")
(("" (expand* "ready" "blockers")
(("" (skosimp) (("" (rewrite "blockers_step") nil nil)) nil))
nil))
nil)
proved-complete
((prog formal-const-decl
"[job -> prog]"
traces nil)
(prog type-eq-decl
nil
programs nil)
(command type-decl nil command_adt nil)
(below type-eq-decl nil naturalnumbers nil)
(dispatch formal-const-decl "[job -> nat]" traces nil)
(prio formal-const-decl "[job -> priority]" traces nil)
(priority nonempty-type-eq-decl nil basic_types nil)
(maxprio const-decl "posnat" basic_types nil)
(posnat nonempty-type-eq-decl nil integers nil)
(> const-decl "bool" reals nil)
(nonneg_int nonempty-type-eq-decl nil integers nil)
(< const-decl "bool" reals nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(>= const-decl "bool" reals nil)
(bool nonempty-type-eq-decl nil booleans nil)
(int nonempty-type-eq-decl nil integers nil)
(integer_pred const-decl "[rational -> boolean]" integers nil)
(rational nonempty-type-from-decl nil rationals nil)
(rational_pred const-decl "[real -> boolean]" rationals nil)
(real nonempty-type-from-decl nil reals nil)
(real_pred const-decl "[number -> boolean]" reals nil)
(boolean nonempty-type-decl nil booleans nil)
(number nonempty-type-decl nil numbers nil)
(job formal-type-decl nil traces nil)
(trace nonempty-type-eq-decl nil traces nil)
(+ const-decl "[real, real -> real]" reals nil)
(T const-decl "bool" priority_ceiling nil)
(init_sch const-decl "good_state" priority_ceiling nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(good_state nonempty-type-eq-decl nil priority_ceiling nil)
(P const-decl "bool" priority_ceiling nil)
(sch_state type-eq-decl nil priority_ceiling nil)
(rsrc_state type-eq-decl nil priority_ceiling nil)
(pc nonempty-type-eq-decl nil programs nil)
(blockers_step formula-decl nil priority_ceiling nil)
(invariance_Q formula-decl nil traces nil)
(step_trace formula-decl nil traces nil)
(ready const-decl "bool" traces nil) nil)
nil nil nil nil))
(blocker_step2 0
(blocker_step2-1 nil 3237060222 nil
("" (expand* "busy" "blockers" "ready")
(("" (auto-rewrite "step_trace")
(("" (skosimp) (("" (rewrite "blockers_step2") nil nil)) nil))
nil))
nil)
proved-complete
((ready const-decl "bool" traces nil) nil
(prog formal-const-decl
"[job -> prog]"
traces nil)
(prog type-eq-decl
nil
programs nil)
(command type-decl nil command_adt nil)
(below type-eq-decl nil naturalnumbers nil)
(dispatch formal-const-decl "[job -> nat]" traces nil)
(prio formal-const-decl "[job -> priority]" traces nil)
(priority nonempty-type-eq-decl nil basic_types nil)
(maxprio const-decl "posnat" basic_types nil)
(posnat nonempty-type-eq-decl nil integers nil)
(> const-decl "bool" reals nil)
(nonneg_int nonempty-type-eq-decl nil integers nil)
(< const-decl "bool" reals nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(>= const-decl "bool" reals nil)
(bool nonempty-type-eq-decl nil booleans nil)
(int nonempty-type-eq-decl nil integers nil)
(integer_pred const-decl "[rational -> boolean]" integers nil)
(rational nonempty-type-from-decl nil rationals nil)
(rational_pred const-decl "[real -> boolean]" rationals nil)
(real nonempty-type-from-decl nil reals nil)
(real_pred const-decl "[number -> boolean]" reals nil)
(boolean nonempty-type-decl nil booleans nil)
(number nonempty-type-decl nil numbers nil)
(job formal-type-decl nil traces nil)
(trace nonempty-type-eq-decl nil traces nil)
(+ const-decl "[real, real -> real]" reals nil)
(T const-decl "bool" priority_ceiling nil)
(init_sch const-decl "good_state" priority_ceiling nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(good_state nonempty-type-eq-decl nil priority_ceiling nil)
(P const-decl "bool" priority_ceiling nil)
(sch_state type-eq-decl nil priority_ceiling nil)
(rsrc_state type-eq-decl nil priority_ceiling nil)
(pc nonempty-type-eq-decl nil programs nil)
(blockers_step2 formula-decl nil priority_ceiling nil)
(step_trace formula-decl nil traces nil))
nil nil nil nil))
(mutual_exclusion 0
(mutual_exclusion-1 nil 3237060222 nil
("" (skosimp)
(("" (expand "alloc")
((""
(auto-rewrite "invariance_P2" "invar_P2_aux"
"mutual_exclusion")
(("" (assert) nil nil)) nil))
nil))
nil)
proved-complete
((invariance_P2 formula-decl nil traces nil)
(prog formal-const-decl
"[job -> prog]"
traces nil)
(prog type-eq-decl
nil
programs nil)
(command type-decl nil command_adt nil)
(below type-eq-decl nil naturalnumbers nil)
(dispatch formal-const-decl "[job -> nat]" traces nil)
(prio formal-const-decl "[job -> priority]" traces nil)
(priority nonempty-type-eq-decl nil basic_types nil)
(maxprio const-decl "posnat" basic_types nil)
(posnat nonempty-type-eq-decl nil integers nil)
(> const-decl "bool" reals nil)
(nonneg_int nonempty-type-eq-decl nil integers nil)
(< const-decl "bool" reals nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(>= const-decl "bool" reals nil)
(bool nonempty-type-eq-decl nil booleans nil)
(int nonempty-type-eq-decl nil integers nil)
(integer_pred const-decl "[rational -> boolean]" integers nil)
(rational nonempty-type-from-decl nil rationals nil)
(rational_pred const-decl "[real -> boolean]" rationals nil)
(real nonempty-type-from-decl nil reals nil)
(real_pred const-decl "[number -> boolean]" reals nil)
(boolean nonempty-type-decl nil booleans nil)
(number nonempty-type-decl nil numbers nil)
(job formal-type-decl nil traces nil)
(invar_P2_aux formula-decl nil priority_ceiling nil)
(mutual_exclusion formula-decl nil priority_ceiling nil)
(alloc const-decl "rsrc_set" traces nil))
nil nil nil nil))
(sch_TCC1 0
(sch_TCC1-1 nil 3237060222 nil
("" (skosimp*)
(("" (use "active_unique") (("" (assert) nil nil)) nil)) nil)
proved-complete
((job formal-type-decl nil traces nil)
(number nonempty-type-decl nil numbers nil)
(boolean nonempty-type-decl nil booleans nil)
(real_pred const-decl "[number -> boolean]" reals nil)
(real nonempty-type-from-decl nil reals nil)
(rational_pred const-decl "[real -> boolean]" rationals nil)
(rational nonempty-type-from-decl nil rationals nil)
(integer_pred const-decl "[rational -> boolean]" integers nil)
(int nonempty-type-eq-decl nil integers nil)
(bool nonempty-type-eq-decl nil booleans nil)
(>= const-decl "bool" reals nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(pc nonempty-type-eq-decl nil programs nil)
(posnat nonempty-type-eq-decl nil integers nil)
(below type-eq-decl nil naturalnumbers nil)
(command type-decl nil command_adt nil)
(prog type-eq-decl
nil
programs nil)
(prog formal-const-decl
"[job -> prog]"
traces nil)
(< const-decl "bool" reals nil)
(nonneg_int nonempty-type-eq-decl nil integers nil)
(> const-decl "bool" reals nil)
(maxprio const-decl "posnat" basic_types nil)
(priority nonempty-type-eq-decl nil basic_types nil)
(prio formal-const-decl "[job -> priority]" traces nil)
(dispatch formal-const-decl "[job -> nat]" traces nil)
(rsrc_state type-eq-decl nil priority_ceiling nil)
(sch_state type-eq-decl nil priority_ceiling nil)
(P const-decl "bool" priority_ceiling nil)
(good_state nonempty-type-eq-decl nil priority_ceiling nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(init_sch const-decl "good_state" priority_ceiling nil)
(T const-decl "bool" priority_ceiling nil)
(+ const-decl "[real, real -> real]" reals nil)
(trace nonempty-type-eq-decl nil traces nil)
(active_unique formula-decl nil traces nil))
nil nil nil nil))
(active_prop 0
(active_prop-1 nil 3237060222 nil
("" (auto-rewrite "sch_TCC1")
(("" (skolem!)
(("" (expand "sch") (("" (rewrite "schedule_from_act1") nil nil))
nil))
nil))
nil)
proved-complete
((sch const-decl "schedule" traces nil)
(job formal-type-decl nil traces nil)
(active const-decl "bool" traces nil)
(trace nonempty-type-eq-decl nil traces nil)
(+ const-decl "[real, real -> real]" reals nil)
(T const-decl "bool" priority_ceiling nil)
(init_sch const-decl "good_state" priority_ceiling nil)
(good_state nonempty-type-eq-decl nil priority_ceiling nil)
(P const-decl "bool" priority_ceiling nil)
(sch_state type-eq-decl nil priority_ceiling nil)
(rsrc_state type-eq-decl nil priority_ceiling nil)
(dispatch formal-const-decl "[job -> nat]" traces nil)
(prio formal-const-decl "[job -> priority]" traces nil)
(priority nonempty-type-eq-decl nil basic_types nil)
(maxprio const-decl "posnat" basic_types nil)
(> const-decl "bool" reals nil)
(nonneg_int nonempty-type-eq-decl nil integers nil)
(< const-decl "bool" reals nil)
(prog formal-const-decl
"[job -> prog]"
traces nil)
(prog type-eq-decl
nil
programs nil)
(command type-decl nil command_adt nil)
(below type-eq-decl nil naturalnumbers nil)
(posnat nonempty-type-eq-decl nil integers nil)
(pc nonempty-type-eq-decl nil programs nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(>= const-decl "bool" reals nil)
(bool nonempty-type-eq-decl nil booleans nil)
(int nonempty-type-eq-decl nil integers nil)
(integer_pred const-decl "[rational -> boolean]" integers nil)
(rational nonempty-type-from-decl nil rationals nil)
(rational_pred const-decl "[real -> boolean]" rationals nil)
(real nonempty-type-from-decl nil reals nil)
(real_pred const-decl "[number -> boolean]" reals nil)
(boolean nonempty-type-decl nil booleans nil)
(number nonempty-type-decl nil numbers nil)
(schedule_from_act1 formula-decl nil schedules nil)
(sch_TCC1 subtype-tcc nil traces nil))
nil nil nil nil))
(process_time1 0
(process_time1-1 nil 3237060222 nil
(""
(induct-and-rewrite "t" 1 "pc_init" "pc_step"
("process_time_init" "process_time_step") "active_prop")
nil nil)
proved-complete
((pc_step formula-decl nil traces nil)
(process_time_step formula-decl nil schedules nil)
(active_prop formula-decl nil traces nil)
(pc_init formula-decl nil traces nil)
(process_time_init formula-decl nil schedules nil)
(nat_induction formula-decl nil naturalnumbers nil)
(pc const-decl "pc(prog(j))" traces nil)
(<= const-decl "bool" reals nil)
(sch const-decl "schedule" traces nil) nil
(schedule type-eq-decl nil schedules nil)
(lift type-decl nil lift_adt nil)
(trace nonempty-type-eq-decl nil traces nil)
(+ const-decl "[real, real -> real]" reals nil)
(T const-decl "bool" priority_ceiling nil)
(init_sch const-decl "good_state" priority_ceiling nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(good_state nonempty-type-eq-decl nil priority_ceiling nil)
(P const-decl "bool" priority_ceiling nil)
(sch_state type-eq-decl nil priority_ceiling nil)
(rsrc_state type-eq-decl nil priority_ceiling nil)
(dispatch formal-const-decl "[job -> nat]" traces nil)
(prio formal-const-decl "[job -> priority]" traces nil)
(priority nonempty-type-eq-decl nil basic_types nil)
(maxprio const-decl "posnat" basic_types nil)
(> const-decl "bool" reals nil)
(nonneg_int nonempty-type-eq-decl nil integers nil)
(< const-decl "bool" reals nil)
(prog formal-const-decl
"[job -> prog]"
traces nil)
(prog type-eq-decl
nil
programs nil)
(command type-decl nil command_adt nil)
(below type-eq-decl nil naturalnumbers nil)
(posnat nonempty-type-eq-decl nil integers nil)
(pc nonempty-type-eq-decl nil programs nil)
(job formal-type-decl nil traces nil)
(pred type-eq-decl nil defined_types nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(>= const-decl "bool" reals nil)
(bool nonempty-type-eq-decl nil booleans nil)
(int nonempty-type-eq-decl nil integers nil)
(integer_pred const-decl "[rational -> boolean]" integers nil)
(rational nonempty-type-from-decl nil rationals nil)
(rational_pred const-decl "[real -> boolean]" rationals nil)
(real nonempty-type-from-decl nil reals nil)
(real_pred const-decl "[number -> boolean]" reals nil)
(boolean nonempty-type-decl nil booleans nil)
(number nonempty-type-decl nil numbers nil))
nil nil nil nil))
(process_time2 0
(process_time2-1 nil 3237060222 nil
("" (auto-rewrite "process_time_equiv2" "process_time1")
(("" (reduce) nil nil)) nil)
proved-complete
((process_time_equiv2 formula-decl nil schedules nil)
(process_time1 formula-decl nil traces nil)
(trace nonempty-type-eq-decl nil traces nil)
(+ const-decl "[real, real -> real]" reals nil)
(T const-decl "bool" priority_ceiling nil)
(init_sch const-decl "good_state" priority_ceiling nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(good_state nonempty-type-eq-decl nil priority_ceiling nil)
(P const-decl "bool" priority_ceiling nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(sch_state type-eq-decl nil priority_ceiling nil)
(rsrc_state type-eq-decl nil priority_ceiling nil)
(dispatch formal-const-decl "[job -> nat]" traces nil)
(prio formal-const-decl "[job -> priority]" traces nil)
(priority nonempty-type-eq-decl nil basic_types nil)
(maxprio const-decl "posnat" basic_types nil)
(> const-decl "bool" reals nil)
(nonneg_int nonempty-type-eq-decl nil integers nil)
(< const-decl "bool" reals nil)
(prog formal-const-decl
"[job -> prog]"
traces nil)
(prog type-eq-decl
nil
programs nil)
(command type-decl nil command_adt nil)
(below type-eq-decl nil naturalnumbers nil)
(posnat nonempty-type-eq-decl nil integers nil)
(pc nonempty-type-eq-decl nil programs nil)
(job formal-type-decl nil traces nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(int nonempty-type-eq-decl nil integers nil)
(integer_pred const-decl "[rational -> boolean]" integers nil)
(rational nonempty-type-from-decl nil rationals nil)
(rational_pred const-decl "[real -> boolean]" rationals nil)
(>= const-decl "bool" reals nil)
(real nonempty-type-from-decl nil reals nil)
(real_pred const-decl "[number -> boolean]" reals nil)
(number nonempty-type-decl nil numbers nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil))
nil nil nil nil))
(process_time_max 0
(process_time_max-1 nil 3237060222 nil
("" (auto-rewrite "process_time1" "pc") (("" (reduce) nil nil)) nil)
proved-complete
((process_time1 formula-decl nil traces nil)
(pc const-decl "pc(prog(j))" traces nil)
(trace nonempty-type-eq-decl nil traces nil)
(+ const-decl "[real, real -> real]" reals nil)
(T const-decl "bool" priority_ceiling nil)
(init_sch const-decl "good_state" priority_ceiling nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(good_state nonempty-type-eq-decl nil priority_ceiling nil)
(P const-decl "bool" priority_ceiling nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(sch_state type-eq-decl nil priority_ceiling nil)
(rsrc_state type-eq-decl nil priority_ceiling nil)
(dispatch formal-const-decl "[job -> nat]" traces nil)
(prio formal-const-decl "[job -> priority]" traces nil)
(priority nonempty-type-eq-decl nil basic_types nil)
(maxprio const-decl "posnat" basic_types nil)
(> const-decl "bool" reals nil)
(nonneg_int nonempty-type-eq-decl nil integers nil)
(< const-decl "bool" reals nil)
(prog formal-const-decl
"[job -> prog]"
traces nil)
(prog type-eq-decl
nil
programs nil)
(command type-decl nil command_adt nil)
(below type-eq-decl nil naturalnumbers nil)
(posnat nonempty-type-eq-decl nil integers nil)
(pc nonempty-type-eq-decl nil programs nil)
(job formal-type-decl nil traces nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(int nonempty-type-eq-decl nil integers nil)
(integer_pred const-decl "[rational -> boolean]" integers nil)
(rational nonempty-type-from-decl nil rationals nil)
(rational_pred const-decl "[real -> boolean]" rationals nil)
(>= const-decl "bool" reals nil)
(real nonempty-type-from-decl nil reals nil)
(real_pred const-decl "[number -> boolean]" reals nil)
(number nonempty-type-decl nil numbers nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil))
nil nil nil nil))
(process_time_before_dispatch 0
(process_time_before_dispatch-1 nil 3237060222 nil
("" (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)
proved-complete
((nat_induction formula-decl nil naturalnumbers nil)
(sch const-decl "schedule" traces nil) nil
(schedule type-eq-decl nil schedules nil)
(lift type-decl nil lift_adt nil) (<= const-decl "bool" reals nil)
(IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
(trace nonempty-type-eq-decl nil traces nil)
(+ const-decl "[real, real -> real]" reals nil)
(T const-decl "bool" priority_ceiling nil)
(init_sch const-decl "good_state" priority_ceiling nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(good_state nonempty-type-eq-decl nil priority_ceiling nil)
(P const-decl "bool" priority_ceiling nil)
(sch_state type-eq-decl nil priority_ceiling nil)
(rsrc_state type-eq-decl nil priority_ceiling nil)
(dispatch formal-const-decl "[job -> nat]" traces nil)
(prio formal-const-decl "[job -> priority]" traces nil)
(priority nonempty-type-eq-decl nil basic_types nil)
(maxprio const-decl "posnat" basic_types nil)
(> const-decl "bool" reals nil)
(nonneg_int nonempty-type-eq-decl nil integers nil)
(< const-decl "bool" reals nil)
(prog formal-const-decl
"[job -> prog]"
traces nil)
(prog type-eq-decl
nil
programs nil)
(command type-decl nil command_adt nil)
(below type-eq-decl nil naturalnumbers nil)
(posnat nonempty-type-eq-decl nil integers nil)
(pc nonempty-type-eq-decl nil programs nil)
(job formal-type-decl nil traces nil)
(pred type-eq-decl nil defined_types nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(>= const-decl "bool" reals nil)
(bool nonempty-type-eq-decl nil booleans nil)
(int nonempty-type-eq-decl nil integers nil)
(integer_pred const-decl "[rational -> boolean]" integers nil)
(rational nonempty-type-from-decl nil rationals nil)
(rational_pred const-decl "[real -> boolean]" rationals nil)
(real nonempty-type-from-decl nil reals nil)
(real_pred const-decl "[number -> boolean]" reals nil)
(boolean nonempty-type-decl nil booleans nil)
(number nonempty-type-decl nil numbers nil)
(pc_init formula-decl nil traces nil)
(process_time1 formula-decl nil traces nil)
(pc_step formula-decl nil traces nil)
(ready_after_dispatch formula-decl nil traces nil)
(active_ready formula-decl nil traces nil))
nil nil nil nil))
(process_time_at_dispatch 0
(process_time_at_dispatch-1 nil 3237060222 nil
("" (skolem!)
(("" (rewrite "process_time_before_dispatch") nil nil)) nil)
proved-complete
((trace nonempty-type-eq-decl nil traces nil)
(+ const-decl "[real, real -> real]" reals nil)
(T const-decl "bool" priority_ceiling nil)
(init_sch const-decl "good_state" priority_ceiling nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(good_state nonempty-type-eq-decl nil priority_ceiling nil)
(P const-decl "bool" priority_ceiling nil)
(sch_state type-eq-decl nil priority_ceiling nil)
(rsrc_state type-eq-decl nil priority_ceiling nil)
(prio formal-const-decl "[job -> priority]" traces nil)
(priority nonempty-type-eq-decl nil basic_types nil)
(maxprio const-decl "posnat" basic_types nil)
(> const-decl "bool" reals nil)
(nonneg_int nonempty-type-eq-decl nil integers nil)
(< const-decl "bool" reals nil)
(prog formal-const-decl
"[job -> prog]"
traces nil)
(prog type-eq-decl
nil
programs nil)
(command type-decl nil command_adt nil)
(below type-eq-decl nil naturalnumbers nil)
(posnat nonempty-type-eq-decl nil integers nil)
(pc nonempty-type-eq-decl nil programs nil)
(dispatch formal-const-decl "[job -> nat]" traces nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(>= const-decl "bool" reals nil)
(bool nonempty-type-eq-decl nil booleans nil)
(int nonempty-type-eq-decl nil integers nil)
(integer_pred const-decl "[rational -> boolean]" integers nil)
(rational nonempty-type-from-decl nil rationals nil)
(rational_pred const-decl "[real -> boolean]" rationals nil)
(real nonempty-type-from-decl nil reals nil)
(real_pred const-decl "[number -> boolean]" reals nil)
(boolean nonempty-type-decl nil booleans nil)
(number nonempty-type-decl nil numbers nil)
(job formal-type-decl nil traces nil)
(process_time_before_dispatch formula-decl nil traces nil))
nil nil nil nil))
(blockers_at_dispatch 0
(blockers_at_dispatch-1 nil 3237060222 nil
("" (skosimp)
((""
(case "FORALL n: ready(u!1, j!1, n + dispatch(j!1)) IMPLIES subset?(blo
ckers(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)
proved-complete
((pred type-eq-decl nil defined_types nil)
(nat_induction formula-decl nil naturalnumbers nil)
(member const-decl "bool" sets nil)
(readiness_step2 formula-decl nil traces nil)
(blocker_step formula-decl nil traces nil)
(ready_after_dispatch formula-decl nil traces nil)
(- const-decl "[real, real -> real]" reals nil)
(blocker const-decl "set[job]" traces nil)
(number nonempty-type-decl nil numbers nil)
(boolean nonempty-type-decl nil booleans nil)
(real_pred const-decl "[number -> boolean]" reals nil)
(real nonempty-type-from-decl nil reals nil)
(rational_pred const-decl "[real -> boolean]" rationals nil)
(rational nonempty-type-from-decl nil rationals nil)
(integer_pred const-decl "[rational -> boolean]" integers nil)
(int nonempty-type-eq-decl nil integers nil)
(bool nonempty-type-eq-decl nil booleans nil)
(>= const-decl "bool" reals nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
(job formal-type-decl nil traces nil)
(pc nonempty-type-eq-decl nil programs nil)
(posnat nonempty-type-eq-decl nil integers nil)
(below type-eq-decl nil naturalnumbers nil)
(command type-decl nil command_adt nil)
(prog type-eq-decl
nil
programs nil)
(prog formal-const-decl
"[job -> prog]"
traces nil)
(< const-decl "bool" reals nil)
(nonneg_int nonempty-type-eq-decl nil integers nil)
(> const-decl "bool" reals nil)
(maxprio const-decl "posnat" basic_types nil)
(priority nonempty-type-eq-decl nil basic_types nil)
(prio formal-const-decl "[job -> priority]" traces nil)
(dispatch formal-const-decl "[job -> nat]" traces nil)
(rsrc_state type-eq-decl nil priority_ceiling nil)
(sch_state type-eq-decl nil priority_ceiling nil)
(P const-decl "bool" priority_ceiling nil)
(good_state nonempty-type-eq-decl nil priority_ceiling nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(init_sch const-decl "good_state" priority_ceiling nil)
(T const-decl "bool" priority_ceiling nil)
(+ const-decl "[real, real -> real]" reals nil)
(trace nonempty-type-eq-decl nil traces nil)
(ready const-decl "bool" traces nil)
(set type-eq-decl nil sets nil)
(subset? const-decl "bool" sets nil) nil)
nil nil nil nil))
(active_priority 0
(active_priority-1 nil 3237060222 nil
("" (skosimp)
(("" (forward-chain "active_prio")
(("" (forward-chain "blockers_at_dispatch")
(("" (apply (then (expand "subset?") (inst?) (assert))) nil
nil))
nil))
nil))
nil)
proved-complete
((blockers_at_dispatch formula-decl nil traces nil)
(subset? const-decl "bool" sets nil)
(trace nonempty-type-eq-decl nil traces nil)
(+ const-decl "[real, real -> real]" reals nil)
(T const-decl "bool" priority_ceiling nil)
(init_sch const-decl "good_state" priority_ceiling nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(good_state nonempty-type-eq-decl nil priority_ceiling nil)
(P const-decl "bool" priority_ceiling nil)
(sch_state type-eq-decl nil priority_ceiling nil)
(rsrc_state type-eq-decl nil priority_ceiling nil)
(dispatch formal-const-decl "[job -> nat]" traces nil)
(prio formal-const-decl "[job -> priority]" traces nil)
(priority nonempty-type-eq-decl nil basic_types nil)
(maxprio const-decl "posnat" basic_types nil)
(> const-decl "bool" reals nil)
(nonneg_int nonempty-type-eq-decl nil integers nil)
(< const-decl "bool" reals nil)
(prog formal-const-decl
"[job -> prog]"
traces nil)
(prog type-eq-decl
nil
programs nil)
(command type-decl nil command_adt nil)
(below type-eq-decl nil naturalnumbers nil)
(posnat nonempty-type-eq-decl nil integers nil)
(pc nonempty-type-eq-decl nil programs nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(>= const-decl "bool" reals nil)
(bool nonempty-type-eq-decl nil booleans nil)
(int nonempty-type-eq-decl nil integers nil)
(integer_pred const-decl "[rational -> boolean]" integers nil)
(rational nonempty-type-from-decl nil rationals nil)
(rational_pred const-decl "[real -> boolean]" rationals nil)
(real nonempty-type-from-decl nil reals nil)
(real_pred const-decl "[number -> boolean]" reals nil)
(boolean nonempty-type-decl nil booleans nil)
(number nonempty-type-decl nil numbers nil)
(job formal-type-decl nil traces nil)
(active_prio formula-decl nil traces nil))
nil nil nil nil))
(blockers_in_critical_section 0
(blockers_in_critical_section-1 nil 3237060222 nil
("" (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)
proved-complete
((readiness_step2 formula-decl nil traces nil)
(active const-decl "bool" traces nil)
(active_prio formula-decl nil traces nil)
(member const-decl "bool" sets nil)
(blocker const-decl "set[job]" traces nil)
(precedes const-decl "bool" precedence nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(blocker_in_cs formula-decl nil traces nil)
(pc_step formula-decl nil traces nil)
(nat_induction formula-decl nil naturalnumbers nil)
(pred type-eq-decl nil defined_types nil)
(ready_after_dispatch formula-decl nil traces nil)
(- const-decl "[real, real -> real]" reals nil)
(number nonempty-type-decl nil numbers nil)
(boolean nonempty-type-decl nil booleans nil)
(real_pred const-decl "[number -> boolean]" reals nil)
(real nonempty-type-from-decl nil reals nil)
(rational_pred const-decl "[real -> boolean]" rationals nil)
(rational nonempty-type-from-decl nil rationals nil)
(integer_pred const-decl "[rational -> boolean]" integers nil)
(int nonempty-type-eq-decl nil integers nil)
(bool nonempty-type-eq-decl nil booleans nil)
(>= const-decl "bool" reals nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
(job formal-type-decl nil traces nil)
(pc nonempty-type-eq-decl nil programs nil)
(posnat nonempty-type-eq-decl nil integers nil)
(below type-eq-decl nil naturalnumbers nil)
(command type-decl nil command_adt nil)
(prog type-eq-decl
nil
programs nil)
(prog formal-const-decl
"[job -> prog]"
traces nil)
(< const-decl "bool" reals nil)
(nonneg_int nonempty-type-eq-decl nil integers nil)
(> const-decl "bool" reals nil)
(maxprio const-decl "posnat" basic_types nil)
(priority nonempty-type-eq-decl nil basic_types nil)
(prio formal-const-decl "[job -> priority]" traces nil)
(dispatch formal-const-decl "[job -> nat]" traces nil)
(rsrc_state type-eq-decl nil priority_ceiling nil)
(sch_state type-eq-decl nil priority_ceiling nil)
(P const-decl "bool" priority_ceiling nil)
(good_state nonempty-type-eq-decl nil priority_ceiling nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(init_sch const-decl "good_state" priority_ceiling nil)
(T const-decl "bool" priority_ceiling nil)
(+ const-decl "[real, real -> real]" reals nil)
(trace nonempty-type-eq-decl nil traces nil)
(ready const-decl "bool" traces nil)
(OR const-decl "[bool, bool -> bool]" booleans nil)
(<= const-decl "bool" reals nil)
(pc const-decl "pc(prog(j))" traces nil) nil)
nil nil nil nil))
(blockers_dispatch 0
(blockers_dispatch-1 nil 3237060222 nil
("" (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)
proved-complete
((blocker const-decl "set[job]" traces nil)
(pc const-decl "pc(prog(j))" traces nil)
(time_invariant formula-decl nil traces nil)
(initially_not_cs2 formula-decl nil programs nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(trace nonempty-type-eq-decl nil traces nil)
(+ const-decl "[real, real -> real]" reals nil)
(T const-decl "bool" priority_ceiling nil)
(init_sch const-decl "good_state" priority_ceiling nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(good_state nonempty-type-eq-decl nil priority_ceiling nil)
(P const-decl "bool" priority_ceiling nil)
(sch_state type-eq-decl nil priority_ceiling nil)
(rsrc_state type-eq-decl nil priority_ceiling nil)
(prio formal-const-decl "[job -> priority]" traces nil)
(priority nonempty-type-eq-decl nil basic_types nil)
(maxprio const-decl "posnat" basic_types nil)
(> const-decl "bool" reals nil)
(nonneg_int nonempty-type-eq-decl nil integers nil)
(< const-decl "bool" reals nil)
(prog formal-const-decl
"[job -> prog]"
traces nil)
(prog type-eq-decl
nil
programs nil)
(command type-decl nil command_adt nil)
(below type-eq-decl nil naturalnumbers nil)
(posnat nonempty-type-eq-decl nil integers nil)
(pc nonempty-type-eq-decl nil programs nil)
(dispatch formal-const-decl "[job -> nat]" traces nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(>= const-decl "bool" reals nil)
(bool nonempty-type-eq-decl nil booleans nil)
(int nonempty-type-eq-decl nil integers nil)
(integer_pred const-decl "[rational -> boolean]" integers nil)
(rational nonempty-type-from-decl nil rationals nil)
(rational_pred const-decl "[real -> boolean]" rationals nil)
(real nonempty-type-from-decl nil reals nil)
(real_pred const-decl "[number -> boolean]" reals nil)
(boolean nonempty-type-decl nil booleans nil)
(number nonempty-type-decl nil numbers nil)
(job formal-type-decl nil traces nil)
(blocker_in_cs formula-decl nil traces nil))
nil nil nil nil))
(the_blocker_TCC1 0
(the_blocker_TCC1-1 nil 3237060222 nil
("" (expand "nonempty?") (("" (propax) nil nil)) nil)
proved-complete ((nonempty? const-decl "bool" sets nil)) nil nil nil
nil))
(blocker_def 0
(blocker_def-1 nil 3237060222 nil
("" (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)
proved-complete
((job formal-type-decl nil traces nil)
(boolean nonempty-type-decl nil booleans nil) nil
(singleton const-decl "(singleton?)" sets nil)
(singleton? const-decl "bool" sets nil)
(bool nonempty-type-eq-decl nil booleans nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(set type-eq-decl nil sets nil) (empty? const-decl "bool" sets nil)
(number nonempty-type-decl nil numbers nil)
(real_pred const-decl "[number -> boolean]" reals nil)
(real nonempty-type-from-decl nil reals nil)
(rational_pred const-decl "[real -> boolean]" rationals nil)
(rational nonempty-type-from-decl nil rationals nil)
(integer_pred const-decl "[rational -> boolean]" integers nil)
(int nonempty-type-eq-decl nil integers nil)
(>= const-decl "bool" reals nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(pc nonempty-type-eq-decl nil programs nil)
(posnat nonempty-type-eq-decl nil integers nil)
(below type-eq-decl nil naturalnumbers nil)
(command type-decl nil command_adt nil)
(prog type-eq-decl
nil
programs nil)
(prog formal-const-decl
"[job -> prog]"
traces nil)
(< const-decl "bool" reals nil)
(nonneg_int nonempty-type-eq-decl nil integers nil)
(> const-decl "bool" reals nil)
(maxprio const-decl "posnat" basic_types nil)
(priority nonempty-type-eq-decl nil basic_types nil)
(prio formal-const-decl "[job -> priority]" traces nil)
(dispatch formal-const-decl "[job -> nat]" traces nil)
(rsrc_state type-eq-decl nil priority_ceiling nil)
(sch_state type-eq-decl nil priority_ceiling nil)
(P const-decl "bool" priority_ceiling nil)
(good_state nonempty-type-eq-decl nil priority_ceiling nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(init_sch const-decl "good_state" priority_ceiling nil)
(T const-decl "bool" priority_ceiling nil)
(+ const-decl "[real, real -> real]" reals nil)
(trace nonempty-type-eq-decl nil traces nil)
(blocker const-decl "set[job]" traces nil)
(nonempty? const-decl "bool" sets nil)
(single_blocker formula-decl nil traces nil)
(choose const-decl "(p)" sets nil)
(member const-decl "bool" sets nil))
nil nil nil nil))
(blocker_prio 0
(blocker_prio-1 nil 3237060222 nil
("" (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)
proved-complete
(nil (boolean nonempty-type-decl nil booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(number nonempty-type-decl nil numbers nil)
(real_pred const-decl "[number -> boolean]" reals nil)
(real nonempty-type-from-decl nil reals nil)
(rational_pred const-decl "[real -> boolean]" rationals nil)
(rational nonempty-type-from-decl nil rationals nil)
(integer_pred const-decl "[rational -> boolean]" integers nil)
(int nonempty-type-eq-decl nil integers nil)
(>= const-decl "bool" reals nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(job formal-type-decl nil traces nil)
(pc nonempty-type-eq-decl nil programs nil)
(posnat nonempty-type-eq-decl nil integers nil)
(below type-eq-decl nil naturalnumbers nil)
(command type-decl nil command_adt nil)
(prog type-eq-decl
nil
programs nil)
(prog formal-const-decl
"[job -> prog]"
traces nil)
(< const-decl "bool" reals nil)
(nonneg_int nonempty-type-eq-decl nil integers nil)
(> const-decl "bool" reals nil)
(maxprio const-decl "posnat" basic_types nil)
(priority nonempty-type-eq-decl nil basic_types nil)
(prio formal-const-decl "[job -> priority]" traces nil)
(dispatch formal-const-decl "[job -> nat]" traces nil)
(rsrc_state type-eq-decl nil priority_ceiling nil)
(sch_state type-eq-decl nil priority_ceiling nil)
(P const-decl "bool" priority_ceiling nil)
(good_state nonempty-type-eq-decl nil priority_ceiling nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(init_sch const-decl "good_state" priority_ceiling nil)
(T const-decl "bool" priority_ceiling nil)
(+ const-decl "[real, real -> real]" reals nil)
(trace nonempty-type-eq-decl nil traces nil)
(set type-eq-decl nil sets nil)
(blocker const-decl "set[job]" traces nil)
(nonempty? const-decl "bool" sets nil)
(choose const-decl "(p)" sets nil))
nil nil nil nil))
(blocker_prop 0
(blocker_prop-1 nil 3237060222 nil
("" (skosimp)
(("" (forward-chain "blocker_prio") (("" (assert) nil nil)) nil))
nil)
proved-complete
((trace nonempty-type-eq-decl nil traces nil)
(+ const-decl "[real, real -> real]" reals nil)
(T const-decl "bool" priority_ceiling nil)
(init_sch const-decl "good_state" priority_ceiling nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(good_state nonempty-type-eq-decl nil priority_ceiling nil)
(P const-decl "bool" priority_ceiling nil)
(sch_state type-eq-decl nil priority_ceiling nil)
(rsrc_state type-eq-decl nil priority_ceiling nil)
(dispatch formal-const-decl "[job -> nat]" traces nil)
(prio formal-const-decl "[job -> priority]" traces nil)
(priority nonempty-type-eq-decl nil basic_types nil)
(maxprio const-decl "posnat" basic_types nil)
(> const-decl "bool" reals nil)
(nonneg_int nonempty-type-eq-decl nil integers nil)
(< const-decl "bool" reals nil)
(prog formal-const-decl
"[job -> prog]"
traces nil)
(prog type-eq-decl
nil
programs nil)
(command type-decl nil command_adt nil)
(below type-eq-decl nil naturalnumbers nil)
(posnat nonempty-type-eq-decl nil integers nil)
(pc nonempty-type-eq-decl nil programs nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(>= const-decl "bool" reals nil)
(bool nonempty-type-eq-decl nil booleans nil)
(int nonempty-type-eq-decl nil integers nil)
(integer_pred const-decl "[rational -> boolean]" integers nil)
(rational nonempty-type-from-decl nil rationals nil)
(rational_pred const-decl "[real -> boolean]" rationals nil)
(real nonempty-type-from-decl nil reals nil)
(real_pred const-decl "[number -> boolean]" reals nil)
(boolean nonempty-type-decl nil booleans nil)
(number nonempty-type-decl nil numbers nil)
(job formal-type-decl nil traces nil)
(blocker_prio formula-decl nil traces nil))
nil nil nil nil))
(blocking_time 0
(blocking_time-1 nil 3237060222 nil
("" (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"
"dispatch(j!1)"))
(("2" (ground)
(("1" (forward-chain "max_cs2") nil nil)
("2" (expand* "member" "the_blocker") nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
proved-complete
((blocker_def formula-decl nil traces nil)
(trace nonempty-type-eq-decl nil traces nil)
(+ const-decl "[real, real -> real]" reals nil)
(T const-decl "bool" priority_ceiling nil)
(init_sch const-decl "good_state" priority_ceiling nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(good_state nonempty-type-eq-decl nil priority_ceiling nil)
(P const-decl "bool" priority_ceiling nil)
(sch_state type-eq-decl nil priority_ceiling nil)
(rsrc_state type-eq-decl nil priority_ceiling nil)
(dispatch formal-const-decl "[job -> nat]" traces nil)
(prio formal-const-decl "[job -> priority]" traces nil)
(priority nonempty-type-eq-decl nil basic_types nil)
(maxprio const-decl "posnat" basic_types nil)
(> const-decl "bool" reals nil)
(nonneg_int nonempty-type-eq-decl nil integers nil)
(< const-decl "bool" reals nil)
(prog formal-const-decl
"[job -> prog]"
traces nil)
(prog type-eq-decl
nil
programs nil)
(command type-decl nil command_adt nil)
(below type-eq-decl nil naturalnumbers nil)
(posnat nonempty-type-eq-decl nil integers nil)
(pc nonempty-type-eq-decl nil programs nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(>= const-decl "bool" reals nil)
(bool nonempty-type-eq-decl nil booleans nil)
(int nonempty-type-eq-decl nil integers nil)
(integer_pred const-decl "[rational -> boolean]" integers nil)
(rational nonempty-type-from-decl nil rationals nil)
(rational_pred const-decl "[real -> boolean]" rationals nil)
(real nonempty-type-from-decl nil reals nil)
(real_pred const-decl "[number -> boolean]" reals nil)
(boolean nonempty-type-decl nil booleans nil)
(number nonempty-type-decl nil numbers nil)
(job formal-type-decl nil traces nil)
(ready_after_dispatch formula-decl nil traces nil)
(process_time2 formula-decl nil traces nil)
(max_cs2 formula-decl nil programs nil)
(<= const-decl "bool" reals nil)
(pc const-decl "pc(prog(j))" traces nil)
(member const-decl "bool" sets nil)
(blockers_in_critical_section formula-decl nil traces nil)
(empty? const-decl "bool" sets nil)
(NOT const-decl "[bool -> bool]" booleans nil) nil
(emptyset_is_empty? formula-decl nil sets_lemmas nil)
(set type-eq-decl nil sets nil)
(blocker const-decl "set[job]" traces nil)
(sch const-decl "schedule" traces nil)
(schedule type-eq-decl nil schedules nil)
(lift type-decl nil lift_adt nil)
(process_time_emptyset formula-decl nil schedules nil))
nil nil nil nil))
(process_time_ready_job 0
(process_time_ready_job-2
"Fixed the proof: (use \"total_cpu\") needs explicit instantiation and (gr
ound) loops."
3237061730 3237061730
("" (skosimp)
(("" (forward-chain "ready_after_dispatch")
(("" (assert)
(("" (auto-rewrite "active_prop" "idle_equiv")
(("" (expand "process_time" 1 1)
(("" (replace -3 - rl)
(("" (use "total_cpu" ("t1" "t1!1" "t2" "t2!1"))
(("" (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 prece
des(k, j!1) }"))
(("1" (split)
(("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)
proved nil 1232216 834530 t shostak)
(process_time_ready_job-1 nil 3237060222 3237060491
("" (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 prece
des(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)
proved
((ready_after_dispatch formula-decl nil traces nil)
(job formal-type-decl nil traces nil)
(number nonempty-type-decl nil numbers nil)
(boolean nonempty-type-decl nil booleans nil)
(real_pred const-decl "[number -> boolean]" reals nil)
(real nonempty-type-from-decl nil reals nil)
(rational_pred const-decl "[real -> boolean]" rationals nil)
(rational nonempty-type-from-decl nil rationals nil)
(integer_pred const-decl "[rational -> boolean]" integers nil)
(int nonempty-type-eq-decl nil integers nil)
(bool nonempty-type-eq-decl nil booleans nil)
(>= const-decl "bool" reals nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(pc nonempty-type-eq-decl nil programs nil)
(posnat nonempty-type-eq-decl nil integers nil)
(below type-eq-decl nil naturalnumbers nil)
(command type-decl nil command_adt nil)
(prog type-eq-decl
nil
programs nil)
(prog formal-const-decl
"[job -> prog]"
traces nil)
(< const-decl "bool" reals nil)
(nonneg_int nonempty-type-eq-decl nil integers nil)
(> const-decl "bool" reals nil)
(maxprio const-decl "posnat" basic_types nil)
(priority nonempty-type-eq-decl nil basic_types nil)
(prio formal-const-decl "[job -> priority]" traces nil)
(dispatch formal-const-decl "[job -> nat]" traces nil)
(rsrc_state type-eq-decl nil priority_ceiling nil)
(sch_state type-eq-decl nil priority_ceiling nil)
(P const-decl "bool" priority_ceiling nil)
(good_state nonempty-type-eq-decl nil priority_ceiling nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(init_sch const-decl "good_state" priority_ceiling nil)
(T const-decl "bool" priority_ceiling nil)
(+ const-decl "[real, real -> real]" reals nil)
(trace nonempty-type-eq-decl nil traces nil)
(readiness formula-decl nil traces nil)
(idle_equiv formula-decl nil schedules nil)
(zero_idle_time formula-decl nil schedules nil)
(process_time_partition4 formula-decl nil schedules nil)
(set type-eq-decl nil sets nil) (fullset const-decl "set" sets nil)
(singleton? const-decl "bool" sets nil)
(singleton const-decl "(singleton?)" sets nil)
(H const-decl "set[job]" traces nil)
(blocker const-decl "set[job]" traces nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(precedes const-decl "bool" precedence nil)
(<= const-decl "bool" reals nil)
(OR const-decl "[bool, bool -> bool]" booleans nil)
(blk const-decl "set[job]" priority_ceiling nil)
(rsrc_set type-eq-decl nil basic_types nil)
(partition4 const-decl "bool" sum_partitions nil)
(partition2 const-decl "bool" sum_partitions nil)
(union const-decl "set" sets nil)
(disjoint? const-decl "bool" sets nil)
(empty? const-decl "bool" sets nil)
(intersection const-decl "set" sets nil)
(/= const-decl "boolean" notequal nil)
(blockers const-decl "set[job]" priority_ceiling nil)
(blockers const-decl "set[job]" traces nil)
(process_time const-decl "nat" schedules nil)
(zero_process_time formula-decl nil schedules nil)
(active_prop formula-decl nil traces nil)
(readiness_interval formula-decl nil traces nil)
(active_priority formula-decl nil traces nil)
(member const-decl "bool" sets nil)
(idle_time const-decl "nat" schedules nil)
(lift type-decl nil lift_adt nil)
(schedule type-eq-decl nil schedules nil)
(sch const-decl "schedule" traces nil)
(total_cpu formula-decl nil schedules nil)
(process_time const-decl "nat" schedules nil))
42519 20590 t nil))
(schedulable_prop 0
(schedulable_prop-1 nil 3237060222 nil
("" (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)
proved-incomplete
((pc const-decl "pc(prog(j))" traces nil)
(complete const-decl "bool" programs nil)
(finished const-decl "bool" priority_ceiling nil)
(finished const-decl "bool" traces nil)
(process_time1 formula-decl nil traces nil)
(process_time_equiv2 formula-decl nil schedules nil)
(ready_equiv formula-decl nil traces nil)
(blocking_time formula-decl nil traces nil)
(process_time_ready_job formula-decl nil traces nil)
(number nonempty-type-decl nil numbers nil)
(boolean nonempty-type-decl nil booleans nil)
(real_pred const-decl "[number -> boolean]" reals nil)
(real nonempty-type-from-decl nil reals nil)
(rational_pred const-decl "[real -> boolean]" rationals nil)
(rational nonempty-type-from-decl nil rationals nil)
(integer_pred const-decl "[rational -> boolean]" integers nil)
(int nonempty-type-eq-decl nil integers nil)
(bool nonempty-type-eq-decl nil booleans nil)
(>= const-decl "bool" reals nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(job formal-type-decl nil traces nil)
(pc nonempty-type-eq-decl nil programs nil)
(posnat nonempty-type-eq-decl nil integers nil)
(below type-eq-decl nil naturalnumbers nil)
(command type-decl nil command_adt nil)
(prog type-eq-decl
nil
programs nil)
(prog formal-const-decl
"[job -> prog]"
traces nil)
(< const-decl "bool" reals nil)
(nonneg_int nonempty-type-eq-decl nil integers nil)
(> const-decl "bool" reals nil)
(maxprio const-decl "posnat" basic_types nil)
(priority nonempty-type-eq-decl nil basic_types nil)
(prio formal-const-decl "[job -> priority]" traces nil)
(dispatch formal-const-decl "[job -> nat]" traces nil)
(rsrc_state type-eq-decl nil priority_ceiling nil)
(sch_state type-eq-decl nil priority_ceiling nil)
(P const-decl "bool" priority_ceiling nil)
(good_state nonempty-type-eq-decl nil priority_ceiling nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(init_sch const-decl "good_state" priority_ceiling nil)
(T const-decl "bool" priority_ceiling nil)
(+ const-decl "[real, real -> real]" reals nil)
(trace nonempty-type-eq-decl nil traces nil)
(ready const-decl "bool" traces nil)
(schedulable const-decl "bool" traces nil))
nil nil nil nil))
(blockers_busy 0
(blockers_busy-1 nil 3237060222 nil
("" (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)
proved-complete
((blocker_step2 formula-decl nil traces nil)
(member const-decl "bool" sets nil)
(nat_induction formula-decl nil naturalnumbers nil)
(pred type-eq-decl nil defined_types nil)
(- const-decl "[real, real -> real]" reals nil)
(number nonempty-type-decl nil numbers nil)
(boolean nonempty-type-decl nil booleans nil)
(real_pred const-decl "[number -> boolean]" reals nil)
(real nonempty-type-from-decl nil reals nil)
(rational_pred const-decl "[real -> boolean]" rationals nil)
(rational nonempty-type-from-decl nil rationals nil)
(integer_pred const-decl "[rational -> boolean]" integers nil)
(int nonempty-type-eq-decl nil integers nil)
(bool nonempty-type-eq-decl nil booleans nil)
(>= const-decl "bool" reals nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
(<= const-decl "bool" reals nil)
(+ const-decl "[real, real -> real]" reals nil)
(job formal-type-decl nil traces nil)
(set type-eq-decl nil sets nil)
(subset? const-decl "bool" sets nil)
(pc nonempty-type-eq-decl nil programs nil)
(posnat nonempty-type-eq-decl nil integers nil)
(below type-eq-decl nil naturalnumbers nil)
(command type-decl nil command_adt nil)
(prog type-eq-decl
nil
programs nil)
(prog formal-const-decl
"[job -> prog]"
traces nil)
(< const-decl "bool" reals nil)
(nonneg_int nonempty-type-eq-decl nil integers nil)
(> const-decl "bool" reals nil)
(maxprio const-decl "posnat" basic_types nil)
(priority nonempty-type-eq-decl nil basic_types nil)
(prio formal-const-decl "[job -> priority]" traces nil)
(dispatch formal-const-decl "[job -> nat]" traces nil)
(rsrc_state type-eq-decl nil priority_ceiling nil)
(sch_state type-eq-decl nil priority_ceiling nil)
(P const-decl "bool" priority_ceiling nil)
(good_state nonempty-type-eq-decl nil priority_ceiling nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(init_sch const-decl "good_state" priority_ceiling nil)
(T const-decl "bool" priority_ceiling nil)
(trace nonempty-type-eq-decl nil traces nil) nil)
nil nil nil nil))
(active_priority2 0
(active_priority2-1 nil 3237060222 nil
("" (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)
proved-complete
(nil (member const-decl "bool" sets nil)
(subset? const-decl "bool" sets nil)
(active_prio2 formula-decl nil traces nil)
(trace nonempty-type-eq-decl nil traces nil)
(+ const-decl "[real, real -> real]" reals nil)
(T const-decl "bool" priority_ceiling nil)
(init_sch const-decl "good_state" priority_ceiling nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(good_state nonempty-type-eq-decl nil priority_ceiling nil)
(P const-decl "bool" priority_ceiling nil)
(sch_state type-eq-decl nil priority_ceiling nil)
(rsrc_state type-eq-decl nil priority_ceiling nil)
(dispatch formal-const-decl "[job -> nat]" traces nil)
(prio formal-const-decl "[job -> priority]" traces nil)
(prog formal-const-decl
"[job -> prog]"
traces nil)
(prog type-eq-decl
nil
programs nil)
(command type-decl nil command_adt nil)
(below type-eq-decl nil naturalnumbers nil)
(pc nonempty-type-eq-decl nil programs nil)
(job formal-type-decl nil traces nil)
(priority nonempty-type-eq-decl nil basic_types nil)
(maxprio const-decl "posnat" basic_types nil)
(posnat nonempty-type-eq-decl nil integers nil)
(> const-decl "bool" reals nil)
(nonneg_int nonempty-type-eq-decl nil integers nil)
(< const-decl "bool" reals nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(>= const-decl "bool" reals nil)
(bool nonempty-type-eq-decl nil booleans nil)
(int nonempty-type-eq-decl nil integers nil)
(integer_pred const-decl "[rational -> boolean]" integers nil)
(rational nonempty-type-from-decl nil rationals nil)
(rational_pred const-decl "[real -> boolean]" rationals nil)
(real nonempty-type-from-decl nil reals nil)
(real_pred const-decl "[number -> boolean]" reals nil)
(boolean nonempty-type-decl nil booleans nil)
(number nonempty-type-decl nil numbers nil)
(blockers_busy formula-decl nil traces nil))
nil nil nil nil))
(blocker_in_critical_section2 0
(blocker_in_critical_section2-1 nil 3237060222 nil
("" (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)
proved-complete
((pc const-decl "pc(prog(j))" traces nil)
(trace nonempty-type-eq-decl nil traces nil)
(T const-decl "bool" priority_ceiling nil)
(init_sch const-decl "good_state" priority_ceiling nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(good_state nonempty-type-eq-decl nil priority_ceiling nil)
(P const-decl "bool" priority_ceiling nil)
(sch_state type-eq-decl nil priority_ceiling nil)
(rsrc_state type-eq-decl nil priority_ceiling nil)
(dispatch formal-const-decl "[job -> nat]" traces nil)
(prio formal-const-decl "[job -> priority]" traces nil)
(priority nonempty-type-eq-decl nil basic_types nil)
(maxprio const-decl "posnat" basic_types nil)
(> const-decl "bool" reals nil)
(nonneg_int nonempty-type-eq-decl nil integers nil)
(< const-decl "bool" reals nil)
(prog formal-const-decl
"[job -> prog]"
traces nil)
(prog type-eq-decl
nil
programs nil)
(command type-decl nil command_adt nil)
(below type-eq-decl nil naturalnumbers nil)
(posnat nonempty-type-eq-decl nil integers nil)
(pc nonempty-type-eq-decl nil programs nil)
(job formal-type-decl nil traces nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(OR const-decl "[bool, bool -> bool]" booleans nil)
(+ const-decl "[real, real -> real]" reals nil)
(<= const-decl "bool" reals nil)
(IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(>= const-decl "bool" reals nil)
(bool nonempty-type-eq-decl nil booleans nil)
(int nonempty-type-eq-decl nil integers nil)
(integer_pred const-decl "[rational -> boolean]" integers nil)
(rational nonempty-type-from-decl nil rationals nil)
(rational_pred const-decl "[real -> boolean]" rationals nil)
(real nonempty-type-from-decl nil reals nil)
(real_pred const-decl "[number -> boolean]" reals nil)
(boolean nonempty-type-decl nil booleans nil)
(number nonempty-type-decl nil numbers nil)
(- const-decl "[real, real -> real]" reals nil)
(pred type-eq-decl nil defined_types nil)
(nat_induction formula-decl nil naturalnumbers nil)
(active const-decl "bool" traces nil)
(active_prio2 formula-decl nil traces nil)
(member const-decl "bool" sets nil)
(blocker_in_cs2 formula-decl nil traces nil) nil
(pc_step formula-decl nil traces nil))
nil nil nil nil))
(blocker_dispatch2 0
(blocker_dispatch2-1 nil 3237060222 nil
("" (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)
proved-complete
(nil (NOT const-decl "[bool -> bool]" booleans nil)
(initially_not_cs2 formula-decl nil programs nil)
(time_invariant formula-decl nil traces nil)
(prog formal-const-decl
"[job -> prog]"
traces nil)
(prog type-eq-decl
nil
programs nil)
(command type-decl nil command_adt nil)
(below type-eq-decl nil naturalnumbers nil)
(dispatch formal-const-decl "[job -> nat]" traces nil)
(prio formal-const-decl "[job -> priority]" traces nil)
(priority nonempty-type-eq-decl nil basic_types nil)
(maxprio const-decl "posnat" basic_types nil)
(posnat nonempty-type-eq-decl nil integers nil)
(> const-decl "bool" reals nil)
(nonneg_int nonempty-type-eq-decl nil integers nil)
(< const-decl "bool" reals nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(>= const-decl "bool" reals nil)
(bool nonempty-type-eq-decl nil booleans nil)
(int nonempty-type-eq-decl nil integers nil)
(integer_pred const-decl "[rational -> boolean]" integers nil)
(rational nonempty-type-from-decl nil rationals nil)
(rational_pred const-decl "[real -> boolean]" rationals nil)
(real nonempty-type-from-decl nil reals nil)
(real_pred const-decl "[number -> boolean]" reals nil)
(boolean nonempty-type-decl nil booleans nil)
(number nonempty-type-decl nil numbers nil)
(job formal-type-decl nil traces nil)
(trace nonempty-type-eq-decl nil traces nil)
(+ const-decl "[real, real -> real]" reals nil)
(T const-decl "bool" priority_ceiling nil)
(init_sch const-decl "good_state" priority_ceiling nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(good_state nonempty-type-eq-decl nil priority_ceiling nil)
(P const-decl "bool" priority_ceiling nil)
(sch_state type-eq-decl nil priority_ceiling nil)
(rsrc_state type-eq-decl nil priority_ceiling nil)
(pc nonempty-type-eq-decl nil programs nil)
(blockers_in_cs2 formula-decl nil priority_ceiling nil))
nil nil nil nil))
(the_blocker_TCC2 0
(the_blocker_TCC2-1 nil 3237060222 nil ("" (subtype-tcc) nil nil)
proved-complete
((nonempty? const-decl "bool" sets nil)
(empty? const-decl "bool" sets nil)
(job formal-type-decl nil traces nil)
(number nonempty-type-decl nil numbers nil)
(boolean nonempty-type-decl nil booleans nil)
(real_pred const-decl "[number -> boolean]" reals nil)
(real nonempty-type-from-decl nil reals nil)
(rational_pred const-decl "[real -> boolean]" rationals nil)
(rational nonempty-type-from-decl nil rationals nil)
(integer_pred const-decl "[rational -> boolean]" integers nil)
(int nonempty-type-eq-decl nil integers nil)
(bool nonempty-type-eq-decl nil booleans nil)
(>= const-decl "bool" reals nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(< const-decl "bool" reals nil)
(nonneg_int nonempty-type-eq-decl nil integers nil)
(> const-decl "bool" reals nil)
(posnat nonempty-type-eq-decl nil integers nil)
(maxprio const-decl "posnat" basic_types nil)
(priority nonempty-type-eq-decl nil basic_types nil)
(prio formal-const-decl "[job -> priority]" traces nil)
(dispatch formal-const-decl "[job -> nat]" traces nil)
(below type-eq-decl nil naturalnumbers nil)
(command type-decl nil command_adt nil)
(prog type-eq-decl
nil
programs nil)
(prog formal-const-decl
"[job -> prog]"
traces nil)
(member const-decl "bool" sets nil) nil
(step const-decl "sch_state" priority_ceiling nil)
(cmd const-decl "command" programs nil)
(idle_step const-decl "sch_state" priority_ceiling nil)
(idle const-decl "bool" priority_ceiling nil)
(eligible const-decl "bool" priority_ceiling nil)
(blocked const-decl "bool" priority_ceiling nil)
(blk const-decl "set[job]" priority_ceiling nil)
(/= const-decl "boolean" notequal nil)
(topjob const-decl "bool" priority_ceiling nil)
(precedes const-decl "bool" precedence nil)
(ready const-decl "bool" priority_ceiling nil)
(finished const-decl "bool" priority_ceiling nil)
(complete const-decl "bool" programs nil)
(init_rsrc const-decl "rsrc_state" priority_ceiling nil)
(set type-eq-decl nil sets nil)
(trace nonempty-type-eq-decl nil traces nil)
(+ const-decl "[real, real -> real]" reals nil)
(T const-decl "bool" priority_ceiling nil)
(init_sch const-decl "good_state" priority_ceiling nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(good_state nonempty-type-eq-decl nil priority_ceiling nil)
(P const-decl "bool" priority_ceiling nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(sch_state type-eq-decl nil priority_ceiling nil)
(rsrc_state type-eq-decl nil priority_ceiling nil)
(pc nonempty-type-eq-decl nil programs nil)
(NOT const-decl "[bool -> bool]" booleans nil))
nil nil nil nil))
(blocker_def2 0
(blocker_def2-1 nil 3237060222 nil
("" (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)
proved-complete
((member const-decl "bool" sets nil)
(single_blocker2 formula-decl nil traces nil)
(number nonempty-type-decl nil numbers nil)
(real_pred const-decl "[number -> boolean]" reals nil)
(real nonempty-type-from-decl nil reals nil)
(rational_pred const-decl "[real -> boolean]" rationals nil)
(rational nonempty-type-from-decl nil rationals nil)
(integer_pred const-decl "[rational -> boolean]" integers nil)
(int nonempty-type-eq-decl nil integers nil)
(bool nonempty-type-eq-decl nil booleans nil)
(>= const-decl "bool" reals nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(pc nonempty-type-eq-decl nil programs nil)
(posnat nonempty-type-eq-decl nil integers nil)
(below type-eq-decl nil naturalnumbers nil)
(command type-decl nil command_adt nil)
(prog type-eq-decl
nil
programs nil)
(prog formal-const-decl
"[job -> prog]"
traces nil)
(< const-decl "bool" reals nil)
(nonneg_int nonempty-type-eq-decl nil integers nil)
(> const-decl "bool" reals nil)
(maxprio const-decl "posnat" basic_types nil)
(priority nonempty-type-eq-decl nil basic_types nil)
(prio formal-const-decl "[job -> priority]" traces nil)
(dispatch formal-const-decl "[job -> nat]" traces nil)
(rsrc_state type-eq-decl nil priority_ceiling nil)
(sch_state type-eq-decl nil priority_ceiling nil)
(P const-decl "bool" priority_ceiling nil)
(good_state nonempty-type-eq-decl nil priority_ceiling nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(init_sch const-decl "good_state" priority_ceiling nil)
(T const-decl "bool" priority_ceiling nil)
(+ const-decl "[real, real -> real]" reals nil)
(trace nonempty-type-eq-decl nil traces nil)
(set type-eq-decl nil sets nil)
(singleton? const-decl "bool" sets nil)
(singleton const-decl "(singleton?)" sets nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(empty? const-decl "bool" sets nil) nil
(boolean nonempty-type-decl nil booleans nil)
(job formal-type-decl nil traces nil))
nil nil nil nil))
(blocker_prio2 0
(blocker_prio2-1 nil 3237060222 nil
("" (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)
proved-complete
((boolean nonempty-type-decl nil booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(number nonempty-type-decl nil numbers nil)
(real_pred const-decl "[number -> boolean]" reals nil)
(real nonempty-type-from-decl nil reals nil)
(rational_pred const-decl "[real -> boolean]" rationals nil)
(rational nonempty-type-from-decl nil rationals nil)
(integer_pred const-decl "[rational -> boolean]" integers nil)
(int nonempty-type-eq-decl nil integers nil)
(>= const-decl "bool" reals nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(job formal-type-decl nil traces nil)
(pc nonempty-type-eq-decl nil programs nil)
(posnat nonempty-type-eq-decl nil integers nil)
(below type-eq-decl nil naturalnumbers nil)
(command type-decl nil command_adt nil)
(prog type-eq-decl
nil
programs nil)
(prog formal-const-decl
"[job -> prog]"
traces nil)
(< const-decl "bool" reals nil)
(nonneg_int nonempty-type-eq-decl nil integers nil)
(> const-decl "bool" reals nil)
(maxprio const-decl "posnat" basic_types nil)
(priority nonempty-type-eq-decl nil basic_types nil)
(prio formal-const-decl "[job -> priority]" traces nil)
(dispatch formal-const-decl "[job -> nat]" traces nil)
(rsrc_state type-eq-decl nil priority_ceiling nil)
(sch_state type-eq-decl nil priority_ceiling nil)
(P const-decl "bool" priority_ceiling nil)
(good_state nonempty-type-eq-decl nil priority_ceiling nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(init_sch const-decl "good_state" priority_ceiling nil)
(T const-decl "bool" priority_ceiling nil)
(+ const-decl "[real, real -> real]" reals nil)
(trace nonempty-type-eq-decl nil traces nil)
(set type-eq-decl nil sets nil) nil
(nonempty? const-decl "bool" sets nil)
(choose const-decl "(p)" sets nil))
nil nil nil nil))
(blocking_time2 0
(blocking_time2-1 nil 3237060222 nil
("" (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)
proved-complete
((sch const-decl "schedule" traces nil)
(schedule type-eq-decl nil schedules nil)
(lift type-decl nil lift_adt nil)
(process_time_emptyset formula-decl nil schedules nil)
(job formal-type-decl nil traces nil)
(trace nonempty-type-eq-decl nil traces nil)
(+ const-decl "[real, real -> real]" reals nil)
(T const-decl "bool" priority_ceiling nil)
(init_sch const-decl "good_state" priority_ceiling nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(good_state nonempty-type-eq-decl nil priority_ceiling nil)
(P const-decl "bool" priority_ceiling nil)
(sch_state type-eq-decl nil priority_ceiling nil)
(rsrc_state type-eq-decl nil priority_ceiling nil)
(dispatch formal-const-decl "[job -> nat]" traces nil)
(prio formal-const-decl "[job -> priority]" traces nil)
(priority nonempty-type-eq-decl nil basic_types nil)
(maxprio const-decl "posnat" basic_types nil)
(> const-decl "bool" reals nil)
(nonneg_int nonempty-type-eq-decl nil integers nil)
(< const-decl "bool" reals nil)
(prog formal-const-decl
"[job -> prog]"
traces nil)
(prog type-eq-decl
nil
programs nil)
(command type-decl nil command_adt nil)
(below type-eq-decl nil naturalnumbers nil)
(posnat nonempty-type-eq-decl nil integers nil)
(pc nonempty-type-eq-decl nil programs nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(>= const-decl "bool" reals nil)
(int nonempty-type-eq-decl nil integers nil)
(integer_pred const-decl "[rational -> boolean]" integers nil)
(rational nonempty-type-from-decl nil rationals nil)
(rational_pred const-decl "[real -> boolean]" rationals nil)
(real nonempty-type-from-decl nil reals nil)
(real_pred const-decl "[number -> boolean]" reals nil)
(number nonempty-type-decl nil numbers nil)
(set type-eq-decl nil sets nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil)
(emptyset_is_empty? formula-decl nil sets_lemmas nil)
(sum def-decl "nat" sum_sequences nil)
(blocker_def2 formula-decl nil traces nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(empty? const-decl "bool" sets nil)
(blocker_in_critical_section2 formula-decl nil traces nil)
(member const-decl "bool" sets nil)
(pc const-decl "pc(prog(j))" traces nil)
(max_cs2 formula-decl nil programs nil)
(process_time2 formula-decl nil traces nil)
(<= const-decl "bool" reals nil) nil)
nil nil nil nil))
(process_time_busy_interval 0
(process_time_busy_interval-1 nil 3237060222 nil
("" (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)
proved-complete
((active_priority2 formula-decl nil traces nil)
(active_prop formula-decl nil traces nil)
(zero_process_time formula-decl nil schedules nil)
(partition3 const-decl "bool" sum_partitions nil)
(partition2 const-decl "bool" sum_partitions nil)
(union const-decl "set" sets nil)
(disjoint? const-decl "bool" sets nil)
(empty? const-decl "bool" sets nil)
(intersection const-decl "set" sets nil)
(ceil const-decl "[semaphore -> priority]" basic_types nil)
(semaphore nonempty-type-decl nil basic_types nil)
(rsrc_set type-eq-decl nil basic_types nil)
(member const-decl "bool" sets nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(K const-decl "set[job]" traces nil)
(fullset const-decl "set" sets nil) (set type-eq-decl nil sets nil)
(process_time_partition3 formula-decl nil schedules nil)
(zero_idle_time formula-decl nil schedules nil)
(idle_equiv formula-decl nil schedules nil)
(readiness formula-decl nil traces nil) nil
(lift type-decl nil lift_adt nil)
(schedule type-eq-decl nil schedules nil)
(pc nonempty-type-eq-decl nil programs nil)
(posnat nonempty-type-eq-decl nil integers nil)
(below type-eq-decl nil naturalnumbers nil)
(command type-decl nil command_adt nil)
(prog type-eq-decl
nil
programs nil)
(prog formal-const-decl
"[job -> prog]"
traces nil)
(< const-decl "bool" reals nil)
(nonneg_int nonempty-type-eq-decl nil integers nil)
(> const-decl "bool" reals nil)
(maxprio const-decl "posnat" basic_types nil)
(priority nonempty-type-eq-decl nil basic_types nil)
(prio formal-const-decl "[job -> priority]" traces nil)
(dispatch formal-const-decl "[job -> nat]" traces nil)
(rsrc_state type-eq-decl nil priority_ceiling nil)
(sch_state type-eq-decl nil priority_ceiling nil)
(P const-decl "bool" priority_ceiling nil)
(good_state nonempty-type-eq-decl nil priority_ceiling nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(init_sch const-decl "good_state" priority_ceiling nil)
(T const-decl "bool" priority_ceiling nil)
(+ const-decl "[real, real -> real]" reals nil)
(trace nonempty-type-eq-decl nil traces nil)
(sch const-decl "schedule" traces nil)
(number nonempty-type-decl nil numbers nil)
(boolean nonempty-type-decl nil booleans nil)
(real_pred const-decl "[number -> boolean]" reals nil)
(real nonempty-type-from-decl nil reals nil)
(rational_pred const-decl "[real -> boolean]" rationals nil)
(rational nonempty-type-from-decl nil rationals nil)
(integer_pred const-decl "[rational -> boolean]" integers nil)
(int nonempty-type-eq-decl nil integers nil)
(bool nonempty-type-eq-decl nil booleans nil)
(>= const-decl "bool" reals nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(job formal-type-decl nil traces nil)
(total_cpu formula-decl nil schedules nil))
nil nil nil nil))
(busy_time2 0
(busy_time2-1 nil 3237060222 nil
("" (skosimp)
(("" (forward-chain "process_time_busy_interval")
(("" (forward-chain "blocking_time2") (("" (assert) nil nil))
nil))
nil))
nil)
proved-complete
((blocking_time2 formula-decl nil traces nil)
(trace nonempty-type-eq-decl nil traces nil)
(+ const-decl "[real, real -> real]" reals nil)
(T const-decl "bool" priority_ceiling nil)
(init_sch const-decl "good_state" priority_ceiling nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(good_state nonempty-type-eq-decl nil priority_ceiling nil)
(P const-decl "bool" priority_ceiling nil)
(sch_state type-eq-decl nil priority_ceiling nil)
(rsrc_state type-eq-decl nil priority_ceiling nil)
(dispatch formal-const-decl "[job -> nat]" traces nil)
(prio formal-const-decl "[job -> priority]" traces nil)
(prog formal-const-decl
"[job -> prog]"
traces nil)
(prog type-eq-decl
nil
programs nil)
(command type-decl nil command_adt nil)
(below type-eq-decl nil naturalnumbers nil)
(pc nonempty-type-eq-decl nil programs nil)
(job formal-type-decl nil traces nil)
(priority nonempty-type-eq-decl nil basic_types nil)
(maxprio const-decl "posnat" basic_types nil)
(posnat nonempty-type-eq-decl nil integers nil)
(> const-decl "bool" reals nil)
(nonneg_int nonempty-type-eq-decl nil integers nil)
(< const-decl "bool" reals nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(>= const-decl "bool" reals nil)
(bool nonempty-type-eq-decl nil booleans nil)
(int nonempty-type-eq-decl nil integers nil)
(integer_pred const-decl "[rational -> boolean]" integers nil)
(rational nonempty-type-from-decl nil rationals nil)
(rational_pred const-decl "[real -> boolean]" rationals nil)
(real nonempty-type-from-decl nil reals nil)
(real_pred const-decl "[number -> boolean]" reals nil)
(boolean nonempty-type-decl nil booleans nil)
(number nonempty-type-decl nil numbers nil)
(process_time_busy_interval formula-decl nil traces nil))
nil nil nil nil))
(blockers_prop 0
(blockers_prop-1 nil 3237060222 nil
("" (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)
proved-complete
((semaphore nonempty-type-decl nil basic_types nil)
(blk const-decl "set[job]" priority_ceiling nil)
(/= const-decl "boolean" notequal nil)
(blockers_busy formula-decl nil traces nil)
(member const-decl "bool" sets nil)
(job formal-type-decl nil traces nil)
(boolean nonempty-type-decl nil booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(set type-eq-decl nil sets nil)
(subset? const-decl "bool" sets nil)
(number nonempty-type-decl nil numbers nil)
(real_pred const-decl "[number -> boolean]" reals nil)
(real nonempty-type-from-decl nil reals nil)
(rational_pred const-decl "[real -> boolean]" rationals nil)
(rational nonempty-type-from-decl nil rationals nil)
(integer_pred const-decl "[rational -> boolean]" integers nil)
(int nonempty-type-eq-decl nil integers nil)
(>= const-decl "bool" reals nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(pc nonempty-type-eq-decl nil programs nil)
(posnat nonempty-type-eq-decl nil integers nil)
(below type-eq-decl nil naturalnumbers nil)
(command type-decl nil command_adt nil)
(prog type-eq-decl
nil
programs nil)
(prog formal-const-decl
"[job -> prog]"
traces nil)
(< const-decl "bool" reals nil)
(nonneg_int nonempty-type-eq-decl nil integers nil)
(> const-decl "bool" reals nil)
(maxprio const-decl "posnat" basic_types nil)
(priority nonempty-type-eq-decl nil basic_types nil)
(prio formal-const-decl "[job -> priority]" traces nil)
(dispatch formal-const-decl "[job -> nat]" traces nil)
(rsrc_state type-eq-decl nil priority_ceiling nil)
(sch_state type-eq-decl nil priority_ceiling nil)
(P const-decl "bool" priority_ceiling nil)
(good_state nonempty-type-eq-decl nil priority_ceiling nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(init_sch const-decl "good_state" priority_ceiling nil)
(T const-decl "bool" priority_ceiling nil)
(+ const-decl "[real, real -> real]" reals nil)
(trace nonempty-type-eq-decl nil traces nil)
(blocker const-decl "set[job]" traces nil) nil)
nil nil nil nil))
(blocking_prop 0
(blocking_prop-1 nil 3237060222 nil
("" (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) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
proved-complete
(nil (blocker_def formula-decl nil traces nil)
(blocker_def2 formula-decl nil traces nil)
(singleton const-decl "(singleton?)" sets nil)
(empty? const-decl "bool" sets nil)
(subset? const-decl "bool" sets nil)
(member const-decl "bool" sets nil)
(trace nonempty-type-eq-decl nil traces nil)
(+ const-decl "[real, real -> real]" reals nil)
(T const-decl "bool" priority_ceiling nil)
(init_sch const-decl "good_state" priority_ceiling nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(good_state nonempty-type-eq-decl nil priority_ceiling nil)
(P const-decl "bool" priority_ceiling nil)
(sch_state type-eq-decl nil priority_ceiling nil)
(rsrc_state type-eq-decl nil priority_ceiling nil)
(dispatch formal-const-decl "[job -> nat]" traces nil)
(prio formal-const-decl "[job -> priority]" traces nil)
(prog formal-const-decl
"[job -> prog]"
traces nil)
(prog type-eq-decl
nil
programs nil)
(command type-decl nil command_adt nil)
(below type-eq-decl nil naturalnumbers nil)
(pc nonempty-type-eq-decl nil programs nil)
(priority nonempty-type-eq-decl nil basic_types nil)
(maxprio const-decl "posnat" basic_types nil)
(posnat nonempty-type-eq-decl nil integers nil)
(> const-decl "bool" reals nil)
(nonneg_int nonempty-type-eq-decl nil integers nil)
(< const-decl "bool" reals nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(>= const-decl "bool" reals nil)
(bool nonempty-type-eq-decl nil booleans nil)
(int nonempty-type-eq-decl nil integers nil)
(integer_pred const-decl "[rational -> boolean]" integers nil)
(rational nonempty-type-from-decl nil rationals nil)
(rational_pred const-decl "[real -> boolean]" rationals nil)
(real nonempty-type-from-decl nil reals nil)
(real_pred const-decl "[number -> boolean]" reals nil)
(boolean nonempty-type-decl nil booleans nil)
(number nonempty-type-decl nil numbers nil)
(job formal-type-decl nil traces nil)
(blockers_prop formula-decl nil traces 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) EN
DIF
%-----------------------
% 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, t
2, 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| "" (SUBTYP
E-TCC) NIL NIL)
(|sum_TCC3| "" (TERMINATION-TCC) NIL NIL) (|sum_TCC4| "" (SUBTYPE-TCC) NIL N
IL)
(|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" ("su
m_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 <
n IMPLIES not E!1(u!1(t1!1 + t)))")
(("1" (INST - "t2!1 - t1!1")
(("1" (REDUCE :IF-MATCH NIL)
(("1" (INST - "t!1 - t1!1") (("1" (ASSERT) NIL NIL)) NIL)
("2" (INST?) (("2" (ASSERT) NIL NIL)) NIL))
NIL))
NIL)
("2" (DELETE 2 3)
(("2"
(INDUCT-AND-SIMPLIFY "n" :IF-MATCH BEST :DEFS NIL :REWRITES
("sum_init" ("sum_step")))
NIL NIL))
NIL))
NIL))
NIL))
NIL))
NIL)
(|sum_full| "" (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) = n IFF (FORALL t: t <
n IMPLIES E!1(u!1(t1!1 + t)))")
(("1" (INST - "t2!1 - t1!1")
(("1" (REDUCE :IF-MATCH NIL)
(("1" (INST - "t!1 - t1!1") (("1" (ASSERT) NIL NIL)) NIL)
("2" (INST?) (("2" (ASSERT) NIL NIL)) NIL))
NIL))
NIL)
("2" (DELETE 2 3)
(("2" (AUTO-REWRITE "sum_init" "sum_step")
(("2" (INDUCT "n")
(("1" (REDUCE) NIL NIL) ("2" (REDUCE) NIL NIL)
("3" (SKOSIMP)
(("3" (CASE "E!1(u!1(t1!1 + j!1))")
(("1" (ASSERT)
(("1" (GROUND)
(("1" (SKOSIMP) (("1" (INST?) (("1" (ASSERT) NIL NIL))
NIL)) NIL)
("2" (SKOSIMP) (("2" (INST?) (("2" (ASSERT) NIL NIL))
NIL)) NIL))
NIL))
NIL)
("2" (DELETE -)
(("2" (ASSERT)
(("2" (USE "max_sum")
(("2" (ASSERT) (("2" (INST?) (("2" (ASSERT) NIL NIL))
NIL)) NIL)) NIL))
NIL))
NIL))
NIL))
NIL))
NIL))
NIL))
NIL))
NIL))
NIL))
NIL))
NIL)
(|sum_split| "" (SKOSIMP)
((""
(CASE "FORALL n: sum(u!1, t1!1, t!1, E!1) + sum(u!1, t!1, t!1 + n, E!1) =
sum(u!1, t1!1, t!1 + n, E!1)")
(("1" (INST - "t2!1 - t!1") (("1" (ASSERT) NIL NIL) ("2" (ASSERT) NIL NIL
)) NIL)
("2" (DELETE 2)
(("2" (INDUCT-AND-REWRITE "n" 1 "sum_init")
(("2" (USE "sum_step" ("t" "t!1" "n" "j!1"))
(("2" (USE "sum_step" ("t" "t1!1" "n" "j!1 + t!1 - t1!1")) (("2" (S
MASH) NIL NIL))
NIL))
NIL))
NIL))
NIL))
NIL))
NIL)
(|sum_increasing| "" (SKOSIMP)
(("" (USE "sum_split" ("t2" "t3!1")) (("" (GROUND) NIL NIL)) NIL)) NIL)
(|equal_sums| "" (SKOSIMP)
(("" (CASE "t2!1 <= t1!1")
(("1" (ASSERT) (("1" (EXPAND "sum") (("1" (PROPAX) NIL NIL)) NIL)) NIL)
("2" (ASSERT)
(("2"
(CASE "FORALL n: t1!1 + n <= t2!1 IMPLIES sum(u1!1, t1!1, t1!1 + n, E
!1) = sum(u2!1, t1!1, t1!1 + n, E!1)")
(("1" (INST - "t2!1 - t1!1") (("1" (ASSERT) NIL NIL)) NIL)
("2" (DELETE 2 3)
(("2" (AUTO-REWRITE "sum_init")
(("2" (INDUCT "n")
(("1" (ASSERT) NIL NIL)
("2" (SKOSIMP)
(("2" (ASSERT)
(("2" (USE "sum_step")
(("2" (USE "sum_step" ("u" "u2!1"))
(("2" (INST?) (("2" (SMASH) NIL NIL)) NIL)) NIL))
NIL))
NIL))
NIL))
NIL))
NIL))
NIL))
NIL))
NIL))
NIL))
NIL)
(|sum_emptyset| "" (SKOLEM!) (("" (REWRITE "sum_zero") (("" (GRIND) NIL NIL)
) NIL)) NIL)
(|sum_fullset| "" (SKOSIMP) (("" (REWRITE "sum_full") (("" (GRIND) NIL NIL))
NIL)) NIL)
(|sum_disj_union| "" (SKOSIMP)
((""
(CASE "FORALL n: sum(u!1, t1!1, t1!1+n, union(E1!1, E2!1)) = sum(u!1, t1!
1, t1!1+n, E1!1) + sum(u!1, t1!1, t1!1+n, E2!1)")
(("1" (INST - "t2!1 - t1!1")
(("1" (ASSERT) NIL NIL)
("2" (ASSERT) (("2" (EXPAND "sum") (("2" (PROPAX) NIL NIL)) NIL)) NIL)
)
NIL)
("2" (DELETE 2)
(("2"
(INDUCT-AND-SIMPLIFY "n" :DEFS NIL :REWRITES ("sum_init" ("sum_step")
) :THEORIES
("sets[T]"))
NIL NIL))
NIL))
NIL))
NIL)
(|sum_diff_subset| "" (SKOSIMP)
((""
(CASE "FORALL n: sum(u!1, t1!1, t1!1+n, difference(E2!1, E1!1)) = sum(u!1
, t1!1, t1!1+n, E2!1) - sum(u!1, t1!1, t1!1+n, E1!1)")
(("1" (INST - "t2!1 - t1!1")
(("1" (ASSERT) NIL NIL)
("2" (ASSERT) (("2" (EXPAND "sum") (("2" (PROPAX) NIL NIL)) NIL)) NIL)
)
NIL)
("2" (DELETE 2)
(("2"
(INDUCT-AND-SIMPLIFY "n" :DEFS NIL :REWRITES ("sum_init" ("sum_step")
) :THEORIES
("sets[T]"))
NIL NIL))
NIL))
NIL))
NIL)
(|sum_union_inter| "" (SKOLEM!)
(("" (CASE "t2!1 <= t1!1")
(("1" (AUTO-REWRITE "sum") (("1" (ASSERT) NIL NIL)) NIL)
("2" (ASSERT)
(("2"
(CASE "FORALL n: sum(u!1, t1!1, t1!1+n, intersection(E1!1, E2!1)) + s
um(u!1, t1!1, t1!1+n, union(E1!1, E2!1)) =
sum(u!1, t1!1, t1!1+n, E1!1) + sum(u!1, t1!1, t1!1+n, E2!1)")
(("1" (INST - "t2!1 - t1!1") (("1" (ASSERT) NIL NIL)) NIL)
("2" (DELETE 2 3)
(("2"
(INDUCT-AND-SIMPLIFY "n" :DEFS NIL :REWRITES ("sum_init" ("sum_st
ep")) :THEORIES
("sets[T]"))
NIL NIL))
NIL))
NIL))
NIL))
NIL))
NIL)
(|sum_complement| "" (SKOSIMP)
(("" (AUTO-REWRITE "sum_fullset")
(("" (ASSERT)
(("" (USE "sum_disj_union" ("E1" "E!1" "E2" "complement(E!1)"))
(("" (GROUND)
(("1" (CASE-REPLACE "union(E!1, complement(E!1)) = fullset")
(("1" (ASSERT) NIL NIL)
("2" (DELETE -1 -2 2)
(("2" (APPLY-EXTENSIONALITY :HIDE? T) (("2" (GRIND) NIL NIL)) N
IL)) NIL))
NIL)
("2" (DELETE -1 2) (("2" (GRIND) NIL NIL)) NIL))
NIL))
NIL))
NIL))
NIL))
NIL)
(|sum_subset| "" (SKOSIMP)
(("" (CASE "t2!1 <= t1!1")
(("1" (AUTO-REWRITE "sum") (("1" (ASSERT) NIL NIL)) NIL)
("2" (ASSERT)
(("2" (USE "sum_diff_subset" ("E2" "E2!1")) (("2" (ASSERT) (("2" (ASSER
T) NIL NIL)) NIL))
NIL))
NIL))
NIL))
NIL)
(|sum_union1| "" (SKOLEM!)
(("" (REWRITE "sum_subset") (("" (DELETE 2) (("" (GRIND) NIL NIL)) NIL)) NI
L)) NIL)
(|sum_union2| "" (SKOLEM!)
(("" (REWRITE "sum_subset") (("" (DELETE 2) (("" (GRIND) NIL NIL)) NIL)) NI
L)) NIL)
(|sum_inter1| "" (SKOLEM!)
(("" (REWRITE "sum_subset") (("" (DELETE 2) (("" (GRIND) NIL NIL)) NIL)) NI
L)) NIL)
(|sum_inter2| "" (SKOLEM!)
(("" (REWRITE "sum_subset") (("" (DELETE 2) (("" (GRIND) NIL NIL)) NIL)) NI
L)) NIL))
$$$schedules.pvs
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Schedules: mapping from nat to idle or some job j %
% %
% Modified 6/13/2000: changed some_or_none[job] %
% to lift[job] (defined in the prelude) %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
schedules [ job: TYPE] : THEORY
BEGIN
IMPORTING sum_sequences, sum_partitions
schedule: TYPE = [nat -> 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(dow
n(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(s
ch, 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(s
ch, 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 bot
tom 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)) <= dis
patch(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) N
IL 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" (ASS
ERT) 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)): preced
es(j, k)")
(("1" (SKOLEM!)
(("1" (USE "epsilon_ax[(A!1)]")
(("1" (GROUND) (("1" (REWRITE "topjob_exists") NIL NIL)) NIL) ("2" (DEL
ETE 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 N
IL)) 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)) IMP
LIES 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 that can block 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)) IMP
LIES 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))
$$$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 0
(sup_unique-1 nil 3237042679 nil
("" (expand "sup") (("" (reduce :if-match all) nil nil)) nil)
untried nil nil nil nil nil))
(sup_exists 0
(sup_exists-1 nil 3237042679 nil
("" (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)
untried nil nil nil nil nil))
(sup_empty 0
(sup_empty-1 nil 3237042679 nil ("" (grind) nil nil) untried nil nil
nil nil nil))
(sup_nonempty 0
(sup_nonempty-1 nil 3237042679 nil
("" (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)
untried nil nil nil nil nil))
(bounded_union1 0
(bounded_union1-1 nil 3237042679 nil
("" (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)
nil nil nil nil nil nil))
(bounded_union2 0
(bounded_union2-1 nil 3237042679 nil
("" (grind :exclude ("bounded?")) nil nil) nil nil nil nil nil nil))
(bounded_inter1 0
(bounded_inter1-1 nil 3237042679 3237044247
("" (grind :if-match nil)
(("" (inst + "x!1")
(("" (apply (then (skolem-typepred) (inst?) (assert))) nil nil))
nil))
nil)
proved
((intersection const-decl "set" sets nil)
(member const-decl "bool" sets nil)
(F!1 skolem-const-decl "bounded_set" max_bounded nil)
(E!1 skolem-const-decl "set[T]" max_bounded nil)
(y!1 skolem-const-decl "(intersection[T](F!1, E!1))" max_bounded
nil)
(boolean nonempty-type-decl nil booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(number nonempty-type-decl nil numbers nil)
(real_pred const-decl "[number -> boolean]" reals nil)
(real nonempty-type-from-decl nil reals nil)
(rational_pred const-decl "[real -> boolean]" rationals nil)
(rational nonempty-type-from-decl nil rationals nil)
(integer_pred const-decl "[rational -> boolean]" integers nil)
(int nonempty-type-eq-decl nil integers nil)
(>= const-decl "bool" reals nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(T_pred const-decl "[nat -> boolean]" max_bounded nil)
(T formal-subtype-decl nil max_bounded nil)
(set type-eq-decl nil sets nil)
(bounded_set type-eq-decl nil max_bounded nil)
(bounded? const-decl "bool" max_bounded nil)
(bound const-decl "bool" max_bounded nil))
67850 4530 t nil))
(bounded_inter2 0
(bounded_inter2-2 "removed inst! from old proof" 3237044295
3237044295
("" (grind :if-match nil)
(("" (inst + "x!1")
(("" (apply (then (skolem-typepred) (inst?) (assert))) nil nil))
nil))
nil)
proved nil 41718 2860 t shostak)
(bounded_inter2-1 nil 3237042679 nil
("" (grind :if-match nil)
(("" (inst + "x!1") (("" (reduce :instantiator inst!) nil nil))
nil))
nil)
proved
((intersection const-decl "set" sets nil)
(member const-decl "bool" sets nil)
(F!1 skolem-const-decl "bounded_set" max_bounded nil)
(E!1 skolem-const-decl "set[T]" max_bounded nil)
(y!1 skolem-const-decl "(intersection[T](E!1, F!1))" max_bounded
nil)
(boolean nonempty-type-decl nil booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(number nonempty-type-decl nil numbers nil)
(real_pred const-decl "[number -> boolean]" reals nil)
(real nonempty-type-from-decl nil reals nil)
(rational_pred const-decl "[real -> boolean]" rationals nil)
(rational nonempty-type-from-decl nil rationals nil)
(integer_pred const-decl "[rational -> boolean]" integers nil)
(int nonempty-type-eq-decl nil integers nil)
(>= const-decl "bool" reals nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(T_pred const-decl "[nat -> boolean]" max_bounded nil)
(T formal-subtype-decl nil max_bounded nil)
(set type-eq-decl nil sets nil)
(bounded_set type-eq-decl nil max_bounded nil)
(bounded? const-decl "bool" max_bounded nil)
(bound const-decl "bool" max_bounded nil))
nil nil nil nil))
(max_TCC1 0
(max_TCC1-1 nil 3237042679 nil
("" (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)
nil nil nil nil nil nil))
(max_prop1 0
(max_prop1-1 nil 3237042679 3237044167
("" (skolem!)
(("" (typepred "max(A!1)") (("" (grind) nil nil)) nil)) nil)
unfinished
((max const-decl "{x: (A) | sup(A, x)}" max_bounded nil)
(sup const-decl "bool" max_bounded nil)
(empty? const-decl "bool" sets nil)
(bounded_set type-eq-decl nil max_bounded nil)
(bounded? const-decl "bool" max_bounded nil)
(set type-eq-decl nil sets nil)
(T formal-subtype-decl nil max_bounded nil)
(T_pred const-decl "[nat -> boolean]" max_bounded nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(>= const-decl "bool" reals nil)
(int nonempty-type-eq-decl nil integers nil)
(integer_pred const-decl "[rational -> boolean]" integers nil)
(rational nonempty-type-from-decl nil rationals nil)
(rational_pred const-decl "[real -> boolean]" rationals nil)
(real nonempty-type-from-decl nil reals nil)
(real_pred const-decl "[number -> boolean]" reals nil)
(number nonempty-type-decl nil numbers nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil)
(bound const-decl "bool" max_bounded nil))
5701 850 t nil))
(max_prop2 0
(max_prop2-1 nil 3237042679 nil
("" (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)
untried nil nil nil nil nil))
(max_subset 0
(max_subset-1 nil 3237042679 nil
("" (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)
untried nil nil nil nil nil))
(max_union 0
(max_union-1 nil 3237042679 nil
("" (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)
untried nil nil nil nil nil))
(max_intersection1 0
(max_intersection1-1 nil 3237042679 nil
("" (skosimp)
(("" (assert)
(("" (rewrite "max_subset")
(("" (delete 2 3) (("" (grind) nil nil)) nil)) nil))
nil))
nil)
untried nil nil nil nil nil))
(max_intersection2 0
(max_intersection2-1 nil 3237042679 nil
("" (skosimp)
(("" (assert)
(("" (rewrite "max_subset")
(("" (delete 2 3) (("" (grind) nil nil)) nil)) nil))
nil))
nil)
untried 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?_var
2;
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" (REWRITE "command_P_extensionality") 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))
--------------030807020401080701020807--
How-To-Repeat:
Fix: