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