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

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

Split up uvmThreadSemantics, add 'ok' predicates

uvmThreadSemantics was becoming a huge file that took several minutes
to compile, so it's been split into uvmThreadsStacks and
uvmInstructionSemantics.

In uvmThreadsStacks, new 'thread_ok' and 'stack_ok' predicates define
basic consistency requirements for thread and stack data structures.
All functions in this file have also been proven to produce valid
thread/stack structures when given valid input. This is a prerequisite
for proving execution state homomorphisms.

'thread_state' has been renamed to 'thread', and 'state_follows' has
been renamed to 'thread_follows'.
parent d4b31059
......@@ -13,5 +13,9 @@ sig
val run_finite_schedule : term frag list -> term -> term
val expect_result : term frag list -> term -> thm
val take_step : term frag list -> term -> term
val take_steps : term frag list -> term -> term
end
......@@ -52,5 +52,11 @@ struct
fun expect_result (expected : term frag list) (actual : term) : thm =
prove(Term(parens expected @ ` = ^actual`), simp[])
fun take_step (step : term frag list) (state : term) : term =
EVAL(Term(`^state >>= take_step` @ parens step)) |> concl |> rhs
fun take_steps (steps : term frag list) (state : term) : term =
EVAL(Term(`^state >>= take_steps` @ parens steps)) |> concl |> rhs
end
open HolKernel Parse boolLib bossLib
open uvmMemoryTheory
open uvmThreadSemanticsTheory
open uvmInstructionSemanticsTheory
open monadsyntax
open pred_setTheory
open finite_mapTheory
......@@ -18,14 +18,14 @@ val _ = Datatype`
sched_state = <|
env: environment;
threads: thread_state option list;
threads: thread option list;
stacks: stack list;
memory: memory
|>
`
val get_thread_def = Define`
get_thread n state : thread_state option =
get_thread n state : thread option =
if n < LENGTH state.threads then EL n state.threads else NONE
`
......@@ -35,7 +35,7 @@ val get_stack_def = Define`
`
val register_locations_def = Define`
register_locations (threads : thread_state option list) : location |-> value symbolic =
register_locations (threads : thread option list) : location |-> value symbolic =
(ZIP (threads, GENLIST Thread (LENGTH threads))
:> MAP (λ(t, tid).
case t of
......@@ -164,9 +164,10 @@ val thread_current_frame_state_def = Define`
val take_step_def = Define`
take_step (Commit (Thread tid) n) state = do
th <- expect (get_thread tid state) InvalidStep;
(next, outbox') <- expect (extract n th.outbox) InvalidStep;
((id, action), outbox') <- expect (extract n th.outbox) InvalidStep;
return (state with <|
memory updated_by (λm. m with committed updated_by CONS next);
memory updated_by λm.
m with committed updated_by CONS (Message (SOME th.tid) id action);
threads updated_by LUPDATE (SOME (th with outbox := outbox')) tid
|>)
od
......@@ -206,7 +207,7 @@ val take_step_def = Define`
| NONE => expect guess InvalidStep >>= get_stackref_id;
sid <- case sid of Stack n => return n;
st <- expect (get_stack sid state) (InvalidState "stack index out of bounds");
(st, th) <- resume_stack st vs (new_thread (Thread tid) (Stack sid));
(st, th) <- resume_stack st vs exec_inst (new_thread (Thread tid) (Stack sid));
return (state with <|
stacks updated_by LUPDATE st sid;
threads := LUPDATE (SOME th) tid threads
......
open HolKernel Parse boolLib bossLib
open uvmMemoryTheory
open uvmIRTheory
open uvmValuesTheory
open uvmErrorsTheory
open sumMonadTheory
open DefineUtils
open arithmeticTheory
open combinTheory
open finite_mapTheory
open listTheory
open optionTheory
open pairTheory
open pred_setTheory
open relationTheory
open string_numTheory
open sortingTheory
open lcsymtacs
open monadsyntax
val _ = new_theory "uvmThreadsStacks"
val _ = add_monadsyntax()
val _ = reveal "C" (* The C (flip) combinator is used in this theory *)
val _ = Datatype`
thread = <|
tid: thread_id;
stack_id: stack_id;
block_id: block_id;
action_id: action_id;
registers: register |-> value symbolic;
outbox: (action_id # action) list
|> ;
frame_id = Frame num stack_id ;
frame = <|
id: frame_id;
fn: function;
state: frame_state
|> ;
frame_state =
| READY ((uvm_type # register) list) (register resumption_data)
| ACTIVE (register terminst)
| DEAD (value symbolic resume_values option) ;
stack = <|
id: stack_id;
frames: frame list;
next_frame_id: num
|>
`
val stack_ok_def = Define`
stack_ok (s : stack)
EVERY (λf. case f.id of Frame n sid => sid = s.id n < s.next_frame_id) s.frames
`
val stacks_ok_def = Define`
stacks_ok (stacks : stack list)
EVERY stack_ok stacks
(MAP (λs. s.id) stacks = GENLIST Stack (LENGTH stacks))
`
val thread_ok_def = Define`
thread_ok (th : thread)
(ssa b. (ssa, b) FDOM th.registers b th.block_id)
EVERY (C $ th.action_id o FST) th.outbox
SORTED (λx y. FST x FST y) th.outbox
`
(* A thread state σ₁ follows a previous state σ₀ iff σ₁'s registers are
a superset of σ₀'s registers--that is, new registers may be defined, but
none can be overwritten or deleted--and iff σ₁'s frame_id and
next_memreqid are ≥ σ₀'s, and the states' tids are the same.
This relation is a partial ordering on thread states.
*)
val thread_follows_def = Define`
thread_follows (prev : thread) (next : thread)
(prev.tid = next.tid)
(prev.block_id next.block_id)
(prev.action_id next.action_id)
(prev.registers next.registers)
(a b. MEM (a, b) next.outbox prev.action_id a MEM (a, b) prev.outbox)
`
val thread_follows_refl = store_thm("thread_follows_refl",
``thread_follows s s``,
rw[thread_follows_def] >> metis_tac[])
val thread_follows_trans = store_thm("thread_follows_trans",
``thread_follows a b thread_follows b c thread_follows a c``,
simp[thread_follows_def] >>
metis_tac[block_id_lt_trans, action_id_lt_trans, SUBMAP_TRANS])
val propagates_def = Define`
propagates P f a b. P a f a = OK b P b
`
local val fail_lemma = prove(
``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
(* Converts a register into a symbolic value. *)
val sym_value_def = Define`
sym_value th (Var reg) = await (Register th.tid reg)
sym_value _ (Const v) = pure v
`
val add_register_def = Define`
add_register ((reg, val) : register # value symbolic) (th : thread) : thread or_error = do
assert (reg FDOM th.registers) (InvalidState "register being reused");
assert (SND reg th.block_id) (InvalidState "invalid register block ID");
return (th with registers updated_by C $|+ (reg, val))
od
`
val add_register_follows = store_thm("add_register_follows",
``add_register r s0 = OK s1 thread_follows s0 s1``,
Cases_on `r` >> rw[add_register_def, thread_follows_def] >> fs[])
val add_register_ok = store_thm("add_register_ok",
``r. propagates thread_ok (add_register r)``,
Cases >> rw[propagates_def, thread_ok_def, add_register_def] >> fs[] >> metis_tac[])
val enqueue_action_def = Define`
enqueue_action (a : action) (th : thread) : thread or_error =
return (th with <|
action_id updated_by action_id_suc;
outbox updated_by SNOC (th.action_id, a)
|>)
`
val enqueue_action_follows = store_thm("enqueue_action_follows",
``enqueue_action a s0 = OK s1 thread_follows s0 s1``,
rw[enqueue_action_def, thread_follows_def] >> fs[])
val enqueue_action_ok = store_thm("enqueue_action_ok",
``r. propagates thread_ok (enqueue_action r)``,
rw[propagates_def, thread_ok_def, enqueue_action_def] >> fs[EVERY_SNOC, C_DEF, o_DEF]
>- metis_tac[]
>- (POP_ASSUM (K ALL_TAC) >> POP_ASSUM MP_TAC >>
Q.MATCH_ABBREV_TAC `EVERY P a.outbox EVERY Q a.outbox` >>
`x. P x Q x` by metis_tac[action_id_lt_suc, action_id_lt_trans] >>
metis_tac[EVERY_MONOTONIC])
>- (Q.MATCH_ABBREV_TAC `SORTED R (SNOC (a.action_id, r) a.outbox)` >>
Cases_on `a.outbox = []` >> rw[SNOC_APPEND] >>
`0 < LENGTH a.outbox` by metis_tac[LENGTH_NIL, LESS_0_CASES] >>
`transitive R R (LAST a.outbox) (a.action_id, r)`
suffices_by fs[SORTED_APPEND_IFF] >>
Q.UNABBREV_TAC `R` >> rw[]
>- (rw[transitive_def, action_id_lt_def] >>
REPEAT (POP_ASSUM MP_TAC) >> REPEAT CASE_TAC >> rw[])
>- fs[LAST_EL, EVERY_EL, INV_PRE_LESS]))
val get_block_def = Define`
get_block (label : block_label)
(fn : function)
(th : thread)
: register bblock or_error = do
block <- expect (FLOOKUP fn.blocks label) (InvalidIR "block not found");
let reg = λv. (v, th.block_id) in return <|
args := MAP (reg ## I) block.args;
body := MAP (map_inst reg) block.body;
exit := map_terminst reg block.exit;
keepalives := MAP reg block.keepalives
|>
od
`
val lookup_function_def = Define`
lookup_function (env : environment) (name : func_name) : function or_error = do
version_opt <- expect (FLOOKUP env.func_versions name) (NoSuchFunction name);
(* TODO: Trap on undefined functions *)
version <- expect version_opt (UndefinedBehavior "undefined function");
expect (FLOOKUP env.functions version) (NoSuchFunction name)
od
`
val push_frame_def = Define`
push_frame (env : environment)
(name : func_name)
(input_args : (uvm_type # register) list)
(args : register or_const list)
(s : stack)
: stack or_error = do
fn <- lookup_function env name;
block <- expect (FLOOKUP fn.blocks fn.entry_block)
(InvalidIR "entry block not found");
return (s with <|
frames updated_by CONS (<|
id := Frame (s.next_frame_id) (s.id);
fn := fn;
state := READY input_args (<|
normal_dest := (fn.entry_block, args);
exceptional_dest := NONE
|>)
|>);
next_frame_id updated_by SUC
|>)
od
`
val push_frame_ok = store_thm("push_frame_ok",
``e x y z. propagates stack_ok (push_frame e x y z)``,
rw[propagates_def, push_frame_def, stack_ok_def] >> fs[] >>
POP_ASSUM (K ALL_TAC) >> POP_ASSUM (K ALL_TAC) >> POP_ASSUM MP_TAC >>
Q.MATCH_ABBREV_TAC `EVERY P a.frames EVERY Q a.frames` >>
`x. P x Q x` suffices_by metis_tac[EVERY_MONOTONIC] >>
Q.UNABBREV_TAC `P` >> Q.UNABBREV_TAC `Q` >> STRIP_TAC >>
simp[] >> CASE_TAC >> simp[])
val pop_frame_def = Define`
pop_frame (s : stack) : stack =
case s.frames of [] => s | _::rest => s with frames := rest
`
val pop_frame_ok = store_thm("pop_frame_ok",
``stack_ok s stack_ok (pop_frame s)``,
Cases_on `s.frames` >> rw[stack_ok_def, pop_frame_def])
val insert_resume_args_def = Define`
insert_resume_args ((_, destargs) : register destination)
(input_args : (uvm_type # register) list)
(args : value symbolic list)
(th : thread)
: value symbolic list =
let f = λarg.
case arg of
| Var v => (
case INDEX_FIND 0 (λ(_, v'). v = v') input_args of
| SOME (i, _) =>
if i < LENGTH args
then EL i args
else symbolic_or_error (Fail (InvalidState
(STRCAT "PASS_VALUES missing argument #" (n2s i))))
| NONE => sym_value th arg)
| Const c => pure c
in MAP f destargs
`
val resume_frame_def = Define`
resume_frame (fr : frame)
(res : value symbolic resume_values)
(exec_inst : register instruction -> thread -> thread or_error)
(th : thread)
: (frame # thread) or_error =
let initial_action_id = th.action_id in
let th = th with <| block_id updated_by block_id_suc |> in
case fr.state of
| READY ia rd => (
case res of
| NOR args => do
block <- get_block (FST rd.normal_dest) fr.fn th;
assert (LENGTH (SND rd.normal_dest) = LENGTH block.args)
(InvalidIR "block arity mismatch");
th <- FOLDL (λs r. s >>= add_register r) (return th)
(ZIP (MAP FST block.args, insert_resume_args rd.normal_dest ia args th));
th <- FOLDL (λs i. s >>= exec_inst i) (return th) block.body;
th <- FOLDL (λs a. s >>= enqueue_action a) (return th)
(LIST_BIND th.outbox (λm.
case m of
| (id, DoAlloca ty sid _) =>
if initial_action_id id
then [DoFree ty (StackAddr sid th.tid id)]
else []
| _ => []));
return (fr with state := ACTIVE block.exit, th)
od
| EXC _ => Fail (NotImplemented "exceptions"))
| _ => Fail (InvalidState "cannot resume a non-ready frame")
`
val resume_frame_follows = store_thm("resume_frame_follows",
``(i t0 t1. exec i t0 = OK t1 thread_follows t0 t1)
resume_frame f0 r exec t0 = OK (f1, t1)
thread_follows t0 t1``,
rw[resume_frame_def] >>
Cases_on `f0.state` >> fs[] >>
Cases_on `r` >> fs[] >>
Q.ABBREV_TAC `t0' = t0 with block_id updated_by block_id_suc` >>
`thread_follows th' t1` by metis_tac[enqueue_action_follows, foldl_follows] >>
`thread_follows th th'` by metis_tac[foldl_follows] >>
`thread_follows t0' th` by metis_tac[add_register_follows, foldl_follows] >>
`thread_follows t0 t0'` suffices_by metis_tac[thread_follows_trans] >>
Q.UNABBREV_TAC `t0'` >>
rw[thread_follows_def] >> fs[])
local val foldl_propagates_ok = prove(
``(r. propagates thread_ok (f r))
thread_ok a FOLDL (λs r. s >>= f r) (OK a) rs = OK b thread_ok b``,
strip_tac >>
`propagates thread_ok (λa. FOLDL (λs r. s >>= f r) (OK a) rs)` suffices_by
(rw[propagates_def] >> metis_tac[]) >>
simp[foldl_propagates])
in val resume_frame_ok = store_thm("resume_frame_ok",
``(i. propagates thread_ok (exec i))
f r. propagates thread_ok (lift_left SND o resume_frame f r exec)``,
rw[] >> rw[propagates_def, resume_frame_def] >> POP_ASSUM MP_TAC >>
REPEAT CASE_TAC >> rw[] >> fs[] >>
`thread_ok (a with block_id updated_by block_id_suc)` suffices_by
metis_tac[foldl_propagates_ok, add_register_ok, enqueue_action_ok] >>
rw[thread_ok_def] >> fs[thread_ok_def] >>
metis_tac[block_id_lt_suc, block_id_lt_trans])
end
val resume_stack_def = Define`
resume_stack (current_stack : stack)
(res : value symbolic resume_values)
(exec_inst : register instruction -> thread -> thread or_error)
(th : thread)
: (stack # thread) or_error =
case current_stack.frames of
| [] => Fail (InvalidState "stack underflow")
| fr::rest => do
(fr, th) <- resume_frame fr res exec_inst th;
return (current_stack with frames := fr::rest, th)
od
`
val resume_stack_follows = store_thm("resume_stack_follows",
``(i t0 t1. exec i t0 = OK t1 thread_follows t0 t1)
resume_stack s0 r exec t0 = OK (s1, t1)
thread_follows t0 t1``,
rw[resume_stack_def] >> Cases_on `s0.frames` >> fs[] >>
Cases_on `y0` >> fs[] >> metis_tac[resume_frame_follows])
val resume_stack_thread_ok = store_thm("resume_stack_thread_ok",
``(i. propagates thread_ok (exec i))
s r. propagates thread_ok (lift_left SND o resume_stack s r exec)``,
rw[] >> rw[propagates_def, resume_stack_def] >> Cases_on `s.frames` >> fs[] >>
Cases_on `y0` >> Cases_on `y0'` >> fs[] >> rw[] >>
`propagates thread_ok (lift_left SND o resume_frame h r exec)` suffices_by
(rw[] >> fs[propagates_def] >> metis_tac[SND]) >>
simp[resume_frame_ok])
val resume_stack_stack_ok = store_thm("resume_stack_stack_ok",
``r exec t. propagates stack_ok (λs. FST <$> resume_stack s r exec t)``,
rw[propagates_def, stack_ok_def, resume_stack_def] >> Cases_on `s.frames` >>
fs[] >> Cases_on `y0` >> Cases_on `y0'` >> fs[resume_frame_def] >> rw[] >>
REPEAT (POP_ASSUM MP_TAC) >> REPEAT CASE_TAC >> rw[] >> fs[])
val update_stack_state_def = Define`
update_stack_state (s : stack) (fs : frame_state) : stack or_error =
case s.frames of
| [] => Fail (InvalidState "stack underflow")
| fr::rest => return (s with frames := (fr with state := fs)::rest)
`
val update_stack_state_ok = store_thm("update_state_stack_ok",
``fs. propagates stack_ok (λs. update_stack_state s fs)``,
rw[propagates_def, stack_ok_def, update_stack_state_def] >>
Cases_on `s.frames` >> fs[] >> rw[])
val pop_and_resume_stack_def = Define`
pop_and_resume_stack (s : stack)
(res : value symbolic resume_values)
(exec : register instruction -> thread -> thread or_error)
(th : thread)
: (stack # thread) or_error =
case s.frames of
| [] => Fail (InvalidState "stack underflow")
| [_] => (λs. (s, th)) <$> update_stack_state s (DEAD (SOME res))
| _ => resume_stack (pop_frame s) res exec th
`
val get_stack_def = Define`
get_stack (Stack n) (stacks : stack list) : stack or_error =
if n < LENGTH stacks
then return (EL n stacks)
else Fail (InvalidState "stack index out of bounds")
`
val get_stack_id = store_thm("get_stack_id",
``stacks_ok stacks get_stack sid stacks = OK s s.id = sid``,
Cases_on `sid` >> rw[get_stack_def, stacks_ok_def] >>
metis_tac[EL_GENLIST, EL_MAP, LENGTH_GENLIST, LENGTH_MAP])
(* Creates a new thread with the given stack. *)
val new_thread_def = Define`
new_thread (tid : thread_id) (sid : stack_id) : thread =
<| tid := tid; stack_id := sid; block_id := Block 0;
action_id := Action 0; registers := FEMPTY; outbox := [] |>
`
val new_thread_ok = store_thm("new_thread_ok",
``tid sid. thread_ok (new_thread tid sid)``,
rw[new_thread_def, thread_ok_def])
val _ = export_theory()
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