diff options
Diffstat (limited to 'aarch64_small')
| -rw-r--r-- | aarch64_small/aarch64_regfp.sail | 31 | ||||
| -rw-r--r-- | aarch64_small/armV8_common_lib.sail | 108 | ||||
| -rw-r--r-- | aarch64_small/armV8_extras.lem | 36 | ||||
| -rw-r--r-- | aarch64_small/armV8_extras_embed.lem | 67 | ||||
| -rw-r--r-- | aarch64_small/armV8_extras_embed_sequential.lem | 69 |
5 files changed, 232 insertions, 79 deletions
diff --git a/aarch64_small/aarch64_regfp.sail b/aarch64_small/aarch64_regfp.sail index ce155f0a..be4a2cba 100644 --- a/aarch64_small/aarch64_regfp.sail +++ b/aarch64_small/aarch64_regfp.sail @@ -223,22 +223,25 @@ function initial_analysis (instr:ast) -> (regfps,regfps,regfps,niafps,diafp,inst }, (ClearExclusiveMonitor(imm)) => (), /*ClearExclusiveLocal*/ (Barrier(op,domain,types)) => { + let (dom, typ) = + (match domain { + MBReqDomain_Nonshareable => A64_NonShare + MBReqDomain_InnerShareable => A64_InnerShare + MBReqDomain_OuterShareable => A64_OuterShare + MBReqDomain_FullSystem => A64_FullShare + }, + match types { + MBReqTypes_Reads => A64_barrier_LD + MBReqTypes_Writes => A64_barrier_ST + MBReqTypes_All => A64_barrier_all + }) + in { ik = match op { - MemBarrierOp_DSB => - match types { - MBReqTypes_Reads => IK_barrier(Barrier_DSB_LD), - MBReqTypes_Writes => IK_barrier(Barrier_DSB_ST), - MBReqTypes_All => IK_barrier(Barrier_DSB) - }, - MemBarrierOp_DMB => - match types { - MBReqTypes_Reads => IK_barrier(Barrier_DMB_LD), - MBReqTypes_Writes => IK_barrier(Barrier_DMB_ST), - MBReqTypes_All => IK_barrier(Barrier_DMB) - }, - MemBarrierOp_ISB => - IK_barrier(Barrier_ISB) + MemBarrierOp_DSB => IK_barrier(Barrier_DSB (dom, typ)) + MemBarrierOp_DMB => IK_barrier(Barrier_DMB (dom, typ)) + MemBarrierOp_ISB => IK_barrier(Barrier_ISB) }; + } }, (DataCache(t,dc_op)) => { diff --git a/aarch64_small/armV8_common_lib.sail b/aarch64_small/armV8_common_lib.sail index b758b28e..d3d82c6d 100644 --- a/aarch64_small/armV8_common_lib.sail +++ b/aarch64_small/armV8_common_lib.sail @@ -563,45 +563,101 @@ function BigEndianReverse (value) = { /** FUNCTION:shared/functions/memory/DataMemoryBarrier */ -/* external */ val DataMemoryBarrier_Reads : unit -> unit effect {barr} -function DataMemoryBarrier_Reads () = __barrier(Barrier_DMB_LD) -/* external */ val DataMemoryBarrier_Writes : unit -> unit effect {barr} -function DataMemoryBarrier_Writes () = __barrier(Barrier_DMB_ST) -/* external */ val DataMemoryBarrier_All : unit -> unit effect {barr} -function DataMemoryBarrier_All () = __barrier(Barrier_DMB) +/* external */ val DataMemoryBarrier_NonShReads : unit -> unit effect {barr} +/* external */ val DataMemoryBarrier_NonShWrites : unit -> unit effect {barr} +/* external */ val DataMemoryBarrier_NonShAll : unit -> unit effect {barr} +/* external */ val DataMemoryBarrier_InnerShReads : unit -> unit effect {barr} +/* external */ val DataMemoryBarrier_InnerShWrites : unit -> unit effect {barr} +/* external */ val DataMemoryBarrier_InnerShAll : unit -> unit effect {barr} +/* external */ val DataMemoryBarrier_OuterShReads : unit -> unit effect {barr} +/* external */ val DataMemoryBarrier_OuterShWrites : unit -> unit effect {barr} +/* external */ val DataMemoryBarrier_OuterShAll : unit -> unit effect {barr} +/* external */ val DataMemoryBarrier_FullShReads : unit -> unit effect {barr} +/* external */ val DataMemoryBarrier_FullShWrites : unit -> unit effect {barr} +/* external */ val DataMemoryBarrier_FullShAll : unit -> unit effect {barr} + +function DataMemoryBarrier_NonShReads = __barrier(Barrier_DMB (A64_NonShare, A64_barrier_LD)) +function DataMemoryBarrier_NonShWrites = __barrier(Barrier_DMB (A64_NonShare, A64_barrier_ST)) +function DataMemoryBarrier_NonShAll = __barrier(Barrier_DMB (A64_NonShare, A64_barrier_all)) +function DataMemoryBarrier_InnerShReads = __barrier(Barrier_DMB (A64_InnerShare, A64_barrier_LD)) +function DataMemoryBarrier_InnerShWrites = __barrier(Barrier_DMB (A64_InnerShare, A64_barrier_ST)) +function DataMemoryBarrier_InnerShAll = __barrier(Barrier_DMB (A64_InnerShare, A64_barrier_all)) +function DataMemoryBarrier_OuterShReads = __barrier(Barrier_DMB (A64_OuterShare, A64_barrier_LD)) +function DataMemoryBarrier_OuterShWrites = __barrier(Barrier_DMB (A64_OuterShare, A64_barrier_ST)) +function DataMemoryBarrier_OuterShAll = __barrier(Barrier_DMB (A64_OuterShare, A64_barrier_all)) +function DataMemoryBarrier_FullShReads = __barrier(Barrier_DMB (A64_FullShare, A64_barrier_LD)) +function DataMemoryBarrier_FullShWrites = __barrier(Barrier_DMB (A64_FullShare, A64_barrier_ST)) +function DataMemoryBarrier_FullShAll = __barrier(Barrier_DMB (A64_FullShare, A64_barrier_all)) val DataMemoryBarrier : (MBReqDomain, MBReqTypes) -> unit effect {barr, escape} function DataMemoryBarrier(domain, types) = { - if domain != MBReqDomain_FullSystem & domain != MBReqDomain_InnerShareable then - not_implemented("DataMemoryBarrier: not MBReqDomain_FullSystem or _InnerShareable"); - - match types { - MBReqTypes_Reads => DataMemoryBarrier_Reads(), - MBReqTypes_Writes => DataMemoryBarrier_Writes(), - MBReqTypes_All => DataMemoryBarrier_All() + match (domain, types) { + (MBReqDomain_Nonshareable, MBReqTypes_Reads) => DataMemoryBarrier_NonShReads() + (MBReqDomain_Nonshareable, MBReqTypes_Writes) => DataMemoryBarrier_NonShWrites() + (MBReqDomain_Nonshareable, MBReqTypes_All) => DataMemoryBarrier_NonShAll() + + (MBReqDomain_InnerShareable, MBReqTypes_Reads) => DataMemoryBarrier_InnerShReads() + (MBReqDomain_InnerShareable, MBReqTypes_Writes) => DataMemoryBarrier_InnerShWrites() + (MBReqDomain_InnerShareable, MBReqTypes_All) => DataMemoryBarrier_InnerShAll() + + (MBReqDomain_OuterShareable, MBReqTypes_Reads) => DataMemoryBarrier_OuterShReads() + (MBReqDomain_OuterShareable, MBReqTypes_Writes) => DataMemoryBarrier_OuterShWrites() + (MBReqDomain_OuterShareable, MBReqTypes_All) => DataMemoryBarrier_OuterShAll() + + (MBReqDomain_FullSystem, MBReqTypes_Reads) => DataMemoryBarrier_FullShReads() + (MBReqDomain_FullSystem, MBReqTypes_Writes) => DataMemoryBarrier_FullShWrites() + (MBReqDomain_FullSystem, MBReqTypes_All) => DataMemoryBarrier_FullShAll() }; } /** FUNCTION:shared/functions/memory/DataSynchronizationBarrier */ -/* external */ val DataSynchronizationBarrier_Reads : unit -> unit effect {barr} -function DataSynchronizationBarrier_Reads () = __barrier(Barrier_DSB_LD) -/* external */ val DataSynchronizationBarrier_Writes : unit -> unit effect {barr} -function DataSynchronizationBarrier_Writes () = __barrier(Barrier_DSB_ST) -/* external */ val DataSynchronizationBarrier_All : unit -> unit effect {barr} -function DataSynchronizationBarrier_All () = __barrier(Barrier_DSB) +/* external */ val DataSynchronizationBarrier_NonShReads : unit -> unit effect {barr} +/* external */ val DataSynchronizationBarrier_NonShWrites : unit -> unit effect {barr} +/* external */ val DataSynchronizationBarrier_NonShAll : unit -> unit effect {barr} +/* external */ val DataSynchronizationBarrier_InnerShReads : unit -> unit effect {barr} +/* external */ val DataSynchronizationBarrier_InnerShWrites : unit -> unit effect {barr} +/* external */ val DataSynchronizationBarrier_InnerShAll : unit -> unit effect {barr} +/* external */ val DataSynchronizationBarrier_OuterShReads : unit -> unit effect {barr} +/* external */ val DataSynchronizationBarrier_OuterShWrites : unit -> unit effect {barr} +/* external */ val DataSynchronizationBarrier_OuterShAll : unit -> unit effect {barr} +/* external */ val DataSynchronizationBarrier_FullShReads : unit -> unit effect {barr} +/* external */ val DataSynchronizationBarrier_FullShWrites : unit -> unit effect {barr} +/* external */ val DataSynchronizationBarrier_FullShAll : unit -> unit effect {barr} + +function DataSynchronizationBarrier_NonShReads = __barrier(Barrier_DSB (A64_NonShare, A64_barrier_LD)) +function DataSynchronizationBarrier_NonShWrites = __barrier(Barrier_DSB (A64_NonShare, A64_barrier_ST)) +function DataSynchronizationBarrier_NonShAll = __barrier(Barrier_DSB (A64_NonShare, A64_barrier_all)) +function DataSynchronizationBarrier_InnerShReads = __barrier(Barrier_DSB (A64_InnerShare, A64_barrier_LD)) +function DataSynchronizationBarrier_InnerShWrites = __barrier(Barrier_DSB (A64_InnerShare, A64_barrier_ST)) +function DataSynchronizationBarrier_InnerShAll = __barrier(Barrier_DSB (A64_InnerShare, A64_barrier_all)) +function DataSynchronizationBarrier_OuterShReads = __barrier(Barrier_DSB (A64_OuterShare, A64_barrier_LD)) +function DataSynchronizationBarrier_OuterShWrites = __barrier(Barrier_DSB (A64_OuterShare, A64_barrier_ST)) +function DataSynchronizationBarrier_OuterShAll = __barrier(Barrier_DSB (A64_OuterShare, A64_barrier_all)) +function DataSynchronizationBarrier_FullShReads = __barrier(Barrier_DSB (A64_FullShare, A64_barrier_LD)) +function DataSynchronizationBarrier_FullShWrites = __barrier(Barrier_DSB (A64_FullShare, A64_barrier_ST)) +function DataSynchronizationBarrier_FullShAll = __barrier(Barrier_DSB (A64_FullShare, A64_barrier_all)) val DataSynchronizationBarrier : (MBReqDomain, MBReqTypes) -> unit effect {barr,escape} function DataSynchronizationBarrier(domain, types) = { - if domain != MBReqDomain_FullSystem then - not_implemented("DataSynchronizationBarrier: not MBReqDomain_FullSystem"); - - match types { - MBReqTypes_Reads => DataSynchronizationBarrier_Reads(), - MBReqTypes_Writes => DataSynchronizationBarrier_Writes(), - MBReqTypes_All => DataSynchronizationBarrier_All() + match (domain, types) { + (MBReqDomain_Nonshareable, MBReqTypes_Reads) => DataSynchronizationBarrier_NonShReads() + (MBReqDomain_Nonshareable, MBReqTypes_Writes) => DataSynchronizationBarrier_NonShWrites() + (MBReqDomain_Nonshareable, MBReqTypes_All) => DataSynchronizationBarrier_NonShAll() + + (MBReqDomain_InnerShareable, MBReqTypes_Reads) => DataSynchronizationBarrier_InnerShReads() + (MBReqDomain_InnerShareable, MBReqTypes_Writes) => DataSynchronizationBarrier_InnerShWrites() + (MBReqDomain_InnerShareable, MBReqTypes_All) => DataSynchronizationBarrier_InnerShAll() + + (MBReqDomain_OuterShareable, MBReqTypes_Reads) => DataSynchronizationBarrier_OuterShReads() + (MBReqDomain_OuterShareable, MBReqTypes_Writes) => DataSynchronizationBarrier_OuterShWrites() + (MBReqDomain_OuterShareable, MBReqTypes_All) => DataSynchronizationBarrier_OuterShAll() + + (MBReqDomain_FullSystem, MBReqTypes_Reads) => DataSynchronizationBarrier_FullShReads() + (MBReqDomain_FullSystem, MBReqTypes_Writes) => DataSynchronizationBarrier_FullShWrites() + (MBReqDomain_FullSystem, MBReqTypes_All) => DataSynchronizationBarrier_FullShAll() }; } diff --git a/aarch64_small/armV8_extras.lem b/aarch64_small/armV8_extras.lem index 9a187ecb..da48c836 100644 --- a/aarch64_small/armV8_extras.lem +++ b/aarch64_small/armV8_extras.lem @@ -65,13 +65,33 @@ let aArch64_excl_res : excl_res = Just ("speculate_exclusive_success", (ER (Just f))) let aArch64_barrier_functions = - [ ("DataMemoryBarrier_Reads", Barrier_DMB_LD); - ("DataMemoryBarrier_Writes", Barrier_DMB_ST); - ("DataMemoryBarrier_All", Barrier_DMB); - ("DataSynchronizationBarrier_Reads", Barrier_DSB_LD); - ("DataSynchronizationBarrier_Writes", Barrier_DSB_ST); - ("DataSynchronizationBarrier_All", Barrier_DSB); - ("InstructionSynchronizationBarrier", Barrier_ISB); + [ ("DataMemoryBarrier_NonShReads", Barrier_DMB (A64_NonShare, A64_barrier_LD)); + ("DataMemoryBarrier_NonShWrites", Barrier_DMB (A64_NonShare, A64_barrier_ST)); + ("DataMemoryBarrier_NonShAll", Barrier_DMB (A64_NonShare, A64_barrier_all)); + ("DataMemoryBarrier_InnerShReads", Barrier_DMB (A64_InnerShare, A64_barrier_LD)); + ("DataMemoryBarrier_InnerShWrites", Barrier_DMB (A64_InnerShare, A64_barrier_ST)); + ("DataMemoryBarrier_InnerShAll", Barrier_DMB (A64_InnerShare, A64_barrier_all)); + ("DataMemoryBarrier_OuterShReads", Barrier_DMB (A64_OuterShare, A64_barrier_LD)); + ("DataMemoryBarrier_OuterShWrites", Barrier_DMB (A64_OuterShare, A64_barrier_ST)); + ("DataMemoryBarrier_OuterShAll", Barrier_DMB (A64_OuterShare, A64_barrier_all)); + ("DataMemoryBarrier_FullShReads", Barrier_DMB (A64_FullShare, A64_barrier_LD)); + ("DataMemoryBarrier_FullShWrites", Barrier_DMB (A64_FullShare, A64_barrier_ST)); + ("DataMemoryBarrier_FullShAll", Barrier_DMB (A64_FullShare, A64_barrier_all)); - ("TMCommitEffect", Barrier_TM_COMMIT); + ("DataSynchronizationBarrier_NonShReads", Barrier_DSB (A64_NonShare, A64_barrier_LD)); + ("DataSynchronizationBarrier_NonShWrites", Barrier_DSB (A64_NonShare, A64_barrier_ST)); + ("DataSynchronizationBarrier_NonShAll", Barrier_DSB (A64_NonShare, A64_barrier_all)); + ("DataSynchronizationBarrier_InnerShReads", Barrier_DSB (A64_InnerShare, A64_barrier_LD)); + ("DataSynchronizationBarrier_InnerShWrites", Barrier_DSB (A64_InnerShare, A64_barrier_ST)); + ("DataSynchronizationBarrier_InnerShAll", Barrier_DSB (A64_InnerShare, A64_barrier_all)); + ("DataSynchronizationBarrier_OuterShReads", Barrier_DSB (A64_OuterShare, A64_barrier_LD)); + ("DataSynchronizationBarrier_OuterShWrites", Barrier_DSB (A64_OuterShare, A64_barrier_ST)); + ("DataSynchronizationBarrier_OuterShAll", Barrier_DSB (A64_OuterShare, A64_barrier_all)); + ("DataSynchronizationBarrier_FullShReads", Barrier_DSB (A64_FullShare, A64_barrier_LD)); + ("DataSynchronizationBarrier_FullShWrites", Barrier_DSB (A64_FullShare, A64_barrier_ST)); + ("DataSynchronizationBarrier_FullShAll", Barrier_DSB (A64_FullShare, A64_barrier_all)); + + ("InstructionSynchronizationBarrier", Barrier_ISB ()); + + ("TMCommitEffect", Barrier_TM_COMMIT ()); ] diff --git a/aarch64_small/armV8_extras_embed.lem b/aarch64_small/armV8_extras_embed.lem index c5a1b8bc..54f9fc8a 100644 --- a/aarch64_small/armV8_extras_embed.lem +++ b/aarch64_small/armV8_extras_embed.lem @@ -43,24 +43,61 @@ let wMem_Val_ATOMIC_ORDERED addr size v = write_mem Write_exclusive_release () a let speculate_exclusive_success () = excl_result () -val DataMemoryBarrier_Reads : forall 'rv 'e. unit -> monad 'rv unit 'e -val DataMemoryBarrier_Writes : forall 'rv 'e. unit -> monad 'rv unit 'e -val DataMemoryBarrier_All : forall 'rv 'e. unit -> monad 'rv unit 'e -val DataSynchronizationBarrier_Reads : forall 'rv 'e. unit -> monad 'rv unit 'e -val DataSynchronizationBarrier_Writes : forall 'rv 'e. unit -> monad 'rv unit 'e -val DataSynchronizationBarrier_All : forall 'rv 'e. unit -> monad 'rv unit 'e -val InstructionSynchronizationBarrier : forall 'rv 'e. unit -> monad 'rv unit 'e +val DataMemoryBarrier_NonShReads : forall 'rv 'e. unit -> monad 'rv unit 'e +val DataMemoryBarrier_NonShWrites : forall 'rv 'e. unit -> monad 'rv unit 'e +val DataMemoryBarrier_NonShAll : forall 'rv 'e. unit -> monad 'rv unit 'e +val DataMemoryBarrier_InnerShReads : forall 'rv 'e. unit -> monad 'rv unit 'e +val DataMemoryBarrier_InnerShWrites : forall 'rv 'e. unit -> monad 'rv unit 'e +val DataMemoryBarrier_InnerShAll : forall 'rv 'e. unit -> monad 'rv unit 'e +val DataMemoryBarrier_OuterShReads : forall 'rv 'e. unit -> monad 'rv unit 'e +val DataMemoryBarrier_OuterShWrites : forall 'rv 'e. unit -> monad 'rv unit 'e +val DataMemoryBarrier_OuterShAll : forall 'rv 'e. unit -> monad 'rv unit 'e +val DataMemoryBarrier_FullShReads : forall 'rv 'e. unit -> monad 'rv unit 'e +val DataMemoryBarrier_FullShWrites : forall 'rv 'e. unit -> monad 'rv unit 'e +val DataMemoryBarrier_FullShAll : forall 'rv 'e. unit -> monad 'rv unit 'e +let DataMemoryBarrier_NonShReads () = barrier (Barrier_DMB (A64_NonShare, A64_barrier_LD)) +let DataMemoryBarrier_NonShWrites () = barrier (Barrier_DMB (A64_NonShare, A64_barrier_ST)) +let DataMemoryBarrier_NonShAll () = barrier (Barrier_DMB (A64_NonShare, A64_barrier_all)) +let DataMemoryBarrier_InnerShReads () = barrier (Barrier_DMB (A64_InnerShare, A64_barrier_LD)) +let DataMemoryBarrier_InnerShWrites () = barrier (Barrier_DMB (A64_InnerShare, A64_barrier_ST)) +let DataMemoryBarrier_InnerShAll () = barrier (Barrier_DMB (A64_InnerShare, A64_barrier_all)) +let DataMemoryBarrier_OuterShReads () = barrier (Barrier_DMB (A64_OuterShare, A64_barrier_LD)) +let DataMemoryBarrier_OuterShWrites () = barrier (Barrier_DMB (A64_OuterShare, A64_barrier_ST)) +let DataMemoryBarrier_OuterShAll () = barrier (Barrier_DMB (A64_OuterShare, A64_barrier_all)) +let DataMemoryBarrier_FullShReads () = barrier (Barrier_DMB (A64_FullShare, A64_barrier_LD)) +let DataMemoryBarrier_FullShWrites () = barrier (Barrier_DMB (A64_FullShare, A64_barrier_ST)) +let DataMemoryBarrier_FullShAll () = barrier (Barrier_DMB (A64_FullShare, A64_barrier_all)) + +val DataSynchronizationBarrier_NonShReads : forall 'rv 'e. unit -> monad 'rv unit 'e +val DataSynchronizationBarrier_NonShWrites : forall 'rv 'e. unit -> monad 'rv unit 'e +val DataSynchronizationBarrier_NonShAll : forall 'rv 'e. unit -> monad 'rv unit 'e +val DataSynchronizationBarrier_InnerShReads : forall 'rv 'e. unit -> monad 'rv unit 'e +val DataSynchronizationBarrier_InnerShWrites : forall 'rv 'e. unit -> monad 'rv unit 'e +val DataSynchronizationBarrier_InnerShAll : forall 'rv 'e. unit -> monad 'rv unit 'e +val DataSynchronizationBarrier_OuterShReads : forall 'rv 'e. unit -> monad 'rv unit 'e +val DataSynchronizationBarrier_OuterShWrites : forall 'rv 'e. unit -> monad 'rv unit 'e +val DataSynchronizationBarrier_OuterShAll : forall 'rv 'e. unit -> monad 'rv unit 'e +val DataSynchronizationBarrier_FullShReads : forall 'rv 'e. unit -> monad 'rv unit 'e +val DataSynchronizationBarrier_FullShWrites : forall 'rv 'e. unit -> monad 'rv unit 'e +val DataSynchronizationBarrier_FullShAll : forall 'rv 'e. unit -> monad 'rv unit 'e +let DataSynchronizationBarrier_NonShReads () = barrier (Barrier_DSB (A64_NonShare, A64_barrier_LD)) +let DataSynchronizationBarrier_NonShWrites () = barrier (Barrier_DSB (A64_NonShare, A64_barrier_ST)) +let DataSynchronizationBarrier_NonShAll () = barrier (Barrier_DSB (A64_NonShare, A64_barrier_all)) +let DataSynchronizationBarrier_InnerShReads () = barrier (Barrier_DSB (A64_InnerShare, A64_barrier_LD)) +let DataSynchronizationBarrier_InnerShWrites () = barrier (Barrier_DSB (A64_InnerShare, A64_barrier_ST)) +let DataSynchronizationBarrier_InnerShAll () = barrier (Barrier_DSB (A64_InnerShare, A64_barrier_all)) +let DataSynchronizationBarrier_OuterShReads () = barrier (Barrier_DSB (A64_OuterShare, A64_barrier_LD)) +let DataSynchronizationBarrier_OuterShWrites () = barrier (Barrier_DSB (A64_OuterShare, A64_barrier_ST)) +let DataSynchronizationBarrier_OuterShAll () = barrier (Barrier_DSB (A64_OuterShare, A64_barrier_all)) +let DataSynchronizationBarrier_FullShReads () = barrier (Barrier_DSB (A64_FullShare, A64_barrier_LD)) +let DataSynchronizationBarrier_FullShWrites () = barrier (Barrier_DSB (A64_FullShare, A64_barrier_ST)) +let DataSynchronizationBarrier_FullShAll () = barrier (Barrier_DSB (A64_FullShare, A64_barrier_all)) -let DataMemoryBarrier_Reads () = barrier Barrier_DMB_LD -let DataMemoryBarrier_Writes () = barrier Barrier_DMB_ST -let DataMemoryBarrier_All () = barrier Barrier_DMB -let DataSynchronizationBarrier_Reads () = barrier Barrier_DSB_LD -let DataSynchronizationBarrier_Writes () = barrier Barrier_DSB_ST -let DataSynchronizationBarrier_All () = barrier Barrier_DSB -let InstructionSynchronizationBarrier () = barrier Barrier_ISB +val InstructionSynchronizationBarrier : forall 'rv 'e. unit -> monad 'rv unit 'e +let InstructionSynchronizationBarrier () = barrier (Barrier_ISB ()) val TMCommitEffect : forall 'rv 'e. unit -> monad 'rv unit 'e -let TMCommitEffect () = barrier Barrier_TM_COMMIT +let TMCommitEffect () = barrier (Barrier_TM_COMMIT ()) val SCTLR_EL1_type_to_SCTLR_type : SCTLR_EL1_type -> SCTLR_type let SCTLR_EL1_type_to_SCTLR_type <| SCTLR_EL1_type_SCTLR_EL1_type_chunk_0 = x |> = <| SCTLR_type_SCTLR_type_chunk_0 = x |> diff --git a/aarch64_small/armV8_extras_embed_sequential.lem b/aarch64_small/armV8_extras_embed_sequential.lem index d2bb8330..91494238 100644 --- a/aarch64_small/armV8_extras_embed_sequential.lem +++ b/aarch64_small/armV8_extras_embed_sequential.lem @@ -35,24 +35,61 @@ let wMem_Val_ATOMIC (_,v) = write_mem_val v >>= fun b -> return (if b then B0 el let speculate_exclusive_success () = excl_result () >>= fun b -> return (if b then B1 else B0) -val DataMemoryBarrier_Reads : unit -> M unit -val DataMemoryBarrier_Writes : unit -> M unit -val DataMemoryBarrier_All : unit -> M unit -val DataSynchronizationBarrier_Reads : unit -> M unit -val DataSynchronizationBarrier_Writes : unit -> M unit -val DataSynchronizationBarrier_All : unit -> M unit -val InstructionSynchronizationBarrier : unit -> M unit - -let DataMemoryBarrier_Reads () = barrier Barrier_DMB_LD -let DataMemoryBarrier_Writes () = barrier Barrier_DMB_ST -let DataMemoryBarrier_All () = barrier Barrier_DMB -let DataSynchronizationBarrier_Reads () = barrier Barrier_DSB_LD -let DataSynchronizationBarrier_Writes () = barrier Barrier_DSB_ST -let DataSynchronizationBarrier_All () = barrier Barrier_DSB -let InstructionSynchronizationBarrier () = barrier Barrier_ISB +val DataMemoryBarrier_NonShReads : forall 'rv 'e. unit -> monad 'rv unit 'e +val DataMemoryBarrier_NonShWrites : forall 'rv 'e. unit -> monad 'rv unit 'e +val DataMemoryBarrier_NonShAll : forall 'rv 'e. unit -> monad 'rv unit 'e +val DataMemoryBarrier_InnerShReads : forall 'rv 'e. unit -> monad 'rv unit 'e +val DataMemoryBarrier_InnerShWrites : forall 'rv 'e. unit -> monad 'rv unit 'e +val DataMemoryBarrier_InnerShAll : forall 'rv 'e. unit -> monad 'rv unit 'e +val DataMemoryBarrier_OuterShReads : forall 'rv 'e. unit -> monad 'rv unit 'e +val DataMemoryBarrier_OuterShWrites : forall 'rv 'e. unit -> monad 'rv unit 'e +val DataMemoryBarrier_OuterShAll : forall 'rv 'e. unit -> monad 'rv unit 'e +val DataMemoryBarrier_FullShReads : forall 'rv 'e. unit -> monad 'rv unit 'e +val DataMemoryBarrier_FullShWrites : forall 'rv 'e. unit -> monad 'rv unit 'e +val DataMemoryBarrier_FullShAll : forall 'rv 'e. unit -> monad 'rv unit 'e +let DataMemoryBarrier_NonShReads () = barrier (Barrier_DMB (A64_NonShare, A64_barrier_LD)) +let DataMemoryBarrier_NonShWrites () = barrier (Barrier_DMB (A64_NonShare, A64_barrier_ST)) +let DataMemoryBarrier_NonShAll () = barrier (Barrier_DMB (A64_NonShare, A64_barrier_all)) +let DataMemoryBarrier_InnerShReads () = barrier (Barrier_DMB (A64_InnerShare, A64_barrier_LD)) +let DataMemoryBarrier_InnerShWrites () = barrier (Barrier_DMB (A64_InnerShare, A64_barrier_ST)) +let DataMemoryBarrier_InnerShAll () = barrier (Barrier_DMB (A64_InnerShare, A64_barrier_all)) +let DataMemoryBarrier_OuterShReads () = barrier (Barrier_DMB (A64_OuterShare, A64_barrier_LD)) +let DataMemoryBarrier_OuterShWrites () = barrier (Barrier_DMB (A64_OuterShare, A64_barrier_ST)) +let DataMemoryBarrier_OuterShAll () = barrier (Barrier_DMB (A64_OuterShare, A64_barrier_all)) +let DataMemoryBarrier_FullShReads () = barrier (Barrier_DMB (A64_FullShare, A64_barrier_LD)) +let DataMemoryBarrier_FullShWrites () = barrier (Barrier_DMB (A64_FullShare, A64_barrier_ST)) +let DataMemoryBarrier_FullShAll () = barrier (Barrier_DMB (A64_FullShare, A64_barrier_all)) + +val DataSynchronizationBarrier_NonShReads : forall 'rv 'e. unit -> monad 'rv unit 'e +val DataSynchronizationBarrier_NonShWrites : forall 'rv 'e. unit -> monad 'rv unit 'e +val DataSynchronizationBarrier_NonShAll : forall 'rv 'e. unit -> monad 'rv unit 'e +val DataSynchronizationBarrier_InnerShReads : forall 'rv 'e. unit -> monad 'rv unit 'e +val DataSynchronizationBarrier_InnerShWrites : forall 'rv 'e. unit -> monad 'rv unit 'e +val DataSynchronizationBarrier_InnerShAll : forall 'rv 'e. unit -> monad 'rv unit 'e +val DataSynchronizationBarrier_OuterShReads : forall 'rv 'e. unit -> monad 'rv unit 'e +val DataSynchronizationBarrier_OuterShWrites : forall 'rv 'e. unit -> monad 'rv unit 'e +val DataSynchronizationBarrier_OuterShAll : forall 'rv 'e. unit -> monad 'rv unit 'e +val DataSynchronizationBarrier_FullShReads : forall 'rv 'e. unit -> monad 'rv unit 'e +val DataSynchronizationBarrier_FullShWrites : forall 'rv 'e. unit -> monad 'rv unit 'e +val DataSynchronizationBarrier_FullShAll : forall 'rv 'e. unit -> monad 'rv unit 'e +let DataSynchronizationBarrier_NonShReads () = barrier (Barrier_DSB (A64_NonShare, A64_barrier_LD)) +let DataSynchronizationBarrier_NonShWrites () = barrier (Barrier_DSB (A64_NonShare, A64_barrier_ST)) +let DataSynchronizationBarrier_NonShAll () = barrier (Barrier_DSB (A64_NonShare, A64_barrier_all)) +let DataSynchronizationBarrier_InnerShReads () = barrier (Barrier_DSB (A64_InnerShare, A64_barrier_LD)) +let DataSynchronizationBarrier_InnerShWrites () = barrier (Barrier_DSB (A64_InnerShare, A64_barrier_ST)) +let DataSynchronizationBarrier_InnerShAll () = barrier (Barrier_DSB (A64_InnerShare, A64_barrier_all)) +let DataSynchronizationBarrier_OuterShReads () = barrier (Barrier_DSB (A64_OuterShare, A64_barrier_LD)) +let DataSynchronizationBarrier_OuterShWrites () = barrier (Barrier_DSB (A64_OuterShare, A64_barrier_ST)) +let DataSynchronizationBarrier_OuterShAll () = barrier (Barrier_DSB (A64_OuterShare, A64_barrier_all)) +let DataSynchronizationBarrier_FullShReads () = barrier (Barrier_DSB (A64_FullShare, A64_barrier_LD)) +let DataSynchronizationBarrier_FullShWrites () = barrier (Barrier_DSB (A64_FullShare, A64_barrier_ST)) +let DataSynchronizationBarrier_FullShAll () = barrier (Barrier_DSB (A64_FullShare, A64_barrier_all)) + +val InstructionSynchronizationBarrier : forall 'rv 'e. unit -> monad 'rv unit 'e +let InstructionSynchronizationBarrier () = barrier (Barrier_ISB ()) val TMCommitEffect : unit -> M unit -let TMCommitEffect () = barrier Barrier_TM_COMMIT +let TMCommitEffect () = barrier (Barrier_TM_COMMIT ()) let duplicate_bits (Vector bits start direction,len) = let bits' = repeat bits len in |