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

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

Almost final version of paper?

parent c4e557c9
......@@ -11,20 +11,31 @@
\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
%%% PACKAGES
\usepackage{booktabs} % for much better looking tables
\usepackage{array} % for better arrays (eg matrices) in maths
%\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
\usepackage{alltt}
\usepackage{amsmath}
\usepackage{mathtools}
\usepackage{amsthm}
\usepackage{textcomp}
%\usepackage{sidecap}
% Theorems and lemmas
\theoremstyle{plain}
\newtheorem{thm}{Theorem}[subsection]
\newtheorem{lem}[thm]{Lemma}
% Thanks to http://tex.stackexchange.com/a/26350
\begingroup
\makeatletter
\@for\theoremstyle:=definition,remark,plain\do{%
\expandafter\g@addto@macro\csname th@\theoremstyle\endcsname{%
\addtolength\thm@preskip\parskip
}%
}
\endgroup
% Borders on figures
\usepackage{float}
......@@ -36,8 +47,8 @@
%%% HEADERS & FOOTERS
\usepackage{fancyhdr} % This should be set AFTER setting up the page geometry
\pagestyle{fancy} % options: empty , plain , fancy
\renewcommand{\headrulewidth}{0pt} % customise the layout...
\pagestyle{fancy} % options: empty, plain, fancy
\renewcommand{\headrulewidth}{0pt} % customize the layout...
\lhead{}\chead{}\rhead{}
\lfoot{}\cfoot{\thepage}\rfoot{}
......
<| 2 \textlangle\!|\,
|> 2 \,|\!\textrangle
o_f 2 \ensuremath{\circ{}_f}
......@@ -4,6 +4,7 @@ open uvmMemoryTheory
open uvmThreadsStacksTheory
open uvmInstructionSemanticsTheory
open monadsyntax
open arithmeticTheory
open pred_setTheory
open finite_mapTheory
open listTheory
......@@ -87,7 +88,7 @@ val resolved_resolvable_disjoint = store_thm("resolved_resolvable_disjoint",
val add_resolved_decreases_unresolved = store_thm("add_resolved_decreases_unresolved",
``extras FEMPTY FDOM extras FDOM (resolvable_locations s)
FDOM (unresolved_locations (s with memory updated_by
(λm. m with resolved updated_by C $FUNION extras)))
(λm. m with resolved updated_by λr. FUNION r extras)))
FDOM (unresolved_locations s)``,
rw[unresolved_locations_def, resolvable_locations_def, all_locations_def] >>
fs[DRESTRICT_DEF, RRESTRICT_DEF, SUBSET_DEF, PSUBSET_DEF] >>
......@@ -97,8 +98,10 @@ val add_resolved_decreases_unresolved = store_thm("add_resolved_decreases_unreso
val resolve_once_def = Define`
resolve_once (s : sched_state) : sched_state =
s with memory updated_by (λm. m with resolved updated_by C $FUNION
((liftM THE o resolve_symbolic s.memory) o_f resolvable_locations s))
s with memory updated_by (λm.
m with resolved updated_by (λr.
FUNION r ((λs'. THE <$> resolve_symbolic s.memory s')
o_f resolvable_locations s)))
`
val resolve_once_ok = store_thm("resolve_once_ok",
......@@ -108,25 +111,26 @@ val resolve_once_ok = store_thm("resolve_once_ok",
val resolve_once_decreases_unresolved = store_thm("resolve_once_decreases_unresolved",
``FCARD (unresolved_locations (resolve_once s)) < FCARD (unresolved_locations s)
s = resolve_once s``,
rw[resolve_once_def, FCARD_DEF] >>
rw[resolve_once_def] >>
Cases_on `resolvable_locations s = FEMPTY` >> fs[]
>- rw[FUNION_FEMPTY_2, memory_component_equality, theorem "sched_state_component_equality"]
>- (Q.ABBREV_TAC `extras = (liftM THE o resolve_symbolic s.memory) o_f resolvable_locations s` >>
>- simp[memory_component_equality, theorem "sched_state_component_equality"]
>- (Q.ABBREV_TAC `extras =
(λs'. THE <$> resolve_symbolic s.memory s') o_f resolvable_locations s` >>
`extras FEMPTY FDOM extras FDOM (resolvable_locations s)` suffices_by
rw[add_resolved_decreases_unresolved, CARD_PSUBSET] >>
rw[FCARD_DEF, add_resolved_decreases_unresolved, CARD_PSUBSET] >>
Q.UNABBREV_TAC `extras` >> rw[] >> metis_tac[FDOM_o_f, FDOM_EQ_EMPTY]))
val resolve_terminates_when_fcard_eq = store_thm("resolve_terminates_when_fcard_eq",
``s' = resolve_once s (FCARD s.memory.resolved = FCARD s'.memory.resolved s = s')``,
rw[resolve_once_def, memory_component_equality, FCARD_DEF, theorem "sched_state_component_equality"] >>
rw[resolve_once_def, memory_component_equality, theorem "sched_state_component_equality"] >>
Cases_on `resolvable_locations s = FEMPTY` >> fs[] >>
Q.MATCH_ABBREV_TAC `a b` >> `¬a ¬b` suffices_by simp[] >>
Q.UNABBREV_TAC `a` >> Q.UNABBREV_TAC `b` >> rw[]
MATCH_MP_TAC (prove(``¬a ¬b (a b)``, simp[])) >> rw[]
>- (`FDOM s.memory.resolved FDOM (resolvable_locations s) = `
by metis_tac[resolved_resolvable_disjoint, DISJOINT_DEF] >>
`CARD (FDOM (resolvable_locations s)) 0`
by metis_tac[FCARD_DEF, FCARD_0_FEMPTY] >>
rw[CARD_UNION_EQN, CARD_EMPTY, FDOM_FINITE])
`FCARD (resolvable_locations s) 0`
by metis_tac[FCARD_0_FEMPTY] >>
fs[FCARD_DEF, CARD_EQ_0, CARD_UNION_EQN, CARD_EMPTY, FDOM_FINITE] >>
metis_tac[CARD_EQ_0, FDOM_FINITE, ADD_INV_0_EQ])
>- (`FDOM s.memory.resolved FDOM s.memory.resolved FDOM (resolvable_locations s)`
suffices_by metis_tac[fmap_EQ, FDOM_o_f, FDOM_FUNION] >>
`x. x FDOM (resolvable_locations s)` by metis_tac[FDOM_EQ_EMPTY, MEMBER_NOT_EMPTY] >>
......@@ -251,7 +255,7 @@ val extract_all_distinct_filter = store_thm("extract_all_distinct_filter",
rw[extract_def] >> simp[FILTER_EQ_APPEND] >>
qexists_tac `TAKE n xs` >> qexists_tac `DROP n xs` >> fs[] >>
`DROP n xs = EL n xs::DROP (SUC n) xs` by
metis_tac[rich_listTheory.DROP_EL_CONS, arithmeticTheory.ADD1] >>
metis_tac[rich_listTheory.DROP_EL_CONS, ADD1] >>
rw[FILTER_EQ_ID, EVERY_MEM, MEM_EL]
>- (Cases_on `n' < n` >>
fs[rich_listTheory.EL_TAKE, ALL_DISTINCT_EL_IMP])
......@@ -347,7 +351,7 @@ val stacks_ok_snoc = store_thm("stacks_ok_snoc",
``s ss. s.id = Stack (LENGTH ss) stack_ok s stacks_ok ss
stacks_ok (SNOC s ss)``,
rw[stacks_ok_def, EVERY_SNOC] >>
metis_tac[GENLIST, SNOC_APPEND, arithmeticTheory.ADD1])
metis_tac[GENLIST, SNOC_APPEND, ADD1])
(* This is it: the most complicated proof in the file. This proof establishes
that all thread and stack invariants are preserved on every step of
......@@ -728,7 +732,6 @@ val fair_finite_def = Define`
local
open listTheory
open optionTheory
open arithmeticTheory
open pred_setTheory
val fair_bounded_lemma = Q.prove(
......@@ -897,8 +900,12 @@ val single_thread_seq_cst_schedule_local_seq_cst = store_thm(
`∃m. m < len ∧ step = EL m fs`
by metis_tac[LTAKE_LENGTH, listTheory.MEM_EL] >>
Induct_on `len` >> fs[] >> rw[] >>
metis_tac[cycle_lnth, listTheory.MEM_EL, arithmeticTheory.MOD_LESS, ]
metis_tac[cycle_lnth, listTheory.MEM_EL, MOD_LESS, ]
fs[run_finite_schedule_def, init_sched_state_def]
*)
(* For some reason HOL doesn't define this symbol by default... *)
val _ = TeX_notation{hol="⊌", TeX=("\\ensuremath{\\uplus}", 1)}
val _ = export_theory()
......@@ -168,21 +168,15 @@ val enqueue_action_follows = store_thm("enqueue_action_follows",
val enqueue_action_ok = store_thm("enqueue_action_ok",
``r. propagates thread_ok (enqueue_action r)``,
rw[propagates_def, thread_ok_def, enqueue_action_def] >> fs[EVERY_SNOC, C_DEF, o_DEF]
rw[propagates_def, thread_ok_def, enqueue_action_def, EVERY_SNOC, SNOC_APPEND,
C_DEF, o_DEF]
>- metis_tac[]
>- (POP_ASSUM (K ALL_TAC) >> POP_ASSUM MP_TAC >>
Q.MATCH_ABBREV_TAC `EVERY P a.outbox EVERY Q a.outbox` >>
`x. P x Q x` by metis_tac[action_id_lt_suc, action_id_lt_trans] >>
metis_tac[EVERY_MONOTONIC])
>- (Q.MATCH_ABBREV_TAC `SORTED R (SNOC (a.action_id, r) a.outbox)` >>
Cases_on `a.outbox = []` >> rw[SNOC_APPEND] >>
`0 < LENGTH a.outbox` by metis_tac[LENGTH_NIL, LESS_0_CASES] >>
`transitive R R (LAST a.outbox) (a.action_id, r)`
suffices_by fs[SORTED_APPEND_IFF] >>
Q.UNABBREV_TAC `R` >> rw[]
>- (rw[transitive_def, action_id_lt_def] >>
REPEAT (POP_ASSUM MP_TAC) >> REPEAT CASE_TAC >> rw[])
>- fs[LAST_EL, EVERY_EL, INV_PRE_LESS]))
>- (first_x_assum (fn x => mp_tac x >> match_mp_tac EVERY_MONOTONIC) >>
metis_tac[action_id_lt_suc, action_id_lt_trans])
>- (Cases_on `a.outbox = []` >> rw[] >>
match_mp_tac SORTED_APPEND >> rw[]
>- (rw[transitive_def] >> metis_tac[action_id_lt_trans])
>- fs[MEM_EL, EVERY_EL]))
val get_block_def = Define`
get_block (label : block_label)
......
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