diff options
| author | Shaked Flur | 2015-03-19 12:02:27 +0000 |
|---|---|---|
| committer | Shaked Flur | 2015-03-19 12:02:27 +0000 |
| commit | 43453cecde967d2ffa61ca11ac62860ec7699ae2 (patch) | |
| tree | d7940c7b276076dda364233c82c7dc271893ad41 /src | |
| parent | 3453e4982f6d3b6112b0d3c8d114c425d91aa330 (diff) | |
added constructors for aarch64 read_kind and write_kind
Diffstat (limited to 'src')
| -rw-r--r-- | src/lem_interp/interp_interface.lem | 24 |
1 files changed, 21 insertions, 3 deletions
diff --git a/src/lem_interp/interp_interface.lem b/src/lem_interp/interp_interface.lem index 0b77909d..213b7d51 100644 --- a/src/lem_interp/interp_interface.lem +++ b/src/lem_interp/interp_interface.lem @@ -197,9 +197,27 @@ end (* Data structures for building up instructions *) -type read_kind = Read_plain | Read_reserve | Read_acquire -type write_kind = Write_plain | Write_conditional | Write_release -type barrier_kind = Sync | LwSync | Eieio | Isync | DMB | DMB_ST | DMB_LD | DSB | DSB_ST | DSB_LD | ISB +type read_kind = + (* common reads *) + Read_plain + (* Power reads *) + | Read_reserve + (* AArch64 reads *) + | Read_acquire | Read_exclusive | Read_exclusive_acquire | Read_stream + +type write_kind = + (* common writes *) + Write_plain + (* Power writes *) + | Write_conditional + (* AArch64 writes *) + | Write_release | Write_exclusive | Write_exclusive_release + +type barrier_kind = + (* Power barriers *) + Sync | LwSync | Eieio | Isync + (* AArch64 barriers *) + | DMB | DMB_ST | DMB_LD | DSB | DSB_ST | DSB_LD | ISB (*Map between external functions as preceived from a Sail spec and the actual implementation of the function *) type external_functions = list (string * (Interp.value -> Interp.value)) |