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

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

Prove local seq consistency for seq_cst_schedule

It's finally done! The first memory consistency proof in the formalization:
a sequentially consistent schedule (one that always commits memory messages
from the front of a thread's outbox queue) will always produce locally
sequentially consistent semantics.

Changes made in the process of this proof include:

- Removed thread IDs and stack IDs from the thread and stack records;
  keeping up with invariants for them was pointless bookkeeping

- Defined custom tactics multi_case_tac and rw_assums, which greatly
  reduced the size and complexity of some proofs

- Added several new invariants to state_ok, including memory consistency
  invariants (committed messages are all distinct, no message can be in
  both the commit list and a thread's outbox, etc.)
parent 8099d33f
open HolKernel
open HolKernel bossLib
signature DefineUtils =
sig
val pair_case_tac : tactic
val multi_case_tac : tactic
val rw_assums : thm list -> tactic
val define_sum : string * string * hol_type * string * hol_type -> unit
val define_num_newtype : string * string -> unit
......
......@@ -7,6 +7,22 @@ struct
val num_infixes_defined: bool ref = ref false
val monad_infixes_defined: bool ref = ref false
val pair_case_tac =
qpat_assum `_ (_: α # β) = _` (fn a =>
let val v = concl a |> lhs |> dest_comb |> #2 in
if pairSyntax.is_pair v then NO_TAC else Cases_on `^v`
end) ORELSE
qpat_assum `_ = _ (_: α # β)` (fn a =>
let val v = concl a |> rhs |> dest_comb |> #2 in
if pairSyntax.is_pair v then NO_TAC else Cases_on `^v`
end)
val multi_case_tac =
REPEAT ((BasicProvers.FULL_CASE_TAC ORELSE pair_case_tac) >> fs[] >> rw[])
fun rw_assums xs =
POP_ASSUM_LIST (map_every (assume_tac o REWRITE_RULE xs) o rev)
fun define_sum(name : string, inl : string, inl_ty : hol_type, inr : string,
inr_ty : hol_type) : unit =
let
......
This diff is collapsed.
......@@ -52,6 +52,16 @@ val _ = TeX_notation {hol="№", TeX=("\\#", 1)}
val _ = overload_on("%", ``SSA``)
val _ = overload_on("#", ``(λa b. (a, Block b)) : ssavar -> num -> register``)
val action_id_lt_transitive = store_thm("action_id_lt_transitive",
``transitive action_id_lt``,
rw[relationTheory.transitive_def, definition "action_id_lt_def"] >>
BasicProvers.every_case_tac >> simp[])
val action_id_lt_irreflexive = store_thm("action_id_lt_irreflexive",
``irreflexive action_id_lt``,
rw[relationTheory.irreflexive_def, definition "action_id_lt_def"] >>
BasicProvers.every_case_tac >> simp[])
val _ = Datatype`
resume_values =
| NOR (α list)
......@@ -145,6 +155,11 @@ val _ = Datatype`
strength = STRONG | WEAK
`
val distinct_messages_def = Define`
distinct_messages (Message tid id _) (Message tid' id' _)
tid tid' id id'
`
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
......@@ -156,6 +171,13 @@ val _ = Datatype`
|>
`
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))``)
......@@ -491,6 +513,11 @@ 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.
*)
......@@ -498,11 +525,9 @@ val local_seq_cst_def = Define`
local_seq_cst (mem : memory) : bool
EVERY
(λn. let m = EL n mem.committed in
case m of Message tid id _ =>
EVERY (λm'. can_read_from mem m m' can_read_from mem m' m
case m' of Message tid' id' _ =>
tid tid' id' id)
(TAKE n mem.committed))
EVERY (λm'. can_read_from mem m m' can_read_from mem m' m
program_order m m')
(TAKE n mem.committed))
(GENLIST I (LENGTH mem.committed))
`
......
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