libsel4bench: do not use TSC as cycle count - #116
Open
dreamliner787-9 wants to merge 1 commit into
Open
Conversation
The Time Stamp Counter is not a cycle counter, as described by the Intel SDM Order Number: 325462-091US March 2026, section "20.17 TIME-STAMP COUNTER", page "20-42 Vol. 3B": ``` The Intel 64 and IA-32 architectures (beginning with the Pentium processor) define a time-stamp counter mechanism that can be used to monitor and identify the relative time occurrence of processor events. ``` Even worse, different CPU generations incremented the TSC differently. See description of this behavior in the same SDM section. sel4bench, relied on the TSC as a cycle counter, which gave incorrect result for all cycle counting benchmarks on certain x86 CPUs. Previous discussion: seL4/sel4bench#81 (comment) For example, on an Intel XEON W-1250, current result as measured with `rdtsc`: ```json [ { "Benchmark": "One way IPC microbenchmarks", "Results": [ { "Function": "seL4_Call", "Direction": "client->server", "Client Prio": 254, "Server Prio": 254, "Same vspace?": true, "IPC length": 0, "Min": 630, "Max": 736, "Mean": 723, "Stddev": 25.065, "Variance": 589, "Mode": 728, "Median": 728, "1st quantile": 724, "3rd quantile": 732, "Samples": 16, "Raw results": [ 630, 736, 736, 730, 728, 732, 722, 724, 722, 732, 724, 726, 728, 730, 732, 728 ] }, ``` When I patched sel4bench to use the proper cycle counter in the PMU with `lfence; rdpmc; lfence` instead: ``` [ { "Benchmark": "One way IPC microbenchmarks", "Results": [ { "Function": "seL4_Call", "Direction": "client->server", "Client Prio": 254, "Server Prio": 254, "Same vspace?": true, "IPC length": 0, "Min": 836, "Max": 977, "Mean": 960, "Stddev": 33.482, "Variance": 1051, "Mode": 968, "Median": 968, "1st quantile": 964.75, "3rd quantile": 970, "Samples": 16, "Raw results": [ 836, 961, 969, 964, 968, 968, 964, 968, 969, 965, 975, 968, 969, 977, 973, 974 ] }, ``` So sel4bench was reporting the wrong result for all x86 CPUs that have TSC frequency != processor frequency. This commit patched this problem and used the proper cycle counter instead of relying on the PMU. Signed-off-by: Bill Nguyen <bill.nguyen@unsw.edu.au>
Indanz
reviewed
Aug 20, 2026
Indanz
left a comment
Indanz
left a comment
Contributor
There was a problem hiding this comment.
I don't think we can count on CONFIG_EXPORT_PMC_USER always being enabled, like for verification build kernels, so I think it will need to be an additional option at most.
Contributor
|
Can you leave most of the explanation of why not using the TSC to the issue or sel4bench PR, and mostly focus on explaining which performance counter you are using and why? I'm not familiar with x86 performance monitor counters, my main concern is that some other PMC configuration elsewhere clashes with this and that you read different values than expected or something. |
Contributor
|
edit: Comment moved: seL4/sel4bench#87 (comment) |
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.
See commit message or seL4/sel4bench#87 for motivation and details.