PP 'node cs' for tikz

Also fix some comments and minor fix to flowing.

notes-2023-03-07-RISC-V-mem-acc-kind.txt

@@ -0,0 +1,42 @@
+Trying to understand how RISC-V memory access annotations flow into RMEM.
+
+See sail-riscv/model/riscv_analysis.sail for the memory access annotations
+currently used by RISC-V (new-Sail). Those are then mapped in
+rmem/src_isa_defs/sail_1_2_convert.lem to old-Sail. And those are
+lifted in rmem/src_concurrency_model/instructionKindPredicates.lem to
+architecture specific predicates.
+
+Examples:
+ASM       | man model                | new-Sail                    | mapped to old-Sail
+LR.D      | reserved                 | Read_RISCV_reserved         | Read_RISCV_reserved
+LR.D.aq   | reserved + acquire-RCsc  | Read_RISCV_reserved_acquire | Read_RISCV_reserved_acquire_RCsc
+LR.D.aqrl | reserved + acquire-RCsc..| Read_RISCV_reserved_strong..| Read_RISCV_reserved_acquire_release
+                   ..+ release-RCsc  | .._acquire                  |
+LR.D.rl --- invalid ---
+
+ASM       | man model                   | new-Sail                        | mapped to old-Sail
+SC.D      | conditional                 | Write_RISCV_conditional         | Write_RISCV_conditional
+SC.D.rl   | conditional + release-RCsc  | Write_RISCV_conditional_release | Write_RISCV_conditional_release_RCsc
+SC.D.aqrl | conditional + acquire-RCsc..| Write_RISCV_conditional_strong..| Write_RISCV_conditional_acquire_release
+                      ..+ release-RCsc  | .._release
+SC.D.aq --- invalid ---
+
+ASM           | man model 'read, write' (new/old-Sail as above)
+AMOADD.D      | reserved, conditional
+AMOADD.D.aq   | reserved acquire-RCsc, conditional
+AMOADD.D.rl   | reserved, conditional + release-RCsc
+AMOADD.D.aqrl | reserved acquire-RCsc + release-RCsc, conditional + acquire-RCsc + release-RCsc
+
+The important rules from the RV manual mem-model:
+5. a has an acquire annotation;
+6. b has a release annotation;
+7. a and b both have RCsc annotations;
+Current RV non-Ztso ISA doesn't use RCpc at all.
+Future encodings might include:
+load + acquire-RCpc
+load + acquire-RCsc
+load + acquire-RCsc + release-RCsc
+store + release-RCpc
+store + release-RCsc
+store + acquire-RCsc + release-RCsc
+and similarly RCpc variants for LR, SC, and AMOs.

rmem_tiles.sh

@@ -197,29 +197,29 @@ run_tmux() {
       set -t : @rmem_layout state\
     " \
     " if -F \"#{==:#{@rmem_layout},state}\" \
-        \"break-pane -s :Console.1 -n SystemState ; \
+        \"break-pane -d -s :Console.top -n SystemState ; \
           join-pane -d -s :Trace.0 -t :Console.0 -h -p 40 ; \
-          join-pane -d -s :SystemState.0 -t :Console.0 -v -b -p 75 ; \
+          join-pane -d -s :SystemState.0 -t :Console.left -v -b -p 75 ; \
           set -t : @rmem_layout full\
         \" \
-        \"break-pane -s :Console.2 -n Trace ; \
-          break-pane -s :Console.1 -n SystemState ; \
+        \"break-pane -s :Console.right -n Trace ; \
+          break-pane -s :Console.top -n SystemState ; \
           select-window -t :Console ; \
           set -t : @rmem_layout console\
         \"\
     "
   tmux bind-key -n BTab \
     if -F "#{==:#{@rmem_layout},console}" \
       " join-pane -d -s :Trace.0 -t :Console.0 -h -p 40 ; \
-        join-pane -d -s :SystemState.0 -t :Console.0 -v -b -p 75 ; \
+        join-pane -d -s :SystemState.0 -t :Console.left -v -b -p 75 ; \
         set -t : @rmem_layout full\
       " \
       " if -F \"#{==:#{@rmem_layout},full}\" \
-          \"break-pane -s :Console.2 -n Trace ; \
+          \"break-pane -d -s :Console.right -n Trace ; \
             select-window -t :Console ; \
             set -t : @rmem_layout state\
           \" \
-          \"break-pane -s :Console.1 -n SystemState ; \
+          \"break-pane -d -s :Console.top -n SystemState ; \
             select-window -t :Console ; \
             set -t : @rmem_layout console\
           \"\

src_concurrency_model/machineDefFlatStorageSubsystem.lem

@@ -681,8 +681,7 @@ let flat_storage =
      ss_is_final_state                    = flat_ss_is_final_state ;
      ss_coherence                         = flat_ss_coherence ;
      ss_clean_reads                       = flat_ss_remove_old_read_requests;
-     ss_enumerate_transitions = enumerate_transitions_ss;
-     ss_receive_transition = 
-         fun p s tl -> flat_ss_receive_transition p s tl;
-     ss_make_ui_storage_state = flat_make_ui_storage_subsystem_state;
+     ss_enumerate_transitions             = enumerate_transitions_ss;
+     ss_receive_transition                = flat_ss_receive_transition;
+     ss_make_ui_storage_state             = flat_make_ui_storage_subsystem_state;
  |>

src_concurrency_model/machineDefFlowingStorageSubsystem.lem

@@ -356,6 +356,13 @@ let exclusives_future_edges exclusives order =
     end
   in
 
+  (* w ---co-> e'              ,--> e'
+   * |         ^              /     ^
+   * rf        |             fr     |
+   * |      ADD-THIS  and   /    ADD-THIS
+   * V         |           /        |
+   * r_exc --> w_exc      r_exc --> w_exc
+   *)
   {(w_exc, e')
     | forall  ((r_exc, (prev_ws, w_exc)) IN exclusives)
               ((e, e') IN order.relon_rel)
@@ -367,19 +374,33 @@ let exclusives_future_edges exclusives order =
       end
   } union
 
+  (* w <-ADD-- o             ,----- o
+   * |   THIS  |            /       |
+   * rf        co   and  ADD-THIS   co
+   * |         |           |        |
+   * V         V           V        V
+   * r_exc --> w_exc      r_exc --> w_exc
+   *)
   {(o, e)
     | forall  ((r_exc, (prev_ws, w_exc)) IN exclusives)
               (o IN (relonLeftOf w_exc order))
               (e IN order.relon_set)
     | o <> e && thread_of_flowing_event o <> thread_of_flowing_event w_exc &&
       (is_fe_write o || is_fe_future_write o) &&
-      overlapping_slices (slices_of_fe o) (slices_of_fe w_exc) &&
+      fe_addrs_intersect o w_exc &&
       match prev_slices r_exc prev_ws e with
       | Just s  -> overlapping_slices (slices_of_fe o) s
       | Nothing -> false
       end
   } union
 
+  (* w -order->fw_exc          ,--> fw_exc
+   * |         ^              /     ^
+   * rf        |           order    |
+   * |      ADD-THIS  and   /    ADD-THIS
+   * V         |           /        |
+   * r_exc --> w_exc      r_exc --> w_exc
+   *)
   {(w_exc, fw_exc)
     | forall  ((r_exc, (prev_ws, w_exc)) IN exclusives)
               ((_, (_, fw_exc)) IN exclusives)

src_concurrency_model/machineDefPOPStorageSubsystem.lem

@@ -337,7 +337,6 @@ let pop_ss_satisfy_read_action params state read_request write_request =
       (* the read is acquire or was partially satisfied *)
       (* update the read to record the write that satisfied it and the remaining unsat slices *)
       let read_request' =
-        let (read, _, write_slices) = unsafeFRead read_request in
         FRead read read_slices' (write_slices' ++ write_slices)
       in
       let state = pop_update_flowing_event state read_request read_request' in

src_concurrency_model/machineDefThreadSubsystem.lem

@@ -721,7 +721,7 @@ let pop_might_be_restarted params
 
 (* returns true iff a po-previous read request was issued after
 'read_request' (i.e. out of order) and was satisfied by a write to the
-same address different from 'wss' and 'wss' is not a forward from a
+same address different from 'wss', and 'wss' is not a forward from a
 write that is po-after that read request.
 NOTE: changes in this function need to be reflected in pop_load_sat_might_self_restart *)
 let pop_is_stale_read params
@@ -1088,7 +1088,9 @@ let pop_no_po_preceding_overlapping_unpropagated_writes
       forall (prev_write MEM prev_unpropagated_writes).
         not (non_empty_intersection write.w_addr prev_write.w_addr)
 
-
+(* TODO: SF: I think we should make it so that transitions are only held back by
+   po-preceding instructions. In this case, instead of checking the
+   po-succeeding loads, we should restart them if the transition is taken. *)
 let pop_all_reads_partially_satisfied_by_forwarding_issued_unsat_slices
       params iic write = 
   let issued _ iafter itafter =
@@ -1505,6 +1507,9 @@ let pop_finish_cand params state (iic: instruction_in_context 'i) : bool =
     true
   else if is_memory_load_instruction (ik iic.iic_instance) then
     pop_finish_load_cand params state iic
+  (* The following two cases seem like some leftovers from something. The above
+     committed_barriers <> [] case already covers these, so I don't know why
+     they are here. *)
   else if is_RISCV_fence_pr (ik iic.iic_instance) then
     true
   else if is_RISCV_fence_pw (ik iic.iic_instance) then
@@ -1775,7 +1780,7 @@ let pop_satisfy_stale_read_from_memory_action
 
 (* the reply from storage includes the forward-writes, but they might
    be old (from when the read was issued), so we need to set the value
-   for writes that were forwarded without value. This only does does
+   for writes that were forwarded without value. This only does
    anything if there is symbolic forwarding. *)
 let pop_read_from_memory_update_forward_writes iic request write_slices =
   (* as this is the point where we get the reply from storage, any

src_concurrency_model/machineDefTypes.lem

@@ -395,7 +395,11 @@ type flowing_storage_subsystem_state =
       flowing_ss_reordered : set (flowing_event * flowing_event);
 
       (* map read_requests of load-exclusives that are paired with store-exclusive
-      that is guaranteed to succeed, to the writes they read from *)
+      that is guaranteed to succeed, to the writes they read from, and to the
+      write of the paired store exclusive. Initially, when the load-exclusive is
+      issued, or when the success of a store-exclusive is guaranteed, we use FFWrite
+      to represent the future-write; later, when the write is propagated to storage
+      this is replaced with the actual FWrite. *)
       flowing_ss_exclusive_reads: map read_request (list (write * slices) * flowing_event);
       (* map writes of store-exclusives that are guaranteed to succeed,
       to the read_request of the paired load-exclusive; this read_request
@@ -439,8 +443,8 @@ type flat_storage_subsystem_state =
       flat_ss_ic_writes : map address (cache_maintenance_request * (list thread_id));
       (* the global buffer of writes that can be fetched from *)
       flat_ss_fetch_buf : list write;
-      (* record writes that flowed to memory in the order in which they
-      flowed (head is new); we need this to reconstruct coherence *)
+      (* record writes that propagated to memory in the order in which they
+      propagated (head is new); we need this to reconstruct coherence *)
       flat_ss_old_writes : list write;
       (* map read_requests of load-exclusives that are paired with store-exclusive
       that is guaranteed to succeed, to the writes they read from *)

src_top/tikz.ml

@@ -70,6 +70,13 @@ let make_tikz_graph
     !res
   in
 
+  (* Old version of pgf has some trouble parsing the special syntax of node cs
+     for eiids with numbers, as you get for mixed-size events, (e.g. '(a0)');
+     this function pp the explicit syntax which is easier to parse. *)
+  let node_cs (name: string) : string =
+    sprintf "node cs:name=%s" name
+  in
+
   let pp_tikz_pretty_ioid ioid =
     let (tid, ioid) = ioid in
     sprintf "%d-%d" tid ioid
@@ -493,8 +500,8 @@ let make_tikz_graph
         List.map
           (fun (w, w') ->
               pp_tikz_edge "co"
-                (pp_tikz_pretty_eiid m w.weiid)
-                (pp_tikz_pretty_eiid m w'.weiid))
+                (node_cs (pp_tikz_pretty_eiid m w.weiid))
+                (node_cs (pp_tikz_pretty_eiid m w'.weiid)))
           co
       in
                 "  % coherence\n" ^
@@ -516,8 +523,8 @@ let make_tikz_graph
                   pp_eiid
               else
                 pp_tikz_edge ("rf'=" ^ pp_tikz_write_slices_uncoloured m (w, ss))
-                  (pp_tikz_pretty_eiid m w.weiid)
-                  (pp_tikz_pretty_eiid m r.reiid)
+                  (node_cs (pp_tikz_pretty_eiid m w.weiid))
+                  (node_cs (pp_tikz_pretty_eiid m r.reiid))
           )
           rf
       in
@@ -533,8 +540,8 @@ let make_tikz_graph
         List.map
           (fun (r, (w, ss)) ->
               pp_tikz_edge ("fr'=" ^ pp_tikz_write_slices_uncoloured m (w, ss))
-                  (pp_tikz_pretty_eiid m r.reiid)
-                  (pp_tikz_pretty_eiid m w.weiid))
+                  (node_cs (pp_tikz_pretty_eiid m r.reiid))
+                  (node_cs (pp_tikz_pretty_eiid m w.weiid)))
           fr
       in
                 "  % from-read:\n" ^