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

Commit 734debc4 authored by Adam Nelson's avatar Adam Nelson
Browse files

Prove invariants for the entire scheduler

parent c07daecc
......@@ -271,6 +271,22 @@ val exec_inst_follows = store_thm("exec_inst_follows",
rw[] >> fs[] >>
metis_tac[enqueue_action_follows, add_register_follows, thread_follows_trans])
val exec_inst_ok = store_thm("exec_inst_ok",
``i. propagates thread_ok (exec_inst i)``,
rw[propagates_def, exec_inst_def, APP_DEF] >> Cases_on `y0` >>
`thread_ok q` suffices_by
(Cases_on `r` >> fs[] >> metis_tac[enqueue_action_ok, propagates_def]) >>
Cases_on `i` >> fs[]
>- (Q.MATCH_ASSUM_ABBREV_TAC
`FOLDL (λs r. s >>= add_return_value r) (OK a) numbered = OK q` >>
`propagates thread_ok (λa. FOLDL (λs r. s >>= add_return_value r) (OK a) numbered)`
suffices_by (rw[propagates_def] >> metis_tac[]) >>
`r. propagates thread_ok (add_return_value r)`
suffices_by metis_tac[foldl_propagates] >>
Q.UNABBREV_TAC `add_return_value` >> rw[propagates_def] >> Cases_on `r'` >>
fs[] >> metis_tac[add_register_ok, propagates_def])
>> metis_tac[add_register_ok, propagates_def])
val const_or_guess_def = Define`
const_or_guess (Const c) _ = return c
const_or_guess (Var _) guess = expect guess InvalidStep
......@@ -408,6 +424,47 @@ val exec_terminst_follows = store_thm("exec_terminst_follows",
REPEAT (POP_ASSUM MP_TAC)) >> rw[] >>
metis_tac[resume_stack_follows, exec_inst_follows, thread_follows_refl])
val exec_terminst_thread_ok = store_thm("exec_terminst_thread_ok",
``i env guess s. propagates thread_ok (liftM SND o exec_terminst env i guess s)``,
`s r t s' t'. thread_ok t resume_stack s r exec_inst t = OK (s', t') thread_ok t'`
by (rw[] >> `propagates thread_ok (liftM SND o resume_stack s r exec_inst)`
suffices_by (rw[propagates_def] >> metis_tac[pairTheory.SND]) >>
metis_tac[exec_inst_ok, resume_stack_thread_ok]) >>
Cases >> rw[propagates_def, exec_terminst_def] >> Cases_on_each [`y0`, `y0'`] >>
rw[] >> fs[pop_and_resume_stack_def]
>- (Cases_on_each [`current_stack.frames`, `t`] >> metis_tac[])
>- (Cases_on_each [`current_stack.frames`, `t`] >> metis_tac[])
>- metis_tac[]
>- metis_tac[]
>- metis_tac[]
>- metis_tac[]
>- metis_tac[]
>- (Cases_on_each [`a.stack_id = sid`, `y0`] >> metis_tac[])
>- (Cases_on_each [`c`, `y0`, `y0`] >> metis_tac[]))
val exec_terminst_stack_ok = store_thm("exec_terminst_stack_ok",
``stacks_ok s0
exec_terminst env i guess s0 t0 = OK (s1, t1)
EVERY stack_ok s1``,
MAP_EVERY ASSUME_TAC [update_stack_state_ok, resume_stack_stack_ok, push_frame_ok] >>
fs[propagates_def] >> Cases_on `i` >> rw[exec_terminst_def] >>
`stack_ok current_stack` by metis_tac[get_stack_ok] >>
TRY (Cases_on `y0`) >> fs[pop_and_resume_stack_def]
>- (Cases_on_each [`current_stack.frames`, `t`] >> metis_tac[pop_frame_ok, FST])
>- (Cases_on_each [`current_stack.frames`, `t`] >> metis_tac[pop_frame_ok, FST])
>- metis_tac[FST]
>- metis_tac[pop_frame_ok, FST]
>- metis_tac[FST]
>- metis_tac[FST]
>- metis_tac[FST]
>- (Cases_on_each [`t0.stack_id = sid`, `y0`] >> rw[] >> metis_tac[FST, get_stack_ok])
>- (Cases_on_each [`c`, `y0`, `y0`] >> rw[]
>- metis_tac[FST]
>- (`stack_ok <|id := Stack (LENGTH s0); frames := []; next_frame_id := 0|>`
by simp[stack_ok_def] >> metis_tac[FST])
>- metis_tac[FST]
>- fs[stack_ok_def, EVERY_MAP]))
val exec_terminst_unique_stacks = store_thm("exec_terminst_unique_stacks",
``stacks_ok s0
exec_terminst env i guess s0 t0 = OK (s1, t1)
......
......@@ -51,6 +51,10 @@ val _ = overload_on("%", ``SSA``)
val _ = overload_on("#", ``(λa b. (a, Block b)) : ssavar -> num -> register``)
val _ = Datatype`
resume_values =
| NOR (α list)
| EXC (α list) α ;
location =
| Register thread_id register
| Memory (thread_id option) action_id ;
......@@ -105,12 +109,6 @@ val _ = Datatype`
message = Message (thread_id option) action_id action ;
strength = STRONG | WEAK ;
resume_values =
| NOR (α list)
| EXC (α list) α ;
cmp_xchg_action_args = <|
addr: location;
strength: strength;
......@@ -120,6 +118,8 @@ val _ = Datatype`
desired: value symbolic
|> ;
strength = STRONG | WEAK ;
atomic_rmw_action_args = <|
addr: location;
order: memory_order;
......@@ -127,15 +127,19 @@ val _ = Datatype`
opnd: location
|> ;
memory = <|
committed : message list;
resolved : location |-> value or_error
|> ;
(* "α symbolic" is an applicative functor representing a computation over
not-yet-known values stored in registers or memory locations.
*)
symbolic = Symbolic (input_location list) (value list -> α or_error)
symbolic = Symbolic (input_location list) (value list -> α or_error) ;
(* A memory state is defined by a list of committed messages. It also contains
a finite map of resolved symbolic values, which should be updated after
every program step.
*)
memory = <|
committed : message list;
resolved : location |-> value or_error
|>
`
(* Core symbolic operations *)
......@@ -253,19 +257,28 @@ val iaddrs_of_message_def = Define`
| DoNewThread _ _ => (empty, empty)
`
val can_read_from = Define`
can_read_from (mem : memory) (writer : message) (reader : message) : bool
let overlap =
bind_oe (FST (iaddrs_of_message mem reader)) (λreads.
C lift_oe (SND (iaddrs_of_message mem writer)) (λwrites.
T IMAGE (UNCURRY iaddr_overlaps) (reads × writes)))
in case overlap of OK (SOME x) => x | _ => F
`
val unresolved_write = Define`
unresolved_write (mem : memory) (write : message) : bool
case SND (iaddrs_of_message mem write) of OK (SOME _) => F | _ => T
`
val last_read_from_def = Define`
last_read_from (mem : memory) (reader : message) : message option or_error =
bind_oe (return (INDEX_OF reader mem.committed)) (λri.
bind_oe (FST (iaddrs_of_message mem reader)) (λreads.
if reads = then return NONE else
let is_overlapping_or_unresolved = λwriter.
case SND (iaddrs_of_message mem writer) of
| OK (SOME writes) => T IMAGE (UNCURRY iaddr_overlaps) (reads × writes)
| OK NONE => T
| Fail _ => F in
case FIND is_overlapping_or_unresolved (DROP (SUC ri) mem.committed) of
let overlaps_or_unresolved = λwriter.
can_read_from mem writer reader unresolved_write mem writer in
case FIND overlaps_or_unresolved (DROP (SUC ri) mem.committed) of
| SOME writer => lift_oe (K writer) (SND (iaddrs_of_message mem writer))
| NONE => Fail (UnallocatedMemory ((CHOICE reads).base))))
| NONE => Fail (UndefinedBehavior "unallocated memory"))
`
val lookup_input_location_def = Define`
......@@ -465,14 +478,19 @@ val message_value_def = Define`
<$> await_before tid id)
`
val extract_def = Define`
extract (n : num) (xs : α list) : (α # α list) option =
case xs of
| y::ys => (
case n of
| SUC m => OPTION_MAP (I ## CONS y) (extract m ys)
| 0 => SOME (y, ys))
| [] => NONE
(* A memory is locally sequentially consistent if all messages that access the
same location from the same thread are committed in program order.
*)
val local_seq_cst_def = Define`
local_seq_cst (mem : memory) : bool
EVERY
(λn. let m = EL n mem.committed in
case m of Message tid id _ =>
EVERY (λm'. can_read_from mem m m' can_read_from mem m' m
case m' of Message tid' id' _ =>
tid tid' id' id)
(TAKE n mem.committed))
(GENLIST I (LENGTH mem.committed))
`
val _ = export_theory()
......
This diff is collapsed.
......@@ -396,7 +396,7 @@ val update_stack_state_def = Define`
| fr::rest => return (s with frames := (fr with state := fs)::rest)
`
val update_stack_state_ok = store_thm("update_state_stack_ok",
val update_stack_state_ok = store_thm("update_stack_state_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[])
......@@ -425,6 +425,10 @@ val get_stack_id = store_thm("get_stack_id",
Cases_on `sid` >> rw[get_stack_def, stacks_ok_def] >>
metis_tac[EL_GENLIST, EL_MAP, LENGTH_GENLIST, LENGTH_MAP])
val get_stack_ok = store_thm("get_stack_ok",
``stacks_ok stacks get_stack sid stacks = OK s stack_ok s``,
Cases_on `sid` >> rw[get_stack_def, stacks_ok_def] >> metis_tac[EVERY_EL])
(* Creates a new thread with the given stack. *)
val new_thread_def = Define`
new_thread (tid : thread_id) (sid : stack_id) : thread =
......
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