Skip to content

[tools] Add mlogselect tool #1973

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
maranget merged 2 commits into from
Sep 18, 2026
Merged

[tools] Add mlogselect tool #1973

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
92e177c
[tools] Add mlogselect tool
maranget Aug 27, 2026
b501e4f
[tools] Add cram test for mlogselect
maranget Sep 4, 2026
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
9 changes: 6 additions & 3 deletions tools/dune
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -10,7 +10,8 @@
mheader
splitdot
trTrue
lexMiaou)
lexMiaou
lexLogSelect)

(executables
(names
Expand Down Expand Up @@ -54,7 +55,8 @@
miaou
cat2lisp
dot2desc
cat2table)
cat2table
mlogselect)
(public_names
mfind7
moutcomes7
Expand Down Expand Up @@ -96,7 +98,8 @@
miaou7
cat2lisp
dot2desc7
cat2table7)
cat2table7
mlogselect7)
(libraries herdtools unix str)
(modules_without_implementation arch_tools))

Expand Down
19 changes: 19 additions & 0 deletions tools/lexLogSelect.mli
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,19 @@
(****************************************************************************)
(* the diy toolsuite *)
(* *)
(* Jade Alglave, University College London, UK. *)
(* Luc Maranget, INRIA Paris-Rocquencourt, France. *)
(* *)
(* Copyright 2026-present Institut National de Recherche en Informatique et *)
(* en Automatique and the authors. All rights reserved. *)
(* *)
(* This software is governed by the CeCILL-B license under French law and *)
(* abiding by the rules of distribution of free software. You can use, *)
(* modify and/ or redistribute the software under the terms of the CeCILL-B *)
(* license as circulated by CEA, CNRS and INRIA at the following URL *)
(* "http://www.cecill.info". We also give a copy in LICENSE.txt. *)
(****************************************************************************)

(** Fast lexing of logs, for selection *)

@fsestini fsestini Sep 4, 2026

Copy link
Copy Markdown
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Fast lexing of logs, for selection

It seems this lexing module is doing quite a bit more than just lexing, as it currently implements the whole tool's functionality including mutable state updates and stdout printing.

Could we separate lexing from log selection and output? I think it would be cleaner if the lexer only classified tokens/lines, with a separate module/function taking care of log filtering and printing.

I would also like to point out that this module adds another lexer/parser alongside existing modules like lexLog_tools, lexHashLog, etc., which, from a quick look, seem to all implement their own slightly different parsing logic for the same log format. Is there a reason for this apparent duplication? Could we instead implement a single lexer/parser for log files that is shared among all the log-processing tools?

@maranget maranget Sep 4, 2026 •
edited
Loading

Copy link
Copy Markdown
Member Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Fast lexing of logs, for selection

It seems this lexing module is doing quite a bit more than just lexing, as it currently implements the whole tool's functionality including mutable state updates and stdout printing.
Could we separate lexing from log selection and output? I think it would be cleaner if the lexer only classified tokens/lines, with a separate module/function taking care of log filtering and printing.

Having one pass tools is old fashioned, I admit. The task at hand here remains simple: identify begin and end markers, extract test name. In my old-fashioned (outdated, maybe) view, a simple tool that does everything is adequate.

I would also like to point out that this module adds another lexer/parser alongside existing modules like lexLog_tools, lexHashLog, etc., which, from a quick look, seem to all implement their own slightly different parsing logic for the same log format. Is there a reason for this apparent duplication? Could we instead implement a single lexer/parser for log files that is shared among all the log-processing tools?

We could do that, and would be more robust against log format evolution. However, this is more involved than writing the simple tool I have needed to select offending test outputs while debugging PR #1970....

@fsestini fsestini Sep 4, 2026

Copy link
Copy Markdown
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Having one pass tools is old fashioned, I admit. The task at hand here remains simple: identify begin and end markers, extract test name. In my old-fashioned (outdated, maybe) view, a simple tool that does everything is adequate.

Could you clarify what you mean by "one pass"? Is this about reading the input file once?

We could do that, and would be more robust against log format evolution. However, this is more involved than writing the simple tool I have needed to select offending test outputs while debugging PR #1970....

Of course, it doesn't need to happen now! Though perhaps I would add a "TODO" comment and/or create a Github ticket about it so that we don't forget.

@maranget maranget Sep 9, 2026

Copy link
Copy Markdown
Member Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Could you clarify what you mean by "one pass"? Is this about reading the input file once?

Hum not exactly one pass, I meant a tool that acts incrementally while reading its input, by opposion with a tool that would read the file completely before performing any specific work.


val from_chan : (string -> bool) -> in_channel -> unit
91 changes: 91 additions & 0 deletions tools/lexLogSelect.mll
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,91 @@
(****************************************************************************)
(* the diy toolsuite *)
(* *)
(* Jade Alglave, University College London, UK. *)
(* Luc Maranget, INRIA Paris-Rocquencourt, France. *)
(* *)
(* Copyright 2026-present Institut National de Recherche en Informatique et *)
(* en Automatique and the authors. All rights reserved. *)
(* *)
(* This software is governed by the CeCILL-B license under French law and *)
(* abiding by the rules of distribution of free software. You can use, *)
(* modify and/ or redistribute the software under the terms of the CeCILL-B *)
(* license as circulated by CEA, CNRS and INRIA at the following URL *)
(* "http://www.cecill.info". We also give a copy in LICENSE.txt. *)
(****************************************************************************)

(** Extract records from herd/litmus/msum logs *)

(*
* The extraction is a bit complicated by the variety of log formats...
* + Fortunately all records starts with `Test `<name>, where <name>
* is the name of the test.
* + Unfortunately, the format of record end differ:
* - The records produced by herd and msum end at the first empty line.
* - The records produced by litmus include an empty line that'
* follows the validation tag (Ok/No). The end at the "Time"
* information that always follow the Hash metadata.
Comment on lines +20 to +27

@fsestini fsestini Sep 4, 2026

Copy link
Copy Markdown
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Could we not, instead, change herd7, litmus7 etc. so that they produce a unified, standardised log format, thus making this kind of lexing/parsing easier?

I also think some of the complexity arises from the fact that tools like mlogselect, mlog2names, moutcomes, etc. , need to interface with a logging format that seems primarily meant for human consumption. I think ideally herd7 and litmus7 would instead provide a way to generate logs in a standard machine-readable format, such as JSON. That would make parsing a non-problem and would remove ambiguity arising from presentation details like blank lines etc. Moreover, with logs in a standard machine-readable format, many of the workflows that now require a bespoke tool like mlogselect could be implemented in a few line using existing tools. As a simple example:

$ cat results.jsonl
{"name":"Test1", "states":[{...},{...}], ...}
{"name":"Test2", "states":[], ...}

# select logs by name (similar to mlogselect7)
$ jq 'select(.name == "Test2")' results.jsonl
{
  "name": "Test2",
  "states": [],
  ...
}

# select logs with at least one outcome state (similar to mlog2name7)
$ jq -r 'select(.states | length > 0) | .name' results.jsonl
Test1

@maranget maranget Sep 4, 2026 •
edited
Loading

Copy link
Copy Markdown
Member Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Slighty changing the log format looks a very good idea. What can easily be done is:

  1. Keep the start marker Test <name>
  2. Adopt the empty line as the end marker. This is a small change to litmus7.
    Unfortunately, we sill have to lex old logs... In partcular I have a decade of litmus logs at hand.

I remain attached to readable text format for logs. I want to be able to read logs without the mediation of a tool. But of course, we should facilitate the processing of logs. In my opinion, mlogselect is not a very complex lexer, even more so if the format of logs is changed a bit.

@psafont psafont Sep 4, 2026 •
edited
Loading

Copy link
Copy Markdown
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I think ideally herd7 and litmus7 would instead provide a way to generate logs in a standard machine-readable format, such as JSON.

I've been thinking about a logging module, that can be used to centralize decisions regarding loglevel, as well as verbosity. My main concern was to reduce the number of functors since logging is per-process usually instead of per-module.

Regardless of my initial purpose, this could be used as an opportunity to start generating structured logging and easily select the format of the logging, using different formatters. There's a nice library available in the ecosystem that allows this kind of separation of concerns: https://erratique.ch/software/logs

Would people be open to this kind change to the codebase?

@fsestini fsestini Sep 4, 2026

Copy link
Copy Markdown
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I remain attached to readable text format for logs. I want to be able to read logs without the mediation of a tool.

Note that "machine-readable" doesn't necessarily imply "hard to read by humans". E.g. YAML is a common machine-readable format that is also quite nice to read by humans, IMO. Moreover the machine-readable format doesn't need to (and shouldn't) replace the existing readable one; it could be put behind an opt-in flag litmus7 --json-logs. Of course these are just examples.

I think my overall point is that if we need tools to routinely consume logs, it's a good idea to make the log format easy to process, and ideally leverage existing standards and tools if possible. Whether that is achieved by making the current format more machine-readable, or by offering an option like litmus7 --json-logs to opt-in to a separate format, is to be determined.

@fsestini fsestini Sep 4, 2026

Copy link
Copy Markdown
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Regardless of my initial purpose, this could be used as an opportunity to start generating structured logging and easily select the format of the logging, using different formatters. There's a nice library available in the ecosystem that allows this kind of separation of concerns: https://erratique.ch/software/logs

Note, in fact, that logs is already included in the herdtools7.opam file, although its usage is not widespread at the moment. FWIW, in general, I'm very much in favour of a more logs-like approach, though I'm not sure it applies to simple tools like mlogselect.

* The output of mlogselect adopts the convention of herd and msum.
*)
{
open LexMisc

let outline = print_endline

type st = { inside:bool; hash_seen:bool; }
let st_false = { inside=false; hash_seen=false; }
let st_true = { inside=true; hash_seen=false; }
}

let digit = [ '0'-'9' ]
let alpha = [ 'a'-'z' 'A'-'Z']
let name = (alpha|'_'|'.'|'$') (alpha|digit|'_'| '.')*
let blank = [' ' '\t']
let testname = (alpha|digit|'_' | '/' | '.' | '-' | '+' | '[' | ']' | ':')+
let nl = '\r'?'\n'
let validation = "Ok"|"No"

rule main ok st = parse
| "Test" blank+ (testname as t)
(blank+ name)? as line nl
{ incr_lineno lexbuf ;
let st = if ok t then st_true else st_false in
if st.inside then outline line ;
main ok st lexbuf }
| nl (* An empty line ends one test log in herd/msum logs *)
{ incr_lineno lexbuf ;
if st.inside then outline "" ;
main ok st_false lexbuf }
| validation as line nl nl
(* Unless the empty line follows a validation tag,
as in some litmus logs *)
{ incr_lineno lexbuf ; incr_lineno lexbuf ;
if st.inside then outline line ;
main ok st lexbuf }
| ['h''H']['a''A']['s''S']['h''H']
blank* '=' blank* [^' ''\t''\n''\r']+ blank* as line nl
(* Detect hash metadata *)
{ incr_lineno lexbuf ;
if st.inside then outline line ;
main ok {st with hash_seen=true; } lexbuf }
| "Time" blank+ testname blank+ (digit|'.')+ blank* as line nl
(* Detect timing information that ends records in litmus logs *)
{ incr_lineno lexbuf ;
if st.inside then outline line ;
if st.hash_seen then begin (* End of record, if follows hash metadata *)
if st.inside then outline "" ; (* Add empty line *)
main ok st_false lexbuf
end else
main ok st lexbuf }
| [^'\n''\r']+ as line nl
{ incr_lineno lexbuf ;
if st.inside then outline line ;
main ok st lexbuf }
| [^'\n''\r']* as line eof
{ if st.inside && line <> "" then outline line }

{

let from_chan ok chan = main ok st_false @@ Lexing.from_channel chan

}
65 changes: 65 additions & 0 deletions tools/mlogselect.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,65 @@
(****************************************************************************)
(* the diy toolsuite *)
(* *)
(* Jade Alglave, University College London, UK. *)
(* Luc Maranget, INRIA Paris-Rocquencourt, France. *)
(* *)
(* Copyright 2026-present Institut National de Recherche en Informatique et *)
(* en Automatique and the authors. All rights reserved. *)
(* *)
(* This software is governed by the CeCILL-B license under French law and *)
(* abiding by the rules of distribution of free software. You can use, *)
(* modify and/ or redistribute the software under the terms of the CeCILL-B *)
(* license as circulated by CEA, CNRS and INRIA at the following URL *)
(* "http://www.cecill.info". We also give a copy in LICENSE.txt. *)
(****************************************************************************)

(* Extract some records from logs. *)
open Printf
open OptNames

let prog =
if Array.length Sys.argv > 0 then Sys.argv.(0)
else "mlogelect"

let arg = ref None

let () =
Arg.parse
OptNames.parse_withselect
(fun s ->
arg :=
match !arg with
| None -> Some s
| Some _ -> raise (Arg.Bad "one argument at most"))
(sprintf "usage: %s [options]* log?" prog)

(* Read names *)

module Check =
CheckName.Make
(struct
let verbose = 0
let rename = []
let select = !select
let names = !names
let oknames = !oknames
let excl = !excl
let nonames = !nonames
end)

let zyva () =
match !arg with
| None ->
LexLogSelect.from_chan Check.ok stdin
| Some f ->
Misc.input_protect
(LexLogSelect.from_chan Check.ok)
f

let () =
try zyva ()
with
| Misc.(Fatal msg|UserError msg) ->
Warn.warn_always "Fatal error: %s" msg
| _ -> assert false
9 changes: 9 additions & 0 deletions tools/tests/mlogselect/dune
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,9 @@
(cram
(deps
%{bin:mlogselect7}
%{bin:msum7}
%{bin:herd7}
(glob_files %{workspace_root}/herd/tests/instructions/X86_64/*.litmus)
(glob_files %{workspace_root}/doc/SB-PPC.litmus)
(glob_files %{workspace_root}/doc/SB-PPC*.log)
(source_tree %{workspace_root}/herd/libdir)))
87 changes: 87 additions & 0 deletions tools/tests/mlogselect/mlogselect.t
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,87 @@
Extract test output from litmus log
$ mlogselect7 -oknames SB-PPC ../../../doc/SB-PPC.log
Test SB-PPC Allowed
Histogram (3 states)
1784 *>0:r3=0; 1:r3=0;
498564:>0:r3=1; 1:r3=0;
499652:>0:r3=0; 1:r3=1;
Ok
Witnesses
Positive: 1784, Negative: 998216
Condition exists (0:r3=0 /\ 1:r3=0) is validated
Hash=4edecf6abc507611612efaecc1c4a9bc
Observation SB-PPC Sometimes 1784 998216
Time SB-PPC 0.55

Extract test output from msum log
$ msum7 ../../../doc/SB-PPC*.log 2>/dev/null | mlogselect7 -select ../../../doc/SB-PPC.litmus
Test SB-PPC Allow
Histogram (3 states)
3549 :> 0:r3=0; 1:r3=0;
999146 :> 0:r3=0; 1:r3=1;
997305 :> 0:r3=1; 1:r3=0;
Ok
Witnesses
Positive: 3549 Negative: 1996451
Condition exists (0:r3=0 /\ 1:r3=0) is validated
Hash=4edecf6abc507611612efaecc1c4a9bc
Time SB-PPC 1.12

Extract test output from herd log
$ for i in $(seq 1 2 9); do echo "A00$i"; done > NAMES
$ herd7 -set-libdir ../../../herd/libdir ../../../herd/tests/instructions/X86_64/*.litmus | mlogselect7 -names NAMES -nonames A003,A004 -oknames A012
Test A001 Required
States 1
0:rip=0;
Ok
Witnesses
Positive: 1 Negative: 0
Condition forall (0:rip=0)
Observation A001 Always 1 0
Time A001 0.00
Hash=5586d6c213112d3683c915b4d7bb700a

Test A005 Required
States 1
0:rax=0;
Ok
Witnesses
Positive: 1 Negative: 0
Condition forall (0:rax=0)
Observation A005 Always 1 0
Time A005 0.00
Hash=33e970980643a03ccf92e4989259cd01

Test A007 Required
States 1
0:rax=4;
Ok
Witnesses
Positive: 1 Negative: 0
Condition forall (0:rax=4)
Observation A007 Always 1 0
Time A007 0.00
Hash=a335aafc9060d9b8c4320424ba909740

Test A009 Required
States 1
0:rcx=-1;
Ok
Witnesses
Positive: 1 Negative: 0
Condition forall (0:rcx=-1)
Observation A009 Always 1 0
Time A009 0.00
Hash=7ca3c35015d75a877ccf509d75062e79

Test A012 Required
States 1
[x]=1;
Ok
Witnesses
Positive: 1 Negative: 0
Condition forall ([x]=1)
Observation A012 Always 1 0
Time A012 0.00
Hash=3b021e40517dcff1f1cb8894d645b677

Loading