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

Commit 59737ac5 authored by Adam Nelson's avatar Adam Nelson
Browse files

Atomic memory cells and operations for WMM/RISC-V

- Memory and registers are split up into typed atomic cells
- Value type now contains only scalar values
- Instructions are compiled down to WMM "operations", allowing stores
  and loads of composite values to be split up into atomic parts
- Scheduler now executes one operation at a time, rather than one block
  at a time
- New scheduler steps for WMM
- Commands (formerly Thread Actions) such as allocation now executed at
  the global scheduler level. Action IDs no longer needed.
- Threads and stacks changed completely; registers now stored in stack
  frames
- Monads pretty-print properly again!
- Patricia trees replaced with sptrees

Lots of code is still commented out, and tests still don't work, but
the main formalization code compiles.
parent 2fd5a16b
......@@ -73,9 +73,8 @@ struct
num_infixes_defined := true
) else ();
overload_on("≺", ``^lt``);
overload_on("≼", ``λl r. (^lt l r) (l = r)``);
TeX_notation {hol="≺", TeX=("\\ensuremath{\\prec}", 1)};
TeX_notation {hol="≼", TeX=("\\ensuremath{\\preceq}", 1)}
overload_on("≼", ``λl r. (^lt l r) (l = r)``)
(* TeX_notation {hol="≺", TeX=("\\ensuremath{\\prec}", 1)}; *)
end
fun QDefine(quoted : string frag list) =
......@@ -83,18 +82,25 @@ struct
| unquote (ANTIQUOTE s) = QUOTE s
in Define (map unquote quoted) end
val greek = ["'a", "'b", "'c", "'d", "'e", "'f", "'g", "'h", "'i", "'j", "'k"]
fun normalize_ty (ty : hol_type) : hol_type =
type_subst (map (op |->) (ListPair.zip (type_vars ty, map mk_vartype greek))) ty
fun define_monad(name : string, ty : hol_type -> hol_type, return : term, bind : term) : unit =
let
val alpha = mk_vartype "'a"
val beta = mk_vartype "'b"
val alpha = mk_vartype "'aa"
val beta = mk_vartype "'bb"
val return_ty = normalize_ty (alpha --> ty alpha)
val return' = ``^return : ^(ty_antiq return_ty)``
val return_name = "return_" ^ name
val return_def = Define[QUOTE return_name, QUOTE " = ", ANTIQUOTE return]
val _ = mk_const(return_name, alpha --> ty alpha)
val _ = overload_on(return_name, return')
val bind_ty = normalize_ty (ty alpha --> (alpha --> ty beta) --> ty beta)
val bind' = ``^bind : ^(ty_antiq bind_ty)``
val bind_name = "bind_" ^ name
val bind_def = Define[QUOTE bind_name, QUOTE " = ", ANTIQUOTE bind]
val _ = mk_const(bind_name, ty alpha --> (alpha --> ty beta) --> ty beta)
val _ = overload_on(bind_name, bind')
val lift_name = "lift_" ^ name
val lift_def = QDefine `^lift_name f x = ^bind_name x (^return_name o f)`
......@@ -126,11 +132,11 @@ struct
set_fixity "<$>" (Infixl 661);
monad_infixes_defined := true
) else ();
overload_on("return", Term [QUOTE return_name]);
overload_on("monad_bind", Term [QUOTE bind_name]);
overload_on("monad_unitbind", ``λm1 m2. monad_bind m1 (K m2)``);
overload_on(">>=", ``monad_bind``);
overload_on("*>", ``monad_unitbind``);
overload_on(">>=", bind');
overload_on("*>", ``λm1 m2. ^bind' m1 (K m2)``);
overload_on("return", return');
overload_on("monad_bind", bind');
overload_on("monad_unitbind", ``λm1 m2. ^bind' m1 (K m2)``);
overload_on("liftM", Term [QUOTE lift_name]);
overload_on("join", Term [QUOTE join_name]);
overload_on("sequence", Term [QUOTE sequence_name]);
......
......@@ -3,7 +3,7 @@ open HolKernel
signature EvalUtils =
sig
val add_extra_eval_thms : unit -> unit
(*
val to_env : term -> term
val start_at : string -> term frag list -> term -> term
......@@ -19,5 +19,6 @@ sig
val take_step : term frag list -> term -> term
val take_steps : term frag list -> term -> term
*)
end
......@@ -12,10 +12,6 @@ struct
``f x s y y'. (f o_f if x s then y else y') = (if s x then f o_f y else f o_f y')``,
rw[IN_APP])
val in_app_symbolic_only = prove(
``(l: α symbolic). (l P) = P l``,
rw[IN_APP])
val lhdtl_lunfold = prove(
``LHD (LUNFOLD f x) = OPTION_MAP SND (f x)
LTL (LUNFOLD f x) = OPTION_MAP (LUNFOLD f o FST) (f x)``,
......@@ -25,14 +21,11 @@ struct
fun add_extra_eval_thms() : unit =
computeLib.add_funs[
SING, CHOICE_SING,
OPTION_MAP_DEF, OPTION_BIND_def, OPTION_CHOICE_def,
DRESTRICT_FEMPTY, DRESTRICT_FUPDATE,
RRESTRICT_FEMPTY, RRESTRICT_FUPDATE,
FUPDATE_EQ, FUNION_FEMPTY_1, FUNION_FUPDATE_1,
MAP_KEYS_FEMPTY, map_keys_register_fupdate, FCARD_DEF,
o_f_FEMPTY, o_f_FUPDATE, o_f_FUNION, reduce_o_f_if,
in_app_symbolic_only, lhdtl_lunfold]
OPTION_MAP_DEF, OPTION_MAP2_DEF, OPTION_BIND_def, OPTION_CHOICE_def,
in_app_symbolic_only, lhdtl_lunfold,
bind_left_monad_left_id, bind_left_monad_right_id, bind_left_monad_assoc]
(*
fun parens q = [QUOTE "("] @ q @ [QUOTE ")"]
fun to_env (bundle : term) : term =
......@@ -63,5 +56,6 @@ struct
fun take_steps (steps : term frag list) (state : term) : term =
EVAL(Term(`^state >>= take_steps` @ parens steps)) |> concl |> rhs
*)
end
## Specifying a Micro Virtual Machine above Weak Memory
- Specification of realistic virtual machine IR down to weak memory
- Execution of concrete IR programs on spec
- Verification of simple optimizations
- Enrichment of WMM
- AtomicRMW
- Connection to higher-level concepts (SeqCst, C11 memory model)
- Why?
- Goal is to produce completely verified stack (from OS to software)
- Verification of spec, so that applications can be verified against spec
......@@ -10,23 +10,24 @@ open DefineUtils
val _ = new_theory "sumMonad"
val _ = define_monad("left", (fn a => mk_sum(a, mk_vartype "'right")),
``INL``, ``λx fn. case x of INL a => fn a | INR b => INR b``)
``INL``, ``λx fn. sum_CASE x fn INR``)
(*
val return_left_INL = store_thm("return_left_INL[simp]",
``return_left x = INL x``,
simp[definition "return_left_def"])
*)
val bind_left_INR_simp = store_thm("bind_left_INR_simp[simp]",
``bind_left (INR x) f = INR x``,
simp[definition "bind_left_def"])
``bind_left (INR x) f = INR x``, simp[])
val bind_left_INL = store_thm("bind_left_INL[simp]",
``(bind_left x f = INL y) = y0. (x = INL y0) (f y0 = INL y)``,
Cases_on `x` >> simp[definition "bind_left_def"])
Cases_on `x` >> simp[])
val bind_left_INR = store_thm("bind_left_INR",
``(y. x = INR y) f. bind_left x f = x``,
Cases_on `x` >> simp[definition "bind_left_def"])
Cases_on `x` >> simp[])
val bind_right_def = Define`
......@@ -50,15 +51,15 @@ val lift_left_INL = store_thm("lift_left_INL[simp]",
val lift_left_INR = store_thm("lift_left_INR[simp]",
``(lift_left f x = INR y) = (x = INR y)``,
Cases_on `x` >> simp[definition "lift_left_def", definition "bind_left_def"])
Cases_on `x` >> simp[definition "lift_left_def"])
val lift_left_id = store_thm("lift_left_id[simp]",
``lift_left I x = x``,
Cases_on `x` >> simp[definition "lift_left_def", definition "bind_left_def"])
Cases_on `x` >> simp[definition "lift_left_def"])
val lift_left_compose = store_thm("lift_left_compose[simp]",
``lift_left (f o g) x = lift_left f (lift_left g x)``,
Cases_on `x` >> simp[definition "lift_left_def", definition "bind_left_def"])
Cases_on `x` >> simp[definition "lift_left_def"])
val lift_right_def = Define`
lift_right (f : α -> β) (sum : γ + α) : γ + β =
......@@ -115,14 +116,15 @@ val right_list_def = Define`
(* Monad laws for bind_left: left identity, right identity, and associativity *)
val bind_left_monad_left_id = store_thm("bind_left_monad_left_id[simp]",
``bind_left (INL a) f = f a``,
simp[definition "bind_left_def"])
``bind_left (INL a) f = f a``, simp[])
val bind_left_monad_right_id = store_thm("bind_left_monad_right_id[simp]",
``bind_left m INL = m``,
Cases_on `m` >> simp[definition "bind_left_def"])
Cases_on `m` >> simp[])
val bind_left_monad_assoc = store_thm("bind_left_monad_assoc",
``bind_left (bind_left m f) g = bind_left m (λx. bind_left (f x) g)``,
Cases_on `m` >> simp[definition "bind_left_def"])
Cases_on `m` >> simp[])
val _ = computeLib.add_funs[
]
(* Monad laws for bind_right: left identity, right identity, and associativity *)
val bind_right_monad_left_id = store_thm("bind_right_monad_left_id[simp]",
......@@ -155,7 +157,7 @@ val bind_left_unit_INL = store_thm("bind_left_unit_INL[simp]",
``monad_unitbind (INL a) b = b``, simp[])
val bind_left_unit_INR = store_thm("bind_left_unit_INR[simp]",
``monad_unitbind (INR a) b = INR a``, simp[definition "bind_left_def"])
``monad_unitbind (INR a) b = INR a``, simp[])
val _ = export_theory()
......@@ -2,7 +2,7 @@ open HolKernel Parse boolLib bossLib;
open arithmeticTheory
open optionTheory
open patriciaTheory
open sptreeTheory
open wordsTheory
open uvmTypesTheory
......@@ -125,23 +125,23 @@ val (canconvert_rules, canconvert_ind, canconvert_cases) = Hol_reln`
*)
`
val _ = type_abbrev("bytes", ``:num # word8 ptree``)
val _ = type_abbrev("bytes", ``:num # word8 spt``)
val new_bytes_def = Define `new_bytes : bytes = (0, <{}>)`
val new_bytes_def = Define `new_bytes : bytes = (0, LN)`
val append_bytes_def = Define`
append_bytes : bytes -> word8 option list -> bytes =
FOLDL (λ(n, t) b. (SUC n, case b of SOME b => t |+ (n, b) | NONE => t))
FOLDL (λ(n, t) b. (SUC n, case b of SOME b => insert n b t | NONE => t))
`
val read_bytes_def = Define`
read_bytes ((_, t) : bytes) (start : num) (len : num) : word8 list option =
FOLDR (OPTION_MAP2 CONS) (SOME []) (GENLIST (PEEK t o $+ start) len)
FOLDR (OPTION_MAP2 CONS) (SOME []) (GENLIST (λn. lookup (start + n) t) len)
`
val write_bytes_def = Define`
write_bytes ((n, t) : bytes) (start : num) (bs : word8 option list) : bytes =
let t' = FOLDL (λt b. case b of SOME b => t |+ (n, b) | NONE => t) t bs in
let t' = FOLDL (λt b. case b of SOME b => insert n b t | NONE => t) t bs in
(MAX n (start + LENGTH bs), t')
`
......
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
......@@ -253,6 +253,19 @@ val (native_safe_rules, native_safe_ind, native_safe_cases) = Hol_reln`
native_safe (Struct fx tys))
`
(*
maybe_vector : (uvm_type -> bool) -> uvm_type -> bool
"maybe_vector P ty" checks to see if P is true of ty. Alternatively,
if ty is a vector type, it checks to see if P is true of the element
type of the vector
*)
val maybe_vector_def = Define`
maybe_vector P ty
P ty case ty of Vector ty0 _ => P ty0 | _ => F
`
(* A type is valid ("ok") if it meets the following criteria:
∙ Ints, arrays, and vectors have a length > 0.
......@@ -352,15 +365,9 @@ val scalar_prefix_def = Define`
scalar_prefix t = t
`
(* The function "component_types" is a special case: although it is similar to
"member_types" in that it returns a list of types, it does not necessarily
return *all* possible components of a type.
(* The function "component_types" returns a list of lists, representing the
types that can be used to access each offset of the parent type.
It flattens nested composite types into scalar type cells, with the start
locations of composite types replaced with the largest composite type at that
location. The set of all components of a type T is the set of all prefixes of
the types in "component_types T".
This is the format that uvmMemoryTheory uses to represent typed cells in the
memory.
*)
......@@ -385,8 +392,9 @@ val _ = DefnBase.add_cong LIST_BIND_CONG
val component_types_def = TotalDefn.tDefine "component_types" `
component_types sz t =
case member_types sz t of
| [] => [t]
| ts => t::TL (LIST_BIND ts (component_types NONE))
| [] => [[t]]
| ts => (let ts' = LIST_BIND ts (component_types NONE) in
SNOC t (HD ts')::TL ts')
` (WF_REL_TAC `measure (uvm_type_depth o SND)` >> prove_tac[member_types_depth])
val max_offset_def = Define `max_offset = LENGTH o component_types NONE`
......
open HolKernel Parse boolLib bossLib
open wordsTheory
open uvmTypesTheory
open uvmErrorsTheory
open sumMonadTheory
open comparisonTheory
open wordsTheory
open monadsyntax
open DefineUtils
......@@ -85,6 +87,15 @@ val zero_value_def = Define`
val _ = type_abbrev("value_or_error", ``:((α, β, σ, τ) gen_value, α, β) errorM``)
val compare_unsigned_values_def = Define`
compare_unsigned_values (IntV _ v1 : (α, β, σ, τ) gen_value)
(IntV _ v2 : (α, β, σ, τ) gen_value)
: (cpn, α, β) errorM =
return (num_cmp v1 v2)
compare_unsigned_values v1 v2 =
Fail (TypeMismatch "comparison" (type_of_value v1) (type_of_value v2))
`
val int_op_def = Define`
int_op (op : num -> num)
(IntV sz n : (α, β, σ, τ) gen_value)
......@@ -153,8 +164,8 @@ val shift_iaddr_def = Define`
val shift_iref_def = Define`
shift_iref (IRefV r a : (α, β, σ, τ) gen_value)
(IntV _ n : (α, β, σ, τ) gen_value)
: (α, β, σ, τ) value_or_error =
(IntV _ n : (α, β, σ, τ) gen_value)
: (α, β, σ, τ) value_or_error =
IRefV r o SOME <$> (expect a NullReference >>= C shift_iaddr n)
shift_iref (IRefV _ _) v = Fail (NotInt "shift_iref" (type_of_value v))
shift_iref v _ = Fail (NotIRef (type_of_value v))
......
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