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

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

Further work on the synthesis paper

parent 49d68678
......@@ -55,7 +55,9 @@ struct
num_infixes_defined := true
) else ();
overload_on("≺", ``^lt``);
overload_on("≼", ``λl r. (^lt l r) (l = r)``)
overload_on("≼", ``λl r. (^lt l r) (l = r)``);
TeX_notation {hol="≺", TeX=("\\ensuremath{\\prec}", 1)};
TeX_notation {hol="≼", TeX=("\\ensuremath{\\preceq}", 1)}
end
fun QDefine(quoted : string frag list) =
......@@ -102,7 +104,7 @@ struct
in
if not (!monad_infixes_defined) then (
set_fixity ">>=" (Infixl 660);
set_fixity ">>" (Infixl 660);
set_fixity "*>" (Infixl 660);
set_fixity "<$>" (Infixl 661);
monad_infixes_defined := true
) else ();
......@@ -110,7 +112,7 @@ struct
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("*>", ``monad_unitbind``);
overload_on("liftM", Term [QUOTE lift_name]);
overload_on("join", Term [QUOTE join_name]);
overload_on("sequence", Term [QUOTE sequence_name]);
......
......@@ -20,7 +20,7 @@ $(holdirfile):
echo "$$holdir" > $(holdirfile)
$(thy_files): $(holdirfile) $(thy_srcs)
cd $(thy_dir); $(shell cat $(holdirfile))/bin/Holmake
cd $(thy_dir); Holmake
munge.exe: $(holdirfile) $(thy_files)
$(shell cat $(holdirfile))/bin/mkmunge.exe $(thy_names)
......@@ -28,15 +28,21 @@ munge.exe: $(holdirfile) $(thy_files)
synthesis.htex: synthesis.md
pandoc $(pandoc_opts) --toc --to=latex -o synthesis.htex synthesis.md
# There's some regex voodoo below; it does two things:
# - The first `sed` replaces `%HOLIMPORT` in the header with an import.
# - The second and third `sed`s escape some underscores that HOL's munger doesn't.
synthesis.tex: munge.exe synthesis.htex header.tex
cp -f header.tex synthesis.tex
./munge.exe < synthesis.htex >> synthesis.tex
sed s:%HOLIMPORT:\\\\usepackage{$(shell cat $(holdirfile))/src/TeX/holtexbasic}: \
< header.tex > synthesis.tex
./munge.exe overrides.txt -w86 < synthesis.htex \
| sed 's/{\([a-z_]\+\)_/{\1\\_/g' \
| sed 's/{\([a-z_]\+\)_/{\1\\_/g' >> synthesis.tex
echo '\end{document}' >> synthesis.tex
synthesis.pdf: synthesis.tex
pdflatex synthesis.tex
#pandoc $(pandoc_opts) -o synthesis.pdf synthesis.tex
clean:
rm synthesis.htex synthesis.tex synthesis.pdf
rm -f synthesis.htex synthesis.tex synthesis.aux synthesis.pdf munge.exe
cd $(thy_dir); Holmake clean
......@@ -8,12 +8,12 @@
\usepackage[utf8]{inputenc} % set input encoding (not needed with XeLaTeX)
%%% PAGE DIMENSIONS
\usepackage{geometry}
\usepackage[margin=1in]{geometry}
\geometry{letterpaper}
\usepackage{graphicx} % support the \includegraphics command and options
% \usepackage[parfill]{parskip} % Activate to begin paragraphs with an empty line rather than an indent
\usepackage[parfill]{parskip} % Activate to begin paragraphs with an empty line rather than an indent
%%% PACKAGES
\usepackage{booktabs} % for much better looking tables
......@@ -21,7 +21,18 @@
%\usepackage{paralist} % very flexible & customisable lists (eg. enumerate/itemize, etc.)
\usepackage{verbatim} % adds environment for commenting out blocks of text & for better verbatim
\usepackage{subfig} % make it possible to include more than one captioned figure/table in a single float
% These packages are all incorporated in the memoir class to one degree or another...
\usepackage{alltt}
\usepackage{amsmath}
\usepackage{textcomp}
%\usepackage{sidecap}
% Borders on figures
\usepackage{float}
\floatstyle{boxed}
\restylefloat{figure}
% Don't delete the below comment; the Makefile replaces it with an import.
%HOLIMPORT
%%% HEADERS & FOOTERS
\usepackage{fancyhdr} % This should be set AFTER setting up the page geometry
......
<| 2 \textlangle\!|\,
|> 2 \,|\!\textrangle
......@@ -602,14 +602,18 @@ val _ = Datatype`
body: σ instruction list;
exit: σ terminst;
keepalives: σ list
|> ;
|>
`
val _ = Datatype`
function = <|
signature: funcsig;
entry_block: block_label;
blocks: block_label |-> ssavar bblock
|> ;
|>
`
val _ = Datatype`
environment = <|
globals: (global_name # uvm_type) list;
constants: const_name |-> (uvm_type # value);
......
......@@ -13,7 +13,6 @@ open pairTheory
open optionTheory
open finite_mapTheory
open pred_setTheory
open string_numTheory
open lcsymtacs
open monadsyntax
......@@ -133,7 +132,7 @@ val eval_expr_def = Define`
| ShuffleVector _ _ _ _ _ => pure (Fail (NotImplemented "SHUFFLEVECTOR"))
| GetIRef ty ref =>
(λref. case ref of RefV ty' (SOME a) =>
assert_type_eq ty ty' "GETIREF" >>
assert_type_eq ty ty' "GETIREF" *>
return [IRefV REF (SOME <|
base := a; base_ty := ty; ty := ty; offsets := []
|>)]
......@@ -394,7 +393,7 @@ val exec_terminst_def = Define`
assert (sig = sig') (TypeMismatch "uvm.new_stack function signature"
(FuncRef REF sig) (FuncRef REF sig'));
new_stack <-
let args = GENLIST (λn. %(n2s n)#0) (LENGTH sig.arg_types) in
let args = GENLIST (λn. %(num_str n)0) (LENGTH sig.arg_types) in
push_frame env name (ZIP (sig.arg_types, args)) (MAP Var args) (<|
id := Stack (LENGTH stacks);
frames := [];
......
......@@ -44,28 +44,34 @@ val _ = add_rule {term_name = "%",
block_style = (AroundEachPhrase, (PP.CONSISTENT, 0))}
val _ = add_rule {term_name = "#",
fixity = Infixl 770,
pp_elements = [TOK "#"],
pp_elements = [TOK ""],
paren_style = OnlyIfNecessary,
block_style = (AroundEachPhrase, (PP.CONSISTENT, 0))}
val _ = TeX_notation {hol="%", TeX=("\\%", 1)}
val _ = TeX_notation {hol="№", TeX=("\\#", 1)}
val _ = overload_on("%", ``SSA``)
val _ = overload_on("#", ``(λa b. (a, Block b)) : ssavar -> num -> register``)
val _ = Datatype`
resume_values =
| NOR (α list)
| EXC (α list) α ;
| EXC (α list) α
`
val _ = Datatype`
location =
| Register thread_id register
| Memory (thread_id option) action_id ;
input_location =
| At location
| Before (thread_id option) action_id ;
| Before (thread_id option) action_id
`
(* Memory order (see the spec)
https://github.com/microvm/microvm-spec/blob/master/memory-model.rest#memory-operations
*)
(* 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
......@@ -73,11 +79,13 @@ val _ = Datatype`
| ACQUIRE
| RELEASE
| ACQ_REL
| SEQ_CST ;
| SEQ_CST
`
(* AtomicRMW operators (see the spec)
https://github.com/microvm/microvm-spec/blob/master/instruction-set.rest#atomicrmw-instruction
*)
(* 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 *)
......@@ -89,7 +97,18 @@ val _ = Datatype`
| RMW_MAX (* <int> - signed max *)
| RMW_MIN (* <int> - signed min *)
| RMW_UMAX (* <int> - unsigned max *)
| RMW_UMIN (* <int> - unsigned min *) ;
| 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)
`
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
......@@ -107,8 +126,6 @@ val _ = Datatype`
| DoGlobalInit global_name uvm_type
| DoNewThread (stack_id symbolic) (value symbolic resume_values) ;
message = Message (thread_id option) action_id action ;
cmp_xchg_action_args = <|
addr: location;
strength: strength;
......@@ -118,8 +135,6 @@ val _ = Datatype`
desired: value symbolic
|> ;
strength = STRONG | WEAK ;
atomic_rmw_action_args = <|
addr: location;
order: memory_order;
......@@ -127,11 +142,10 @@ val _ = Datatype`
opnd: location
|> ;
(* "α 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) ;
strength = STRONG | WEAK
`
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.
......@@ -144,7 +158,7 @@ val _ = Datatype`
(* Core symbolic operations *)
val pure_symbolic_def = Define `pure_symbolic : α -> α symbolic = Symbolic [] o K o OK`
val _ = overload_on("pure", ``λv. Symbolic [] (K (OK v))``)
val apply_symbolic_def = Define`
apply_symbolic (Symbolic locs fn) (Symbolic locs' a) =
......@@ -153,10 +167,9 @@ val apply_symbolic_def = Define`
`
val lift_symbolic_def = Define`
lift_symbolic : (α -> β) -> α symbolic -> β symbolic = apply_symbolic o pure_symbolic
lift_symbolic : (α -> β) -> α symbolic -> β symbolic = apply_symbolic o pure
`
val _ = overload_on("pure", ``pure_symbolic``)
val _ = overload_on("APPLICATIVE_FAPPLY", ``apply_symbolic``)
val _ = overload_on("<$>", ``lift_symbolic``)
......@@ -366,7 +379,7 @@ val drop_drop_lemma = prove(
val well_behaved_pure = store_thm("well_behaved_pure[simp]",
``well_behaved_symbolic (pure x)``,
simp[well_behaved_symbolic_def, pure_symbolic_def])
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)``,
......@@ -399,25 +412,25 @@ val well_behaved_await_before = store_thm("well_behaved_await_before[simp]",
(* Applicative laws for symbolic *)
val symbolic_identity = store_thm("symbolic_identity",
``pure_symbolic I <*> v = v``,
Cases_on `v` >> simp[pure_symbolic_def, apply_symbolic_def, ap_left_def] >>
``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_symbolic f <*> pure x = pure (f x)``,
simp[pure_symbolic_def, apply_symbolic_def, ap_left_def] >>
``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_symbolic (λx. x y) <*> u = u <*> pure y``,
``well_behaved_symbolic u pure (λx. x y) <*> u = u <*> pure y``,
Cases_on `u` >>
rw[well_behaved_symbolic_def, pure_symbolic_def, apply_symbolic_def, ap_left_def])
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_symbolic $o <*> u <*> v <*> w = u <*> (v <*> w)``,
pure $o <*> u <*> v <*> w = u <*> (v <*> w)``,
Cases_on `u` >> Cases_on `v` >> Cases_on `w` >>
rw[well_behaved_symbolic_def, pure_symbolic_def, apply_symbolic_def, ap_left_composition] >>
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 *)
......
......@@ -17,15 +17,19 @@ val _ = reveal "C" (* The C (flip) combinator is used in this theory *)
val _ = Datatype`
sched_step =
| Commit thread_id num
| Proceed thread_id (value option) ;
| Proceed thread_id (value option)
`
val _ = Datatype`
sched_state = <|
env: environment;
threads: thread option list;
stacks: stack list;
memory: memory
|> ;
|>
`
val _ = Datatype`
program = <|
env: environment;
main: func_name;
......@@ -197,7 +201,7 @@ val init_sched_state_def = Define`
do
fn <- lookup_function p.env p.main;
st <- (
let args = GENLIST (λn. %(n2s n)#0) (LENGTH fn.signature.arg_types)
let args = GENLIST (λn. %(num_str n)0) (LENGTH fn.signature.arg_types)
in push_frame p.env p.main (ZIP (fn.signature.arg_types, args)) (MAP Var args) st);
return (<|
env := p.env;
......@@ -475,7 +479,7 @@ val get_global_value_def = Define`
let id = action_id_suc (FOLDR (λm a.
case m of Message _ a' _ => if a a' then a' else a)
(Action 0) state.memory.committed) in
let reg = Register (Thread (LENGTH state.threads)) (%"result"#0) in
let reg = Register (Thread (LENGTH state.threads)) (%"result"0) in
state with memory updated_by (λm. m with <|
resolved updated_by C $|+ (reg, return (IRefV REF (SOME <|
base := GlobalAddr (Global name);
......
......@@ -15,7 +15,6 @@ open optionTheory
open pairTheory
open pred_setTheory
open relationTheory
open string_numTheory
open sortingTheory
open lcsymtacs
open monadsyntax
......@@ -32,21 +31,27 @@ val _ = Datatype`
action_id: action_id;
registers: register |-> value symbolic;
outbox: (action_id # action) list
|> ;
|>
`
val _ = Datatype`frame_id = Frame num stack_id`
frame_id = Frame num stack_id ;
val _ = Datatype`
frame_state =
| READY ((uvm_type # register) list) (register resumption_data)
| ACTIVE (register terminst)
| DEAD (value symbolic resume_values option)
`
val _ = Datatype`
frame = <|
id: frame_id;
fn: function;
state: frame_state
|> ;
frame_state =
| READY ((uvm_type # register) list) (register resumption_data)
| ACTIVE (register terminst)
| DEAD (value symbolic resume_values option) ;
|>
`
val _ = Datatype`
stack = <|
id: stack_id;
frames: frame list;
......@@ -246,6 +251,13 @@ val pop_frame_ok = store_thm("pop_frame_ok",
``stack_ok s stack_ok (pop_frame s)``,
Cases_on `s.frames` >> rw[stack_ok_def, pop_frame_def])
val num_str_def = TotalDefn.tDefine "num_str" `
num_str 0 = "0" num_str 1 = "1" num_str 2 = "2" num_str 3 = "3"
num_str 4 = "4" num_str 5 = "5" num_str 6 = "6" num_str 7 = "7"
num_str 8 = "8" num_str 9 = "9"
num_str n = STRCAT (num_str (n DIV 10)) (num_str (n MOD 10))
` (WF_REL_TAC `$<` >> rw[] >> `v MOD 10 < 10` by simp[] >> simp[])
val insert_resume_args_def = Define`
insert_resume_args ((_, destargs) : register destination)
(input_args : (uvm_type # register) list)
......@@ -260,12 +272,19 @@ val insert_resume_args_def = Define`
if i < LENGTH args
then EL i args
else symbolic_or_error (Fail (InvalidState
(STRCAT "PASS_VALUES missing argument #" (n2s i))))
(STRCAT "PASS_VALUES missing argument #" (num_str i))))
| NONE => sym_value th arg)
| Const c => pure c
in MAP f destargs
`
val to_ref_void_def = Define`
to_ref_void e =
case e of
| RefV _ a => return (RefV Void a)
| _ => Fail (TypeMismatch "exception" (Ref (Type Void)) (type_of_value e))
`
val resume_frame_def = Define`
resume_frame (fr : frame)
(res : value symbolic resume_values)
......@@ -280,11 +299,7 @@ val resume_frame_def = Define`
case res of
| NOR args => return (args, NONE, rd.normal_dest)
| EXC args exc =>
let exc = symbolic_error_join (
(λe. case e of
| RefV _ a => return (RefV Void a)
| _ => Fail (TypeMismatch "exception"
(Ref (Type Void)) (type_of_value e))) <$> exc) in
let exc = symbolic_error_join (to_ref_void <$> exc) in
expect rd.exceptional_dest (UndefinedBehavior "uncaught exception")
:> liftM (λdest. (args, SOME exc, dest));
block <- get_block (FST dest) fr.fn th;
......@@ -313,7 +328,7 @@ val resume_frame_follows = store_thm("resume_frame_follows",
``(i t0 t1. exec i t0 = OK t1 thread_follows t0 t1)
resume_frame f0 r exec t0 = OK (f1, t1)
thread_follows t0 t1``,
rw[resume_frame_def] >> Cases_on `f0.state` >> fs[] >>
rw[resume_frame_def, to_ref_void_def] >> Cases_on `f0.state` >> fs[] >>
Cases_on `r` >> fs[] >> rw[] >> fs[] >>
Q.ABBREV_TAC `t0' = t0 with block_id updated_by block_id_suc` >>
`thread_follows t0 t0'`
......
......@@ -112,7 +112,7 @@ val zero_value_def = TotalDefn.tDefine "zero_value" `
val simple_int_binop_def = Define`
simple_int_binop name op (IntV sz1 n1) (IntV sz2 n2) =
assert_type_eq (Int sz1) (Int sz2) name >>
assert_type_eq (Int sz1) (Int sz2) name *>
return (IntV sz1 (op n1 n2 && n2w (2 ** sz1 - 1)))
simple_int_binop name _ (IntV sz _) rhs =
Fail (TypeMismatch name (Int sz) (type_of_value rhs))
......@@ -137,8 +137,8 @@ val value_ashr_def = Define`
val value_udiv_def = Define`
value_udiv (IntV sz1 n1) (IntV sz2 n2) =
assert_type_eq (Int sz1) (Int sz2) "UDIV" >>
assert (n2 0w) DivideByZero >>
assert_type_eq (Int sz1) (Int sz2) "UDIV" *>
assert (n2 0w) DivideByZero *>
return (IntV sz1 (word_div n1 n2))
value_udiv (IntV sz _) rhs =
Fail (TypeMismatch "UDIV" (Int sz) (type_of_value rhs))
......@@ -147,8 +147,8 @@ val value_udiv_def = Define`
val value_urem_def = Define`
value_urem (IntV sz1 n1) (IntV sz2 n2) =
assert_type_eq (Int sz1) (Int sz2) "UREM" >>
assert (n2 0w) DivideByZero >>
assert_type_eq (Int sz1) (Int sz2) "UREM" *>
assert (n2 0w) DivideByZero *>
return (IntV sz1 (word_div n1 n2))
value_urem (IntV sz _) rhs =
Fail (TypeMismatch "UREM" (Int sz) (type_of_value rhs))
......@@ -161,7 +161,7 @@ val value_urem_def = Define`
val simple_int_cmpop_def = Define`
simple_int_cmpop name op (IntV sz1 n1) (IntV sz2 n2) =
assert_type_eq (Int sz1) (Int sz2) name >>
assert_type_eq (Int sz1) (Int sz2) name *>
return (IntV 1 (if op n1 n2 then 1w else 0w))
simple_int_cmpop name _ (IntV sz _) rhs =
Fail (TypeMismatch name (Int sz) (type_of_value rhs))
......@@ -175,13 +175,13 @@ val value_ule_def = Define `value_ule = simple_int_cmpop "ULE" word_le`
val value_eq_def = Define`
value_eq v1 v2 =
assert_type_eq (type_of_value v1) (type_of_value v2) "EQ" >>
assert_type_eq (type_of_value v1) (type_of_value v2) "EQ" *>
return (IntV 1 (if v1 = v2 then 1w else 0w))
`
val value_ne_def = Define`
value_ne v1 v2 =
assert_type_eq (type_of_value v1) (type_of_value v2) "NE" >>
assert_type_eq (type_of_value v1) (type_of_value v2) "NE" *>
return (IntV 1 (if v1 v2 then 1w else 0w))
`
......@@ -196,19 +196,19 @@ val value_offset_get_def = Define`
let out_of_bounds = ReadOutOfBounds (type_of_value v) off in
case v of
| ArrayV t vs =>
assert (off < LENGTH vs) out_of_bounds >>
assert (off < LENGTH vs) out_of_bounds *>
return (EL off vs)
| VectorV t vs =>
assert (off < LENGTH vs) out_of_bounds >>
assert (off < LENGTH vs) out_of_bounds *>
return (EL off vs)
| HybridV fvs vt vvs =>
if (off < LENGTH fvs) then
return (FST (EL off fvs))
else
assert (off < (LENGTH fvs + LENGTH vvs)) out_of_bounds >>
assert (off < (LENGTH fvs + LENGTH vvs)) out_of_bounds *>
return (EL (off - LENGTH fvs) vvs)
| StructV _ vs =>
assert (off < LENGTH vs) out_of_bounds >>
assert (off < LENGTH vs) out_of_bounds *>
return (FST (EL off vs))
| _ => Fail out_of_bounds
`
......
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