Clarify the description of the set_timer function

[jamestiotio]

Improve the phrasing on the clearing of the pending timer interrupt bit when timer interrupts are masked.

Additionally, clarify that this function can never fail.

CC: @atishp04 @jones-drew

[aswaterman]

This isn't a clarification, it's a change.

[jamestiotio]

@aswaterman Hmm, in that case, can I kindly check on what is the current expected behavior? More concretely:

• If the timer interrupt is masked, is it expected that the pending timer interrupt bit is cleared?
• What are the expected sbiret.value and possible sbiret.error values when the set_timer function is called?

Or did you mean that explicitly specifying these in the spec is a significant change? I used the phrase "may not" for the pending interrupt bit clearing and the possible error codes seem to make sense, but do correct me if I am wrong or if I assumed something along the way.

[aswaterman]

The way the current spec is written, it’s clear that supervisor-level software can rely on the pending interrupt being cleared regardless of whether it’s masked. So this is a backwards-incompatible change from supervisor-level software’s perspective.

Whether this is a “significant” change depends on factors I can’t personally speak to, but it’s still a change, and therefore it’s not a clarification.

[avpatel]

I agree with @aswaterman .

Allowing supervisor software to set stime_value in the past is intentional because supervisor software may want the timer interrupt to trigger immediately.

Overall, NACK to this PR from my side.

[jamestiotio]

The way the current spec is written, it’s clear that supervisor-level software can rely on the pending interrupt being cleared regardless of whether it’s masked.

Ah got it, it was not clear on my side about this. It seems that OpenSBI is not implementing this though, at least when I was testing it with my kvm-unit-tests patches. When the timer interrupt was masked, the sip.STIP CSR bit was not cleared. I would assume that this is a bug with OpenSBI instead, so I will first confirm that I wrote the test right and we can put this in a separate discussion.

Allowing supervisor software to set stime_value in the past is intentional because supervisor software may want the timer interrupt to trigger immediately.

I was also not aware of this. In that case, let me remove that part from this PR.

[aswaterman]

Defining this call to possibly fail is also backwards-incompatible. I think it’s best to close this PR.

[jamestiotio]

Hmm does that mean that set_timer can never fail?

In that case, then I agree that this PR should be closed. Thank you for all of the clarifications. I will incorporate this feedback when I am writing my tests for kvm-unit-tests.

[jones-drew]

I think some clarification is necessary. We shouldn't allow a nonzero sbiret.error to be set and still consider the SBI call to be successful, so I think explicitly stating that sbiret.error must be SBI_SUCCESS is necessary (even it if it's technically not a backward compatible change).

For the masking clarification, I think the "either...or..." wording of the second paragraph implies that masking the timer interrupt will "clear the timer interrupt". Changing the wording to something like

"""
If the supervisor wishes to clear the timer interrupt without scheduling the next timer event, it can request a timer interrupt infinitely far into the future (i.e., (uint64_t)-1). Alternatively, timer interrupts can be masked by clearing the sie.STIE CSR bit.
"""

[jamestiotio]

I can reopen this PR if folks feel that some clarifications on the 2 points above can benefit the community.

[jamestiotio]

As recommended by @jones-drew, I have reopened this PR.

Since the intention has always been to clarify the description, I have made some adjustments to the phrasing of the sentences that involve clearing the pending timer interrupt bit to hopefully better portray the intended meaning.

As I am not very familiar with the language of formal specifications, any feedback is welcome and greatly appreciated. Thank you!

[jones-drew]

Reviewed-by: Andrew Jones [email protected]