Given the comments excerpted down below that argue for specifying that extension state is UNSPECIFIED after being disabled and then re-enabled, and given that no particular arguments or use cases have been raised for having a defined behavior like all such state being preserved, can we agree on adding something along the lines of the following statement to the Priv spec's description of the misa CSR.  Note that this still allows an extension to specify something different if it so chooses.

When software enables an extension that was previously disabled, then all state uniquely associated with that extension is UNSPECIFIED (unless otherwise specified by that extension).

Greg

On Thu, Sep 10, 2020 at 1:51 PM Paul Donahue <pdonahue@...> wrote:

On Wed, Sep 9, 2020 at 8:33 PM Andrew Waterman <andrew@...> wrote:

On Wed, Sep 9, 2020 at 12:14 PM Paul Donahue <pdonahue@...> wrote:

I propose that there should be a sentence in the misa description that says that, unless otherwise specified, when software enables an extension that was previously disabled then all state uniquely associated with that extension is UNSPECIFIED.

I don’t object, but I’m wondering: would different implementations actually be motivated to have different behavior w.r.t. hypervisor state when H is disabled then re-enabled? Put another way, do we have any reason to believe that making the behavior fully specified would unduly burden certain styles of implementation?

I think that the general statement for misa should definitely be that it's UNSPECIFIED.  For instance, implementations may want to power gate a vector unit when V is disabled and that becomes more complicated (though certainly not impossible) if there's a requirement to preserve state.  But the "unless otherwise specified" is important.  That allows for the mepc[1] behavior and, to your question, it would allow H to tighten up the requirements.

As for tightening up H requirements, I agree with Greg that it doesn't seem to add value.  If software wants to preserve the state across a temporary disable then it can context switch the state.  I also don't think that compliance tests would be burdened since they can (if they even have a need for a single test that disables H then reenables H then goes on to use H state) live with the same context switch requirements.  The formal model doesn't need to implement all possible behaviors because no proper software can ever observe the behavior.

Thanks,

-Paul