(* This is a ________ _______ __ _________ _________ |_ ___ \.|_ __ \ / \ |_ ___ | _ _ | | | \. \ | |__) | / /\ \ | |_ \_|_/ | | \_| | | | | | __ / / ____ \ | _| | | _| |___.' /_| | \ \_ _/ / \ \_ _| |_ _| |_ |________.'|____| |___|____| |____|_____| |_____| model for ^~^ , ('Y') ) / \/ ASL __QQ (\|||/) (_)_"> / Please do consider this as a work in progress. *) ASL (* Renamings *) let NASLLocal = ~ASLLocal let ASLDATA = DATA let asl_iico_ctrl = iico_ctrl let asl_iico_data = iico_data let asl_rf_reg = rf-reg let asl_rf = rf (* Warning, partial_po is _implicitely_ transitive *) let asl_po = partial_po (* Working relations *) let aarch64 = NASLLocal * NASLLocal let asl_fr_reg = inter_transitive (asl_po,[Rreg];loc;[Wreg]) (* loc extended to registers *) let asl_fr = inter_transitive (asl_po,[R] ; loc ; [W]) let asl_data = asl_iico_data | asl_rf_reg let asl_deps = asl_data (* | asl_iico_ctrl *) let asl_deps_restricted = id | (asl_deps ; ([ASLLocal] ; asl_deps)+) let aarch64_iico_data = ( asl_deps_restricted ; asl_data+ ) & aarch64 let aarch64_iico_ctrl = ([B]; asl_iico_ctrl; asl_iico_data*)+ & aarch64 let aarch64_iico_order = ( asl_fr | asl_fr_reg ) & aarch64 let aarch64_intrinsic = aarch64_iico_ctrl | aarch64_iico_data | aarch64_iico_order (* Event sets *) let restrict-finals s = (* Asumming that non-final writes are read internally *) let non-final = domain(rf-reg) in s \ non-final let AArch64 = NASLLocal let AArch64Finals = restrict-finals(AArch64&Wreg) (* DATA and NDATA *) let to_data = (asl_deps_restricted ; [DATA] ; asl_iico_data ; [W | Wreg]) & aarch64 let AArch64_DATA = NASLLocal & domain (to_data) show [AArch64_DATA] as AArch64_DATA show [DATA] as debug_data (* TODO *) (* B = write to PC *) (* BCC = range(aarch64_iico_ctrl) & B *) (* Pred = BranchTo(VBAR something) ??? *) (* F = call to (data memory ?) barrier *) (* Tests *) acyclic (aarch64_intrinsic | asl_po) as asl_determinism (***********) (* Display *) (***********) (* Keep significant branching effects only. * Significant branching effect are the ones * that stand on a control path from AArch64 * relevant accesses. *) let AArch64NoB = AArch64 \ B let reaching = domain ([B]; aarch64_iico_ctrl; [AArch64NoB]) let reachable = range ([AArch64NoB]; aarch64_iico_data; aarch64_iico_ctrl?; [B]) let AArch64B = reaching & reachable let AArch64 = AArch64NoB | AArch64B show AArch64,AArch64Finals,AArch64_DATA show aarch64_iico_ctrl as aarch64_iico_ctrl show aarch64_iico_data, aarch64_iico_order (* Branching events to PC writes are of the branch conditional kind *) let AArch64_BCC = domain ([B]; aarch64_iico_ctrl; [WPC]) show AArch64_BCC