blob: abab216376dd405cba798067d2947993c2910e16 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
|
open import Pervasives
open import Sail_impl_base
open import Vector
open import Sail_values
open import Prompt
val rMem_NORMAL : forall 'e. (vector bitU * integer) -> M 'e (vector bitU)
val rMem_STREAM : forall 'e. (vector bitU * integer) -> M 'e (vector bitU)
val rMem_ORDERED : forall 'e. (vector bitU * integer) -> M 'e (vector bitU)
val rMem_ATOMICL : forall 'e. (vector bitU * integer) -> M 'e (vector bitU)
val rMem_ATOMIC_ORDERED : forall 'e. (vector bitU * integer) -> M 'e (vector bitU)
let rMem_NORMAL (addr,size) = read_memory Read_plain addr size
let rMem_STREAM (addr,size) = read_memory Read_stream addr size
let rMem_ORDERED (addr,size) = read_memory Read_acquire addr size
let rMem_ATOMIC (addr,size) = read_memory Read_exclusive addr size
let rMem_ATOMIC_ORDERED (addr,size) = read_memory Read_exclusive_acquire addr size
val wMem_Addr_NORMAL : forall 'e. (vector bitU * integer) -> M 'e unit
val wMem_Addr_ORDERED : forall 'e. (vector bitU * integer) -> M 'e unit
val wMem_Addr_ATOMIC : forall 'e. (vector bitU * integer) -> M 'e unit
val wMem_Addr_ATOMIC_ORDERED : forall 'e. (vector bitU * integer) -> M 'e unit
let wMem_Addr_NORMAL (addr,size) = write_memory_ea Write_plain addr size
let wMem_Addr_ORDERED (addr,size) = write_memory_ea Write_release addr size
let wMem_Addr_ATOMIC (addr,size) = write_memory_ea Write_exclusive addr size
let wMem_Addr_ATOMIC_ORDERED (addr,size) = write_memory_ea Write_exclusive_release addr size
val wMem_Val_NORMAL : forall 'e. (integer * vector bitU) -> M 'e unit
val wMem_Val_ATOMIC : forall 'e. (integer * vector bitU) -> M 'e bitU
let wMem_Val_NORMAL (_,v) = write_memory_val v >>= fun _ -> return ()
(* in ARM the status returned is inversed *)
let wMem_Val_ATOMIC (_,v) = write_memory_val v >>= fun b -> return (if b then O else I)
val DataMemoryBarrier_Reads : forall 'e. unit -> M 'e unit
val DataMemoryBarrier_Writes : forall 'e. unit -> M 'e unit
val DataMemoryBarrier_All : forall 'e. unit -> M 'e unit
val DataSynchronizationBarrier_Reads : forall 'e. unit -> M 'e unit
val DataSynchronizationBarrier_Writes : forall 'e. unit -> M 'e unit
val DataSynchronizationBarrier_All : forall 'e. unit -> M 'e unit
val InstructionSynchronizationBarrier : forall 'e. unit -> M 'e unit
let DataMemoryBarrier_Reads () = barrier DMB_LD
let DataMemoryBarrier_Writes () = barrier DMB_ST
let DataMemoryBarrier_All () = barrier DMB
let DataSynchronizationBarrier_Reads () = barrier DSB_LD
let DataSynchronizationBarrier_Writes () = barrier DSB_ST
let DataSynchronizationBarrier_All () = barrier DSB
let InstructionSynchronizationBarrier () = barrier Isync
|
