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.

1 files changed, 17 insertions, 0 deletions

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))