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

Commit 68dd6b4a authored by Adam Nelson's avatar Adam Nelson
Browse files

Scheduler fixes: per-thread addr, free stack memory

- The scheduler now has a per-thread current address, which prevents
  the naïve (exec → dequeue → next thread → next addr) schedule from
  causing a deadlock by never selecting an address used by the current
  thread
- Popping a frame now frees that frame's stack memory
parent cdb06670
......@@ -272,7 +272,7 @@ val memory_stack_alloc_def = Define`
`
val free_stack_def = Define`
free_stack as sid fid =
free_stack sid fid as =
as with stack updated_by delete (stack_id_dest sid frame_id_dest fid)
`
......
......@@ -40,8 +40,8 @@ val _ = Datatype`
next_sid: stack_id;
stacks: stack spt;
memory: memory;
cur_tid: thread_id;
cur_addr: addr
sched_tid: thread_id;
sched_addrs: addr spt;
|>
`
......@@ -51,10 +51,13 @@ val state_ok_def = Define`
sn = stack_id_dest s.next_sid
in wf s.threads
wf s.stacks
wf s.sched_addrs
s.threads LN
s.stacks LN
EVERY (PROD_ALL ($> tn) thread_ok) (toAList s.threads)
EVERY (PROD_ALL ($> sn) stack_ok) (toAList s.stacks)
EVERY (PROD_ALL ($> tn domain s.sched_addrs) thread_ok)
(toAList s.threads)
EVERY (PROD_ALL ($> sn) stack_ok)
(toAList s.stacks)
memory_ok s.memory
`
......@@ -68,24 +71,27 @@ val get_stack_def = Define`
lookup (stack_id_dest sid) state.stacks
`
val sched_addr_def = Define`
sched_addr (st : sched_state) : addr =
option_CASE (lookup (thread_id_dest st.sched_tid) st.sched_addrs)
(Global, 0) I
`
val next_thread_def = Define`
next_thread state : thread_id =
let tids = QSORT $< (MAP FST (toAList state.threads)) in
ThreadID (
case FIND ($> (thread_id_dest state.cur_tid)) tids of
| SOME a => a
| NONE => HD tids)
let tids = QSORT $< (MAP FST (toAList state.threads))
in ThreadID (
option_CASE (FIND ($> (thread_id_dest state.sched_tid)) tids)
(HD tids) I)
`
val next_addr_def = Define`
next_addr state : addr =
let all_addrs = nub (QSORT addr_lt do
th <- toList state.threads;
addrs_of th.sb ++ addrs_of th.ib
od) in
case FIND (C addr_lt state.cur_addr) all_addrs of
| SOME a => a
| NONE => if NULL all_addrs then (Global, 0) else HD all_addrs
next_addr st : addr =
let addrs =
option_CASE (get_thread st.sched_tid st)
[] (λth. nub (QSORT addr_lt (addrs_of th.sb ++ addrs_of th.ib)))
in option_CASE (FIND (C addr_lt (sched_addr st)) addrs)
(if NULL addrs then (Global, 0) else HD addrs) I
`
val new_sched_state_def = Define`
......@@ -115,8 +121,8 @@ val new_sched_state_def = Define`
next_frame := FrameID 1
|> LN;
memory := mem;
cur_tid := ThreadID 0;
cur_addr := (Global, 0)
sched_tid := ThreadID 0;
sched_addrs := insert 0 (Global, 0) LN
|>
od
`
......@@ -212,7 +218,7 @@ val exec_store_def = Define`
(ia, v) <- run_reg_reader rdr (HD sk.frames).regs;
ad <- HD <$> lift_mem_error (get_iaddr_cell_addrs st.memory ia);
return (st with threads updated_by
insert (thread_id_dest st.cur_tid) (enqueue_store (ad, v) th) o
insert (thread_id_dest st.sched_tid) (enqueue_store (ad, v) th) o
map (enqueue_invalidation (ad, v)))
od
`
......@@ -228,7 +234,7 @@ val exec_commit_def = Define`
val exec_reconcile_def = Define`
exec_reconcile (th : thread) (sk : stack) (st : sched_state)
: sched_state or_error option =
SOME (OK (st with threads updated_by insert (thread_id_dest st.cur_tid)
SOME (OK (st with threads updated_by insert (thread_id_dest st.sched_tid)
(th with ib := new_address_space)))
`
......@@ -245,9 +251,11 @@ val exec_command_def = Define`
return (st with stacks updated_by insert (stack_id_dest th.sid) sk')
od
| DoPopStack rvs => do
sk' <- pop_stack st.program rvs sk;
(* TODO: Free stack memory *)
return (st with stacks updated_by insert (stack_id_dest th.sid) sk')
(sk', fr) <- pop_stack st.program rvs sk;
return (st with <|
stacks updated_by insert (stack_id_dest th.sid) sk';
memory updated_by free_stack th.sid fr.id
|>)
od
| DoJump label args => do
sk' <- jump st.program label args NONE sk;
......@@ -277,7 +285,7 @@ val exec_command_def = Define`
val take_step_def = Define`
take_step ExecInst st : sched_state or_error option = do
th <- get_thread st.cur_tid st;
th <- get_thread st.sched_tid st;
case do
sk <- get_stack th.sid st or_fail Impossible "missing stack";
case (HD sk.frames).state of
......@@ -300,26 +308,27 @@ val take_step_def = Define`
| Fail x => SOME (Fail x)
od
take_step NextThread st =
SOME (OK (st with cur_tid := next_thread st))
SOME (OK (st with sched_tid := next_thread st))
take_step NextAddr st =
SOME (OK (st with cur_addr := next_addr st))
SOME (OK (st with sched_addrs updated_by
insert (thread_id_dest st.sched_tid) (next_addr st)))
take_step DequeueStore st = do
th <- get_thread st.cur_tid st;
(sb, v) <- buffer_dequeue th.sb st.cur_addr;
th <- get_thread st.sched_tid st;
(sb, v) <- buffer_dequeue th.sb (sched_addr st);
return do
mem <- lift_mem_error (memory_put st.memory st.cur_addr v);
mem <- lift_mem_error (memory_put st.memory (sched_addr st) v);
return (st with <|
threads updated_by
insert (thread_id_dest st.cur_tid) (th with sb := sb);
insert (thread_id_dest st.sched_tid) (th with sb := sb);
memory := mem
|>)
od
od
take_step DequeueInvalidation st = do
th <- get_thread st.cur_tid st;
(ib, _) <- buffer_dequeue th.ib st.cur_addr;
th <- get_thread st.sched_tid st;
(ib, _) <- buffer_dequeue th.ib (sched_addr st);
return (OK (st with threads updated_by
insert (thread_id_dest st.cur_tid) (th with ib := ib)))
insert (thread_id_dest st.sched_tid) (th with ib := ib)))
od
`
......@@ -759,8 +768,6 @@ val cycle_ltake_mem = store_thm("cycle_ltake_mem",
`0 ≠ LENGTH xs` by metis_tac[LENGTH_NIL] >> fs[])
*)
(* FIXME: This schedule could get stuck in a cycle.
Change the schedule steps to something easier to reason about. *)
val naive_schedule_def = Define`
naive_schedule : sched_step llist =
cycle [ExecInst; DequeueStore; NextAddr; NextThread; DequeueInvalidation]
......
......@@ -298,23 +298,23 @@ val jump_def = Define`
(lbl : num)
(args : value list)
(exc : value option)
(st : stack)
(sk : stack)
: stack or_error =
let fr = HD st.frames in do
assert (¬NULL st.frames) or_fail Impossible "stack underflow";
let fr = HD sk.frames in do
assert (¬NULL sk.frames) or_fail Impossible "stack underflow";
blocks <- FLOOKUP prg fr.fn or_fail UndefBehavior (NoSuchFunction fr.fn);
block <- lookup lbl blocks
or_fail Impossible ("undefined label: " ++ num_to_dec_string lbl);
fr' <- enter_block block args exc fr;
return (st with frames := fr'::TL st.frames)
return (sk with frames := fr'::TL sk.frames)
od
`
val resume_stack_def = Define`
resume_stack (prg : program) (rvs : value resume_values) (st : stack)
resume_stack (prg : program) (rvs : value resume_values) (sk : stack)
: stack or_error =
(assert (¬NULL st.frames) or_fail Impossible "stack underflow") *>
let f = HD st.frames in
(assert (¬NULL sk.frames) or_fail Impossible "stack underflow") *>
let f = HD sk.frames in
case f.state of
| READY tys next => do
(res_args, exc, label, params) <-
......@@ -333,7 +333,7 @@ val resume_stack_def = Define`
return (EL n res_args)
od)
params;
jump prg label args exc st
jump prg label args exc sk
od
| _ => Fail (UndefBehavior (FrameNotReady f.id))
`
......@@ -344,10 +344,10 @@ val push_stack_def = Define`
(sig : funcsig)
(args : value list)
(next : jumps option)
(st : stack)
(sk : stack)
: stack or_error =
let new_frame = <|
id := st.next_frame; fn := fn; regs := LN;
id := sk.next_frame; fn := fn; regs := LN;
state := READY sig.arg_types <|
nor_jump := (0, GENLIST INL (LENGTH args));
exc_jump := NONE
......@@ -356,28 +356,31 @@ val push_stack_def = Define`
resume_stack prg (NOR args) (
case next of
(* SOME = normal call *)
| SOME js => st with <|
| SOME js => sk with <|
frames updated_by (λf.
new_frame::(HD f with state := READY sig.return_types js)::TL f);
next_frame updated_by suc
|>
(* NONE = tail call *)
| NONE => st with <|
| NONE => sk with <|
frames updated_by (λf. new_frame::TL f);
next_frame updated_by suc
|>)
`
val pop_stack_def = Define`
pop_stack (prg : program) (rvs : value resume_values) (st : stack)
: stack or_error = do
assert (¬NULL st.frames) or_fail Impossible "stack underflow";
assert (case (HD st.frames).state of DEAD _ => F | _ => T)
pop_stack (prg : program) (rvs : value resume_values) (sk : stack)
: (stack # frame) or_error = do
assert (¬NULL sk.frames) or_fail Impossible "stack underflow";
assert (case (HD sk.frames).state of DEAD _ => F | _ => T)
or_fail Impossible "pop_stack on dead frame";
if NULL (TL st.frames)
then return (st with frames :=
[HD st.frames with state := DEAD (SOME rvs)])
else resume_stack prg rvs (st with frames updated_by TL)
if NULL (TL sk.frames)
then (let fr = HD sk.frames with state := DEAD (SOME rvs)
in return (sk with frames := [fr], fr))
else do
sk' <- resume_stack prg rvs (sk with frames updated_by TL);
return (sk', HD sk.frames)
od
od
`
......
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