From 721e2df47258531373b5db5ac38aa09dd960e718 Mon Sep 17 00:00:00 2001 From: Shaked Flur Date: Thu, 26 Oct 2023 08:49:46 +0100 Subject: [PATCH] PP 'node cs' for tikz Also fix some comments and minor fix to flowing. --- notes-2023-03-07-RISC-V-mem-acc-kind.txt | 42 +++++++++++++++++++ rmem_tiles.sh | 14 +++---- .../machineDefFlatStorageSubsystem.lem | 7 ++-- .../machineDefFlowingStorageSubsystem.lem | 23 +++++++++- .../machineDefPOPStorageSubsystem.lem | 1 - .../machineDefThreadSubsystem.lem | 11 +++-- src_concurrency_model/machineDefTypes.lem | 10 +++-- src_top/tikz.ml | 19 ++++++--- 8 files changed, 102 insertions(+), 25 deletions(-) create mode 100644 notes-2023-03-07-RISC-V-mem-acc-kind.txt diff --git a/notes-2023-03-07-RISC-V-mem-acc-kind.txt b/notes-2023-03-07-RISC-V-mem-acc-kind.txt new file mode 100644 index 0000000..9db69a5 --- /dev/null +++ b/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. diff --git a/rmem_tiles.sh b/rmem_tiles.sh index e88f293..1c07af2 100755 --- a/rmem_tiles.sh +++ b/rmem_tiles.sh @@ -197,13 +197,13 @@ 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\ \"\ @@ -211,15 +211,15 @@ run_tmux() { 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\ \"\ diff --git a/src_concurrency_model/machineDefFlatStorageSubsystem.lem b/src_concurrency_model/machineDefFlatStorageSubsystem.lem index 58420f4..34b0528 100644 --- a/src_concurrency_model/machineDefFlatStorageSubsystem.lem +++ b/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; |> diff --git a/src_concurrency_model/machineDefFlowingStorageSubsystem.lem b/src_concurrency_model/machineDefFlowingStorageSubsystem.lem index 03f8c8b..ffb0a68 100644 --- a/src_concurrency_model/machineDefFlowingStorageSubsystem.lem +++ b/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) diff --git a/src_concurrency_model/machineDefPOPStorageSubsystem.lem b/src_concurrency_model/machineDefPOPStorageSubsystem.lem index fdf5294..5702a2a 100644 --- a/src_concurrency_model/machineDefPOPStorageSubsystem.lem +++ b/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 diff --git a/src_concurrency_model/machineDefThreadSubsystem.lem b/src_concurrency_model/machineDefThreadSubsystem.lem index dd1a3a0..a301b7f 100644 --- a/src_concurrency_model/machineDefThreadSubsystem.lem +++ b/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 diff --git a/src_concurrency_model/machineDefTypes.lem b/src_concurrency_model/machineDefTypes.lem index 8f9d057..c0e40d4 100644 --- a/src_concurrency_model/machineDefTypes.lem +++ b/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 *) diff --git a/src_top/tikz.ml b/src_top/tikz.ml index 29abbc9..e38f4f0 100644 --- a/src_top/tikz.ml +++ b/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" ^