From 89771ed18298be5665f742f8cccc408284cc2939 Mon Sep 17 00:00:00 2001
From: Prashanth Mundkur
Date: Fri, 6 Jul 2018 15:07:27 -0700
Subject: An initial fix to riscv lr/sc, needs a review.

This uses a stronger model than the version in Sail-1 in order to
perform address alignment checks.  The reservation is kept on virtual
addresses, and maintained in the platform model, but now the lr/sc
definitions need calls to externs to update this state.  An
alternative was to reserve physical addresses, but that appeared to be
more complicated without a lot more changes.  Ideally, the model
should be parameterizable over both options.
---
 riscv/platform.ml | 17 +++++++++++++++++
 1 file changed, 17 insertions(+)

(limited to 'riscv/platform.ml')

diff --git a/riscv/platform.ml b/riscv/platform.ml
index 0366e601..ddae4840 100644
--- a/riscv/platform.ml
+++ b/riscv/platform.ml
@@ -97,7 +97,24 @@ let clint_size () = bits_of_int64 P.clint_size
 
 let insns_per_tick () = Big_int.of_int P.insns_per_tick
 
+(* load reservation *)
+
+let reservation = ref "none"  (* shouldn't match any valid address *)
+
+let load_reservation addr =
+  Printf.eprintf "reservation <- %s\n" (!reservation);
+  reservation := string_of_bits addr
+
+let match_reservation addr =
+  Printf.eprintf "reservation: %s, key=%s\n" (!reservation) (string_of_bits addr);
+  string_of_bits addr = !reservation
+
+let cancel_reservation () =
+  Printf.eprintf "reservation <- none\n";
+  reservation := "none"
+
 (* terminal I/O *)
+
 let term_write char_bits =
   let big_char = Big_int.bitwise_and (uint char_bits) (Big_int.of_int 255) in
   P.term_write (char_of_int (Big_int.to_int big_char))
-- 
cgit v1.2.3


From 03acdbccf2793cf7105fdd365df6f876681a99b2 Mon Sep 17 00:00:00 2001
From: Prashanth Mundkur
Date: Sat, 7 Jul 2018 15:24:23 -0700
Subject: Cancel riscv reservation before i/o scheduling, tweak reservation
 tracing.

---
 riscv/platform.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'riscv/platform.ml')

diff --git a/riscv/platform.ml b/riscv/platform.ml
index ddae4840..092df80f 100644
--- a/riscv/platform.ml
+++ b/riscv/platform.ml
@@ -102,7 +102,7 @@ let insns_per_tick () = Big_int.of_int P.insns_per_tick
 let reservation = ref "none"  (* shouldn't match any valid address *)
 
 let load_reservation addr =
-  Printf.eprintf "reservation <- %s\n" (!reservation);
+  Printf.eprintf "reservation <- %s\n" (string_of_bits addr);
   reservation := string_of_bits addr
 
 let match_reservation addr =
-- 
cgit v1.2.3