diff options
| author | Alasdair Armstrong | 2020-02-21 19:55:43 +0000 |
|---|---|---|
| committer | Alasdair Armstrong | 2020-02-21 19:55:43 +0000 |
| commit | dd32e257ddecdeece792b508cc05c9acab153e70 (patch) | |
| tree | 90bd5914841bca24d82315ae781f7e5c34c0c1f5 | |
| parent | a9627e00d3141153958e448c2814ea906f837566 (diff) | |
Add barriers to regfp.sail for full ARMv8
Again use an $ifdef to avoid breaking RMEM. We can't use the same
barrier_kind, because we *really* want a plain enumeration both for
its simple SMT representation and a simple 1 to 1 mapping to the cat
models used by herd.
Technically for Isla, all the read_kind/write_kind/barrier_kind etc
types can be defined separately on a per-architecture basis anyway, so
maybe using this file at all is a bit of an anachronism.
| -rw-r--r-- | lib/regfp.sail | 30 |
1 files changed, 30 insertions, 0 deletions
diff --git a/lib/regfp.sail b/lib/regfp.sail index 86b3cf17..7e5c9153 100644 --- a/lib/regfp.sail +++ b/lib/regfp.sail @@ -78,6 +78,35 @@ enum write_kind = { Write_X86_locked } +$ifdef ARM_SPEC +enum barrier_kind = { + Barrier_DMB_SY, + Barrier_DMB_ST, + Barrier_DMB_LD, + Barrier_DMB_ISH, + Barrier_DMB_ISHST, + Barrier_DMB_ISHLD, + Barrier_DMB_NSH, + Barrier_DMB_NSHST, + Barrier_DMB_NSHLD, + Barrier_DMB_OSH, + Barrier_DMB_OSHST, + Barrier_DMB_OSHLD, + Barrier_DSB_SY, + Barrier_DSB_ST, + Barrier_DSB_LD, + Barrier_DSB_ISH, + Barrier_DSB_ISHST, + Barrier_DSB_ISHLD, + Barrier_DSB_NSH, + Barrier_DSB_NSHST, + Barrier_DSB_NSHLD, + Barrier_DSB_OSH, + Barrier_DSB_OSHST, + Barrier_DSB_OSHLD, + Barrier_ISB +} +$else enum a64_barrier_domain = { A64_FullShare, A64_InnerShare, @@ -113,6 +142,7 @@ union barrier_kind = { Barrier_RISCV_i : unit, Barrier_x86_MFENCE : unit } +$endif enum trans_kind = { Transaction_start, |