-
Adam Nelson authored
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.)
fb68640a