To protect your data, the CISO officer has suggested users to enable GitLab 2FA as soon as possible.

Commit ea8b91db authored by Adam Nelson's avatar Adam Nelson
Browse files

Various scheduler proofs

parent 02bc6f3e
......@@ -40,7 +40,8 @@ struct
fun start_at (func_name : string) (args : term frag list) (env : term) : term =
let val func_name' = fromMLstring func_name in
EVAL(Term(`^env >>= init_sched_state (Func ^func_name') ` @ parens args)) |> concl |> rhs
EVAL(Term(`^env >>= λe. init_sched_state <|env:=e;main:=Func ^func_name';args:=` @ parens args @ `|>`))
|> concl |> rhs
end
fun run_schedule (schedule : term frag list) (state : term) : term =
......
......@@ -21,6 +21,12 @@ val _ = Datatype`
threads: thread option list;
stacks: stack list;
memory: memory
|> ;
program = <|
env: environment;
main: func_name;
args: value list
|>
`
......@@ -119,28 +125,56 @@ val resolve_all_def = TotalDefn.tDefine "resolve_all" `
` (WF_REL_TAC `measure (FCARD o unresolved_locations)` >>
metis_tac[resolve_terminates_when_fcard_eq, resolve_once_decreases_unresolved])
val resolve_all_simp = store_thm("resolve_all_simp",
``resolve_all s = let s' = resolve_once s in if s = s' then s else resolve_all s'``,
rw[Once resolve_all_def, resolve_terminates_when_fcard_eq])
val fully_resolved_def = Define`
fully_resolved (s : sched_state)
FCARD s.memory.resolved = FCARD (resolve_once s).memory.resolved
`
val resolve_once_fully_resolved = store_thm("resolve_once_fully_resolved",
``s. fully_resolved s s = resolve_once s``,
rw[fully_resolved_def] >> simp[resolve_terminates_when_fcard_eq])
val resolve_all_fully_resolved = store_thm("resolve_all_fully_resolved",
``s. fully_resolved s s = resolve_all s``,
ASSUME_TAC resolve_once_fully_resolved >> rw[Once resolve_all_def] >>
metis_tac[fully_resolved_def])
val fully_resolved_after_resolve_all = store_thm("fully_resolved_after_resolve_all",
``s. fully_resolved (resolve_all s)``,
measureInduct_on `FCARD (unresolved_locations s)` >>
rw[Once resolve_all_simp] >> fs[resolve_once_fully_resolved] >>
metis_tac[resolve_once_decreases_unresolved])
val resolve_all_idem = store_thm("resolve_all_idem",
``IDEM resolve_all``,
rw[relationTheory.IDEM_DEF] >>
`x. resolve_all x = resolve_all (resolve_all x)`
suffices_by metis_tac[combinTheory.o_THM] >> rw[] >>
fs[resolve_all_fully_resolved, fully_resolved_after_resolve_all])
val init_sched_state_def = Define`
init_sched_state (main : func_name)
(args : value list)
(env : environment)
: sched_state or_error =
init_sched_state (p : program) : sched_state or_error =
let st = <|
id := Stack 0;
frames := [];
next_frame_id := 0
|> in
let original_thread = DoNewThread (pure (Stack 0)) (NOR (MAP pure args)) in
let original_thread = DoNewThread (pure (Stack 0)) (NOR (MAP pure p.args)) in
let committed = SND (FOLDR (λg (id, cs).
(action_id_suc id, CONS (Message NONE id (UNCURRY DoGlobalInit g)) cs))
(Action 1, [Message NONE (Action 0) original_thread])
env.globals) in
p.env.globals) in
do
fn <- lookup_function env main;
fn <- lookup_function p.env p.main;
st <- (
let args = GENLIST (λn. %(n2s n)#0) (LENGTH fn.signature.arg_types)
in push_frame env main (ZIP (fn.signature.arg_types, args)) (MAP Var args) st);
in push_frame p.env p.main (ZIP (fn.signature.arg_types, args)) (MAP Var args) st);
return (<|
env := env;
env := p.env;
threads := [];
stacks := [st];
memory := <| committed := committed; resolved := FEMPTY |>
......@@ -216,12 +250,16 @@ val take_step_def = Define`
od
`
val try_step_def = Define`
try_step (step : sched_step) (state : sched_state) : sched_state or_error =
case take_step step state of
| Fail InvalidStep => return state
| next => resolve_all <$> next
`
val take_steps_def = Define`
take_steps (steps : sched_step list) (state : sched_state) : sched_state or_error =
FOLDL (λs step. case s >>= take_step step of
| Fail InvalidStep => s
| res => resolve_all <$> res)
(OK state) steps
FOLDL (λs step. s >>= try_step step) (OK state) steps
`
val has_terminated_def = Define`
......@@ -278,31 +316,102 @@ val run_finite_schedule_def = Define`
run_finite_schedule (schedule : sched_step list)
(state : sched_state)
: sched_state or_error =
resolve_all <$> FOLDL
(λs step. case s >>= λs.
if has_terminated s then return s else take_step step s of
| Fail InvalidStep => s
| res => resolve_all <$> res)
(OK state) schedule
FOLDL (λs step. s >>= λs. if has_terminated s then return s else try_step step s)
(OK (resolve_all state))
schedule
`
val run_schedule_def = Define`
run_schedule (schedule : sched_step llist)
(state : sched_state)
: sched_state or_error =
resolve_all <$> SND (WHILE
(λ(_, m). case m of
| OK state => ¬has_terminated state
| Fail _ => F)
SND (WHILE
(λ(steps, state).
case LHD steps of
| SOME step => (THE (LTL steps), case state >>= take_step step of
| Fail InvalidStep => state
| res => resolve_all <$> res)
| NONE => (steps, Fail (InvalidState "schedule exhausted")))
(schedule, OK state))
IS_SOME (LHD steps)
(case state of OK state => ¬has_terminated state | Fail _ => F))
(λ(steps, state). THE (LTL steps), state >>= try_step (THE (LHD steps)))
(schedule, OK (resolve_all state)))
`
val run_schedule_terminated = store_thm("run_schedule_terminated",
``st. has_terminated (resolve_all st) sc. run_schedule sc st = OK (resolve_all st)``,
rw[run_schedule_def, Once whileTheory.WHILE])
val run_finite_schedule_eq_run_schedule = store_thm("run_finite_schedule_eq_run_schedule",
``sc st. run_finite_schedule sc st = run_schedule (fromList sc) st``,
Induct >> rw[run_finite_schedule_def, run_schedule_def]
>- simp[Once whileTheory.WHILE]
>- (`run_schedule (fromList sc) st = run_schedule (h:::fromList sc) st`
suffices_by fs[run_schedule_def, run_finite_schedule_def] >>
rw[run_schedule_def] >> Cases_on `sc` >>
simp[Once whileTheory.WHILE] >> simp[Once whileTheory.WHILE])
>- (simp[Once whileTheory.WHILE] >>
Cases_on `st'. try_step h (resolve_all st) = OK (resolve_all st')`
>- (fs[run_schedule_def, run_finite_schedule_def] >> metis_tac[])
>- (`x. try_step h (resolve_all st) = Fail x` suffices_by (
rw[Once whileTheory.WHILE] >> Cases_on `try_step h (resolve_all st)` >>
fs[uvmThreadsStacksTheory.foldl_fail]) >>
fs[try_step_def] >> CASE_TAC >> fs[] >> TRY CASE_TAC >> fs[] >>
metis_tac[])))
val finite_schedule_terminates_def = Define`
finite_schedule_terminates (prg : program) (schedule : sched_step list)
st. init_sched_state prg >>= run_finite_schedule schedule = OK st
has_terminated st
`
val schedule_terminates_def = Define`
schedule_terminates (prg : program) (schedule : sched_step llist)
n fs. LTAKE n schedule = SOME fs finite_schedule_terminates prg fs
`
val finite_schedule_valid_def = Define`
finite_schedule_valid (validator : sched_state -> bool)
(prg : program)
(schedule : sched_step list)
len. len LENGTH schedule
merge_left (K T) (validator <$>
(init_sched_state prg >>= run_finite_schedule (TAKE len schedule)))
`
val schedule_valid_def = Define`
schedule_valid (validator : sched_state -> bool)
(prg : program)
(schedule : sched_step llist)
len fs. LTAKE len schedule = SOME fs
merge_left (K T) (validator <$>
(init_sched_state prg >>= run_finite_schedule fs))
`
val finite_schedule_terminates_snoc = store_thm("finite_schedule_terminates_snoc",
``p s. finite_schedule_terminates p s x. finite_schedule_terminates p (SNOC x s)``,
rw[finite_schedule_terminates_def, run_finite_schedule_def, listTheory.FOLDL_SNOC] >>
qexists_tac `st` >> fs[])
val finite_schedule_terminates_snoc_eq = store_thm("finite_schedule_terminates_snoc_eq",
``p s. finite_schedule_terminates p s
x. init_sched_state p >>= run_finite_schedule s
= init_sched_state p >>= run_finite_schedule (SNOC x s)``,
rw[finite_schedule_terminates_def, run_finite_schedule_def, init_sched_state_def] >>
rw[run_finite_schedule_def, listTheory.FOLDL_SNOC])
val finite_schedule_valid_snoc = store_thm("finite_schedule_valid_snoc",
``p s. finite_schedule_terminates p s
v. finite_schedule_valid v p s
x. finite_schedule_valid v p (SNOC x s)``,
rw[finite_schedule_valid_def] >> Cases_on `len = SUC (LENGTH s)` >> fs[] >> rw[]
>- (`TAKE (SUC (LENGTH s)) (SNOC x s) = SNOC x s` by (
`LENGTH (SNOC x s) = SUC (LENGTH s)` by simp[] >>
metis_tac[listTheory.TAKE_LENGTH_ID]) >>
`init_sched_state p >>= run_finite_schedule (SNOC x s) =
init_sched_state p >>= run_finite_schedule s`
by simp[finite_schedule_terminates_snoc_eq] >>
rw[] >> `LENGTH s LENGTH s` by simp[] >>
metis_tac[listTheory.TAKE_LENGTH_ID])
>- (`len LENGTH s` by simp[] >>
`TAKE len (SNOC x s) = TAKE len s` suffices_by metis_tac[] >>
fs[listTheory.TAKE_APPEND1]))
(* A schedule is fair iff, at any point in the schedule, all possible steps
occur at some future point in the schedule.
*)
......
......@@ -101,32 +101,31 @@ val propagates_def = Define`
propagates P f a b. P a f a = OK b P b
`
local val fail_lemma = prove(
val foldl_fail = store_thm("foldl_fail",
``f e. FOLDL (λs r. s >>= f r) (Fail e) rs = Fail e``,
Induct_on `rs` >> fs[] >> Cases_on `h` >> fs[])
in
val foldl_follows = store_thm("foldl_follows",
``(r t0 t1. (f r t0 = OK t1) thread_follows t0 t1)
t0 t1. FOLDL (λs r. s >>= f r) (OK t0) rs = OK t1
thread_follows t0 t1``,
Induct_on `rs` >> fs[FOLDL, thread_follows_refl] >>
strip_tac >> rw[] >> Cases_on `f h t0` >>
metis_tac[thread_follows_trans, fail_lemma])
(* val foldl_thread_ok = store_thm("foldl_thread_ok",
``(∀r t0 t1. thread_ok t0 ⇒ f r t0 = OK t1 ⇒ thread_ok t1)
⇒ ∀t0 t1. thread_ok t0
⇒ FOLDL (λs r. s >>= f r) (OK t0) rs = OK t1
⇒ thread_ok t1``,
strip_tac >> Induct_on `rs` >> rw[]
>- (simp[FOLDL] >> metis_tac[])
>- (Cases_on `f h t0` >> metis_tac[fail_lemma])) *)
val foldl_propagates = store_thm("foldl_propagates",
``(r. propagates P (f r))
propagates P (λa. FOLDL (λs r. s >>= f r) (OK a) rs)``,
strip_tac >> Induct_on `rs` >> rw[]
>- (rw[propagates_def] >> simp[FOLDL])
>- (rw[propagates_def] >> Cases_on `f h a` >> fs[propagates_def] >> metis_tac[fail_lemma]))
end
val foldl_follows = store_thm("foldl_follows",
``(r t0 t1. (f r t0 = OK t1) thread_follows t0 t1)
t0 t1. FOLDL (λs r. s >>= f r) (OK t0) rs = OK t1
thread_follows t0 t1``,
Induct_on `rs` >> fs[FOLDL, thread_follows_refl] >>
strip_tac >> rw[] >> Cases_on `f h t0` >>
metis_tac[thread_follows_trans, foldl_fail])
(* val foldl_thread_ok = store_thm("foldl_thread_ok",
``(∀r t0 t1. thread_ok t0 ⇒ f r t0 = OK t1 ⇒ thread_ok t1)
⇒ ∀t0 t1. thread_ok t0
⇒ FOLDL (λs r. s >>= f r) (OK t0) rs = OK t1
⇒ thread_ok t1``,
strip_tac >> Induct_on `rs` >> rw[]
>- (simp[FOLDL] >> metis_tac[])
>- (Cases_on `f h t0` >> metis_tac[foldl_fail])) *)
val foldl_propagates = store_thm("foldl_propagates",
``(r. propagates P (f r))
propagates P (λa. FOLDL (λs r. s >>= f r) (OK a) rs)``,
strip_tac >> Induct_on `rs` >> rw[]
>- (rw[propagates_def] >> simp[FOLDL])
>- (rw[propagates_def] >> Cases_on `f h a` >> fs[propagates_def] >> metis_tac[foldl_fail]))
(* Converts a register into a symbolic value. *)
val sym_value_def = Define`
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment