(*
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