diff --git a/flat b/flat index 7d2386d..6ed7c63 100755 --- a/flat +++ b/flat @@ -1,2 +1,2 @@ #!/bin/sh -./rmem -model flat "$@" +$(dirname "$0")/rmem -model flat "$@" diff --git a/flatFetchOpt b/flatFetchOpt index 8d4e9b2..3d4fd5a 100755 --- a/flatFetchOpt +++ b/flatFetchOpt @@ -1,2 +1,2 @@ #!/bin/sh -./rmem -model flat -shallow_embedding true -eager true -hash_prune true -priority_reduction true -model fetch-relaxed -eager_fetch_unmodified true -loop_limit 2 -thread_fetch_limit 10 "$@" +$(dirname "$0")/rmem -model flat -shallow_embedding true -eager true -hash_prune true -priority_reduction true -model fetch-relaxed -eager_fetch_unmodified true -loop_limit 2 -thread_fetch_limit 10 "$@" diff --git a/flatOpt b/flatOpt index 219e134..9ebb7db 100755 --- a/flatOpt +++ b/flatOpt @@ -1,2 +1,2 @@ #!/bin/sh -./rmem -model flat -shallow_embedding true -eager true -hash_prune true -priority_reduction true "$@" +$(dirname "$0")/rmem -model flat -shallow_embedding true -eager true -hash_prune true -priority_reduction true "$@" diff --git a/promising b/promising index 58e49a4..7dc6f25 100755 --- a/promising +++ b/promising @@ -1,2 +1,2 @@ #!/bin/sh -./rmem -hash_prune false -model promising -shallow_embedding true "$@" +$(dirname "$0")/rmem -hash_prune false -model promising -shallow_embedding true "$@" diff --git a/promisingOpt b/promisingOpt index 3f92f5b..e91011c 100755 --- a/promisingOpt +++ b/promisingOpt @@ -1,2 +1,2 @@ #!/bin/sh -./rmem -model promising -shallow_embedding true -model promise_first "$@" -hash_prune false -model promising_parallel_thread_state_search +$(dirname "$0")/rmem -model promising -shallow_embedding true -model promise_first "$@" -hash_prune false -model promising_parallel_thread_state_search diff --git a/src_top/isa_model.ml b/src_top/isa_model.ml index 234b518..9492967 100644 --- a/src_top/isa_model.ml +++ b/src_top/isa_model.ml @@ -167,6 +167,7 @@ module Make (ISADefs: ISADefs) (TransSail: Trans.TransSail) : S = struct | V_ctor ("Barrier_RISCV_r_w", _) -> Barrier_RISCV_r_w | V_ctor ("Barrier_RISCV_w_r", _) -> Barrier_RISCV_w_r | V_ctor ("Barrier_RISCV_i", _) -> Barrier_RISCV_i + | V_ctor ("Barrier_RISCV_tso", _) -> Barrier_RISCV_tso | V_ctor ("Barrier_x86_MFENCE", _) -> Barrier_x86_MFENCE | _ -> failwith "unknown barrier kind in interp2__bk_to_bk" in