Merge remote branch 'experiments' into experiments

2 files changed, 52 insertions, 3 deletions

diff --git a/etc/power_header b/etc/power_header
new file mode 100644
index 00000000..eb01510e
--- /dev/null
+++ b/etc/power_header
@@ -0,0 +1,31 @@
+
+Copyright (c) 2015-2017 Gabriel Kerneis, Susmit Sarkar, Kathyrn Gray
+Copyright (c) 2015-2017 Peter Sewell
+All rights reserved.
+
+This software was developed by the University of Cambridge Computer
+Laboratory as part of the Rigorous Engineering of Mainstream Systems
+(REMS) project, funded by EPSRC grant EP/K008528/1.
+
+Redistribution and use in source and binary forms, with or without
+modification, are permitted provided that the following conditions
+are met:
+1. Redistributions of source code must retain the above copyright
+   notice, this list of conditions and the following disclaimer.
+2. Redistributions in binary form must reproduce the above copyright
+   notice, this list of conditions and the following disclaimer in
+   the documentation and/or other materials provided with the
+   distribution.
+
+THIS SOFTWARE IS PROVIDED BY THE AUTHOR AND CONTRIBUTORS ``AS IS''
+AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED
+TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A
+PARTICULAR PURPOSE ARE DISCLAIMED.  IN NO EVENT SHALL THE AUTHOR OR
+CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL,
+SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT
+LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF
+USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND
+ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY,
+OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT
+OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF
+SUCH DAMAGE.
diff --git a/etc/regfp.sail b/etc/regfp.sail
index fb15310a..cc057f2e 100644
--- a/etc/regfp.sail
+++ b/etc/regfp.sail
@@ -32,21 +32,31 @@ typedef diafp = const union {
 
 typedef read_kind = enumerate {
   Read_plain;
-  Read_tag;
   Read_reserve;
   Read_acquire;
   Read_exclusive;
   Read_exclusive_acquire;
-  Read_stream
+  Read_stream;
+  Read_RISCV_acquire;
+  Read_RISCV_strong_acquire;
+  Read_RISCV_reserved;
+  Read_RISCV_reserved_acquire;
+  Read_RISCV_reserved_strong_acquire;
+  Read_X86_locked;
 }
 
 typedef write_kind = enumerate {
   Write_plain;
-  Write_tag;
   Write_conditional;
   Write_release;
   Write_exclusive;
   Write_exclusive_release;
+  Write_RISCV_release;
+  Write_RISCV_strong_release;
+  Write_RISCV_conditional;
+  Write_RISCV_conditional_release;
+  Write_RISCV_conditional_strong_release;
+  Write_X86_locked;
 }
 
 typedef barrier_kind = enumerate {
@@ -62,6 +72,13 @@ typedef barrier_kind = enumerate {
   Barrier_DSB_LD;
   Barrier_ISB;
   Barrier_MIPS_SYNC;
+  Barrier_RISCV_rw_rw;
+  Barrier_RISCV_r_rw;
+  Barrier_RISCV_r_r;
+  Barrier_RISCV_rw_w;
+  Barrier_RISCV_w_w;
+  Barrier_RISCV_i;
+  Barrier_x86_MFENCE;
 }
 
 typedef trans_kind = enumerate {
@@ -72,6 +89,7 @@ typedef instruction_kind = const union {
   (barrier_kind) IK_barrier;
   (read_kind) IK_mem_read;
   (write_kind) IK_mem_write;
+  (read_kind, write_kind) IK_mem_rmw;
   IK_cond_branch;
   (trans_kind) IK_trans;
   IK_simple