[herd] Petty optimisation of the Cat interpreter#1855
Merged
Conversation
maranget
force-pushed
the
petty-opt-interpreter
branch
2 times, most recently
from
0287e14 to
ad9bfb2
Compare
maranget
changed the title
HadrienRenaud
changed the title
Comment on lines
+259
to
+264
| M.fold | ||
| (fun n _ r -> | ||
| if Elts.mem n nodes then | ||
| let _,r = dfs n r in r | ||
| else r) | ||
| m |
Collaborator
There was a problem hiding this comment.
Suggested change
| M.fold | |
| (fun n _ r -> | |
| if Elts.mem n nodes then | |
| let _,r = dfs n r in r | |
| else r) | |
| m | |
| Elts.fold (fun n r -> dfs n r |> snd) m |
But is it really different from scan_nodes_rel?
Member
Author
There was a problem hiding this comment.
I guess you mean:
Elts.fold (fun n r -> dfs n r |> snd) nodesThis is slightly different from scan_nodes_rel as regards the type of nodes (set vs. list).
I choosed to iterate over the map and not over the set because I worried about the cost of dfs n r in the case where there is no binding for n in the map m. However if nodes is small it would be better to iterate over the set. I have no good solution here.
Collaborator
There was a problem hiding this comment.
Oh I see what you mean, I had forgotten the case where nodes ⊄ domain(m).
I think probably your solution is better than mine.
In an ideal world it'd be nice to iterate over both at the same time, for example what baby does to compute the domain of a map.
HadrienRenaud
approved these changes
Jun 11, 2026
maranget
force-pushed
the
petty-opt-interpreter
branch
3 times, most recently
from
36b6275 to
2451721
Compare
maranget
force-pushed
the
petty-opt-interpreter
branch
4 times, most recently
from
7b1db3e to
3da02cd
Compare
maranget
force-pushed
the
petty-opt-interpreter
branch
from
3da02cd to
be7f652
Compare
Member
Author
|
Hi @HadrienRenaud, I'd like to merge soon. May I have your opinion on this last version? |
HadrienRenaud
approved these changes
Jul 7, 2026
HadrienRenaud
left a comment
HadrienRenaud
left a comment
Collaborator
There was a problem hiding this comment.
Just some documentation comments. Please merge at your convenience.
+ [restrict_codomain_to_set] Optimised evaluation of `r;[s]` + [restrict_domain_transitive_closure] Optimised evaluation of `[s];r+` Gains are probably minor, but implementation is easy. +
+ Compute `(...|r+|....)+` as `(...|r|...)+` + Optimise `r;[s]`. + Optimise `[s];r+`.
maranget
force-pushed
the
petty-opt-interpreter
branch
from
be7f652 to
1e23070
Compare
Member
Author
|
Merged, thanks @HadrienRenaud. |
Contributor
|
Hi @maranget , Another report of LKMM issue. After this merge, I get this fatal error in running herd7 on many LKMM litmus tests: Said line in linux-kernel.bell looks like this: I see a lot of activity in herd these days and this might be a transitory issue, but can you please have a look? FYI, reverting 1e23070 on current master can paper over the error, but ends up in behavior changes of most litmus tests. |
Member
Author
|
Thanks for this @akiyks. This is indeed a "petty" bug. I publish a fix soon. |
maranget
added a commit
that referenced
this pull request
Jul 10, 2026
Since PR #1855, the polymorphic value empty circulates more. Some primitives were performing set and relation normalisation by themselves, overlooking the cases of empty and universe. We fix this by using the already present and complete normalisation functions `as_set` and `as_rel` slightly generalised to handle different error reporting.
maranget
added a commit
that referenced
this pull request
Jul 10, 2026
Since PR #1855, the polymorphic value empty circulates more. Some primitives were performing set and relation normalisation by themselves, overlooking the cases of empty and universe. We fix this by using the already present and complete normalisation functions `as_set` and `as_rel` slightly generalised to handle different error reporting.
Member
Author
|
Fix is PR #1912. |
maranget
added a commit
that referenced
this pull request
Jul 10, 2026
Since PR #1855, the polymorphic value empty circulates more. Some primitives were performing set and relation normalisation by themselves, overlooking the cases of empty and universe. We fix this by using the already present and complete normalisation functions `as_set` and `as_rel` slightly generalised to handle different error reporting. Reported-by: Akira Yokosawa <akiyks@gmail.com>
maranget
added a commit
that referenced
this pull request
Jul 10, 2026
Since PR #1855, the polymorphic value empty circulates more. Some primitives were performing set and relation normalisation by themselves, overlooking the cases of empty and universe. We fix this by using the already present and complete normalisation functions `as_set` and `as_rel` slightly generalised to handle different error reporting. Reported-by: Akira Yokosawa <akiyks@gmail.com>
maranget
added a commit
that referenced
this pull request
Jul 10, 2026
Since PR #1855, the polymorphic value empty circulates more. Some primitives were performing set and relation normalisation by themselves, overlooking the cases of empty and universe. We fix this by using the already present and complete normalisation functions `as_set` and `as_rel` slightly generalised to handle different error reporting. Reported-by: Akira Yokosawa <akiyks@gmail.com>
maranget
added a commit
that referenced
this pull request
Jul 10, 2026
Since PR #1855, the polymorphic value empty circulates more. Some primitives were performing set and relation normalisation by themselves, overlooking the cases of empty and universe. We fix this by using the already present and complete normalisation functions `as_set` and `as_rel` slightly generalised to handle different error reporting. Reported-by: Akira Yokosawa <akiyks@gmail.com>
maranget
added a commit
that referenced
this pull request
Jul 13, 2026
[herd,cat] Fix some problems with the C architecture This PR fixes two problems: 1. Since PR #1855, the polymorphic value `V.Empty` circulates more. Some primitives were performing set and relation normalisation by themselves, overlooking the cases of empty and universe. We fix this by using the already present and complete normalisation functions `as_set` and `as_rel` slightly generalised to handle different error reporting. 2. PR #1889 changed how the relation `rmw` is computed by defining it in stdlb.cat. The Cat definition of the relation `rmw` assumes that atomic effects are gathered in the set `X`, which was not the case of the C semantics. As a result the `rmw` relation was empty when the read-modify-write instructions are implemented by two (atomic) effects.
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
3 participants
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Some optimisations that may help and never harm.