[herd] Global count of useful hardware update#1733
Open
Conversation
maranget
force-pushed
the
global-hwupdates
branch
from
c9f7855 to
bbcb779
Compare
maranget
force-pushed
the
global-hwupdates
branch
from
bbcb779 to
f760a93
Compare
The function [delay_kont] can be used to extract the value returned
by a monad (second argument below, type `'a`).
```
val delay_kont : string -> 'a t -> ('a -> 'a t -> 'b t) -> 'b t
```
The continuation function `(fun v mv -> ... )` can then examine
the returned value `v` and combine the monad `mv` independently,
which proves very convenient in many occasion.
The change performed by this commit permits affine (_i.e._ one or zero
effective occurrence), while linear usage (exactly one occurrence) was
mandatory before.
+ Efficient group function: sort, then group.
+ Suffix based generators:
- generate all suffixes,
- cross product of suffixes.
When TTHM=HA or TTHM=HD are active, HW update of the AF flag is performed. This include the so-called "spurious" updates that are performed independently of test code. For efficiency reason we limit the number of such spurious updates to what is necessary. We do so by a global scan of the execution candidates counting the writes that may unset the AF flag in the final set of effects. Notice that we also consider the initial writes in this scan. We perform one optimisation: by exception, when a write effect value is the same as the value read by the same instruction from the same location, there is no need to add a supplementary spurious update as the (potential) update associated to the write that stored the value has already been counted and is sufficient.
maranget
force-pushed
the
global-hwupdates
branch
from
f760a93 to
172203a
Compare
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
2 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.
This draft PR is an evolution of PR #1730. The number of useful hardware updates is evaluated by a global scan of events at the very end of execution candidate construction. The scan counts the number of explicit write effects to locations that can be page table entries of values whose AF flag can be zero.
The technique sounds more general and should yield a better upper bound than the local technique of PR #1730. Some points are still to consider :