Fix pp of ifetch

src_concurrency_model/machineDefFlatStorageSubsystem.lem

@@ -661,6 +661,15 @@ let flat_make_ui_storage_subsystem_state
           | Nothing ->
               flat_ui_ic_writes_unchanged ss'.flat_ss_ic_writes
           end;
+
+        ui_flat_ss_transitions_icache_update =
+          List.filter
+            (fun (n, t) ->
+              match t with
+              | SS_trans (SS_only (SS_Flat_icache_update _ _ _) _) -> true
+              | _ -> false
+              end)
+            transitions;
     |>
 
 

src_concurrency_model/machineDefSystem.lem

@@ -289,7 +289,7 @@ let enumerate_transitions_of_system
     | Just ioid ->
       (* this is currently dead code, the lock is only used with the
       Flat model which has no ss transitions *)
-      [t | forall (t MEM ss_transitions) | principal_ioid_of_ss_trans t = ioid]
+      [t | forall (t MEM ss_transitions) | principal_ioid_of_ss_trans t = Just ioid]
     end
     $> List.map (storage_trans_to_trans state)
   in
@@ -724,7 +724,7 @@ let make_cex_instruction_instance
     cex_instance_ioid = i.instance_ioid;
     cex_program_loc = i.program_loc;
     cex_program_opcode = i.program_opcode;
-    cex_instruction = ensure_fetched i.instruction; 
+    cex_instruction = (* ensure_fetched *) i.instruction;
     cex_instruction_kind = i.instruction_kind;
     (* register part *)
     cex_regs_in = i.regs_in;

src_concurrency_model/machineDefTypes.lem

@@ -843,20 +843,20 @@ type ss_only_trans =
   | SS_Flat_icache_update of thread_id * address * (write * slices)
 
 let principal_ioid_of_ss_only_trans = function
-  | SS_PLDI11_partial_coherence_commit w1 _      -> w1.w_ioid (* or maybe the other one? *)
-  | SS_PLDI11_propagate_write_to_thread (w, _) _ -> w.w_ioid
-  | SS_PLDI11_write_reaches_coherence_point w    -> w.w_ioid
-  | SS_PLDI11_propagate_barrier_to_thread b _    -> b.b_ioid
-  | SS_POP_propagate_event_to_thread e tid       -> principal_ioid_of_flowing_event e
-  | SS_POP_partially_satisfy_read r _            -> r.r_ioid
-  | SS_Flowing_flow_write_to_memory w            -> w.w_ioid
-  | SS_Flowing_flow_barrier_to_memory b          -> b.b_ioid
-  | SS_Flowing_flow_satisfied_read_to_memory r   -> r.r_ioid
-  | SS_Flowing_reorder_events e1 _               -> principal_ioid_of_flowing_event e1
-  | SS_Flowing_flow_to_segment e                 -> principal_ioid_of_flowing_event e
-  | SS_Flowing_partially_satisfy_read r _        -> r.r_ioid
-  | SS_TSO_propagate_write_to_memory w           -> w.w_ioid
-  | SS_Flat_icache_update _ _ _                  -> (0, 0) (* TODO: is this right? *)
+  | SS_PLDI11_partial_coherence_commit w1 _      -> Just w1.w_ioid (* or maybe the other one? *)
+  | SS_PLDI11_propagate_write_to_thread (w, _) _ -> Just w.w_ioid
+  | SS_PLDI11_write_reaches_coherence_point w    -> Just w.w_ioid
+  | SS_PLDI11_propagate_barrier_to_thread b _    -> Just b.b_ioid
+  | SS_POP_propagate_event_to_thread e tid       -> Just (principal_ioid_of_flowing_event e)
+  | SS_POP_partially_satisfy_read r _            -> Just r.r_ioid
+  | SS_Flowing_flow_write_to_memory w            -> Just w.w_ioid
+  | SS_Flowing_flow_barrier_to_memory b          -> Just b.b_ioid
+  | SS_Flowing_flow_satisfied_read_to_memory r   -> Just r.r_ioid
+  | SS_Flowing_reorder_events e1 _               -> Just (principal_ioid_of_flowing_event e1)
+  | SS_Flowing_flow_to_segment e                 -> Just (principal_ioid_of_flowing_event e)
+  | SS_Flowing_partially_satisfy_read r _        -> Just r.r_ioid
+  | SS_TSO_propagate_write_to_memory w           -> Just w.w_ioid
+  | SS_Flat_icache_update _ _ _                  -> Nothing
   end
 
 (* transitions that are initiated by the storage subsystem but also change the thread state *)
@@ -917,7 +917,7 @@ type sys_ss_trans 'ts 'ss = ss_trans_t 'ss (maybe (thread_cont unit 'ts))
 
 let principal_ioid_of_ss_trans = function
   | SS_only t _   -> principal_ioid_of_ss_only_trans t
-  | SS_sync t _ _ -> principal_ioid_of_ss_sync_trans t
+  | SS_sync t _ _ -> Just (principal_ioid_of_ss_sync_trans t)
   end
 
 (** thread transitions *)
@@ -1153,7 +1153,7 @@ type trans 'i 'ts 'ss =
 
 let principal_ioid_of_trans (t: trans 'i 'ts 'ss) =
   match t with
-  | SS_trans t -> Just (principal_ioid_of_ss_trans t)
+  | SS_trans t -> principal_ioid_of_ss_trans t
   | T_trans t  -> Just (ioid_of_thread_trans t)
   end
 
@@ -1245,7 +1245,7 @@ type ui_icache =
      ui_ic_tid: thread_id;
   |>
 
-type flat_ui_storage_subsystem_state 'ts 'ss =
+type flat_ui_storage_subsystem_state 'i 'ts 'ss =
   <|  (* storage state *)
       ui_flat_ss_memory_writes : list (changed3 (write * slices));
       (* storage transitions: none *)
@@ -1256,6 +1256,7 @@ type flat_ui_storage_subsystem_state 'ts 'ss =
       ui_flat_ss_icaches : map thread_id ui_icache;
       (* the global buffer of writes that can be fetched from *)
       ui_flat_ss_fetch_buf : list (changed3 write);
+      ui_flat_ss_transitions_icache_update: list (ui_trans 'i 'ts 'ss);
   |>
 
 type tso_ui_storage_subsystem_state 'i 'ts 'ss =
@@ -1271,7 +1272,7 @@ type tso_ui_storage_subsystem_state 'i 'ts 'ss =
 type ui_storage_subsystem_state 'i 'ts 'ss =
   | PLDI11_UI_storage  of pldi11_ui_storage_subsystem_state 'i 'ts 'ss
   | Flowing_UI_storage of flowing_ui_storage_subsystem_state 'i 'ts 'ss
-  | Flat_UI_storage    of flat_ui_storage_subsystem_state 'ts 'ss
+  | Flat_UI_storage    of flat_ui_storage_subsystem_state 'i 'ts 'ss
   | POP_UI_storage     of pop_ui_storage_subsystem_state 'i 'ts 'ss
   | TSO_UI_storage     of tso_ui_storage_subsystem_state 'i 'ts 'ss
 

src_concurrency_model/promising.lem

@@ -509,7 +509,7 @@ let p_make_cex_instruction_info
     cex_instance_ioid = i.ii_ioid;
     cex_program_loc = i.ii_program_loc;
     cex_program_opcode = i.ii_program_opcode;
-    cex_instruction = i.ii_instruction; 
+    cex_instruction = Fetched i.ii_instruction;
     cex_instruction_kind = i.ii_kind;
     (* register part *)
     cex_regs_in = Set.fromList (List.map fst i.ii_reg_reads);

src_top/graphviz_base.ml

@@ -142,7 +142,13 @@ type i = ConcModel.instruction_ast
    (match i.cex_instruction_kind with
    | IK_barrier _ -> String.concat "" (List.map (fun b -> Pp.pp_pretty_eiid m b.beiid) i.cex_committed_barriers)
    | _ -> "")
-   (*^ "i"*) ^ baseid_of_instruction i ^ " " ^ ConcModel.pp_instruction_ast m m.pp_symbol_table i.cex_instruction i.cex_program_loc
+   (*^ "i"*) ^ baseid_of_instruction i ^ " " ^
+   (match i.cex_instruction with
+    | InstructionSemantics.Unfetched -> "UNFETCHED"
+    | InstructionSemantics.Fetched inst ->
+        ConcModel.pp_instruction_ast m m.pp_symbol_table inst i.cex_program_loc
+    | InstructionSemantics.Fetch_error -> "FETCH-ERROR")
+
 
 
  let portid_of_write (w:write) = str_to_write_portid (Pp.pp_eiid w.weiid)

src_top/pp.ml

@@ -2267,7 +2267,7 @@ let flowing_pp_ui_storage_subsystem_state pp_instruction_ast m model ss =
   end*)
 
 
-let flat_pp_ui_storage_subsystem_state m model ss =
+let flat_pp_ui_storage_subsystem_state pp_instruction_ast m model ss =
   let memory =
     pp_changed3_list m pp_write_slices_uncoloured ss.ui_flat_ss_memory_writes in
 
@@ -2293,6 +2293,8 @@ let flat_pp_ui_storage_subsystem_state m model ss =
     sprintf "[%s]"
       (pp_list m pp_ic_write (Pmap.bindings_list ss.ui_flat_ss_ic_writes)) in
 
+  let pp_ss_transitions ts =
+    String.concat "\n" (List.map (pp_cand pp_instruction_ast m) ts) ^ "\n" in
 
   (*begin match m.Globals.pp_kind with
   | Ascii ->*)
@@ -2302,6 +2304,7 @@ let flat_pp_ui_storage_subsystem_state m model ss =
        if m.pp_kind <> Hash then "" else
        sprintf "  Old writes = %s"            old_writes; !linebreak;
        sprintf "  Icaches = %s"                 icaches; !linebreak;
+       sprintf "%s"                             (pp_ss_transitions ss.ui_flat_ss_transitions_icache_update);
        sprintf "  Buffer = %s"                  buffer; !linebreak;
        sprintf "  IC waiting = %s"              ic_writes; !linebreak;
       ]
@@ -2455,7 +2458,7 @@ let pp_ui_storage_subsystem_state pp_instruction_ast m model ss =
   match ss with
   | PLDI11_UI_storage  ui_storage_subsystem -> pldi11_pp_ui_storage_subsystem_state  pp_instruction_ast m model ui_storage_subsystem
   | Flowing_UI_storage ui_storage_subsystem -> flowing_pp_ui_storage_subsystem_state pp_instruction_ast m model ui_storage_subsystem
-  | Flat_UI_storage    ui_storage_subsystem -> flat_pp_ui_storage_subsystem_state    m model ui_storage_subsystem
+  | Flat_UI_storage    ui_storage_subsystem -> flat_pp_ui_storage_subsystem_state    pp_instruction_ast m model ui_storage_subsystem
   | POP_UI_storage     ui_storage_subsystem -> pop_pp_ui_storage_subsystem_state     pp_instruction_ast m model ui_storage_subsystem
   | TSO_UI_storage     ui_storage_subsystem -> tso_pp_ui_storage_subsystem_state     pp_instruction_ast m model ui_storage_subsystem
 

src_top/tikz.ml

@@ -372,7 +372,11 @@ let make_tikz_graph
       instructions_path_from_tree [] state.cex_instruction_tree
       |> List.map (fun inst ->
           let pp_instruction =
-            pp_instruction_ast m m.pp_symbol_table inst.cex_instruction inst.cex_program_loc
+            match inst.cex_instruction with
+            | InstructionSemantics.Unfetched -> "UNFETCHED"
+            | InstructionSemantics.Fetched i ->
+                pp_instruction_ast m m.pp_symbol_table i inst.cex_program_loc
+            | InstructionSemantics.Fetch_error -> "FETCH-ERROR"
             (* escape some characters; see the documentation of the
             LaTeX listings package (6.1 Listins inside arguments) *
             |> replace '\\' "\\\\"

web_interface_tests.mk

@@ -33,7 +33,7 @@ $(INSTALLDIR)/tests/AArch64:
 # since litmus-tests-armv8a-system is separated from -private,
 # there could be clash of names (e.g. @all),
 # so put the system tests in a subdir.
-	cp -ar $(AArch64SystemTESTSDIR)/tests $@/AArch64_System
+	cp -ar $(AArch64SystemTESTSDIR)/tests $@/system
 
 install_AArch64_tests: | $(INSTALLDIR)/tests/AArch64-elf
 $(INSTALLDIR)/tests/AArch64-elf:
@@ -159,7 +159,7 @@ $(eval $(call gen-at,AArch64,tutorial.files,Tutorial,  non-mixed-size/TUTORIAL/@
 $(eval $(call gen-at,AArch64,POPL16.files,Modelling the ARMv8 architecture (POPL16),non-mixed-size/@popl16))
 $(eval $(call gen-at,AArch64,POPL17.files,Mixed-size Concurrency (POPL17),mixed-size/HAND/@popl17))
 $(eval $(call gen-at,AArch64,POPL18.files,Simplifying ARM Concurrency (POPL18),@popl18))
-$(eval $(call gen-at,AArch64,POPL20.files,Systems concurrency (POPL20),AArch64_System/@popl2020))
+$(eval $(call gen-at,AArch64,ESOP20.files,Instruction fetch (ESOP20),system/@esop2020))
 $(eval $(call gen-at,AArch64,HAND.files,Hand-written,non-mixed-size/HAND/@all))
 $(eval $(call gen-at,AArch64,SHAKED.files,More hand-written,non-mixed-size/SHAKED/@all))
 $(eval $(call gen-at,AArch64,linuxComp.files,Linux compiled,non-mixed-size/LinuxCompiled/@all))