[tools] Enhance compatibility of tools that read logs by maranget · Pull Request #1970 · herd/herdtools7

maranget · 2026-08-18T15:42:55Z

The printing of faults has changed over time:

Initially faults did not hold a type string
Introduction of type string.
MMU faults are prefixed with "D-" or "I-" to specify the memory accessed (data or instruction).

Tools that compare or compute on logs , such as mcompare7 and msum7 are impacted. It is always possible to use the -faulttype false option to ignore fault types for tools to produce correct results.

However those results are not as precise as they should. This PR is an attempt to fix the problem by:

Ignore the "D-" and "I-" prefixes while comparing with a non-prefixed type string (standard behaviour).
Consider that all MMU faults are from data (activated by option -mmu-faults-as-data true).

Notice that the default for all tools are -faulttype true mmu-faults-as-data true .

fsestini

Hi @maranget , I've left some comments.

Could you also please provide some example inputs that I can use to reproduce the issue, and to see for myself how this PR impacts the output?

On a similar note, I think this PR should also include some dune cram tests, as those are designed to check expected input-output behaviour of CLI programs, which seems appropriate here. In particular it would be useful to have tests that show mcompare and mcmp side by side on equal inputs.

fsestini · 2026-08-25T08:15:54Z

+      "<bool> consider fault types, default %b" !ft)
+
+let parse_datafault ft =
+   ("-datafault", Arg.Bool (fun b -> ft := b),


I wonder if we could use a more informative name for this option. Maybe something along the lines of -mmu-faults-as-data?

Fixed, thanks.

fsestini · 2026-08-25T08:18:18Z

+let parse_datafault ft =
+   ("-datafault", Arg.Bool (fun b -> ft := b),
+    Printf.sprintf
+      "<bool> all MMU faults are from data, default %b" !ft)


all MMU faults are from data

If I understand correctly, this is not quite the case. For example, a fault that already has a I- prefix is not treated as being from data, regardless of the status of this option. If so, can we make this documentation text more precise?

Yes we can! What about all non-specific MMU faults are from data (i.e. are implicitly prefixed with "D-")

fsestini · 2026-08-25T08:36:52Z

+let split_at_diprefix s =
+  let len = String.length s in
+  if len > 2 then
+    match String.sub s 0 2 with
+    | ("D-"|"I-") as pref -> pref,String.sub s 2 (len-2)
+    | _ -> "",s
+  else "",s


split_at_diprefix could reuse has_diprefix for checking the presence of a DI prefix.

Moreover, this function uses "" as a sentinel to signal "no prefix", which feels stringly typed, since callers never actually use the first pair component and only need the stripped suffix when a prefix exists. Therefore, returning an optional like this would be clearer IMO:

let strip_diprefix s = if has_diprefix s then let len = String.length s in Some (String.sub s 2 (len - 2)) else None

Of course, strip_diprefix should reuse `has_diprefix". Ok for the new return type.

maranget · 2026-08-26T14:04:17Z

Could you also please provide some example inputs that I can use to reproduce the issue, and to see for myself how this PR impacts the output?

On a similar note, I think this PR should also include some dune cram tests, as those are designed to check expected input-output behaviour of CLI programs, which seems appropriate here. In particular it would be useful to have tests that show mcompare and mcmp side by side on equal inputs.

I'll know little about cram test, I'll have a go.

maranget · 2026-08-28T13:25:59Z

Significant rewriting of diff and compare functions under way -> draft

maranget · 2026-08-31T11:40:17Z

Hi @fsestini, @psafont and @relokin. I have finally decided not to rely on state lines to be totally ordered (which they are not) for merging, diffing and intersecting them. Instead, I have adopted a two level algorithm: group lines by identical bindings, those groups of lines are totally ordered, and then rely on, naive, quadratic algorithms for operating inside these groups. See commit 7715bee for details.

I have also added a small cram test. The test checks that mcompare7 and mcmp7 produce the same result on a small example.

psafont

I'm surprised by the amount of files and code changes needed to do this change, but I can't really say I would approach it in a different way, or why. I do have some questions to understand these changes better

psafont · 2026-09-01T09:56:54Z

   ("-faulttype", Arg.Bool (fun b -> ft := b),
    Printf.sprintf
-      "<bool> consider fault types, default %b" !ft);
+      "<bool> consider fault types in comparisons, default %b" !ft)


Please bear with me for a minute. I'm trying to understand the reason why is this PR changing the code is changing, and I'm confused regarding the relation between parsing a boolean argument and the module "checkName".

From what I understand this module was made to parse names of litmus tests coming from user-provided CLI arguments.

What's has this with parsing the faults?

The module "CheckName" functionality is to select the input tests. It includes the definition of command line options such as -names, -excl etc. The place looked convenient to host other command line definitions that are common to several tools (-int32 for instance). This is a mistake and it sould be fixed, perhaps not in this PR?

This is a mistake and it sould be fixed, perhaps not in this PR?

Absolutely, I've seen other modules for handling args, so it might make sense to consolidate the code into a single module or something like that.

TODO in a future PR.

psafont · 2026-09-01T10:20:33Z

+  then
+    Printf.eprintf "Found heterogeneous test %s\n%!" name ;
+  if FaultKinds.equal fk1 fk2
+  then opt xs ys


Is the opt diffing safe to use when both tests are not homogeneous with regards to the fault kinds, even when these are equal?

I guess not. I had assumed that outcomes with equal bindings have fault types of the same kind. There is no reason for this to be true. I'll fix it. Nice catch.

I think union_faults solves it nicely now

Well, some work still under way. I have decided to have a proper compare function on faults that will distinguish fauts syntactically, as correct hashconsing of states rely on it. That some syntactically different faults are the same will be handled in a more explicit way, by a equivalent function.

Well, some work still under way. I have decided to have a proper compare function on faults that will distinguish fauts syntactically, as correct hashconsing of states rely on it. That some syntactically different faults are the same will be handled in a more explicit way, by a equivalent function.

@maranget I don't see these changes reflected in the PR, so just wanted to check whether you are still planning to work on this, or if you think this PR is ready for re-review.

I had overwritten those changes by an untimely "git push --force". They are now present again. See here for the definitions of the equivalent and compare functions on hashconsed faults and here for the call to HashedFault.equivalent in tool/logState.ml.

maranget · 2026-09-01T16:07:49Z

I'm surprised by the amount of files and code changes needed to do this change, but I can't really say I would approach it in a different way, or why. I do have some questions to understand these changes better

I am surprised too. Maybe the -mmu-faults-as-data option could belong to a different PR. I have also changed the "hashconsed" module a bit, to avoid using == directly, resulting in changing files beyond what is strictly necessary for the objective of handling the new "D-" and "I-" prefixes.

maranget · 2026-09-04T09:04:33Z

Hi @psafont and @relokin . I have squashed and rebased this PR and would like to merge today. I'd value any comment.

fsestini · 2026-09-04T16:01:45Z

I think we should add a few more cases to this test. In particular, the current cram test does not exercise the new -mmu-faults-as-data flag in the false case. In would appear that mcompare7 and mcmp7 disagree under -mmu-faults-as-data false, which I don't think is intended:

$ cat old.log Test T Allowed States 1 ~Fault(P0:L0,x,MMU:Translation); Ok Hash=x $ cat new.log Test T Allowed States 1 ~Fault(P0:L0,x,D-MMU:Translation); Ok Hash=x $ dune exec mcompare7 -- -mmu-faults-as-data false old.log new.log *Diffs* |Kind | old.log new.log -------------------------------------------------- -------------------------------------------------- T|Allow| [~fault(P0:L0,x,MMU:Translation)] == |Ok | $ dune exec mcmp7 -- -mmu-faults-as-data false old.log new.log T

Interesting. If I am not wrong mcompare7 ignores negative fault occurrences. The fast path of mcmp7 does not ignore them, as it relies on hashedconsed identity nodes to perform comparisons.

Well, if mcompare7 ignore negative fault occurrences, mcmp7 can also ignore them, by simply not inserting them in its internal data structure. I'll implement this technique.

maranget · 2026-09-04T22:06:34Z

Here is a copy of a comment that might otherwise get lost.

I had overwritten significant changes changes by an untimely "git push --force". Namely I have separated the ordering of state llnes (or outcomes) and the equivalence of faults. They are now present again. See here for the definitions of the equivalent and compare functions on hashconsed faults and here for the call to HashedFault.equivalent in tool/logState.ml.

maranget · 2026-09-07T15:12:33Z

Hi @psafont and @relokin (and maybe @artkhyzha, I guess you have been involved in adding the "D-" and "I-" prefixes) . This PR experienced many adventures, resulting in partial and total rewrites. Things went far beyond to where I initially expected: fixing the compare tools so that I can compare new herd vmsa logs to old logs from before the introduction of the "D-" and "I-" prefixes...

Thanks to all the remarks and suggestions that have been made, the situation of log comparisions is now much cleaner than before: from series of fixes to the clear understanding that we cannot totally order the lines of a test log, especially when those logs have been recorded at different times. But the compare tools must still evolve now. I'd really like to have your informed opinion once more before merging.

relokin · 2026-09-09T17:45:00Z

+let datafault_key = "-mmu-faults-as-data"
+
+let parse_datafault ft =
+   (datafault_key, Arg.Bool (fun b -> ft := b),
+    Printf.sprintf


I think this is fine but also not necessary, all old logs that said MMU:<type> should match with D-MMU:<type>. I don't see a situation where we would set the parameter to false.

Hi @relokin. I agree with you that MMU: in old logs most certainly refer to D-MMU:. Setting the switch "-mmu-faults-as-data" to false may help debugging by having the internal functions to operate on stuctures as close as possible to the input.

relokin · 2026-09-09T17:49:00Z

+let equivalent_ftype_names s1 s2 =
+  match strip_diprefix s1,strip_diprefix s2 with
+  | None,Some s2 -> String.equal s1 s2
+  | Some s1,None -> String.equal s1 s2
+  | _,_ -> String.equal s1 s2


Maybe I have misunderstood this, but wouldn't we want to just change D-MMU to MMU for backwards compatibility but maintain I-MMU?

This would contradict the intuitive meaning of faults in final conditions. For instance exists Fault(..,..,MMU:Permission) is intuitively understood as: "there exists a permission fault, would it be from data or instruction". This "intuitive" semantics already governs the behaviour of herd7, while PR #1988 adjusts litmus7.

I mean I saw no reason for tools and herd7 to interpret prefixless MMU fault types differently. Given our hypothesis on old logs tests generating only "D-MMU:..." faults, there should be no practical implications for log comparisons and sums.

MMU fault types have been prefixed with "D-" or "I-" (PR #1518). This commit ignores such prefixes in comparisons of final states and select the prefixed names for unions. The tools that read logs such as **mcompare7** and **msum7** should now be able to handle new and old logs to compare and sum them. Let us defined "states" as lists of outcomes, an outcome being a list of final location values, faults and fault absence. For instance: ``` 0:x0=1; [x]=1; Fault(P0:L0,D-MMU:Permission); ~Fault(P1:L1,y); ``` Given the change of format of faults over time, it cannot be guaranted that list of outcomes are totally ordered. As a consequent the traditional linear algorithm on sorted list cannot be trusted. However, location bindings are totally ordered. Hence, we can group states that are identical up to faults, apply the linear algorithms at this level and apply the naive, quadratic algorithms, to those groups of states with identical bindings. For instance consider aggregating (unioning): ``` [x]=0; ~Fault(P0); ~Fault(P1); [x]=1; Fault(P0,x,D-MMU:Permission); ~Fault(P1,x); [x]=1; Fault(P0,x,D-MMU:Permission); Fault(P1,x,D-MMU:Translation); ``` and the old, without fault types, log: ``` [x]=1; Fault(P0,x); ~Fault(P1,x); [x]=1; Fault(P0,x); Fault(P1,x); [x]=1; ~Fault(P0,x); Fault(P1,x); [x]=2; Fault(P0); ~Fault(P1); ``` The `[x]=0;...` and `[x]=2;...` find their way to the result by the sole comparison of their binding components. By contrast the `[x]=1;...` outcomes undergo pairwise comparisons, resulting in the three outcomes: ``` [x]=1; Fault(P0,x,D-MMU:Permission); ~Fault(P1,x); [x]=1; Fault(P0,x,D-MMU:Permission); Fault(P1,x,D-MMU:Translation); [x]=1; ~Fault(P0,x); Fault(P1,x); ``` Notice that, when possible, the newer and more precise ouctome is selected We also add a new option `-mmu-faults-as-data <bool>` When true (default), all MMU faults that are not prefixed by "D-" or "I-" are considered to be from data. That is, the names of faults that start with "MMU:" are implicitly prefixed with "D-". This treatement of old logs is not strictly necessary. It offers a simple solution to the "new prefixes" problem though.

maranget · 2026-09-14T08:42:29Z

PR #1970 merged, thanks @psafont, @fsestini and @relokin for your suggestions and reviews.

[tools] Fix bug in state comparison Very unfortunate error in implementing the difference of two sorted lists, introduced by PR #1970.

maranget force-pushed the compat-mcompare branch from 3f8436a to 89e42ae Compare August 19, 2026 14:44

maranget marked this pull request as ready for review August 19, 2026 15:03

maranget requested review from fsestini and relokin August 19, 2026 15:04

maranget force-pushed the compat-mcompare branch 2 times, most recently from 4239e5d to 394ba68 Compare August 21, 2026 14:11

psafont reviewed Aug 24, 2026

View reviewed changes

Comment thread tools/HashedFault.ml Outdated

fsestini reviewed Aug 25, 2026

View reviewed changes

Comment thread tools/logState.ml Outdated

maranget force-pushed the compat-mcompare branch from 394ba68 to 9c946af Compare August 26, 2026 13:56

maranget force-pushed the compat-mcompare branch 3 times, most recently from 3474bd1 to 9b395d9 Compare August 28, 2026 13:22

maranget marked this pull request as draft August 28, 2026 13:24

maranget force-pushed the compat-mcompare branch 2 times, most recently from 2d42c8e to 429106a Compare August 31, 2026 09:08

maranget marked this pull request as ready for review August 31, 2026 11:35

maranget force-pushed the compat-mcompare branch 4 times, most recently from f6e1411 to 7465906 Compare September 1, 2026 09:33

psafont reviewed Sep 1, 2026

View reviewed changes

maranget force-pushed the compat-mcompare branch from 7465906 to d476ff0 Compare September 1, 2026 16:27

psafont approved these changes Sep 2, 2026

View reviewed changes

maranget force-pushed the compat-mcompare branch from d476ff0 to fba068e Compare September 4, 2026 08:16

fsestini reviewed Sep 4, 2026

View reviewed changes

Comment thread tools/tests/mcompare.t/run.t Outdated

maranget force-pushed the compat-mcompare branch 2 times, most recently from be78c39 to 1fdbc1e Compare September 4, 2026 09:26

maranget mentioned this pull request Sep 4, 2026

[tools] Add mlogselect tool #1973

Merged

fsestini reviewed Sep 4, 2026

View reviewed changes

maranget force-pushed the compat-mcompare branch 2 times, most recently from d9fd7f6 to a703b50 Compare September 4, 2026 20:23

maranget force-pushed the compat-mcompare branch from a703b50 to 419ad69 Compare September 9, 2026 15:26

relokin reviewed Sep 9, 2026

View reviewed changes

maranget force-pushed the compat-mcompare branch from 419ad69 to c5f8eea Compare September 10, 2026 11:06

maranget added 2 commits September 14, 2026 09:51

[tools] Add cram test for mcompare/mcmp

c1e4ae6

maranget force-pushed the compat-mcompare branch from c5f8eea to c1e4ae6 Compare September 14, 2026 07:54

maranget merged commit 2a3e9d0 into master Sep 14, 2026
5 checks passed

maranget deleted the compat-mcompare branch September 14, 2026 08:43

maranget mentioned this pull request Sep 14, 2026

[tools] Fix bug in state comparison #2000

Merged

maranget added a commit that referenced this pull request Sep 14, 2026

Merge pull request #2000 from herd/fix-mcompare

46da782

[tools] Fix bug in state comparison Very unfortunate error in implementing the difference of two sorted lists, introduced by PR #1970.

Conversation

maranget commented Aug 18, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

Uh oh!

fsestini left a comment

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

maranget Aug 26, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

maranget commented Aug 26, 2026

Uh oh!

maranget commented Aug 28, 2026

Uh oh!

maranget commented Aug 31, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

psafont left a comment

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

maranget Sep 1, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Uh oh!

psafont Sep 1, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

maranget Sep 4, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Uh oh!

maranget commented Sep 1, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

maranget commented Sep 4, 2026

Uh oh!

Uh oh!

Choose a reason for hiding this comment

Uh oh!

maranget Sep 4, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Choose a reason for hiding this comment

Uh oh!

maranget Sep 4, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

maranget commented Aug 18, 2026 •

edited

Loading

maranget Aug 26, 2026 •

edited

Loading

maranget commented Aug 31, 2026 •

edited

Loading

maranget Sep 1, 2026 •

edited

Loading

psafont Sep 1, 2026 •

edited

Loading

maranget Sep 4, 2026 •

edited

Loading

maranget commented Sep 1, 2026 •

edited

Loading

maranget Sep 4, 2026 •

edited

Loading

maranget Sep 4, 2026 •

edited

Loading

maranget commented Sep 4, 2026 •

edited

Loading

maranget commented Sep 7, 2026 •

edited

Loading

maranget Sep 10, 2026 •

edited

Loading

maranget Sep 10, 2026 •

edited

Loading