Ensuring SFENCE Instruction Correctness: A Formal Verification Framework Based on Invariants.