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

Commit 1006251d authored by Adam Nelson's avatar Adam Nelson
Browse files

Incomplete work on improved eval performance

parent fb68640a
......@@ -17,8 +17,8 @@ struct
if pairSyntax.is_pair v then NO_TAC else Cases_on `^v`
end)
val multi_case_tac =
REPEAT ((BasicProvers.FULL_CASE_TAC ORELSE pair_case_tac) >> fs[] >> rw[])
fun multi_case_tac x =
(REPEAT ((BasicProvers.FULL_CASE_TAC ORELSE pair_case_tac) >> fs[] >> rw[])) x
fun rw_assums xs =
POP_ASSUM_LIST (map_every (assume_tac o REWRITE_RULE xs) o rev)
......
......@@ -98,17 +98,19 @@ val merge_left_def = Define`
`
val left_set_def = Define`
left_set (sum : α + β) : α set =
case sum of
| INL a => {a}
| INR _ => {}
left_set (sum : α + β) = case sum of INL a => {a} | INR _ =>
`
val right_set_def = Define`
right_set (sum : α + β) : β set =
case sum of
| INL _ => {}
| INR b => {b}
right_set (sum : α + β) = case sum of INL _ => | INR b => {b}
`
val left_list_def = Define`
left_list (sum : α + β) = case sum of INL a => [a] | INR _ => []
`
val right_list_def = Define`
right_list (sum : α + β) = case sum of INL _ => [] | INR b => [b]
`
(* Monad laws for bind_left: left identity, right identity, and associativity *)
......
......@@ -329,7 +329,7 @@ val _ = Datatype`
uvm_type
(σ or_const)
(σ destination)
(value |-> σ destination)
((value # σ destination) list)
| Watchpoint
((wpid # σ destination) option)
(* NONE = unconditional trap *)
......@@ -478,7 +478,7 @@ val map_terminst_def = Define`
| Branch2 cond dst1 dst2 =>
Branch2 (f <$> cond) (map_dest f dst1) (map_dest f dst2)
| Switch t cond dst branches =>
Switch t (f <$> cond) (map_dest f dst) (map_dest f o_f branches)
Switch t (f <$> cond) (map_dest f dst) (MAP (I ## map_dest f) branches)
| Watchpoint wpdst tys rd =>
Watchpoint (OPTION_MAP (I ## map_dest f) wpdst) tys (map_rd rd)
| WPBranch id dst1 dst2 => WPBranch id (map_dest f dst1) (map_dest f dst2)
......@@ -489,67 +489,69 @@ val map_terminst_def = Define`
`
val new_stack_clause_vars_def = Define`
new_stack_clause_vars (PassValues vs) = BIGUNION (set (MAP (left_set o FST) vs))
new_stack_clause_vars (ThrowExc e) = left_set e
new_stack_clause_vars (PassValues vs) = LIST_BIND vs (left_list o FST)
new_stack_clause_vars (ThrowExc e) = left_list e
`
(* Given an expression, returns a set of all variables read by the expression
(* Given an expression, returns a list of all variables read by the expression
(its _input variables_).
*)
val expr_vars_def = Define`
expr_vars (Id _ v) = {v}
expr_vars (BinOp _ _ a b) = {a; b}
expr_vars (CmpOp _ _ a b) = {a; b}
expr_vars (ConvOp _ _ _ v) = {v}
expr_vars (Select _ _ c t f) = {c; t; f}
expr_vars (ExtractValue _ _ s) = {s}
expr_vars (InsertValue _ _ s v) = {s; v}
expr_vars (ExtractElement _ _ a i) = {a; i}
expr_vars (InsertElement _ _ a i v) = {a; i; v}
expr_vars (ShuffleVector _ _ v1 v2 m) = {v1; v2; m}
expr_vars (GetIRef _ ref) = {ref}
expr_vars (GetFieldIRef _ _ _ ref) = {ref}
expr_vars (GetElementIRef _ _ _ ref index) = {ref; index}
expr_vars (ShiftIRef _ _ _ ref offset) = {ref; offset}
expr_vars (GetVarPartIRef _ _ ref) = {ref}
expr_vars (Id _ v) = [v]
expr_vars (BinOp _ _ a b) = nub [a; b]
expr_vars (CmpOp _ _ a b) = nub [a; b]
expr_vars (ConvOp _ _ _ v) = [v]
expr_vars (Select _ _ c t f) = nub [c; t; f]
expr_vars (ExtractValue _ _ s) = nub [s]
expr_vars (InsertValue _ _ s v) = nub [s; v]
expr_vars (ExtractElement _ _ a i) = nub [a; i]
expr_vars (InsertElement _ _ a i v) = nub [a; i; v]
expr_vars (ShuffleVector _ _ v1 v2 m) = nub [v1; v2; m]
expr_vars (GetIRef _ ref) = [ref]
expr_vars (GetFieldIRef _ _ _ ref) = [ref]
expr_vars (GetElementIRef _ _ _ ref index) = nub [ref; index]
expr_vars (ShiftIRef _ _ _ ref offset) = nub [ref; offset]
expr_vars (GetVarPartIRef _ _ ref) = nub [ref]
`
(* Given an instruction, returns a pair of sets (input variables, output
variables). The union of these sets is the set of all variables referenced
(* Given an instruction, returns a pair of lists (input variables, output
variables). The union of these lists is the list of all variables referenced
by the instruction.
*)
val inst_vars_def = Define`
inst_vars (Assign vs e) = (BIGUNION (IMAGE left_set (expr_vars e)), set vs)
inst_vars (Load v _ _ src _) = ({src}, {v})
inst_vars (Store src _ _ dst _) = (left_set src, {dst})
inst_vars (Assign vs e) = (LIST_BIND (expr_vars e) left_list, nub vs)
inst_vars (Load v _ _ src _) = ([src], [v])
inst_vars (Store src _ _ dst _) = (left_list src, [dst])
inst_vars (CmpXchg v1 v2 _ _ _ _ _ loc exp des) =
({loc} left_set exp left_set des, {v1; v2})
inst_vars (AtomicRMW v _ _ _ _ loc opnd) = ({loc} left_set opnd, {v})
inst_vars (Fence _) = (, )
inst_vars (New v _) = (, {v})
inst_vars (Alloca v _) = (, {v})
inst_vars (NewHybrid v _ _ len) = (left_set len, {v})
inst_vars (AllocaHybrid v _ _ len) = (left_set len, {v})
(nub (loc::left_list exp ++ left_list des), nub [v1; v2])
inst_vars (AtomicRMW v _ _ _ _ loc opnd) = (nub (loc::left_list opnd), [v])
inst_vars (Fence _) = ([], [])
inst_vars (New v _) = ([], [v])
inst_vars (Alloca v _) = ([], [v])
inst_vars (NewHybrid v _ _ len) = (left_list len, [v])
inst_vars (AllocaHybrid v _ _ len) = (left_list len, [v])
inst_vars (NewThread v s tl nsc) =
(left_set s left_set tl new_stack_clause_vars nsc , {v})
(nub (left_list s ++ left_list tl ++ new_stack_clause_vars nsc), [v])
`
val inst_input_vars_def = Define`inst_input_vars i = FST (inst_vars i)`
val inst_output_vars_def = Define`inst_output_vars i = SND (inst_vars i)`
val inst_all_vars_def = Define`inst_all_vars i = let (a, b) = inst_vars i in a b`
val inst_all_vars_def = Define`
inst_all_vars i = let (a, b) = inst_vars i in nub (a ++ b)
`
val comminst_vars_def = Define`
comminst_vars (NewStack _ fref) = left_set fref
comminst_vars CurrentStack =
comminst_vars ThreadExit =
comminst_vars (NewStack _ fref) = left_list fref
comminst_vars CurrentStack = []
comminst_vars ThreadExit = []
`
(* Given a terminal instruction, returns a pair of sets (input variables, passed
variables). The union of these sets is the set of all variables referenced by
(* Given a terminal instruction, returns a pair of lists (input variables, passed
variables). The union of these lists is the list of all variables referenced by
the instruction.
Note that "input variables" are variables whose values are required in order
......@@ -558,39 +560,39 @@ val comminst_vars_def = Define`
read.
*)
val terminst_vars_def = Define`
terminst_vars (inst : α terminst) : α set # α set =
let flat_left_set = λl. BIGUNION (IMAGE left_set (set l)) in
let dest_vars : α destination -> α set =
λ(_, args) v. MEM (Var v) args in
let rd_vars : α resumption_data -> α set =
λrd. dest_vars rd.normal_dest (
case rd.exceptional_dest of
| SOME d => dest_vars d
| NONE => ) in
terminst_vars (inst : α terminst) : α list # α list =
let dest_vars dest = LIST_BIND (SND dest) left_list in
let rd_vars rd =
dest_vars rd.normal_dest ++
option_CASE rd.exceptional_dest [] dest_vars in
case inst of
| Ret vals => , flat_left_set vals
| Throw v => , left_set v
| Call vs cd rd => left_set cd.name, set vs flat_left_set cd.args rd_vars rd
| TailCall cd => left_set cd.name, flat_left_set cd.args
| Branch1 dst => , dest_vars dst
| Branch2 cond dst1 dst2 => left_set cond, dest_vars dst1 dest_vars dst2
| Ret vals => [], nub (LIST_BIND vals left_list)
| Throw v => [], nub (left_list v)
| Call vs cd rd =>
left_list cd.name,
nub (vs ++ LIST_BIND cd.args left_list ++ rd_vars rd)
| TailCall cd => left_list cd.name, nub (LIST_BIND cd.args left_list)
| Branch1 dst => [], nub (dest_vars dst)
| Branch2 cond dst1 dst2 => left_list cond, nub (dest_vars dst1 ++ dest_vars dst2)
| Switch _ cond def_dst branches =>
left_set cond,
dest_vars def_dst λvr.vl. vr dest_vars (branches ' vl)
| Watchpoint NONE _ rd => , rd_vars rd
| Watchpoint (SOME (id, dst)) _ rd => , dest_vars dst rd_vars rd
| WPBranch id dst1 dst2 => , dest_vars dst1 dest_vars dst2
left_list cond,
nub (dest_vars def_dst ++ LIST_BIND branches (dest_vars o SND))
| Watchpoint NONE _ rd => [], nub (rd_vars rd)
| Watchpoint (SOME (id, dst)) _ rd => [], nub (dest_vars dst ++ rd_vars rd)
| WPBranch id dst1 dst2 => [], nub (dest_vars dst1 ++ dest_vars dst2)
| SwapStack vs id _ nsc rd =>
left_set id, set vs new_stack_clause_vars nsc rd_vars rd
| CommInst vs ci rd => comminst_vars ci, set vs rd_vars rd
| ExcClause inst rd => inst_input_vars inst, rd_vars rd
left_list id, nub (vs ++ new_stack_clause_vars nsc ++ rd_vars rd)
| CommInst vs ci rd => comminst_vars ci, nub (vs ++ rd_vars rd)
| ExcClause inst rd => inst_input_vars inst, nub (rd_vars rd)
`
val terminst_input_vars_def = Define`terminst_input_vars i = FST (terminst_vars i)`
val terminst_passed_vars_def = Define`terminst_passed_vars i = SND (terminst_vars i)`
val terminst_all_vars_def = Define`terminst_all_vars i = let (a, b) = terminst_vars i in a b`
val terminst_all_vars_def = Define`
terminst_all_vars i = let (a, b) = terminst_vars i in nub (a ++ b)
`
(* A basic block (see the spec)
https://github.com/microvm/microvm-spec/blob/master/uvm-ir.rest#function-body
......@@ -668,8 +670,14 @@ local
metis_tac[PAIR, PAIR_MAP])
val pair_fst_compose = prove(``f o g ## I = (f ## I) o (g ## I)``,
rw[pair_map_def, o_DEF])
val pair_snd_compose = prove(``I ## f o g = (I ## f) o (I ## g)``,
rw[pair_map_def, o_DEF])
val pair_map_I = prove(``(I ## MAP I) = I``, metis_tac[pair_I, I_THM, MAP_ID])
val option_map_I = prove(``x. OPTION_MAP I x = x``, Cases >> rw[OPTION_MAP_DEF])
val left_list_set = prove(``set (left_list x) = left_set x``,
rw[left_list_def, left_set_def] >> REPEAT CASE_TAC >> fs[])
val left_list_map = prove(``left_list (f <$> x) = MAP f (left_list x)``,
rw[left_list_def, lift_left_def, o_DEF] >> REPEAT CASE_TAC >> fs[])
in
(* The mapping functions should obey the functor laws:
- `map I x = x`
......@@ -727,43 +735,44 @@ in
val map_terminst_id = store_thm("map_terminst_id[simp]",
``map_terminst I x = x``,
`map_dest I = I` by metis_tac[map_dest_id, I_THM] >>
Cases_on `x` >>
fs[map_terminst_def, lift_I, pair_I, pair_map_I, option_map_I, I_THM,
theorem "resumption_data_component_equality"]
>- metis_tac[I_THM, o_f_FAPPLY, o_f_FDOM, fmap_EQ_THM])
theorem "resumption_data_component_equality",
prove(``map_dest I = I``, metis_tac[map_dest_id, I_THM])])
val map_terminst_compose = store_thm("map_terminst_compose[simp]",
``map_terminst (f o g) x = map_terminst f (map_terminst g x)``,
Cases_on `x` >>
rw[map_terminst_def, lift_left_compose, MAP_o, OPTION_MAP_COMPOSE,
theorem "resumption_data_component_equality",
prove(
``x. MAP (lift_left (f o g)) x = MAP (lift_left f) (MAP (lift_left g) x)``,
metis_tac[MAP_MAP_o, lift_left_compose, o_DEF]),
prove(
``map_dest (f o g) = map_dest f o map_dest g``,
metis_tac[map_dest_compose, o_DEF])]
>- (Cases_on `o'` >> simp[OPTION_MAP_DEF, pair_map_def]))
theorem "resumption_data_component_equality"] >>
TRY (
match_mp_tac
(prove(``(x. f x = g x) OPTION_MAP f x = OPTION_MAP g x``, metis_tac[])) >>
simp[map_dest_compose]) >>
metis_tac[MAP_MAP_o, lift_left_compose, o_THM, pair_snd_compose,
map_dest_compose])
(* The mapping functions should map all variables included in an expression or
instruction's variable set(s).
*)
val map_expr_vars = store_thm("map_expr_vars",
``expr_vars (map_expr f x) = IMAGE f (expr_vars x)``,
Cases_on `x` >> simp[map_expr_def, expr_vars_def])
``set (expr_vars (map_expr f x)) = set (MAP f (expr_vars x))``,
Cases_on `x` >> simp[map_expr_def, expr_vars_def, LIST_TO_SET_MAP])
val map_inst_vars = store_thm("map_inst_vars",
``FST (inst_vars (map_inst f x)) = IMAGE f (FST (inst_vars x))
SND (inst_vars (map_inst f x)) = IMAGE f (SND (inst_vars x))``,
``set (FST (inst_vars (map_inst f x))) = set (MAP f (FST (inst_vars x)))
set (SND (inst_vars (map_inst f x))) = set (MAP f (SND (inst_vars x)))``,
Cases_on `x` >>
simp[map_inst_def, inst_vars_def, map_expr_vars, left_set_def,
map_new_stack_clause_def, left_set_image,
LIST_TO_SET_MAP, IMAGE_BIGUNION, IMAGE_COMPOSE]
>- metis_tac[left_set_def, lift_left_def, left_set_image, o_THM,
IMAGE_BIGUNION, IMAGE_COMPOSE]
>- (Cases_on `n` >> simp[new_stack_clause_vars_def, left_set_image] >>
metis_tac[left_set_def, lift_left_def, left_set_image, o_THM,
IMAGE_BIGUNION, IMAGE_COMPOSE, LIST_TO_SET_MAP,
FST_PAIR_MAP, SND_PAIR_MAP]))
simp[map_inst_def, inst_vars_def, map_expr_vars,
map_new_stack_clause_def, LIST_TO_SET_MAP, IMAGE_BIGUNION,
IMAGE_COMPOSE, LIST_BIND_def, LIST_TO_SET_FLAT, left_list_set,
left_set_image]
>- metis_tac[left_set_image, left_list_map, left_list_set, IMAGE_BIGUNION,
IMAGE_COMPOSE, o_THM]
>- (CASE_TAC >>
simp[new_stack_clause_vars_def, LIST_BIND_def, LIST_TO_SET_FLAT,
LIST_TO_SET_MAP, IMAGE_COMPOSE] >>
metis_tac[left_set_def, left_list_def, lift_left_def, left_list_map,
left_list_set, left_set_image, o_THM, IMAGE_BIGUNION, IMAGE_COMPOSE,
LIST_TO_SET_MAP, FST_PAIR_MAP, SND_PAIR_MAP]))
(*
val map_terminst_vars = Q.store_thm(
"map_terminst_vars",
......
......@@ -9,10 +9,10 @@ open sumMonadTheory
open DefineUtils
open listTheory
open alistTheory
open combinTheory
open pairTheory
open optionTheory
open finite_mapTheory
open pred_setTheory
open lcsymtacs
open monadsyntax
......@@ -21,22 +21,6 @@ val _ = new_theory "uvmInstructionSemantics"
val _ = add_monadsyntax()
val _ = reveal "C" (* The C (flip) combinator is used in this theory *)
(* multi_case_tac is redefined here because importing it from DefineUtils
doesn't work properly for some reason.
*)
val pair_case_tac =
qpat_assum `_ (_: α # β) = _` (fn a =>
let val v = concl a |> lhs |> dest_comb |> #2 in
if pairSyntax.is_pair v then NO_TAC else Cases_on `^v`
end) ORELSE
qpat_assum `_ = _ (_: α # β)` (fn a =>
let val v = concl a |> rhs |> dest_comb |> #2 in
if pairSyntax.is_pair v then NO_TAC else Cases_on `^v`
end)
val multi_case_tac =
REPEAT ((BasicProvers.FULL_CASE_TAC ORELSE pair_case_tac) >> fs[] >> rw[])
(* Evaluates a binary operation, returning the result. Returns an error if the
values `v1`, `v2` are incorrectly typed, or if the result is undefined.
*)
......@@ -98,7 +82,7 @@ val eval_conv_def = Define`
behavior (such as division by zero).
*)
val eval_expr_def = Define`
eval_expr (e : register or_const expression) (tid : thread_id) : value list symbolic =
eval_expr (e : num or_const expression) (tid : thread_id) : value list symbolic =
let assert_ref_type_eq = λrt rt' ty ty' msg.
assert_type_eq (IRef rt (Type ty)) (IRef rt' (Type ty')) msg in
symbolic_error_join (case e of
......@@ -207,13 +191,13 @@ val eval_expr_def = Define`
`
val exec_inst_def = Define`
exec_inst (inst : register instruction) (tid : thread_id) (th : thread) : thread or_error =
exec_inst (inst : num instruction) (tid : thread_id) (th : thread) : thread or_error =
let id = th.action_id in do
(th', action) <-
case inst of
| Assign vs expr =>
let results = eval_expr expr tid in
let add_return_value = λ(r, i) s.
let add_return_value (r, i) s =
let v = symbolic_error_join (
(λresults. if i < LENGTH results
then return (EL i results)
......@@ -224,7 +208,7 @@ val exec_inst_def = Define`
:> FOLDL (λs r. s >>= add_return_value r) (return th)
:> liftM (λs. (s, NONE))
| Load dst _ ty src ord =>
let src_loc = Register tid src in
let src_loc = Register src tid in
let value = symbolic_error_join ((λiref value. do
ia <- get_iref_addr iref;
assert_type_eq ty ia.ty "LOAD referent type";
......@@ -233,7 +217,7 @@ val exec_inst_def = Define`
add_register (dst, value) th
:> liftM (λth. (th, SOME (DoLoad src_loc ord)))
| Store src _ _ dst ord =>
let dst_loc = Register tid dst in
let dst_loc = Register dst tid in
return (th, SOME (DoStore dst_loc ord (sym_value tid src)))
| CmpXchg _ _ _ _ _ _ _ _ _ _ => Fail (NotImplemented "CMPXCHG")
| AtomicRMW _ _ _ _ _ _ _ => Fail (NotImplemented "ATOMICRMW")
......@@ -267,30 +251,31 @@ val exec_inst_def = Define`
od
`
val exec_inst_follows = store_thm("exec_inst_follows",
``exec_inst i tid t0 = OK t1 thread_follows t0 t1``,
Cases_on `i` >> rw[exec_inst_def, APP_DEF] >> fs[] >>
map_every imp_res_tac [add_register_follows, enqueue_action_follows, foldl_follows]
>- (fs[] >> pop_assum match_mp_tac >> rw[] >> Cases_on `r` >> fs[] >>
prove_tac[add_register_follows]) >>
prove_tac[thread_follows_trans])
val exec_inst_ok = store_thm("exec_inst_ok",
``i tid. propagates thread_ok (exec_inst i tid)``,
rw[propagates_def, exec_inst_def, APP_DEF] >> multi_case_tac >> fs[] >> rw[]
val exec_inst_ok_follows = store_thm("exec_inst_follows",
``i tid. thread_ok_follows (exec_inst i tid)``,
rw[exec_inst_def, APP_DEF, thread_ok_follows_def, propagates_def] >>
multi_case_tac >> fs[] >> rw[]
>- (imp_res_tac (ISPEC ``thread_ok`` imp_foldl_propagates) >>
first_x_assum match_mp_tac >> rw[propagates_def] >>
Cases_on `r` >> fs[] >> prove_tac[propagates_def, add_register_ok]) >>
map_every (imp_res_tac o REWRITE_RULE[propagates_def])
[add_register_ok, enqueue_action_ok])
map_every imp_res_tac [
REWRITE_RULE[propagates_def] add_register_ok,
REWRITE_RULE[propagates_def] enqueue_action_ok,
add_register_follows, enqueue_action_follows, foldl_propagates_follows] >>
fs[AND_IMP_INTRO]
>- (pop_assum match_mp_tac >> rw[propagates_def] >| [
Cases_on `r` >> fs[] >> metis_tac[add_register_follows],
Cases_on `x` >> fs[] >> metis_tac[add_register_ok, propagates_def]
]) >>
prove_tac[thread_follows_trans])
val exec_inst_preserves = store_thm("exec_inst_preserves",
``i tid. preserves thread_stack_id (exec_inst i tid)
preserves thread_block_id (exec_inst i tid)``,
preserves thread_next_register (exec_inst i tid)``,
rw[preserves_def, propagates_def, exec_inst_def, APP_DEF] >>
multi_case_tac >> fs[] >> rw[] >> FIRST (
([``thread_stack_id``, ``thread_block_id``] |> map (fn a =>
([``thread_stack_id``, ``thread_next_register``] |> map (fn a =>
imp_res_tac (ISPEC a imp_foldl_preserves) >>
first_x_assum match_mp_tac >> rw[preserves_def, propagates_def] >>
Cases_on `r` >> fs[] >>
......@@ -330,13 +315,13 @@ val const_or_guess_def = Define`
*)
val exec_terminst_def = Define`
exec_terminst (env : environment)
(inst : register terminst)
(inst : num terminst)
(guess : value option)
(stacks : stack list)
(tid : thread_id)
(th : thread)
: ((stack_id # stack) list # thread) or_error =
let fn_name = λn. case n of
let fn_name n = case n of
| INR name => return name
| INL _ => SND <$> (expect guess InvalidStep >>= get_funcref_data) in
let return_stack = lift_left (λ(s, t). ([(t.stack_id, s)], t)) in
......@@ -382,7 +367,7 @@ val exec_terminst_def = Define`
assert (type_of_value param_value = ty)
(TypeMismatch "SWITCH" ty (type_of_value param_value));
next_stack <- update_stack_state current_stack (READY [] <|
normal_dest := case FLOOKUP branches param_value of
normal_dest := case ALOOKUP branches param_value of
| SOME dest => dest
| NONE => default_dest;
exceptional_dest := NONE
......@@ -421,7 +406,7 @@ val exec_terminst_def = Define`
assert (sig = sig') (TypeMismatch "uvm.new_stack function signature"
(FuncRef REF sig) (FuncRef REF sig'));
new_stack <-
let args = GENLIST (λn. %(num_str n)0) (LENGTH sig.arg_types) in
let args = GENLIST I (LENGTH sig.arg_types) in
push_frame env name (ZIP (sig.arg_types, args)) (MAP Var args) <|
frames := [];
next_frame_id := Frame 0
......@@ -442,12 +427,13 @@ val exec_terminst_def = Define`
`
val exec_terminst_follows = store_thm("exec_terminst_follows",
``exec_terminst env i guess s0 tid t0 = OK (s1, t1) thread_follows t0 t1``,
``thread_ok t0 exec_terminst env i guess s0 tid t0 = OK (s1, t1)
thread_follows t0 t1``,
simp[exec_terminst_def, pop_and_resume_stack_def, update_stack_state_def] >>
multi_case_tac >> simp[thread_follows_refl] >> TRY (Cases_on `y0`) >>
fs[] >> rw[] >>
imp_res_tac (resume_stack_follows |> Q.GEN `exec` |> SPEC ``exec_inst``
|> REWRITE_RULE [exec_inst_follows] |> GEN_ALL))
|> REWRITE_RULE [exec_inst_ok_follows] |> GEN_ALL))
val exec_terminst_thread_ok = store_thm("exec_terminst_thread_ok",
``i env guess s tid. propagates thread_ok (liftM SND o exec_terminst env i guess s tid)``,
......@@ -455,7 +441,7 @@ val exec_terminst_thread_ok = store_thm("exec_terminst_thread_ok",
multi_case_tac >> TRY (Cases_on `y0'`) >> fs[] >> rw[] >>
first_x_assum (fn x =>
mp_tac x >> match_mp_tac (ISPEC ``thread_ok`` imp_propagates_snd)) >>
prove_tac[resume_stack_thread_ok, exec_inst_ok])
prove_tac[resume_stack_thread_ok, exec_inst_ok_follows, thread_ok_follows_def])
val exec_terminst_stack_ok = store_thm("exec_terminst_stack_ok",
``EVERY stack_ok s0
......
......@@ -16,7 +16,6 @@ val _ = ParseExtras.tight_equality()
val _ = define_num_newtype("thread_id", "Thread")
val _ = define_num_newtype("stack_id", "Stack")
val _ = define_num_newtype("block_id", "Block")
val _ = define_num_newtype("action_id", "Action")
val _ = Datatype`
......@@ -35,22 +34,14 @@ val _ = type_abbrev("value", ``:(addr, func_name, stack_id, thread_id) gen_value
val _ = type_abbrev("iaddr", ``:addr gen_iaddr``)
val _ = type_abbrev("uvm_error", ``:(addr, func_name) gen_uvm_error``)
val _ = type_abbrev("or_error", ``:α + uvm_error``)
val _ = type_abbrev("register", ``:ssavar # block_id``)
val _ = add_rule {term_name = "%",
fixity = Prefix 780,
pp_elements = [TOK "%"],
paren_style = OnlyIfNecessary,
block_style = (AroundEachPhrase, (PP.CONSISTENT, 0))}
val _ = add_rule {term_name = "#",
fixity = Infixl 770,
pp_elements = [TOK "№"],
paren_style = OnlyIfNecessary,
block_style = (AroundEachPhrase, (PP.CONSISTENT, 0))}
val _ = TeX_notation {hol="%", TeX=("\\%", 1)}
val _ = TeX_notation {hol="№", TeX=("\\#", 1)}
val _ = overload_on("%", ``SSA``)
val _ = overload_on("#", ``(λa b. (a, Block b)) : ssavar -> num -> register``)
val action_id_lt_transitive = store_thm("action_id_lt_transitive",
``transitive action_id_lt``,
......@@ -70,7 +61,7 @@ val _ = Datatype`
val _ = Datatype`
location =
| Register thread_id register
| Register num thread_id
| Memory (thread_id option) action_id ;
input_location =
......
......@@ -12,29 +12,12 @@ open listTheory
open llistTheory
open sortingTheory
open BasicProvers
open DefineUtils
val _ = new_theory "uvmScheduler"
val _ = add_monadsyntax()
val _ = reveal "C" (* The C (flip) combinator is used in this theory *)
(* multi_case_tac is redefined here because importing it from DefineUtils
doesn't work properly for some reason.
*)
val pair_case_tac =
qpat_assum `_ (_: α # β) = _` (fn a =>
let val v = concl a |> lhs |> dest_comb |> #2 in
if pairSyntax.is_pair v then NO_TAC else Cases_on `^v`
end) ORELSE
qpat_assum `_ = _ (_: α # β)` (fn a =>
let val v = concl a |> rhs |> dest_comb |> #2 in
if pairSyntax.is_pair v then NO_TAC else Cases_on `^v`
end)
val multi_case_tac =
REPEAT ((BasicProvers.FULL_CASE_TAC ORELSE pair_case_tac) >> fs[] >> rw[])
(* *** *** *** *)
val _ = Datatype`
sched_step =
| Commit thread_id num
......
......@@ -9,8 +9,9 @@ open DefineUtils
open arithmeticTheory
open combinTheory
open finite_mapTheory
open patriciaTheory
open listTheory
open indexedListsTheory
open optionTheory
open pairTheory
open pred_setTheory
......@@ -26,9 +27,9 @@ val _ = reveal "C" (* The C (flip) combinator is used in this theory *)
val _ = Datatype`