• Adam Nelson's avatar
    Prove local seq consistency for seq_cst_schedule · fb68640a
    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.)
DefineUtils.sml 5.62 KB