(* ------------------ Key derived facts about the POWER machine thread rules ---------------------- *) open MachineDefTypes open MachineDefInstructionSemantics open MachineDefThreadSubsystem open Intermediate_actions open Statement (* ----- Preliminary: Finding key transitions and instructions in the trace ----- *) val write_actions_of_trace : trace -> action set let write_actions_of_trace t = { Write (w_aid_comp w.w_eiid) w.w_thread w.w_addr w.w_value | forall w | exist idx tid i ws. idx + 1 IN PL t && nth_label idx t = Commit_write tid i ws && w IN ws } let commit_transition_of t ia = Set.choose { l | exist idx i. i + 1 IN PL t && nth_label i t = l && (idx,ia) IN commit_to_inter l } let commit_transition_of_inst_instance t ii = Set.choose { l | exist idx i. i + 1 IN PL t && nth_label i t = l && ((exist tid ws. l = Commit_write tid ii ws) || (exist tid b. l = Commit_barrier tid ii b) || (exist tid rs. l = Commit_read tid ii rs) || (exist tid. l = Commit_reg_or_branch tid ii)) } let last_satisfy_transition_of t ia = { l | exist r commitidx satidx tid ii w rrs. (* ia is a read *) ia = Read (r_aid_comp r.rr_eiid) r.rr_thread r.rr_write.w_addr r.rr_write.w_value && w = r.rr_write && (* satidx is the index of a read-satisfy transition for a instruction ii which reads w *) satidx + 1 IN PL t && nth_label satidx t = Read_from_storage_subsystem tid ii w && (* ii is the instruction which commits the read r, committed at index commitidx *) commitidx + 1 IN PL t && nth_label commitidx t = Commit_read tid ii rrs && r IN rrs && (* There is no satidx' in between satidx and commitidx with a read-satisfy for that instruction *) (not (exist satidx' w'. satidx' + 1 IN PL t && nth_label satidx' t = Read_from_storage_subsystem tid ii w' && satidx < satidx' && satidx' < commitidx))} let committed_instruction_instance_of t ia = match ia with | Read aid tid a v -> Set.choose { ii | exist tid rrs. (ii.ioid,ia) IN commit_to_inter (Commit_read tid ii rrs) && (exist idx. idx + 1 IN PL t && nth_label idx t = Commit_read tid ii rrs)} | Write aid tid a v -> Set.choose { ii | exist tid ws. (ii.ioid,ia) IN commit_to_inter (Commit_write tid ii ws) && (exist idx. idx + 1 IN PL t && nth_label idx t = Commit_write tid ii ws)} end (* ---------------- Lemmas about the commit transition for various instructions -------------- *) let separated_by_sync_or_lwsync_lemma = forall ia1 ia2 t ii1 ii2. (ii1 = committed_instruction_instance_of t ia1) && (ii2 = committed_instruction_instance_of t ia2) && (exist iib ts. iib IN strict_program_order_suffix ts ii1 && ii2 IN strict_program_order_suffix ts iib && (iib.is_sync || iib.is_lwsync)) --> (commit_transition_of t ia1,commit_transition_of t ia2) IN trace_to_order t (* Proof: By CommitPrevBarrLS premise of commit, before ii2 can be committed, iib must be committed. By CommitMemoryAccessBeforeBarrier, before iib is committed, ii1 must be committed. QED *) let register_dependency_lemma = forall ia1 ia2 t ii1 ii2. (ii1 = committed_instruction_instance_of t ia1) && (ii2 = committed_instruction_instance_of t ia2) && (exist ts. ii2 IN strict_dependent_suffix ts ii1) --> (commit_transition_of t ia1,commit_transition_of t ia2) IN trace_to_order t (*Proof: By CommitDataFlow premise of commit, ii2 cannot be committed before ii1. QED *) let memory_location_dependency_lemma = forall ia1 ia2 t ii1 ii2. (ii1 = committed_instruction_instance_of t ia1) && (ii2 = committed_instruction_instance_of t ia2) && (exist ts. ii2 IN strict_program_order_suffix ts ii1) && (exist a. (possibly_reads_from_address ii1.behaviour a || possibly_writes_to_address ii1.behaviour a) && (possibly_reads_from_address ii2.behaviour a || possibly_writes_to_address ii2.behaviour a)) --> (commit_transition_of t ia1,commit_transition_of t ia2) IN trace_to_order t (*Proof: By CommitPrevMightSameAddress premise, ii2 cannot be committed before ii1. QED *) let control_dependency_lemma = forall ia1 ia2 t ii1 ii2. (ii1 = committed_instruction_instance_of t ia1) && (ii2 = committed_instruction_instance_of t ia2) && (exist iib ts. iib IN strict_dependent_suffix ts ii1 && ii2 IN strict_program_order_suffix ts iib && iib.is_branch) --> (commit_transition_of t ia1,commit_transition_of t ia2) IN trace_to_order t (*Proof: By CommitControlFlow premise, ii2 cannot be committed before iib. By CommitDataFlow premise, iib cannot be committed before ii1. QED *) (* ---------------- Lemmas about the last read-satisfy transition ------------------ *) let ctrlisync_implies_order_lemma = forall ia1 ia2 t. (ia1,ia2) IN trace_to_ctrlisync t --> (forall (l IN last_satisfy_transition_of t ia2). (commit_transition_of t ia1,l) IN trace_to_order t) (*Proof: By the PrevSyncLwsyncIsyncCommitted precondition of the thread read-satisfy transition, ia2 cannot be satisfied until previous isync is committed. By CommitControlFlow precondition of commit transition, that isync cannot be committed before the previous branch is committed. By CommitDataFlow precondition of commit transition, the branch cannot be committed before ia1. QED *) let barrier_implies_order_lemma = forall ia1 ia2 t b. (ia1,ia2) IN trace_to_xsync t b --> (forall (l IN last_satisfy_transition_of t ia2). (commit_transition_of t ia1,l) IN trace_to_order t) (*Proof: By the PrevSyncLwsyncIsyncCommitted precondition of the thread read-satisfy transition, ia2 cannot be satisfied until previous lwsync or sync is committed. By CommitMemoryAccessBeforeBarrier precondition of commit transition, the barrier cannot be committed before ia1. QED *) (* ---------------- Lemmas about possible program-order holes in committed instructions (due to speculation) -------------- *) (* For this section, suppose we have ia1 and ia2 such that ia1 --po--> ia2 but ia2 is committed in trace t before ia1 *) val ia1 : action val ia2 : action val t : trace let _ = (ia1,ia2) IN trace_to_po t let _ = (commit_transition_of t ia2,commit_transition_of t ia1) IN trace_to_order t (* Then call all the instructions in "the program order hole" (po-after ia1 and po-before-or-equal-to ia2 and committed after ia2) as iis_hole *) let iis_hole = { ii | exist ts. ii IN strict_program_order_suffix ts (committed_instruction_instance_of t ia1) && ((committed_instruction_instance_of t ia2) IN (strict_program_order_suffix ts ii) || (committed_instruction_instance_of t ia2) = ii) && (commit_transition_of t ia2,commit_transition_of_inst_instance t ii) IN trace_to_order t } (* Then we have the three facts about instructions in iis_hole *) let no_branch_in_hole_lemma = forall ii. ii IN iis_hole --> not (ii.is_branch) (*Proof: Suppose there is one, say ii_b. By CommitControlFlow premise, ia2's instruction cannot have been committed before ii_b. Contradiction. QED *) let no_barrier_in_hole_lemma = forall ii. ii IN iis_hole --> not (ii.is_sync || ii.is_lwsync) (*Proof: Suppose there is one, say ii_barr. By CommitPrevBarrierLS premise, ia2's instruction cannot have been committed before ii_barr. Contradiction. QED *) let no_dependent_instrs_in_hole_lemma = forall ia3 ia4. (ia3,ia4) IN trace_to_dd t --> not ((committed_instruction_instance_of t ia3) IN iis_hole && (committed_instruction_instance_of t ia4) IN iis_hole) (*Proof: By CommitPrevMightSameAddress, ia2 cannot have been committed before ia3 in this situation. QED *)