Disabling and re-enabling extensions
In a belated followup to https://github.com/riscv/riscv-isa-manual/issues/332#issuecomment-466581845, I have the same question as John Hauser. One thing that has changed is that now the architecture has an explicit goal of either describing behavior or using the term UNSPECIFIED.
To restate the question: Various extensions that add architectural state can be enabled/disabled via misa. What happens to that architectural state if the extension is disabled and later re-enabled?
In particular, what happens to the following state if the associated misa bit is cleared and then set:
misa.F: FP registers and fcsr
misa.D: upper part of FP registers (when misa.D=0 and misa.F=1)
misa.Q: upper part of FP registers (when misa.Q=0 and misa.F=1)
misa.S: supervisor CSR state
misa.H: hypervisor CSR state
misa.V: vector state
The spec is clear about the treatment of mepc[1] and sepc[1] when misa.C is disabled and subsequently re-enabled. That bit will contain the last written value even if the write comes while C is disabled.
In a different approach, the spec is also clear that if mstatus.FS is set to Off that the FP state is preserved. However, this S-mode operation is different from the M-mode misa.F control. And the question remains about disabling portions of the FP registers where implementations may continue to do single-precision operations that write (at least) the lower part of the register.
Implementations that support H are encouraged to make misa.H writable. While support for disabling D without disabling F is potentially academic, most implementations are expected to allow software to disable and re-enable H.
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.
Thanks,
-Paul
In a belated followup to https://github.com/riscv/riscv-isa-manual/issues/332#issuecomment-466581845, I have the same question as John Hauser. One thing that has changed is that now the architecture has an explicit goal of either describing behavior or using the term UNSPECIFIED.
To restate the question: Various extensions that add architectural state can be enabled/disabled via misa. What happens to that architectural state if the extension is disabled and later re-enabled?
In particular, what happens to the following state if the associated misa bit is cleared and then set:
misa.F: FP registers and fcsr
misa.D: upper part of FP registers (when misa.D=0 and misa.F=1)
misa.Q: upper part of FP registers (when misa.Q=0 and misa.F=1)
misa.S: supervisor CSR state
misa.H: hypervisor CSR state
misa.V: vector state
The spec is clear about the treatment of mepc[1] and sepc[1] when misa.C is disabled and subsequently re-enabled. That bit will contain the last written value even if the write comes while C is disabled.
In a different approach, the spec is also clear that if mstatus.FS is set to Off that the FP state is preserved. However, this S-mode operation is different from the M-mode misa.F control. And the question remains about disabling portions of the FP registers where implementations may continue to do single-precision operations that write (at least) the lower part of the register.
Implementations that support H are encouraged to make misa.H writable. While support for disabling D without disabling F is potentially academic, most implementations are expected to allow software to disable and re-enable H.
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.
Thanks,
-Paul
In a belated followup to https://github.com/riscv/riscv-isa-manual/issues/332#issuecomment-466581845, I have the same question as John Hauser. One thing that has changed is that now the architecture has an explicit goal of either describing behavior or using the term UNSPECIFIED.
To restate the question: Various extensions that add architectural state can be enabled/disabled via misa. What happens to that architectural state if the extension is disabled and later re-enabled?
In particular, what happens to the following state if the associated misa bit is cleared and then set:
misa.F: FP registers and fcsr
misa.D: upper part of FP registers (when misa.D=0 and misa.F=1)
misa.Q: upper part of FP registers (when misa.Q=0 and misa.F=1)
misa.S: supervisor CSR state
misa.H: hypervisor CSR state
misa.V: vector state
The spec is clear about the treatment of mepc[1] and sepc[1] when misa.C is disabled and subsequently re-enabled. That bit will contain the last written value even if the write comes while C is disabled.
In a different approach, the spec is also clear that if mstatus.FS is set to Off that the FP state is preserved. However, this S-mode operation is different from the M-mode misa.F control. And the question remains about disabling portions of the FP registers where implementations may continue to do single-precision operations that write (at least) the lower part of the register.
Implementations that support H are encouraged to make misa.H writable. While support for disabling D without disabling F is potentially academic, most implementations are expected to allow software to disable and re-enable H.
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.
Thanks,
-Paul
In a belated followup to https://github.com/riscv/riscv-isa-manual/issues/332#issuecomment-466581845, I have the same question as John Hauser. One thing that has changed is that now the architecture has an explicit goal of either describing behavior or using the term UNSPECIFIED.
To restate the question: Various extensions that add architectural state can be enabled/disabled via misa. What happens to that architectural state if the extension is disabled and later re-enabled?
In particular, what happens to the following state if the associated misa bit is cleared and then set:
misa.F: FP registers and fcsr
misa.D: upper part of FP registers (when misa.D=0 and misa.F=1)
misa.Q: upper part of FP registers (when misa.Q=0 and misa.F=1)
misa.S: supervisor CSR state
misa.H: hypervisor CSR state
misa.V: vector state
The spec is clear about the treatment of mepc[1] and sepc[1] when misa.C is disabled and subsequently re-enabled. That bit will contain the last written value even if the write comes while C is disabled.
In a different approach, the spec is also clear that if mstatus.FS is set to Off that the FP state is preserved. However, this S-mode operation is different from the M-mode misa.F control. And the question remains about disabling portions of the FP registers where implementations may continue to do single-precision operations that write (at least) the lower part of the register.
Implementations that support H are encouraged to make misa.H writable. While support for disabling D without disabling F is potentially academic, most implementations are expected to allow software to disable and re-enable H.
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.
Thanks,
-Paul
Is there a checklist of requirements for priv specifications?if not should there be?
When misa.H is cleared, the values of all state that become either inaccessible or masked (e.g. treated as _effectively_ a fixed value) are preserved such that these values become visible again when misa.H is set and this state becomes accessible and unmasked.
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?
A potential second general requirement for all Priv extensions:- The hart reset state must be fully specified and should generally be UNSPECIFIED except for any key control/status bits that need to be in a specific state. (This minimizes hardware cost and leaves probably the large majority of state to be initialized by software.)- The reset state should also specify one of:a) The extension is "disabled" (and most, if not all, other extension state is don't care).b) The extension is "enabled" and any key control/status bits are initialized to specific values as necessary (with all the rest UNSPECIFIED and left to be initialized by software).Greg
I thought there was already a speced requirement that, at reset, all extensions are enabled.:"At reset, the Extensions field shall contain the maximal set of supported extensions, and I shall be selected over E if both are available."And then there are the corner cases: if there are no misa bits for subsets (e.g Zbb, Zv<whatever>), then they can't be enabled or disabled.So, why should misa. bits for the full extensions allow enabling/disabling?What does it mean for misa.G to be enabled or disabled? misa.I ?(if misa.E isn't also present)?Has anyone identified use cases for turning extensions on and off? (as opposed to FP-like disabled state to save power).Has anyone ever implemented RW misa bits?IF not: why not just require those MISA bits to be RdOnly?On Thu, Sep 10, 2020 at 10:44 AM Greg Favor <gfavor@...> wrote:A potential second general requirement for all Priv extensions:- The hart reset state must be fully specified and should generally be UNSPECIFIED except for any key control/status bits that need to be in a specific state. (This minimizes hardware cost and leaves probably the large majority of state to be initialized by software.)- The reset state should also specify one of:a) The extension is "disabled" (and most, if not all, other extension state is don't care).b) The extension is "enabled" and any key control/status bits are initialized to specific values as necessary (with all the rest UNSPECIFIED and left to be initialized by software).Greg
The hypervisor spec specifically says that implementations should have writable misa so this isn't theoretical:"The hypervisor extension is enabled by setting bit 7 in the misa CSR, which corresponds to the letter H. When misa[7] is clear, the hart behaves as though this extension were not implemented, and attempts to use hypervisor CSRs or instructions raise an illegal instruction exception. Implementations that include the hypervisor extension are encouraged not to hardwire misa[7], so that the extension may be disabled. "And, of course, the misa register says that extensions may be disabled, that both E and I may be implemented and that misa is the way to select between them, etc. I don't know if anybody has actually done those things, though.Thanks,-PaulOn Thu, Sep 10, 2020 at 4:05 PM Allen Baum <allen.baum@...> wrote:I thought there was already a speced requirement that, at reset, all extensions are enabled.:"At reset, the Extensions field shall contain the maximal set of supported extensions, and I shall be selected over E if both are available."And then there are the corner cases: if there are no misa bits for subsets (e.g Zbb, Zv<whatever>), then they can't be enabled or disabled.So, why should misa. bits for the full extensions allow enabling/disabling?What does it mean for misa.G to be enabled or disabled? misa.I ?(if misa.E isn't also present)?Has anyone identified use cases for turning extensions on and off? (as opposed to FP-like disabled state to save power).Has anyone ever implemented RW misa bits?IF not: why not just require those MISA bits to be RdOnly?On Thu, Sep 10, 2020 at 10:44 AM Greg Favor <gfavor@...> wrote:A potential second general requirement for all Priv extensions:- The hart reset state must be fully specified and should generally be UNSPECIFIED except for any key control/status bits that need to be in a specific state. (This minimizes hardware cost and leaves probably the large majority of state to be initialized by software.)- The reset state should also specify one of:a) The extension is "disabled" (and most, if not all, other extension state is don't care).b) The extension is "enabled" and any key control/status bits are initialized to specific values as necessary (with all the rest UNSPECIFIED and left to be initialized by software).Greg
OK - taking a step back, what about requiring: any extension spec that doesn't specifically discuss enabling and disabling should be prohibited from enabling or disabling..I can't see any good use cases - even for power, given the F/D method of dealing with that via the XS bits.
That is a very explicit mechanism, specifically architected for enabling and disabling, with all the side effects and corner cases defined (one hopes).On Thu, Sep 10, 2020 at 4:13 PM Paul Donahue <pdonahue@...> wrote:The hypervisor spec specifically says that implementations should have writable misa so this isn't theoretical:"The hypervisor extension is enabled by setting bit 7 in the misa CSR, which corresponds to the letter H. When misa[7] is clear, the hart behaves as though this extension were not implemented, and attempts to use hypervisor CSRs or instructions raise an illegal instruction exception. Implementations that include the hypervisor extension are encouraged not to hardwire misa[7], so that the extension may be disabled. "And, of course, the misa register says that extensions may be disabled, that both E and I may be implemented and that misa is the way to select between them, etc. I don't know if anybody has actually done those things, though.Thanks,-PaulOn Thu, Sep 10, 2020 at 4:05 PM Allen Baum <allen.baum@...> wrote:I thought there was already a speced requirement that, at reset, all extensions are enabled.:"At reset, the Extensions field shall contain the maximal set of supported extensions, and I shall be selected over E if both are available."And then there are the corner cases: if there are no misa bits for subsets (e.g Zbb, Zv<whatever>), then they can't be enabled or disabled.So, why should misa. bits for the full extensions allow enabling/disabling?What does it mean for misa.G to be enabled or disabled? misa.I ?(if misa.E isn't also present)?Has anyone identified use cases for turning extensions on and off? (as opposed to FP-like disabled state to save power).Has anyone ever implemented RW misa bits?IF not: why not just require those MISA bits to be RdOnly?On Thu, Sep 10, 2020 at 10:44 AM Greg Favor <gfavor@...> wrote:A potential second general requirement for all Priv extensions:- The hart reset state must be fully specified and should generally be UNSPECIFIED except for any key control/status bits that need to be in a specific state. (This minimizes hardware cost and leaves probably the large majority of state to be initialized by software.)- The reset state should also specify one of:a) The extension is "disabled" (and most, if not all, other extension state is don't care).b) The extension is "enabled" and any key control/status bits are initialized to specific values as necessary (with all the rest UNSPECIFIED and left to be initialized by software).Greg
On Thu, Sep 10, 2020 at 7:14 PM Allen Baum <allen.baum@...> wrote:OK - taking a step back, what about requiring: any extension spec that doesn't specifically discuss enabling and disabling should be prohibited from enabling or disabling..I can't see any good use cases - even for power, given the F/D method of dealing with that via the XS bits.Emulating less-capable systems.That is a very explicit mechanism, specifically architected for enabling and disabling, with all the side effects and corner cases defined (one hopes).On Thu, Sep 10, 2020 at 4:13 PM Paul Donahue <pdonahue@...> wrote:The hypervisor spec specifically says that implementations should have writable misa so this isn't theoretical:"The hypervisor extension is enabled by setting bit 7 in the misa CSR, which corresponds to the letter H. When misa[7] is clear, the hart behaves as though this extension were not implemented, and attempts to use hypervisor CSRs or instructions raise an illegal instruction exception. Implementations that include the hypervisor extension are encouraged not to hardwire misa[7], so that the extension may be disabled. "And, of course, the misa register says that extensions may be disabled, that both E and I may be implemented and that misa is the way to select between them, etc. I don't know if anybody has actually done those things, though.Thanks,-PaulOn Thu, Sep 10, 2020 at 4:05 PM Allen Baum <allen.baum@...> wrote:I thought there was already a speced requirement that, at reset, all extensions are enabled.:"At reset, the Extensions field shall contain the maximal set of supported extensions, and I shall be selected over E if both are available."And then there are the corner cases: if there are no misa bits for subsets (e.g Zbb, Zv<whatever>), then they can't be enabled or disabled.So, why should misa. bits for the full extensions allow enabling/disabling?What does it mean for misa.G to be enabled or disabled? misa.I ?(if misa.E isn't also present)?Has anyone identified use cases for turning extensions on and off? (as opposed to FP-like disabled state to save power).Has anyone ever implemented RW misa bits?IF not: why not just require those MISA bits to be RdOnly?On Thu, Sep 10, 2020 at 10:44 AM Greg Favor <gfavor@...> wrote:A potential second general requirement for all Priv extensions:- The hart reset state must be fully specified and should generally be UNSPECIFIED except for any key control/status bits that need to be in a specific state. (This minimizes hardware cost and leaves probably the large majority of state to be initialized by software.)- The reset state should also specify one of:a) The extension is "disabled" (and most, if not all, other extension state is don't care).b) The extension is "enabled" and any key control/status bits are initialized to specific values as necessary (with all the rest UNSPECIFIED and left to be initialized by software).Greg
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
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).
GregOn 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
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).GregOn 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
Perhaps “all state no longer associated with any active extension is UNSPECIFIED”?But it also might be slightly cleaner to talk about the state being unspecified right after an extension is reactivated. I kind of think about extension state as ceasing to exist when disabled which isn’t conceptually quite the same as having a specific but unspecified value.JonathanOn Sat, Sep 19, 2020 at 11:13 PM Greg Favor via lists.riscv.org <gfavor=ventanamicro.com@...> wrote: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).GregOn 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
Errr... disregard that second part, I misread the previous emailOn Sat, Sep 19, 2020 at 11:27 PM Jonathan Behrens <behrensj@...> wrote:Perhaps “all state no longer associated with any active extension is UNSPECIFIED”?But it also might be slightly cleaner to talk about the state being unspecified right after an extension is reactivated. I kind of think about extension state as ceasing to exist when disabled which isn’t conceptually quite the same as having a specific but unspecified value.JonathanOn Sat, Sep 19, 2020 at 11:13 PM Greg Favor via lists.riscv.org <gfavor=ventanamicro.com@...> wrote: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).GregOn 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