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

Commit 29a034a9 authored by Adam Nelson's avatar Adam Nelson
Browse files

WIP optimization proofs; lots of changes

Factorial test is currently broken, but everything compiles (with cheats).
parent a52438d8
......@@ -9,7 +9,7 @@ val _ = app prefix_op ["%", "∁", "⍽", "✔", "✘"]
val _ = set_fixity "≺" (Infix(NONASSOC, 450))
val _ = set_fixity "≼" (Infix(NONASSOC, 450))
val _ = overload_on("∁", ``COMPL``)
val _ = Unicode.unicode_version{tmnm="COMPL", u="∁"}
(* Unicode ∷ disabled because it prevented [] list syntax from working... *)
(* val _ = Unicode.unicode_version{tmnm="CONS", u="∷"} *)
......
......@@ -9,6 +9,7 @@ open extraTactics
open alistTheory
open finite_mapTheory
open listTheory
open monadsyntax
val _ = new_theory "uvmIR"
......@@ -493,7 +494,7 @@ val expr_types_def = Define`
val inst_vars_def = Define`
inst_vars (Assign vs e) = (expr_vars e >>= var_list, nub vs)
inst_vars (Load v _ _ src _) = ([src], [v])
inst_vars (Store src _ _ dst _) = (var_list src, [dst])
inst_vars (Store src _ _ dst _) = (var_list src ++ [dst], [])
inst_vars (CmpXchg v1 v2 _ _ _ _ _ loc exp des) =
(nub (loc::var_list exp ++ var_list des), nub [v1; v2])
inst_vars (AtomicRMW v _ _ _ _ loc opnd) = (nub (loc::var_list opnd), [v])
......@@ -544,13 +545,8 @@ val comminst_types_def = Define`
`
(* Given a terminating instruction, returns a pair of lists (input variables,
passed variables). The union of these lists is the list of all variables
output 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
to determine the outcome of the instruction, whereas "passed variables" are
variables whose values are passed to another block or function without being
read.
*)
val terminst_vars_def = Define`
terminst_vars (inst : terminst) : ssavar list # ssavar list =
......@@ -559,29 +555,34 @@ val terminst_vars_def = Define`
dest_vars rd.normal_dest ++
option_CASE rd.exceptional_dest [] dest_vars in
case inst of
| Ret vals => [], nub (vals >>= var_list)
| Throw v => [], nub (var_list v)
| Ret vals => nub (vals >>= var_list), []
| Throw v => nub (var_list v), []
| Call vs cd rd =>
left_list cd.name,
nub (vs ++ (cd.args >>= var_list) ++ rd_vars rd)
| TailCall cd => left_list cd.name, nub (cd.args >>= var_list)
| Branch1 dst => [], nub (dest_vars dst)
| Branch2 cond dst1 dst2 => var_list cond, nub (dest_vars dst1 ++ dest_vars dst2)
nub (left_list cd.name ++ cd.args >>= var_list ++ rd_vars rd),
nub vs
| TailCall cd => nub (left_list cd.name ++ cd.args >>= var_list), []
| Branch1 dst => nub (dest_vars dst), []
| Branch2 cond dst1 dst2 =>
nub (var_list cond ++ dest_vars dst1 ++ dest_vars dst2),
[]
| Switch _ cond def_dst branches =>
var_list cond,
nub (dest_vars def_dst ++ (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)
nub (var_list cond ++ dest_vars def_dst ++ 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 =>
var_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)
nub (var_list id ++ new_stack_clause_vars nsc ++ rd_vars rd),
nub vs
| CommInst vs ci rd => nub (comminst_vars ci ++ rd_vars rd), nub vs
| ExcClause inst rd =>
nub (inst_input_vars inst ++ rd_vars rd),
inst_output_vars inst
`
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_output_vars_def = Define`terminst_output_vars i = SND (terminst_vars i)`
val terminst_all_vars_def = Define`
terminst_all_vars i = let (a, b) = terminst_vars i in nub (a ++ b)
......@@ -599,6 +600,45 @@ val terminst_types_def = Define`
terminst_types _ = []
`
(* An instruction is well-formed (OK) if
- All output variables are distinct
- For Assign instructions, the number of output variables matches the number
of return values
- For NewHybrid/AllocaHybrid, the types are valid
*)
val inst_ok_def = Define`
inst_ok (Assign vs e) =
(LENGTH vs = LENGTH (expr_types e) ALL_DISTINCT vs)
inst_ok (CmpXchg v1 v2 _ _ _ _ _ _ _ _) = (v1 v2)
inst_ok (New _ (Hybrid _ _)) = F
inst_ok (New _ _) = T
inst_ok (Alloca _ (Hybrid _ _)) = F
inst_ok (Alloca _ _) = T
inst_ok (NewHybrid _ (Hybrid _ _) (Int _) _) = T
inst_ok (NewHybrid _ _ _ _) = F
inst_ok (AllocaHybrid _ (Hybrid _ _) (Int _) _) = T
inst_ok (AllocaHybrid _ _ _ _) = F
inst_ok _ = T
`
val terminst_ok_def = Define`
terminst_ok (Call vs cd _) = (
LENGTH cd.args = LENGTH cd.signature.arg_types
LENGTH vs = LENGTH cd.signature.return_types
ALL_DISTINCT vs)
terminst_ok (TailCall cd) = (
LENGTH cd.args = LENGTH cd.signature.arg_types)
terminst_ok (SwapStack vs _ KillOld _ _) = ALL_DISTINCT vs
terminst_ok (SwapStack vs _ (RetWith tys) _ _) = (
ALL_DISTINCT vs
LENGTH vs = LENGTH tys)
terminst_ok (CommInst vs ci _) = (
ALL_DISTINCT vs
LENGTH vs = LENGTH (comminst_types ci))
terminst_ok (ExcClause i _) = inst_ok i
terminst_ok _ = T
`
(* A basic block (see the spec)
https://github.com/microvm/microvm-spec/blob/master/uvm-ir.rest#function-body
*)
......@@ -612,22 +652,79 @@ val _ = Datatype`
|>
`
val block_arg_types_def = Define`
block_arg_types (block : bblock) : (ssavar # uvm_type) list =
block.args ++
option_CASE block.exc [] (λe. [(e, Ref (Type Void))])
`
(* A basic block is well-formed (OK) if
- All instructions are OK
- Every SSA variable is assigned only once
- Every SSA variable is assigned before it is read
*)
val block_ok_def = Define`
block_ok (block : bblock)
let args = MAP FST (block_arg_types block) in
EVERY inst_ok block.body
terminst_ok block.exit
ALL_DISTINCT (args ++ block.body >>= inst_output_vars ++
terminst_output_vars block.exit)
(i. i LENGTH block.body
EVERY (λv. MEM v (args ++ TAKE i block.body >>= inst_output_vars))
(inst_input_vars (EL i block.body)))
EVERY (λv. MEM v (args ++ block.body >>= inst_output_vars))
(terminst_input_vars block.exit)
`
val block_vars_def = Define`
block_vars (block : bblock) : ssavar list =
nub (MAP FST block.args ++
option_CASE block.exc [] return ++
(block.body >>= inst_all_vars) ++
nub (MAP FST (block_arg_types block) ++
block.body >>= inst_output_vars ++
terminst_all_vars block.exit ++
block.keepalives)
`
val block_types_def = Define`
block_types (block : bblock) : (ssavar # uvm_type) list =
block.args ++
option_CASE block.exc [] (λe. [(e, Ref (Type Void))]) ++
(block.body >>= inst_types) ++
terminst_types block.exit
`
block_types (blk : bblock) : (ssavar # uvm_type) list =
block_arg_types blk ++ blk.body >>= inst_types ++ terminst_types blk.exit
`
val inst_types_output_vars = store_thm("inst_types_output_vars",
``i x. inst_ok i
(MEM x (MAP FST (inst_types i)) MEM x (inst_output_vars i))``,
Cases >>
rw[inst_ok_def, inst_types_def, inst_output_vars_def, inst_vars_def, MAP_ZIP])
val inst_types_output_vars_bind = store_thm("inst_types_output_vars_bind",
``is x. EVERY inst_ok is
(MEM x (MAP FST (is >>= inst_types))
MEM x (is >>= inst_output_vars))``,
Induct >> rw[] >> Cases_on `MEM x (is >>= inst_output_vars)` >>
simp[inst_types_output_vars])
val inst_ok_inst_types_distinct = store_thm("inst_ok_inst_types_distinct",
``i. inst_ok i ALL_DISTINCT (MAP FST (inst_types i))``,
Cases >> rw[inst_ok_def, inst_types_def, MAP_ZIP])
val block_ok_block_types_distinct = store_thm("block_ok_block_types_distinct",
``b. block_ok b ALL_DISTINCT (MAP FST (block_types b))``,
rw[block_ok_def, block_arg_types_def, block_types_def] >>
rw[ALL_DISTINCT_APPEND] >> BasicProvers.every_case_tac >>
fs[ALL_DISTINCT_APPEND, inst_types_output_vars_bind]
>- prove_tac[] >>
TRY (qmatch_assum_rename_tac `ALL_DISTINCT (body >>= inst_output_vars)` >>
qpat_x_assum `ALL_DISTINCT (_ _ inst_output_vars)` mp_tac >>
qpat_x_assum `EVERY inst_ok _` mp_tac >> POP_ASSUM_LIST (K ALL_TAC) >>
Induct_on `body` >- rw[] >> fs[ALL_DISTINCT_APPEND] >> Cases_on `h` >>
fs[inst_ok_def, inst_types_def, inst_output_vars_def, inst_vars_def] >>
rw[] >> fs[] >> rfs[MAP_ZIP, inst_types_output_vars_bind]) >>
Cases_on `b.exit` >>
fs[terminst_types_def, terminst_output_vars_def, terminst_vars_def,
terminst_ok_def, MAP_ZIP, inst_ok_inst_types_distinct,
inst_types_output_vars] >>
TRY (Cases_on `c` >> fs[terminst_types_def, terminst_ok_def, MAP_ZIP]) >>
prove_tac[inst_types_output_vars_bind])
val _ = Datatype`
function = <|
......
This diff is collapsed.
......@@ -438,6 +438,36 @@ val mem_region_set_value_ok = store_thm("mem_region_set_value_ok",
multi_case_tac >> res_tac >> fs[mem_cell_ok_def] >>
first_x_assum(fn x => mp_tac x >> match_mp_tac LIST_REL_mono) >> rw[])
val mem_region_set_value_foldr = store_thm("mem_region_set_value_foldr",
``rs m1 m2 m1' m2'.
(∀r. lookup r m1 = lookup r m2)
FOLDR (λr s. s >>= (λ(r,v) rs. mem_region_set_value r v rs) r) (OK m1) rs = OK m1'
FOLDR (λr s. s >>= (λ(r,v) rs. mem_region_set_value r v rs) r) (OK m2) rs = OK m2'
r. lookup r m1' = lookup r m2'``,
Induct >> rw[] >> fs[UNCURRY] >>
REPEAT (qpat_x_assum `mem_region_set_value _ _ _ = _`
(assume_tac o ONCE_REWRITE_RULE[mem_region_set_value_def])) >>
fs[UNCURRY] >> rw[lookup_insert] >> res_tac >| [fs[], rfs[]])
val mem_region_set_value_foldr_fail = store_thm("mem_region_set_value_foldr_fail",
``rs m1 m2 e.
(∀r. lookup r m1 = lookup r m2)
FOLDR (λr s. s >>= (λ(r,v) rs. mem_region_set_value r v rs) r) (OK m1) rs = Fail e
FOLDR (λr s. s >>= (λ(r,v) rs. mem_region_set_value r v rs) r) (OK m2) rs = Fail e``,
Induct >> rw[] >> Cases_on `h` >> fs[] >>
ONCE_REWRITE_TAC[bind_left_case] >>
pop_assum (assume_tac o ONCE_REWRITE_RULE[bind_left_case]) >> multi_case_tac >>
TRY (qpat_x_assum `mem_region_set_value _ _ _ = _`
(assume_tac o ONCE_REWRITE_RULE[mem_region_set_value_def])) >>
ONCE_REWRITE_TAC[mem_region_set_value_def] >> fs[] >| [
`lookup q x' = lookup q x` by prove_tac[mem_region_set_value_foldr] >>
fs[] >> Cases_on `lookup q x` >> fs[UNCURRY] >>
Cases_on `type_of r = HD (FST (SND x''))` >> fs[],
res_tac >> fs[],
`r. lookup r m2 = lookup r m1` by simp[] >> res_tac >> fs[],
res_tac >> fs[]
])
(*
val new_mem_cells_ok = store_thm("new_mem_cells_ok",
``∀sz ty f n n' cells.
......
This diff is collapsed.
......@@ -109,7 +109,6 @@ val new_sched_state_def = Define`
frames := [<|
id := FrameID 0;
fn := main;
regs := LN;
state := READY func.signature.arg_types <|
nor_jump := (0, GENLIST INL (LENGTH func.signature.arg_types));
exc_jump := NONE
......@@ -179,40 +178,48 @@ val start_with_args_def = Define`
od
`
val run_reg_reader_stack_def = Define`
run_reg_reader_stack (r : α or_error reg_reader) (sk : stack) : α or_error =
(assert (¬NULL sk.frames) or_fail Impossible "stack underflow") *>
case (HD sk.frames).state of
| ACTIVE _ regs => join (run_reg_reader r regs)
| _ => Fail (Impossible "exec on inactive stack")
`
val exec_non_memory_action_def = Define`
exec_non_memory_action (rdr : (num, value) alist reg_reader)
exec_non_memory_action (rdr : (num, value) alist or_error reg_reader)
(th : thread)
(sk : stack)
(st : sched_state)
: sched_state or_error option = SOME do
rs <- run_reg_reader rdr (HD sk.frames).regs;
sk' <- FOLDL (λs r. s >>= set_register r) (OK sk) rs;
rs <- run_reg_reader_stack rdr sk;
sk' <- set_registers rs sk;
return (st with stacks updated_by insert (stack_id_dest th.sid) sk')
od
`
val exec_load_def = Define`
exec_load (rdr : iaddr reg_reader)
exec_load (rdr : iaddr or_error reg_reader)
(dst : num)
(th : thread)
(sk : stack)
(st : sched_state)
: sched_state or_error option = SOME do
ia <- run_reg_reader rdr (HD sk.frames).regs;
ia <- run_reg_reader_stack rdr sk;
ad <- HD <$> lift_mem_error (get_iaddr_cell_addrs st.memory ia);
ld <- lift_mem_error (memory_load st.memory th.sb th.ib ad);
sk' <- set_register (dst, ld) sk;
sk' <- set_registers [(dst, ld)] sk;
return (st with stacks updated_by insert (stack_id_dest th.sid) sk')
od
`
val exec_store_def = Define`
exec_store (rdr : (iaddr # value) reg_reader)
exec_store (rdr : (iaddr # value) or_error reg_reader)
(th : thread)
(sk : stack)
(st : sched_state)
: sched_state or_error option = SOME do
(ia, v) <- run_reg_reader rdr (HD sk.frames).regs;
(ia, v) <- run_reg_reader_stack rdr sk;
ad <- HD <$> lift_mem_error (get_iaddr_cell_addrs st.memory ia);
return (st with threads updated_by
insert (thread_id_dest st.sched_tid) (enqueue_store (ad, v) th) o
......@@ -236,12 +243,12 @@ val exec_reconcile_def = Define`
`
val exec_command_def = Define`
exec_command (rdr : command reg_reader)
exec_command (rdr : command or_error reg_reader)
(th : thread)
(sk : stack)
(st : sched_state)
: sched_state or_error option = SOME do
cmd <- run_reg_reader rdr (HD sk.frames).regs;
cmd <- run_reg_reader_stack rdr sk;
case cmd of
| DoPushStack fn sig args next => do
sk' <- push_stack st.program fn sig args next sk;
......@@ -260,7 +267,7 @@ val exec_command_def = Define`
od
| DoHeapAlloc ty sz dst => do
(mem, ad) <- memory_heap_alloc st.memory sz ty;
sk' <- set_register (dst, RefV ty (SOME ad)) sk;
sk' <- set_registers [(dst, RefV ty (SOME ad))] sk;
return (st with <|
stacks updated_by insert (stack_id_dest th.sid) sk';
memory := mem
......@@ -268,7 +275,7 @@ val exec_command_def = Define`
od
| DoStackAlloc ty sz dst => do
(mem, ad) <- memory_stack_alloc st.memory th.sid (HD sk.frames).id sz ty;
sk' <- set_register (dst, RefV ty (SOME ad)) sk;
sk' <- set_registers [(dst, RefV ty (SOME ad))] sk;
return (st with <|
stacks updated_by insert (stack_id_dest th.sid) sk';
memory := mem
......@@ -286,10 +293,10 @@ val take_step_def = Define`
case do
sk <- get_stack th.sid st or_fail Impossible "missing stack";
case (HD sk.frames).state of
| ACTIVE (opn::rest) =>
| ACTIVE (opn::rest) regs =>
let
sk = sk with frames updated_by λf.
(HD f with state := ACTIVE rest)::TL f;
(HD f with state := ACTIVE rest regs)::TL f;
st = st with stacks updated_by insert (stack_id_dest th.sid) sk;
step = case opn of
| Nm rdr => exec_non_memory_action rdr
......@@ -545,25 +552,172 @@ val schedule_valid_inter = store_thm("schedule_valid_inter",
rw[schedule_valid_def, monadsTheory.merge_left_def] >> RES_TAC >>
multi_case_tac >> rw[IN_APP] >> rfs[] >> rw[])
val has_thread_with_frame_def = Define`
has_thread_with_frame tid P st
th sk. get_thread tid st = SOME th
get_stack th.sid st = SOME sk
¬NULL sk.frames
P (HD sk.frames)
`
val (advances_pc_by_rules, advances_pc_by_ind, advances_pc_by_cases) = Hol_reln`
(st tid. advances_pc_by 0 [] st tid)
(st st' n x xs tid.
try_step x st = OK st'
advances_pc_by n xs st' tid
advances_pc_by (
if (th sk sk' opns.
step = ExecInst
st.sched_tid = tid
get_thread tid st = SOME th
get_stack th.sid st = SOME sk
get_stack th.sid st' = SOME sk'
(HD sk.frames).state = ACTIVE opns
(HD sk'.frames).state = ACTIVE (TL opns)
(MAP frame_id sk.frames = MAP frame_id sk'.frames))
then SUC n else n
) (x::xs) st' tid)
advances_pc_by (if (x = ExecInst st.sched_tid = tid st st')
then SUC n else n) (x::xs) st tid)
`
val advances_pc_by_0_tl = store_thm("advances_pc_by_0_tl",
``sc0 sc st st' tid.
advances_pc_by 0 (sc0::sc) st tid
try_step sc0 st = OK st'
advances_pc_by 0 sc st' tid``,
rw[] >> rw_assums_once[advances_pc_by_cases] >> fs[] >> CASE_TAC >> fs[])
val advances_pc_by_le = store_thm("advances_pc_by_le",
``n sc0 sc st st' tid.
advances_pc_by n (sc0::sc) st tid
try_step sc0 st = OK st'
n'. n' n advances_pc_by n' sc st' tid``,
rw[] >> rw_assums_once[advances_pc_by_cases] >> fs[] >> CASE_TAC >> fs[]
>- (qexists_tac `n'` >> simp[]) >> prove_tac[LESS_OR_EQ])
(*
val advances_pc_by_le_append = store_thm("advances_pc_by_le_append",
`` ``
)
val advances_pc_by_ACTIVE = store_thm("advances_pc_by_ACTIVE",
``∀sc st st' tid o0 os.
opns_ok (o0::os)
∧ advances_pc_by 1 sc st tid
∧ has_thread_with_frame tid (λf. f.state = ACTIVE (o0::os)) st
∧ run_finite_schedule sc st = OK st'
⇒ has_thread_with_frame tid (λf. f.state = ACTIVE os) st'``
)
val has_thread_with_frame_advances_pc_by_0 = store_thm(
"has_thread_with_frame_advances_pc_by_0",
``∀sc st st' tid P.
advances_pc_by 0 sc st tid
∧ has_thread_with_frame tid P st
∧ run_finite_schedule sc st = OK st'
⇒ has_thread_with_frame tid P st'``,
Induct >> rw[] >> fs[run_finite_schedule_def, has_thread_with_frame_def] >>
imp_res_tac advances_pc_by_0_tl >> first_x_assum match_mp_tac >>
Cases_on `try_step h st` >> rw[] >> fs[foldl_fail] >> qexists_tac `x` >>
rw[] >> fs[try_step_def] >> multi_case_tac >> Cases_on `h` >| [
(* ExecInst *)
POP_ASSUM_LIST (map_every assume_tac) (* reverse argument list *) >>
pop_assum (assume_tac o ONCE_REWRITE_RULE [advances_pc_by_cases]) >>
rfs[COND_RAND, try_step_def] >> rw[] >> multi_case_tac >>
fs[take_step_def] >> multi_case_tac >>
rfs[exec_non_memory_action_def, exec_load_def, exec_store_def,
exec_commit_def, exec_reconcile_def, exec_command_def] >>
TRY (map_every qexists_tac [`th`, `sk`] >> fs[get_thread_def, get_stack_def] >>
multi_case_tac >> rw[lookup_insert] >> NO_TAC)
>> FIRST [
map_every (fn q => qpat_assum q mp_tac)
[`FOLDL _ _ rs = _`, `¬NULL sk.frames`] >>
POP_ASSUM_LIST (K ALL_TAC) >> map_every qid_spec_tac [`sk'`, `rs`] >>
listLib.SNOC_INDUCT_TAC >> rw[FOLDL_SNOC] >> fs[] >> Cases_on `x` >>
fs[set_register_def] >> multi_case_tac >> NO_TAC,
map_every (fn q => qpat_assum q mp_tac)
[`FOLDL _ _ rs = _`, `P (HD sk.frames)`] >>
POP_ASSUM_LIST (K ALL_TAC) >> map_every qid_spec_tac [`sk'`, `rs`] >>
listLib.SNOC_INDUCT_TAC >> rw[FOLDL_SNOC]
]
BasicProvers.every_case_t
>| [
(* st.sched_tid = tid *)
fs[has_thread_with_frame_def] >> rfs[] >> rw[] >>
spose_not_then (K all_tac) >> pop_assum mp_tac >> simp[] >>
map_every qexists_tac [`th`, `sk`] >> rw[] >>
rfs[take_step_def] >> multi_case_tac >>
rfs[exec_non_memory_action_def, exec_load_def, exec_store_def,
exec_commit_def, exec_reconcile_def, exec_command_def,
get_thread_def] >> rw[] >| [
(* Nm *)
rfs[exec_non_memory_action_def] >>
map_every qexists_tac [`th`, `sk'`] >>
fs[get_thread_def, get_stack_def] >> rw[] >> fs[lookup_insert] >| [
map_every (fn q => qpat_assum q mp_tac)
[`FOLDL _ _ rs = _`, `¬NULL sk.frames`] >>
POP_ASSUM_LIST (K ALL_TAC) >> map_every qid_spec_tac [`sk'`, `rs`] >>
listLib.SNOC_INDUCT_TAC >> rw[FOLDL_SNOC] >> fs[] >> Cases_on `x` >>
fs[set_register_def] >> multi_case_tac,
map_every (fn q => qpat_assum q mp_tac)
[`FOLDL _ _ rs = _`, `P (HD sk.frames)`] >>
]
Induct_on `rs`
]
rfs[]
]
rw_assums_once[advances_pc_by_cases]
]
TRY (res_tac >> NO_TAC) >> rw[] >> fs[has_thread_with_frame_def] >>
pop_assum mp_tac >> rw_assums_once[advances_pc_by_cases] >>
fs[] >> multi_case_tac >> Cases_on `h`
Cases_on `x` >| [
`has_thread_with_frame tid P x' ∧
advances_pc_by 0 sc x' tid` suffices_by prove_tac[] >> rw[] >| [
pop_assum mp_tac >> rw_assums_once[advances_pc_by_cases] >>
fs[COND_RAND, try_step_def] >> rw[]
Cases_on `h` >> fs[has_thread_with_frame_def, take_step_def] >| [
Cases_on `st''.sched_tid = tid` >| [
]
fs[exec_non_memory_action_def, exec_load_def, exec_store_def,
exec_commit_def, exec_reconcile_def, exec_command_def,
get_thread_def]
]
multi_case_tac >>
(* Case 1: Step fails, returns NONE *)
imp_reprove_tac[],
(* Case 2: State has already terminated *)
imp_res_tac advances_pc_by_0_tl >> prove_tac[],
(* Case 3: Normal execution, state has not terminated *)
]
ntac 2 (pop_assum mp_tac) >> >> rw[] >>
multi_case_tac >> Cases_on `h = ExecInst` >>
Cases_on `st''.sched_tid = tid` >> fs[try_step_def, run_finite_schedule_def] >>
multi_case_tac
]
val advances_pc_by_0_append = store_thm("advances_pc_by_0_append",
``∀sc1 sc2 st st' tid.
advances_pc_by 0 (sc1 ++ sc2) st tid
∧ run_finite_schedule sc1 st = OK st'
⇒ advances_pc_by 0 sc1 st tid
∧ advances_pc_by 0 sc2 st' tid``,
rw[run_finite_schedule_def] >| [
pop_assum mp_tac >> qid_spec_tac `st'` >> Induct_on `sc1` >> rw[] >>
fs[Once advances_pc_by_cases] >> multi_case_tac >>
map_every qexists_tac [`DequeueStore`, `st''`, `0`] >> multi_case_tac >>
Cases_on `sc1` >> fs[advances_pc_by_rules] >> first_x_assum match_mp_tac
]
*)
(*
val finite_schedule_valid_state_ok = store_thm("finite_schedule_valid_state_ok",
``∀st sc. finite_schedule_valid state_ok st sc``,
......
......@@ -38,8 +38,16 @@ val _ = Datatype`
val _ = Datatype`
frame_state =
(* READY = waiting to be resumed
Arguments: parameter types, normal/exceptional jumps *)
| READY (uvm_type list) jumps
| ACTIVE (opn list)
(* ACTIVE = currently running
Arguments: upcoming opns, registers *)
| ACTIVE (opn list) mem_region
(* DEAD = top-level function returned, or uvm.thread_exit
Argument: return values of top-level function, if any *)
| DEAD (value resume_values option)
`
......@@ -47,7 +55,6 @@ val _ = Datatype`
frame = <|
id: frame_id;
fn: func_name;
regs: mem_region;
state: frame_state
|>
`
......@@ -61,14 +68,15 @@ val _ = Datatype`
val frame_ok_def = Define`
frame_ok (f : frame)
mem_region_ok f.regs
opns regs. f.state = ACTIVE opns regs
opns_ok opns mem_region_ok regs
`
val stack_ok_def = Define`
stack_ok (s : stack)
¬NULL s.frames
EVERY (λf. frame_ok f (f.id s.next_frame)) s.frames
EVERY (λ</