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

Commit 7142aea2 authored by Adam Nelson's avatar Adam Nelson
Browse files

Add NEWTHREAD, SWAPSTACK tests; threading works

parent 29d9e42d
......@@ -14,6 +14,8 @@ sig
val expect_result : term frag list -> term -> thm
val expect_global_value : string -> term frag list -> term -> thm
val take_step : term frag list -> term -> term
val take_steps : term frag list -> term -> term
......
......@@ -49,14 +49,18 @@ struct
fun run_finite_schedule (schedule : term frag list) (state : term) : term =
EVAL(Term(`^state >>= run_finite_schedule` @ parens schedule)) |> concl |> rhs
fun expect_result (expected : term frag list) (actual : term) : thm =
prove(Term(parens expected @ ` = ^actual`), simp[])
fun expect_result (expected : term frag list) (state : term) : thm =
let val actual = EVAL(``^state >>= get_return_values``) |> concl |> rhs
in prove(Term(parens expected @ ` = ^actual`), simp[]) end
fun expect_global_value (name : string) (value : term frag list) (state : term) : thm =
let val actual = EVAL(``^state >>= get_global_value ^(fromMLstring name)``) |> concl |> rhs
in prove(Term(parens value @ ` = ^actual`), simp[]) end
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
......@@ -50,7 +50,7 @@ struct
]
val comminsts = [
"uvm.new_stack", "uvm.current_stack"
"uvm.new_stack", "uvm.current_stack", "uvm.thread_exit"
]
val ty_ssa = mk_type("ssavar", [])
......@@ -111,6 +111,17 @@ struct
| _ => raise ParseError "expected newStackClause (PASS_VALUES or THROW_EXC)"
end
fun parse_cur_stack_clause (env : env_context) (tokens : uir_token list)
: (term * uir_token list) =
let val ty = mk_type("cur_stack_clause", []) in
case tokens of
Word "RET_WITH" :: Type tys :: rest =>
(mk_lift(mk_const("RetWith", ty_list ty_type --> ty),
mk_sequence(parse_type_list env tys, ty_type)), rest)
| Word "KILL_OLD" :: rest => (mk_return(mk_const("KillOld", ty)), rest)
| _ => raise ParseError "expected curStackClause (RET_WITH or KILL_OLD)"
end
fun lhs0 (lhs : uir_token) (inst : string) =
case lhs of
Parens [] => ()
......@@ -332,6 +343,8 @@ struct
("uvm.new_stack", [], [], [s], [f]) => ir_ap("NewStack", [s, f], ty_ci)
| ("uvm.current_stack", [], [], [], []) =>
mk_return(mk_const("CurrentStack", ty_ci))
| ("uvm.thread_exit", [], [], [], []) =>
mk_return(mk_const("ThreadExit", ty_ci))
| _ =>
if exists (fn x => x = name) comminsts then
raise ParseError ("invalid arguments for " ^ name)
......@@ -423,9 +436,28 @@ struct
| Word "WPBRANCH"::_ =>
(* TODO: WPBRANCH *)
raise ParseError "WPBRANCH is not yet implemented"
| Word "SWAPSTACK"::_ =>
(* TODO: SWAPSTACK *)
raise ParseError "SWAPSTACK is not yet implemented"
| Word "SWAPSTACK"::SSA swappee::rest =>
let
val (csc, rest') = parse_cur_stack_clause env rest
val (nsc, rest'') = parse_new_stack_clause env rest'
in
case rest'' of
[Word "EXC", Parens exc] => ir_ap("SwapStack",
[mk_return(mk_list([], ty_ssa)), ssa_var env swappee, csc, nsc, exc_clause exc],
ty_inst)
| _ => raise ParseError "terminating SWAPSTACK must have an EXC clause"
end
| lhs::Eq::Word "SWAPSTACK"::SSA swappee::rest =>
let
val (csc, rest') = parse_cur_stack_clause env rest
val (nsc, rest'') = parse_new_stack_clause env rest'
in
case rest'' of
[Word "EXC", Parens exc] => ir_ap("SwapStack",
[mk_return(lhs_n lhs "SWAPSTACK"), ssa_var env swappee, csc, nsc, exc_clause exc],
ty_inst)
| _ => raise ParseError "terminating SWAPSTACK must have an EXC clause"
end
| Word "COMMINST"::SSA (Global, name)::args =>
let val (ci, rest) = parse_comminst env name args in
case rest of
......@@ -443,7 +475,7 @@ struct
| _ => raise ParseError "terminating COMMINST must have an EXC clause"
end
| _::Eq::_ =>
raise ParseError "assignment is not valid in terminating position"
raise ParseError "assignment not valid for this terminating instruction"
| Word opn::_ =>
if exists (fn x => x = opn) terminsts then
raise ParseError ("invalid arguments for " ^ opn)
......
open HolKernel Parse boolLib bossLib
open uvmSchedulerTheory
open wordsLib
open BundleParser
open EvalUtils
val _ = new_theory "basicThreadOpsTest"
val _ = add_extra_eval_thms()
val spawn_thread_test = load_uir_file "uir/spawn-thread.uir"
|> to_env |> start_at "spawn" `[]`
|> run_schedule `seq_cst_schedule 2`
|> expect_global_value "out" `OK (IntV 8 2w)`
val swapstack_test = load_uir_file "uir/swapstack.uir"
|> to_env |> start_at "sender" `[]`
|> run_schedule `single_thread_seq_cst_schedule`
|> expect_global_value "out" `OK (IntV 8 2w)`
......@@ -89,6 +89,11 @@ val _ =
normal_dest := (BlockLabel "n", [Var %"x"]);
exceptional_dest := SOME (BlockLabel "e", [])
|>``);
assert_parse_terminst("(%x %y) = SWAPSTACK %st RET_WITH <int<8> int<8>> THROW_EXC %e EXC (%n(%x %y))",
``SwapStack [%"x"; %"y"] (Var %"st") (RetWith [Int 8; Int 8]) (ThrowExc (Var %"e"))
<| normal_dest := (BlockLabel "n", [Var %"x"; Var %"y"]);
exceptional_dest := NONE
|>``);
assert_parse_terminst("%x = COMMINST @uvm.new_stack <[@sig]> (%st) EXC (%n(%x))",
``CommInst [%"x"] (NewStack <|arg_types := []; return_types := []|> (Var %"st"))
<| normal_dest := (BlockLabel "n", [Var %"x"]);
......
// Spawns a thread, then writes to a global variable from that thread.
.typedef @i8 = int<8>
.typedef @stack = stackref
.const @two <@i8> = 2
.global @out <@i8>
.funcsig @voidfn = () -> ()
.funcdef @spawn VERSION %v1 <@voidfn> {
%entry():
%stack = COMMINST @uvm.new_stack <[@voidfn]> (@write) EXC (%spawn(%stack))
%spawn(<@stack> %stack):
%th = NEWTHREAD %stack PASS_VALUES <> ()
COMMINST @uvm.thread_exit EXC(%entry())
}
.funcdef @write VERSION %v1 <@voidfn> {
%entry():
%i = GETIREF <@i8> @out
STORE <@i8> %i @two
COMMINST @uvm.thread_exit EXC(%entry())
}
// Basic SWAPSTACK test
.typedef @i8 = int<8>
.typedef @stack = stackref
.const @two <@i8> = 2
.global @out <@i8>
.funcsig @voidfn = () -> ()
.funcsig @i8fn = (@i8) -> ()
.funcdef @sender VERSION %v1 <@voidfn> {
%entry():
%stack = COMMINST @uvm.new_stack <[@i8fn]> (@receiver) EXC (%spawn(%stack))
%spawn(<@stack> %stack):
SWAPSTACK %stack KILL_OLD PASS_VALUES <@i8> (@two) EXC (%entry())
}
.funcdef @receiver VERSION %v1 <@i8fn> {
%entry(<@i8> %arg):
%i = GETIREF <@i8> @out
STORE <@i8> %i %arg
COMMINST @uvm.thread_exit EXC(%entry())
}
......@@ -341,8 +341,8 @@ val _ = Datatype`
| SwapStack
(σ list)
(σ or_const) (* swappee - stackref *)
(σ or_const new_stack_clause)
cur_stack_clause
(σ or_const new_stack_clause)
(σ resumption_data)
| CommInst
(σ list)
......@@ -375,6 +375,7 @@ val _ = Datatype`
comminst =
| NewStack funcsig (σ or_const)
| CurrentStack
| ThreadExit
`
val comminst_return_types_def = Define`
......@@ -458,6 +459,7 @@ val map_inst_def = Define`
val map_comminst_def = Define`
map_comminst f (NewStack sig fref) = NewStack sig (f <$> fref)
map_comminst f CurrentStack = CurrentStack
map_comminst f ThreadExit = ThreadExit
`
val map_terminst_def = Define`
......@@ -480,8 +482,8 @@ val map_terminst_def = Define`
| 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)
| SwapStack vs v nsc csc rd =>
SwapStack (MAP f vs) (f <$> v) (map_new_stack_clause f nsc) csc (map_rd rd)
| SwapStack vs v csc nsc rd =>
SwapStack (MAP f vs) (f <$> v) csc (map_new_stack_clause f nsc) (map_rd rd)
| CommInst vs ci rd => CommInst (MAP f vs) (map_comminst f ci) (map_rd rd)
| ExcClause inst rd => ExcClause (map_inst f inst) (map_rd rd)
`
......@@ -543,6 +545,7 @@ val inst_all_vars_def = Define`inst_all_vars i = let (a, b) = inst_vars i in a
val comminst_vars_def = Define`
comminst_vars (NewStack _ fref) = left_set fref
comminst_vars CurrentStack =
comminst_vars ThreadExit =
`
(* Given a terminal instruction, returns a pair of sets (input variables, passed
......@@ -577,7 +580,7 @@ val terminst_vars_def = Define`
| 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
| SwapStack vs id nsc _ rd =>
| 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
......
......@@ -322,7 +322,7 @@ val exec_terminst_def = Define`
|>);
return_stack (resume_stack next_stack (NOR []) exec_inst th)
od
| SwapStack vs sr nsc csc rd => do
| SwapStack vs sr csc nsc rd => do
stack_ref <- const_or_guess sr guess;
sid <- get_stackref_id stack_ref;
last_stack <- get_stack th.stack_id stacks;
......@@ -367,6 +367,9 @@ val exec_terminst_def = Define`
| CurrentStack =>
return_stack (resume_stack next_stack
(NOR [pure (StackRefV (SOME current_stack.id))]) exec_inst th)
| ThreadExit =>
return ([current_stack with frames updated_by
MAP (λf. f with state := DEAD NONE)], th)
od
| _ => Fail (NotImplemented "not all terminsts are implemented")
(* TODO: Watchpoint, WPBranch, ExcClause *)
......
......@@ -200,6 +200,7 @@ val take_step_def = Define`
| Message _ _ (DoNewThread s vs) => [(s, vs)]
| _ => [])) in
let threads = GENLIST (C get_thread state) (LENGTH new_threads) in
if LENGTH new_threads tid then Fail InvalidStep else
let (s, vs) = EL tid new_threads in do
known_sid <- resolve_symbolic state.memory s;
sid <- case known_sid of
......@@ -225,11 +226,18 @@ val take_steps_def = Define`
val has_terminated_def = Define`
has_terminated (state : sched_state) : bool
case thread_current_frame_state (Thread 0) state of
| SOME (DEAD (SOME (NOR vs))) => EVERY (resolvable_in state.memory) vs
| SOME (DEAD (SOME (EXC v))) => resolvable_in state.memory v
| SOME (DEAD NONE) => T
| _ => F
let n_threads = (state.memory.committed
:> FILTER (λm. case m of Message _ _ (DoNewThread _ _) => T | _ => F)
:> LENGTH) in
n_threads LENGTH state.threads
EVERY IS_SOME (TAKE n_threads state.threads)
EVERY (λth. NULL th.outbox (
case thread_current_frame_state th.tid state of
| SOME (DEAD (SOME (NOR vs))) => EVERY (resolvable_in state.memory) vs
| SOME (DEAD (SOME (EXC v))) => resolvable_in state.memory v
| SOME (DEAD NONE) => T
| _ => F
)) (MAP THE (FILTER IS_SOME state.threads))
`
val get_return_values_def = Define`
......@@ -244,24 +252,44 @@ val get_return_values_def = Define`
| _ => Fail (InvalidState "schedule exhausted")
`
val get_global_value_def = Define`
get_global_value name state = (
let id = action_id_suc (FOLDR (λm a.
case m of Message _ a' _ => if a a' then a' else a)
(Action 0) state.memory.committed) in
let reg = Register (Thread (LENGTH state.threads)) (%"result"#0) in
state with memory updated_by (λm. m with <|
resolved updated_by C $|+ (reg, return (IRefV REF (SOME <|
base := GlobalAddr (Global name);
offsets := [];
base_ty := Void;
ty := Void
|>)));
committed updated_by CONS
(Message NONE id (DoLoad reg NOT_ATOMIC))
|>)
:> resolve_once
:> λs. resolve_symbolic s.memory (await (Memory NONE id)))
>>= C expect (InvalidState (name ++ " is undefined"))
`
val run_finite_schedule_def = Define`
run_finite_schedule (schedule : sched_step list)
(state : sched_state)
: value resume_values or_error =
(resolve_all <$> FOLDL
: 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)
>>= get_return_values
(OK state) schedule
`
val run_schedule_def = Define`
run_schedule (schedule : sched_step llist)
(state : sched_state)
: value resume_values or_error =
(resolve_all <$> SND (WHILE
: sched_state or_error =
resolve_all <$> SND (WHILE
(λ(_, m). case m of
| OK state => ¬has_terminated state
| Fail _ => F)
......@@ -271,8 +299,7 @@ val run_schedule_def = Define`
| Fail InvalidStep => state
| res => resolve_all <$> res)
| NONE => (steps, Fail (InvalidState "schedule exhausted")))
(schedule, OK state)))
>>= get_return_values
(schedule, OK state))
`
(* A schedule is fair iff, at any point in the schedule, all possible steps
......
......@@ -269,7 +269,7 @@ val iaddr_overlaps_def = Define`
iaddr_overlaps (a : α gen_iaddr) (b : α gen_iaddr) : bool
let is_suffix = λxs ys.
LENGTH xs LENGTH ys (xs = DROP (LENGTH ys - LENGTH xs) ys) in
(a.base = b.base) (a.base_ty = b.base_ty)
(a.base = b.base) (* (a.base_ty = b.base_ty) ∧ *)
(is_suffix a.offsets b.offsets is_suffix b.offsets a.offsets)
`
......
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