Add a fast-cap-dirty PTE behavior

At present, the extra SC_Mod bit is ignored.  I have not yet done
the plumbing to add the requisite CASes to the PTW machinery.

Gate cap-store traps on storing a tagged value; if we're going to
clear the tag, act like we're storing data.

Author: nwf

src/cheri_insts.sail

@@ -1167,7 +1167,7 @@ function handle_store_cap_via_cap(rs, cs, cap_val, vaddrBits) = {
   } else if not(is_aligned_addr(vaddrBits, cap_size)) then {
     handle_mem_exception(vaddrBits, E_SAMO_Addr_Align());
     RETIRE_FAIL
-  } else match translateAddr(vaddrBits, Write(Cap)) {
+  } else match translateAddr(vaddrBits, Write(if rs_val.tag then Cap else Data)) {
     TR_Failure(E_Extension(EXC_CHERI_VMEM_STORE_CAP), _) => {
       handle_cheri_cap_exception(CapEx_TLBNoStoreCap, cs);
       RETIRE_FAIL
@@ -1315,7 +1315,7 @@ function handle_store_cond_cap_via_cap(cs2, cs, cap_val, vaddrBits) = {
     cancel_reservation();
     RETIRE_SUCCESS
   } else {
-    match translateAddr(vaddrBits, Write(Cap)) {
+    match translateAddr(vaddrBits, Write(if cs2_val.tag then Cap else Data)) {
       TR_Failure(E_Extension(EXC_CHERI_VMEM_STORE_CAP), _) => {
         handle_cheri_cap_exception(CapEx_TLBNoStoreCap, cs);
         RETIRE_FAIL

src/cheri_pte.sail

@@ -42,14 +42,40 @@ bitfield PTE_Bits : pteAttribs = {
  * gate their capability-load traps on the PTE bits (and sccsr.gclg[su]); that
  * is, we permit relaxing only the dependence on the tag bit itself.
  *
+ * While for StoreCap* the behaviors are as follows.  Again, SCI is an inhibit.
+ *
+ *   SCI  SC_Mod  Action
+ *
+ *    0      0    Permit tagged capability store
+ *    0      1    [Reserved]
+ *
+ *    1      0    Trap on tagged capability store
+ *    1      1    CAS the PTE to SC=0, SC_Mod=0 (i.e., reset both bits)
+ *
+ * It is permitted for implementations to ignore SC_Mod and behave as if it
+ * were always 0, at the expense of traps on cap-dirtying stores.  Note that
+ * SCI and SC_Mod are not quite like W and D: SCI is both the (negated)
+ * permission and dirty bit; SC_Mod just encapsulates a particular trap
+ * handler behavior.  This is again done for simplicity of gradual roll-out:
+ * permitting SC_Mod to be treated as always zero means fewer things to
+ * initially implement.
+ *
+ * The SCI=1 SC_Mod=1 behavior is described as a CAS of the PTE to close race
+ * conditions, much as with W and D.  Should the TLB have this state cached
+ * and then observe a SCI=0 SC_Mod=0 PTE, no PTE write is necessary.  On the
+ * other hand, if SCI=1 SC_Mod=0 is observed, the store operation must trap
+ * rather than transition the PTE to SCI=0 SC_Mod=0.
+ *
+ * At present, SC_Mod is ignored by the code below.
  */
 type extPte = bits(10)
 
 bitfield Ext_PTE_Bits : extPte = {
   LoadCapInh   : 9, /* Inhibit capability loads */
-  StoreCap     : 8, /* Permit capability stores */
+  StoreCapInh  : 8, /* Inhibit capability stores */
   LoadCap_Mod  : 7, /* Modify capability load inhibit; see above table */
   LoadCap_LCLG : 6, /* When cap. load gens. are in use, the "local" CLG */
+  StoreCap_Mod : 5, /* Modify capability store inhibit; see above table */
 }
 
 function isPTEPtr(p : pteAttribs, ext : extPte) -> bool = {
@@ -118,7 +144,7 @@ function checkPTEPermission(ac : AccessType(ext_access_type), priv : Privilege,
     (Write(Cap),      User)       => { if   p.U() == 0b1 & p.W() == 0b1
                                        then {
                                          let  e = Mk_Ext_PTE_Bits(ext);
-                                         if   e.StoreCap() == 0b1
+                                         if   e.StoreCapInh() == 0b0
                                          then (true, PTE_CAP_OK)
                                          else {
                                            /* Do not allow the address translation to proceed */
@@ -132,9 +158,9 @@ function checkPTEPermission(ac : AccessType(ext_access_type), priv : Privilege,
                                        then {
                                          let  e = Mk_Ext_PTE_Bits(ext);
                                          let  lcm = checkPTEPermission_LC(p, e);
-                                         if   e.StoreCap() == 0b1 & lcm == PTE_CAP_OK
+                                         if   e.StoreCapInh() == 0b0 & lcm == PTE_CAP_OK
                                          then (true, PTE_CAP_OK)
-                                         else if e.StoreCap() == 0b0
+                                         else if e.StoreCapInh() == 0b1
                                          /* return a failure since we should cause an exception */
                                          then (false, PTE_STORE_CAP_ERR)
                                          /* return a success since the translation should proceed */
@@ -154,7 +180,7 @@ function checkPTEPermission(ac : AccessType(ext_access_type), priv : Privilege,
     (Write(Cap),      Supervisor) => { let e = Mk_Ext_PTE_Bits(ext);
                                        if   (p.U() == 0b0 | do_sum) & p.W() == 0b1
                                        then {
-                                         if   e.StoreCap() == 0b1
+                                         if   e.StoreCapInh() == 0b0
                                          then (true,  PTE_CAP_OK)
                                          else (false, PTE_STORE_CAP_ERR)
                                        }
@@ -165,9 +191,9 @@ function checkPTEPermission(ac : AccessType(ext_access_type), priv : Privilege,
                                        if   (p.U() == 0b0 | do_sum) & p.R() == 0b1 & p.W() == 0b1
                                        then {
                                          let  lcm = checkPTEPermission_LC(p, e);
-                                         if   e.StoreCap() == 0b1 & lcm == PTE_CAP_OK
+                                         if   e.StoreCapInh() == 0b0 & lcm == PTE_CAP_OK
                                          then (true, PTE_CAP_OK)
-                                         else if e.StoreCap() == 0b0
+                                         else if e.StoreCapInh() == 0b1
                                          /* return a failure since we should cause an exception */
                                          then (false, PTE_STORE_CAP_ERR)
                                          /* return a success since the translation should proceed */