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

Commit e6a34aa8 authored by Adam Nelson's avatar Adam Nelson
Browse files

Rename memory_message, memory_action to message, action

parent 2e0a1c69
......@@ -109,22 +109,27 @@ val _ = Datatype`
| RMW_UMAX (* <int> - unsigned max *)
| RMW_UMIN (* <int> - unsigned min *) ;
(* "memory_action" is the type of memory mutation actions waiting to be
performed. Because some of the messages have complicated argument lists,
their arguments are defined as records.
(* "action" is the type of memory mutation actions waiting to be performed.
Because some of the messages have complicated argument lists, their
arguments are defined as records.
*)
memory_action =
| MemLoad location memory_order
| MemStore location memory_order (value symbolic)
| MemCmpXchg memory_action_cmp_xchg_args
| MemAtomicRMW memory_action_atomic_rmw_args
| MemFence memory_order
| MemNew uvm_type (num option symbolic)
| MemAlloca uvm_type stack_id frame_id (num option symbolic)
| MemFree uvm_type addr
| MemGlobalInit global_name uvm_type ;
memory_action_cmp_xchg_args = <|
action =
| LoadAction location memory_order
| StoreAction location memory_order (value symbolic)
| CmpXchgAction cmp_xchg_action_args
| AtomicRMWAction atomic_rmw_action_args
| FenceAction memory_order
| NewAction uvm_type (num option symbolic)
| AllocaAction uvm_type stack_id frame_id (num option symbolic)
| FreeAction uvm_type addr
| GlobalInitAction global_name uvm_type
| NewThreadAction func_name (value symbolic list) ;
message = Message thread_id action_id action ;
strength = STRONG | WEAK ;
cmp_xchg_action_args = <|
addr: location;
strength: strength;
success_order: memory_order;
......@@ -133,19 +138,15 @@ val _ = Datatype`
desired: value symbolic
|> ;
memory_action_atomic_rmw_args = <|
atomic_rmw_action_args = <|
addr: location;
order: memory_order;
op: atomicrmw_op;
opnd: location
|> ;
strength = STRONG | WEAK ;
memory_message = Message thread_id action_id memory_action ;
memory = <|
committed : memory_message list;
committed : message list;
resolved : location |-> value or_error
|> ;
......@@ -233,34 +234,34 @@ val iaddrs_of_message_def = Define`
let set_of = lift_oe (λx. {x}) in
let empty = return (SOME ) in
case action of
| MemLoad loc _ =>
| LoadAction loc _ =>
(set_of (bind_error_oe (lookup_location mem loc) get_iref_addr), empty)
| MemStore loc _ _ =>
| StoreAction loc _ _ =>
(λx. (set_of x, set_of x)) (bind_error_oe (lookup_location mem loc) get_iref_addr)
| MemCmpXchg args =>
| CmpXchgAction args =>
(λx. (set_of x, set_of x)) (bind_error_oe (lookup_location mem args.addr) get_iref_addr)
| MemAtomicRMW args =>
| AtomicRMWAction args =>
(λx. (set_of x, set_of x)) (bind_error_oe (lookup_location mem args.addr) get_iref_addr)
| MemFence _ => (empty, empty)
| MemNew ty _ => (empty, return (SOME {<|
| FenceAction _ => (empty, empty)
| NewAction ty _ => (empty, return (SOME {<|
base := HeapAddr tid id;
offsets := [];
base_ty := ty;
ty := ty
|>}))
| MemAlloca ty sid fid _ => (empty, return (SOME {<|
| AllocaAction ty sid fid _ => (empty, return (SOME {<|
base := StackAddr tid sid fid id;
offsets := [];
base_ty := ty;
ty := ty
|>}))
| MemFree ty a => (empty, return (SOME {<|
| FreeAction ty a => (empty, return (SOME {<|
base := a;
offsets := [];
base_ty := ty;
ty := ty
|>}))
| MemGlobalInit name ty => (empty, return (SOME {<|
| GlobalInitAction name ty => (empty, return (SOME {<|
base := GlobalAddr name;
offsets := [];
base_ty := ty;
......@@ -269,7 +270,7 @@ val iaddrs_of_message_def = Define`
`
val last_read_from_def = Define`
last_read_from (mem : memory) (reader : memory_message) : memory_message option or_error =
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
......@@ -425,20 +426,20 @@ val symbolic_composition = store_thm("symbolic_composition",
(* Relations between memory messages *)
val is_read_message_def = Define`
is_read_message (Message _ _ (MemLoad _ _)) = T
is_read_message (Message _ _ (MemCmpXchg _)) = T
is_read_message (Message _ _ (MemAtomicRMW _)) = T
is_read_message (Message _ _ (LoadAction _ _)) = T
is_read_message (Message _ _ (CmpXchgAction _)) = T
is_read_message (Message _ _ (AtomicRMWAction _)) = T
is_read_message _ = F
`
val is_write_message_def = Define`
is_write_message (Message _ _ (MemStore _ _ _)) = T
is_write_message (Message _ _ (MemCmpXchg _)) = T
is_write_message (Message _ _ (MemAtomicRMW _)) = T
is_write_message (Message _ _ (MemNew _ _)) = T
is_write_message (Message _ _ (MemAlloca _ _ _ _)) = T
is_write_message (Message _ _ (MemGlobalInit _ _)) = T
is_write_message (Message _ _ (MemFree _ _)) = T
is_write_message (Message _ _ (StoreAction _ _ _)) = T
is_write_message (Message _ _ (CmpXchgAction _)) = T
is_write_message (Message _ _ (AtomicRMWAction _)) = T
is_write_message (Message _ _ (NewAction _ _)) = T
is_write_message (Message _ _ (AllocaAction _ _ _ _)) = T
is_write_message (Message _ _ (GlobalInitAction _ _)) = T
is_write_message (Message _ _ (FreeAction _ _)) = T
is_write_message _ = F
`
......@@ -451,27 +452,27 @@ val reads_from_def = Define`
reads_from mem reader writer last_read_from mem reader = OK (SOME writer)
`
val memory_message_value_def = Define`
memory_message_value (Message tid id (MemLoad _ _)) = await_before tid id
memory_message_value (Message tid id (MemStore addr_loc _ new_value)) =
val message_value_def = Define`
message_value (Message tid id (LoadAction _ _)) = await_before tid id
message_value (Message tid id (StoreAction addr_loc _ new_value)) =
symbolic_error_join (
(λold_value iref new_value. do
ia <- get_iref_addr iref;
iaddr_update old_value ia new_value
od) <$> await_before tid id <*> await addr_loc <*> new_value)
memory_message_value (Message _ _ (MemCmpXchg _)) =
symbolic_or_error (Fail (NotImplemented "MemCmpXchg"))
memory_message_value (Message _ _ (MemAtomicRMW _)) =
symbolic_or_error (Fail (NotImplemented "MemAtomicRMW"))
memory_message_value (Message _ _ (MemNew ty len)) =
message_value (Message _ _ (CmpXchgAction _)) =
symbolic_or_error (Fail (NotImplemented "CmpXchgAction"))
message_value (Message _ _ (AtomicRMWAction _)) =
symbolic_or_error (Fail (NotImplemented "AtomicRMWAction"))
message_value (Message _ _ (NewAction ty len)) =
symbolic_error_join (zero_value ty <$> len)
memory_message_value (Message _ _ (MemAlloca ty _ _ len)) =
message_value (Message _ _ (AllocaAction ty _ _ len)) =
symbolic_error_join (zero_value ty <$> len)
memory_message_value (Message _ _ (MemGlobalInit _ ty)) =
message_value (Message _ _ (GlobalInitAction _ ty)) =
symbolic_or_error (zero_value ty NONE)
memory_message_value (Message _ _ (MemFree _ a)) =
message_value (Message _ _ (FreeAction _ a)) =
symbolic_or_error (Fail (UnallocatedMemory a))
memory_message_value (Message tid id (MemFence _)) = await_before tid id
message_value (Message tid id (FenceAction _)) = await_before tid id
`
val extract_def = Define`
......
......@@ -44,7 +44,7 @@ val get_thread_def = Define`
val spawn_thread_def = Define`
spawn_thread (main : func_name)
(args : register or_const list)
(init_actions : memory_action list)
(init_actions : action list)
(state : sched_state)
: sched_state or_error = do
main_ver <- expect (OPTION_JOIN (FLOOKUP state.env.func_versions main))
......@@ -69,7 +69,7 @@ val register_locations_def = Define`
val all_locations_def = Define`
all_locations (s : sched_state) : location |-> value symbolic =
register_locations s.threads |++
MAP (λm. case m of Message tid id _ => (Memory tid id, memory_message_value m))
MAP (λm. case m of Message tid id _ => (Memory tid id, message_value m))
s.memory.committed
`
......@@ -149,7 +149,7 @@ val init_sched_state_def = Define`
return <| env := env; threads := [];
memory := <| committed := []; resolved := FEMPTY |>
|>
>>= spawn_thread main (MAP Const args) (MAP (UNCURRY MemGlobalInit) env.globals)
>>= spawn_thread main (MAP Const args) (MAP (UNCURRY GlobalInitAction) env.globals)
>>= return o resolve_all
`
......@@ -159,12 +159,12 @@ val take_step_def = Define`
(next, thread') <-
case thread_or_exit of
| Next thread => do
(next, actions') <- expect (extract n thread.actions) InvalidStep;
return (next, Next (thread with actions := actions'))
(next, outbox') <- expect (extract n thread.outbox) InvalidStep;
return (next, Next (thread with outbox := outbox'))
od
| Exit es => do
(next, actions') <- expect (extract n es.remaining_actions) InvalidStep;
return (next, Exit (es with remaining_actions := actions'))
(next, outbox') <- expect (extract n es.outbox) InvalidStep;
return (next, Exit (es with outbox := outbox'))
od;
return (state with <|
memory updated_by (λm. m with committed updated_by CONS next);
......
......@@ -29,7 +29,7 @@ val _ = Datatype`
fn: function;
next_step: register terminst;
registers: register |-> value symbolic;
actions: memory_message list;
outbox: message list;
next_action_id: action_id
|> ;
......@@ -56,8 +56,8 @@ val state_follows_def = Define`
(prev.frame_id next.frame_id)
(prev.next_action_id next.next_action_id)
(prev.registers next.registers)
(a b id. MEM (Message a id b) next.actions
prev.next_action_id id MEM (Message a id b) prev.actions)
(a b id. MEM (Message a id b) next.outbox
prev.next_action_id id MEM (Message a id b) prev.outbox)
`
val state_follows_refl = store_thm("state_follows_refl",
......@@ -256,10 +256,10 @@ val copy_register_follows = store_thm("copy_register_follows",
Cases_on `r` >> metis_tac[copy_register_def, add_register_follows])
val enqueue_action_def = Define`
enqueue_action (a : memory_action) (state : thread_state) : thread_state or_error =
enqueue_action (a : action) (state : thread_state) : thread_state or_error =
return (state with <|
next_action_id updated_by action_id_suc;
actions updated_by SNOC (Message state.tid state.next_action_id a)
outbox updated_by SNOC (Message state.tid state.next_action_id a)
|>)
`
......@@ -292,29 +292,29 @@ val exec_inst_def = Define`
iaddr_get value ia
od) <$> await src_loc <*> await_before state.tid id) in
add_register (dst, value) state
:> liftM (λstate. (state, SOME (MemLoad src_loc ord)))
:> liftM (λstate. (state, SOME (LoadAction src_loc ord)))
| Store src _ _ dst ord =>
let dst_loc = Register state.tid dst in
return (state, SOME (MemStore dst_loc ord (sym_value state src)))
return (state, SOME (StoreAction dst_loc ord (sym_value state src)))
| CmpXchg _ _ _ _ _ _ _ _ _ _ => Fail (NotImplemented "CMPXCHG")
| AtomicRMW _ _ _ _ _ _ _ => Fail (NotImplemented "ATOMICRMW")
| Fence ord => return (state, SOME (MemFence ord))
| Fence ord => return (state, SOME (FenceAction ord))
| New v ty =>
add_register (v, pure (RefV ty (HeapAddr state.tid id))) state
:> liftM (λstate. (state, SOME (MemNew ty (pure NONE))))
:> liftM (λstate. (state, SOME (NewAction ty (pure NONE))))
| Alloca v ty =>
add_register (v, pure (RefV ty (StackAddr state.tid state.stack_id state.frame_id id))) state
:> liftM (λstate. (state, SOME (MemAlloca ty state.stack_id state.frame_id (pure NONE))))
:> liftM (λstate. (state, SOME (AllocaAction ty state.stack_id state.frame_id (pure NONE))))
| NewHybrid v ty _ len =>
let len = symbolic_error_join
(liftM SOME o get_int_as_num "NEWHYBRID length" <$> sym_value state len) in
add_register (v, pure (RefV ty (HeapAddr state.tid id))) state
:> liftM (λstate. (state, SOME (MemNew ty len)))
:> liftM (λstate. (state, SOME (NewAction ty len)))
| AllocaHybrid v ty _ len =>
let len = symbolic_error_join
(liftM SOME o get_int_as_num "ALLOCAHYBRID length" <$> sym_value state len) in
add_register (v, pure (RefV ty (StackAddr state.tid state.stack_id state.frame_id id))) state
:> liftM (λstate. (state, SOME (MemAlloca ty state.stack_id state.frame_id len)))
:> liftM (λstate. (state, SOME (AllocaAction ty state.stack_id state.frame_id len)))
| NewThread _ _ _ => Fail (NotImplemented "NEWTHREAD")
| CommInst _ _ => Fail (NotImplemented "COMMINST");
case action of
......@@ -365,11 +365,11 @@ val exec_block_def = Define`
state <- ZIP (args, MAP FST block.args)
:> FOLDL (λs r. s >>= copy_register r) (return state);
state <- FOLDL (λs i. s >>= exec_inst i) (return state) block.body;
FOLDL (λs a. s >>= enqueue_action a) (return state) (LIST_BIND state.actions
FOLDL (λs a. s >>= enqueue_action a) (return state) (LIST_BIND state.outbox
(λm. case m of
| Message tid id (MemAlloca ty sid fid _) =>
| Message tid id (AllocaAction ty sid fid _) =>
if fid = state.frame_id
then [MemFree ty (StackAddr tid sid fid id)]
then [FreeAction ty (StackAddr tid sid fid id)]
else []
| _ => []))
od
......@@ -417,7 +417,7 @@ val _ = Datatype`
exit_type: resume_type;
values: value symbolic list;
registers: register |-> value symbolic;
remaining_actions: memory_message list
outbox: message list
|>
`
......@@ -441,7 +441,7 @@ val return_thread_def = Define`
exit_type := res;
values := MAP (sym_value state) return_vals;
registers := state.registers;
remaining_actions := state.actions
outbox := state.outbox
|>)
| frame::stack_tail => do
(label, destargs) <-
......@@ -477,7 +477,7 @@ val return_thread_follows = store_thm("return_thread_follows",
*)
val new_thread_def = Define`
new_thread (tid : thread_id) (fn : function) (args : register or_const list)
(init_actions : memory_action list)
(init_actions : action list)
: thread_state or_error =
let state = <|
stack := [];
......@@ -487,12 +487,12 @@ val new_thread_def = Define`
fn := fn;
next_step := ARB; (* Temporary value; should be immediately overwritten *)
registers := FEMPTY;
actions := [];
outbox := [];
next_action_id := Action 0
|> in
let state = FOLDL (λstate action. state with <|
next_action_id updated_by action_id_suc;
actions updated_by SNOC (Message tid state.next_action_id action)
outbox updated_by SNOC (Message tid state.next_action_id action)
|>) state init_actions in
get_block fn.entry_block state
>>= λblock. exec_block block args state
......
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