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

Commit 43f5e11e authored by Adam Nelson's avatar Adam Nelson
Browse files

Partial RISC-V implementation; tests don't work yet

parent 1006251d
......@@ -18,6 +18,38 @@ val _ = Datatype`
trap_data = TrapData num
`
(* Memory order (see the spec)
https://github.com/microvm/microvm-spec/blob/master/memory-model.rest#memory-operations
*)
val _ = Datatype`
memory_order =
| NOT_ATOMIC
| RELAXED
| CONSUME
| ACQUIRE
| RELEASE
| ACQ_REL
| SEQ_CST
`
(* AtomicRMW operators (see the spec)
https://github.com/microvm/microvm-spec/blob/master/instruction-set.rest#atomicrmw-instruction
*)
val _ = Datatype`
atomicrmw_op =
| RMW_XCHG (* <any> - exchange *)
| RMW_ADD (* <int> - add *)
| RMW_SUB (* <int> - subtract *)
| RMW_AND (* <int> - bitwise and *)
| RMW_NAND (* <int> - bitwise nand *)
| RMW_OR (* <int> - bitwise or *)
| RMW_XOR (* <int> - bitwise xor *)
| RMW_MAX (* <int> - signed max *)
| RMW_MIN (* <int> - signed min *)
| RMW_UMAX (* <int> - unsigned max *)
| RMW_UMIN (* <int> - unsigned min *)
`
(* Binary operations (see the spec)
https://github.com/microvm/microvm-spec/blob/master/instruction-set.rest#binary-operations
*)
......@@ -364,6 +396,8 @@ val _ = Datatype`
wpid = WPID num ;
strength = STRONG | WEAK ;
new_stack_clause =
| PassValues ((σ # uvm_type) list)
| ThrowExc σ ;
......@@ -381,6 +415,7 @@ val _ = Datatype`
val comminst_return_types_def = Define`
comminst_return_types (NewStack _ _) = [StackRef]
comminst_return_types CurrentStack = [StackRef]
comminst_return_types ThreadExit = []
`
(* Map functions: map the SSA variables in expressions, instructions, etc. to
......@@ -617,7 +652,7 @@ val _ = Datatype`
val _ = Datatype`
environment = <|
globals: (global_name # uvm_type) list;
globals: (string # uvm_type) list;
constants: const_name |-> (uvm_type # value);
types: type_name |-> uvm_type;
funcsigs: sig_name |-> funcsig;
......
This diff is collapsed.
......@@ -6,6 +6,8 @@ open uvmErrorsTheory
open DefineUtils
open monadsyntax
open listTheory
open patriciaTheory
open numpairTheory
open Parse
val _ = new_theory "uvmMemory"
......@@ -20,14 +22,11 @@ val _ = define_num_newtype("action_id", "Action")
val _ = Datatype`
ssavar = SSA string ;
global_name = Global string ;
func_name = Func string ;
func_version = FuncVersion func_name num ;
addr =
| GlobalAddr global_name
| StackAddr stack_id thread_id action_id
| HeapAddr thread_id action_id
addr = GlobalAddr num | LocalAddr thread_id action_id alloc ;
alloc = OnHeap | OnStack
`
val _ = type_abbrev("value", ``:(addr, func_name, stack_id, thread_id) gen_value``)
......@@ -60,228 +59,139 @@ val _ = Datatype`
`
val _ = Datatype`
location =
| Register num thread_id
| Memory (thread_id option) action_id ;
input_location =
| At location
| Before (thread_id option) action_id
`
(* Memory order (see the spec)
https://github.com/microvm/microvm-spec/blob/master/memory-model.rest#memory-operations
*)
val _ = Datatype`
memory_order =
| NOT_ATOMIC
| RELAXED
| CONSUME
| ACQUIRE
| RELEASE
| ACQ_REL
| SEQ_CST
`
(* AtomicRMW operators (see the spec)
https://github.com/microvm/microvm-spec/blob/master/instruction-set.rest#atomicrmw-instruction
*)
val _ = Datatype`
atomicrmw_op =
| RMW_XCHG (* <any> - exchange *)
| RMW_ADD (* <int> - add *)
| RMW_SUB (* <int> - subtract *)
| RMW_AND (* <int> - bitwise and *)
| RMW_NAND (* <int> - bitwise nand *)
| RMW_OR (* <int> - bitwise or *)
| RMW_XOR (* <int> - bitwise xor *)
| RMW_MAX (* <int> - signed max *)
| RMW_MIN (* <int> - signed min *)
| RMW_UMAX (* <int> - unsigned max *)
| RMW_UMIN (* <int> - unsigned min *)
`
(* "α symbolic" is an applicative functor representing a computation over
not-yet-known values stored in registers or memory locations.
*)
val _ = Datatype`
symbolic = Symbolic (input_location list) (value list -> α or_error)
store =
| Store iaddr value
| StoreNew uvm_type (num option) alloc
| StoreFree uvm_type addr
`
val _ = Datatype`
message = Message (thread_id option) action_id action ;
(* "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 =
| DoLoad location memory_order
| DoStore location memory_order (value symbolic)
| DoCmpXchg cmp_xchg_action_args
| DoAtomicRMW atomic_rmw_action_args
| DoFence memory_order
| DoNew uvm_type (num option symbolic)
| DoAlloca uvm_type stack_id (num option symbolic)
| DoFree uvm_type addr
| DoGlobalInit global_name uvm_type
| DoNewThread (stack_id symbolic) (value symbolic resume_values) ;
(*
| StoreCmpXchg cmp_xchg_action_args
| StoreAtomicRMW atomic_rmw_action_args ;
cmp_xchg_action_args = <|
addr: location;
addr: iaddr;
strength: strength;
success_order: memory_order;
failure_order: memory_order;
expected: value symbolic;
desired: value symbolic
expected: value;
desired: value
|> ;
atomic_rmw_action_args = <|
addr: location;
addr: iaddr;
order: memory_order;
op: atomicrmw_op;
opnd: location
opnd: value
|> ;
strength = STRONG | WEAK
`
*)
val distinct_messages_def = Define`
distinct_messages (Message tid id _) (Message tid' id' _)
tid tid' id id'
`
val _ = type_abbrev("store_message", ``:thread_id # action_id # store``)
val _ = Datatype`
(* 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
globals : value ptree;
locals : value ptree
|>
`
val memory_ok_def = Define`
memory_ok (mem : memory)
ALL_DISTINCT mem.committed
a b. MEM a mem.committed MEM b mem.committed a b
distinct_messages a b
`
(* Core symbolic operations *)
val _ = overload_on("pure", ``λv. Symbolic [] (K (OK v))``)
val apply_symbolic_def = Define`
apply_symbolic (Symbolic locs fn) (Symbolic locs' a) =
Symbolic (locs ++ locs') (λxs.
fn (TAKE (LENGTH locs) xs) <*> a (DROP (LENGTH locs) xs))
`
val lift_symbolic_def = Define`
lift_symbolic : (α -> β) -> α symbolic -> β symbolic = apply_symbolic o pure
val new_memory_def = Define`
new_memory (globals : (string # uvm_type) list) : memory or_error =
(λgs. <|
globals := Empty |++ ZIP (GENLIST I (LENGTH gs), gs);
locals := Empty
|>) <$> mapM (C zero_value NONE o SND) globals
`
val memory_get_def = Define`
memory_get mem (GlobalAddr n) = mem.globals ' n
memory_get mem (LocalAddr (Thread tid) (Action id) _) =
mem.locals ' (tid id)
`
val memory_update_def = Define`
memory_update (mem : memory) (v : value) (ia : iaddr) : memory or_error = do
base <- expect (memory_get mem ia.base) (UnallocatedMemory ia.base);
updated <- iaddr_update base ia v;
return (
case ia.base of
| GlobalAddr n => mem with globals updated_by C $|+ (n, updated)
| LocalAddr (Thread tid) (Action id) _ =>
mem with locals updated_by C $|+ (tid id, updated))
od
`
val apply_store_def = Define`
apply_store mem (_, _, Store ia v) = memory_update mem v ia
apply_store mem (Thread tid, Action id, StoreNew ty sz _) =
(λz. mem with locals updated_by C $|+ (tid id, z))
<$> zero_value ty sz
apply_store mem (_, _, StoreFree _ (GlobalAddr n)) =
return (mem with globals updated_by C REMOVE n)
apply_store mem (_, _, StoreFree _ (LocalAddr (Thread tid) (Action id) _)) =
return (mem with locals updated_by C REMOVE (tid id))
`
val update_with_store_def = Define`
update_with_store (LocalAddr tid' id' _ : addr)
((tid, id, StoreNew ty sz _) : store_message)
(old : value option)
: value option or_error =
(if tid = tid' id = id'
then SOME <$> zero_value ty sz
else return old)
update_with_store (GlobalAddr _) (_, _, StoreNew _ _ _) old = return old
update_with_store base (_, _, Store ia v') (SOME v) =
(if base = ia.base
then SOME <$> iaddr_update v ia v'
else return (SOME v))
update_with_store _ (_, _, Store _ _) NONE = return NONE
update_with_store a (_, _, StoreFree _ a') old =
return (if a = a' then NONE else old)
`
val memory_load_def = Define`
memory_load (mem : memory)
(pending_stores : store_message list)
(ia : iaddr)
: value or_error =
FOLDR (λa b. b >>= update_with_store ia.base a)
(return (memory_get mem ia.base))
pending_stores
>>= C expect (UnallocatedMemory ia.base)
>>= C iaddr_get ia
`
val _ = overload_on("APPLICATIVE_FAPPLY", ``apply_symbolic``)
val _ = overload_on("<$>", ``lift_symbolic``)
val symbolic_or_error_def = Define`
symbolic_or_error : α or_error -> α symbolic = Symbolic [] o K
`
val symbolic_error_join_def = Define`
symbolic_error_join (Symbolic locs fn) = Symbolic locs (join_left o fn)
`
val await_def = Define`
await (loc : location) : value symbolic = Symbolic [At loc] (OK o HD)
`
val await_before_def = Define`
await_before (tid : thread_id option) (id : action_id) : value symbolic =
Symbolic [Before tid id] (OK o HD)
`
(* Utility functions for "oe" (option or_error) nested monads *)
val bind_error_oe_def = Define`
bind_error_oe (v : α option or_error) (f : α -> β or_error) : β option or_error =
v >>= λopt. case opt of SOME v => SOME <$> f v | NONE => return NONE
`
val bind_oe_def = Define`
bind_oe (v : α option or_error) (f : α -> β option or_error) : β option or_error =
case v of
| OK (SOME x) => f x
| OK NONE => OK NONE
| Fail err => Fail err
`
val lift_oe_def = Define`
lift_oe : (α -> β) -> α option or_error -> β option or_error =
lift_left o OPTION_MAP
`
val sequence_option_def = Define`
sequence_option : α option list -> α list option =
FOLDR (λp q. OPTION_BIND p (λx. OPTION_BIND q (λy. SOME (x::y)))) (SOME [])
val program_order_def = Define`
program_order (tid : thread_id, id : action_id, _ : α)
(tid' : thread_id, id' : action_id, _ : α)
tid tid' id id'
`
val sequence_oe_def = Define`
sequence_oe : α option or_error list -> α list option or_error =
lift_left sequence_option o sequence_left
val iaddrs_of_store_def = Define`
iaddrs_of_store ((_, _, Store ia _) : store_message) : iaddr set = {ia}
iaddrs_of_store (tid, id, StoreNew ty _ al) = {<|
base := LocalAddr tid id al;
offsets := [];
base_ty := ty;
ty := ty
|>}
iaddrs_of_store (_, _, StoreFree ty a) = {<|
base := a;
offsets := [];
base_ty := ty;
ty := ty
|>}
`
(* Symbolic value resolution in the context of a memory. *)
val lookup_location_def = Define`
lookup_location (mem : memory) (loc : location) : value option or_error =
bind_error_oe (return (FLOOKUP mem.resolved loc)) I
val overlapping_stores_def = Define`
overlapping_stores (a : store_message) (b : store_message)
T IMAGE (UNCURRY iaddr_overlaps) (iaddrs_of_store a × iaddrs_of_store b)
`
val iaddrs_of_message_def = Define`
iaddrs_of_message (mem : memory) (Message tid id action)
: iaddr set option or_error # iaddr set option or_error =
let set_of = lift_oe (λx. {x}) in
let empty = return (SOME ) in
case action of
| DoLoad loc _ =>
(set_of (bind_error_oe (lookup_location mem loc) get_iref_addr), empty)
| DoStore loc _ _ =>
(λx. (set_of x, set_of x)) (bind_error_oe (lookup_location mem loc) get_iref_addr)
| DoCmpXchg args =>
(λx. (set_of x, set_of x)) (bind_error_oe (lookup_location mem args.addr) get_iref_addr)
| DoAtomicRMW args =>
(λx. (set_of x, set_of x)) (bind_error_oe (lookup_location mem args.addr) get_iref_addr)
| DoFence _ => (empty, empty)
| DoNew ty _ => (empty, return (SOME {<|
base := HeapAddr (THE tid) id;
offsets := [];
base_ty := ty;
ty := ty
|>}))
| DoAlloca ty sid _ => (empty, return (SOME {<|
base := StackAddr sid (THE tid) id;
offsets := [];
base_ty := ty;
ty := ty
|>}))
| DoFree ty a => (empty, return (SOME {<|
base := a;
offsets := [];
base_ty := ty;
ty := ty
|>}))
| DoGlobalInit name ty => (empty, return (SOME {<|
base := GlobalAddr name;
offsets := [];
base_ty := ty;
ty := ty
|>}))
| DoNewThread _ _ => (empty, empty)
`
(*
val can_read_from = Define`
can_read_from (mem : memory) (writer : message) (reader : message) : bool ⇔
......@@ -319,133 +229,6 @@ val lookup_input_location_def = Define`
lookup_location mem (Memory last_tid last_id)))
`
val resolve_symbolic_def = Define`
resolve_symbolic (mem : memory) (Symbolic locs fn : α symbolic) : α option or_error =
(locs :> MAP (lookup_input_location mem) :> sequence_oe :> C bind_error_oe fn)
`
val resolvable_in_def = Define`
resolvable_in (mem : memory) : α symbolic set =
λsym. case sym of Symbolic locs _ => (
let vals = MAP (lookup_input_location mem) locs in
case sequence_oe vals of
| Fail _ => T
| OK (SOME _) => T
| OK NONE => F)
`
val resolvable_without_error_in_def = Define`
resolvable_without_error_in (mem : memory) : α symbolic set =
λsym. case sym of Symbolic locs _ => (
let vals = MAP (lookup_input_location mem) locs in
case sequence_oe vals of
| Fail _ => F
| OK (SOME _) => T
| OK NONE => F)
`
val get_resolved_def = Define`
get_resolved (mem : memory) : α symbolic -> α = THE o OUTL o resolve_symbolic mem
`
(* A "well-behaved" symbolic value is a symbolic value that expects exactly the
number of arguments that it claims it does, and does not do anything with
extra arguments. All symbolic values constructed by any method other than
directly invoking the Symbolic constructor should be well-behaved by
definition.
*)
val well_behaved_symbolic_def = Define`
well_behaved_symbolic (Symbolic locs fn)
locs'. fn (TAKE (LENGTH locs) locs') = fn locs'
`
val well_behaved_add_length = store_thm("well_behaved_add_length",
``(locs. f (TAKE (LENGTH l) locs) = f locs) locs. f (TAKE (LENGTH l + n) locs) = f locs``,
strip_tac >> strip_tac >>
Cases_on `LENGTH locs LENGTH l`
>- simp[listTheory.TAKE_LENGTH_TOO_LONG]
>- (`TAKE (LENGTH l) (TAKE (LENGTH l + n) locs) = TAKE (LENGTH l) locs`
suffices_by metis_tac[] >>
simp[listTheory.LENGTH_TAKE, listTheory.TAKE_SUM, listTheory.TAKE_APPEND1,
listTheory.TAKE_LENGTH_ID_rwt]))
val well_behaved_drop_take = store_thm("well_behaved_drop_take",
``(locs. f (TAKE (LENGTH l) locs) = f locs)
locs. f (DROP n (TAKE (n + LENGTH l) locs)) = f (DROP n locs)``,
strip_tac >> strip_tac >>
Cases_on `LENGTH locs n`
>- simp[listTheory.TAKE_LENGTH_TOO_LONG]
>- (`x. DROP n (TAKE n locs ++ x) = x` suffices_by simp[listTheory.TAKE_SUM] >>
`LENGTH (TAKE n locs) = n`
suffices_by metis_tac[prove(``a. DROP (LENGTH a) (a++x) = x``,
Induct >> simp[])] >>
simp[]))
val drop_drop_lemma = prove(
``DROP n (DROP n' xs) = DROP (n + n') xs``,
Cases_on `n LENGTH xs`
>- (Cases_on `n + n' LENGTH xs`
>- simp[rich_listTheory.DROP_DROP]
>- simp[listTheory.DROP_LENGTH_TOO_LONG])
>- simp[listTheory.DROP_LENGTH_TOO_LONG])
val well_behaved_pure = store_thm("well_behaved_pure[simp]",
``well_behaved_symbolic (pure x)``,
simp[well_behaved_symbolic_def])
val well_behaved_apply = store_thm("well_behaved_apply[simp]",
``well_behaved_symbolic a well_behaved_symbolic b well_behaved_symbolic (a <*> b)``,
Cases_on `a` >> Cases_on `b` >>
rw[well_behaved_symbolic_def, apply_symbolic_def, ap_left_def] >>
simp[well_behaved_add_length, well_behaved_drop_take])
val well_behaved_lift = store_thm("well_behaved_lift[simp]",
``well_behaved_symbolic x well_behaved_symbolic (f <$> x)``,
simp[lift_symbolic_def])
val well_behaved_symbolic_or_error = store_thm("well_behaved_symbolic_or_error[simp]",
``well_behaved_symbolic (symbolic_or_error x)``,
simp[well_behaved_symbolic_def, symbolic_or_error_def])
val well_behaved_symbolic_error_join = store_thm("well_behaved_symbolic_error_join[simp]",
``well_behaved_symbolic x well_behaved_symbolic (symbolic_error_join x)``,
Cases_on `x` >> simp[well_behaved_symbolic_def, symbolic_error_join_def])
val well_behaved_await = store_thm("well_behaved_await[simp]",
``well_behaved_symbolic (await loc)``,
rw[well_behaved_symbolic_def, await_def] >>
Cases_on `locs'` >> simp[])
val well_behaved_await_before = store_thm("well_behaved_await_before[simp]",
``well_behaved_symbolic (await_before tid id)``,
rw[well_behaved_symbolic_def, await_before_def] >>
Cases_on `locs'` >> simp[])
(* Applicative laws for symbolic *)
val symbolic_identity = store_thm("symbolic_identity",
``pure I <*> v = v``,
Cases_on `v` >> simp[apply_symbolic_def, ap_left_def] >>
metis_tac[bind_left_monad_right_id])
val symbolic_homomorphism = store_thm("symbolic_homomorphism[simp]",
``pure f <*> pure x = pure (f x)``,
simp[apply_symbolic_def, ap_left_def] >>
metis_tac[combinTheory.K_DEF])
val symbolic_interchange = store_thm("symbolic_interchange[simp]",
``well_behaved_symbolic u pure (λx. x y) <*> u = u <*> pure y``,
Cases_on `u` >>
rw[well_behaved_symbolic_def, apply_symbolic_def, ap_left_def])
val symbolic_composition = store_thm("symbolic_composition",
``well_behaved_symbolic u well_behaved_symbolic v well_behaved_symbolic w
pure $o <*> u <*> v <*> w = u <*> (v <*> w)``,
Cases_on `u` >> Cases_on `v` >> Cases_on `w` >>
rw[well_behaved_symbolic_def, apply_symbolic_def, ap_left_composition] >>
simp[well_behaved_add_length, well_behaved_drop_take, drop_drop_lemma])
(* Relations between memory messages *)
val is_read_message_def = Define`
......@@ -504,11 +287,6 @@ val message_value_def = Define`
<$> await_before tid id)
`
val program_order_def = Define`
program_order (Message tid id _) (Message tid' id' _)
tid tid' id id'
`
(* A memory is locally sequentially consistent if all messages that access the
same location from the same thread are committed in program order.
*)
......@@ -521,6 +299,7 @@ val local_seq_cst_def = Define`
(TAKE n mem.committed))
(GENLIST I (LENGTH mem.committed))
`
*)
val _ = export_theory()
This diff is collapsed.
This diff is collapsed.
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