How our ISA Formal Spec TG plans to model 'implementation defined' behaviors

[Rishiyur Nikhil]

BACKGROUND: In the text specification, there are a number of places

  where it is not clear what happens when an architectural spec

  parameter is itself changed.  We've already seen some discussion

  about dynamic changes to MISA.C but other examples would be changing

  MISA.MXL, disabling one or more floating point extensions, ...  Some

  of these transitions have been given (or are being given) detailed

  specs, such as MISA.C transitions, but others may be implementation

  defined.

QUESTION from the ISA Formal Spec Group: in general, how should such

  transitions be modeled, formally?

PROPOSAL: We propose that (excepting transitions for which a more

  detailed spec has been given), that the general way to model such

  transitions is an opaque but deterministic function that is applied

  to the machine state to transform it.  I.e., each implementation

  does some implementation-specific, deterministic, transformation to

  the state (including possibly a no-op).

  We are keen to avoid introducing non-determinism into the formal

  spec except where it is absolutely required (e.g., in the mem model

  orderings, etc.), because unnecessary non-determinism would

  complicate the semantic model considerably.

Please let us know if you see any problems with this.

Rishiyur Nikhil,

Chair, RISC-V ISA Formal Spec Technical Group

[Cesar Eduardo Barros]

Em 05-04-2018 11:09, Rishiyur Nikhil escreveu:
> BACKGROUND: In the text specification, there are a number of places
>   where it is not clear what happens when an architectural spec
>   parameter is itself changed.  We've already seen some discussion
>   about dynamic changes to MISA.C but other examples would be changing
>   MISA.MXL, disabling one or more floating point extensions, ...  Some
>   of these transitions have been given (or are being given) detailed
>   specs, such as MISA.C transitions, but others may be implementation
>   defined.
>
> QUESTION from the ISA Formal Spec Group: in general, how should such
>   transitions be modeled, formally?
>
> PROPOSAL: We propose that (excepting transitions for which a more
>   detailed spec has been given), that the general way to model such

>   transitions is an /*opaque but deterministic function*/ that is applied

>   to the machine state to transform it.  I.e., each implementation
>   does some implementation-specific, deterministic, transformation to
>   the state (including possibly a no-op).
>
>   We are keen to avoid introducing non-determinism into the formal
>   spec except where it is absolutely required (e.g., in the mem model
>   orderings, etc.), because unnecessary non-determinism would
>   complicate the semantic model considerably.

Sounds good to me, but I think the definition should be a tiny bit
stronger: the "implementation-specific" part should be restricted as to
which parts of the state it can touch. For instance, disabling or
enabling the floating point extensions shouldn't touch the virtual
memory CSRs or the interrupt CSRs (in fact, it should touch no
non-float-related registers at all). That puts a boundary around the
effects of each transition, which should make them simpler to model and
understand.

Yeah, MISA.MXL is the worst one, since XLEN touches nearly everything,
including registers directly affecting the currently executing code (the
program counter, memory protection registers, ...) That particular
transition needs to have its effect on several CSRs explicitly specified
(the program counter sign-extends, the memory protection registers are
mapped to their equivalents, perhaps others), otherwise there can be no
guaranteed way for software to do the XLEN transition reliably.

Also, what about hidden state? Taking floating point again as an
example, suppose the software disables all floating point extensions,
and later enables them again. What happens to the floating point
registers? There are three possible deterministic outcomes:

1. All floating-point registers are reset to a fixed value;
2. Some floating-point registers are reset, some keep their value;
3. All floating-point registers keep their old value.

The last two options have "hidden" state, which was not accessible while
there were no enabled instructions which could access it. The first
option has no hidden state.

(There was some argument in the MISA.C discussion over a single bit of
hidden state, so it should be important to be clear about whether or not
hidden state is allowed. My personal opinion is that hidden state should
be allowed, but it shouldn't be able to affect anything while it's hidden.)

--
Cesar Eduardo Barros
ces...@cesarb.eti.br

[Andrew Waterman]

I agree it should be constrained to be deterministic.

 

Please let us know if you see any problems with this.

Rishiyur Nikhil,

Chair, RISC-V ISA Formal Spec Technical Group

--
You received this message because you are subscribed to the Google Groups "RISC-V ISA Dev" group.
To unsubscribe from this group and stop receiving emails from it, send an email to isa-dev+unsubscribe@groups.riscv.org.
To post to this group, send email to isa...@groups.riscv.org.
Visit this group at https://groups.google.com/a/groups.riscv.org/group/isa-dev/.
To view this discussion on the web visit https://groups.google.com/a/groups.riscv.org/d/msgid/isa-dev/CAAVo%2BPnt71gYPct4aLh58ouN3KomKcuC-3BuwPheuG4qYihLog%40mail.gmail.com.

[Jacob Bachmeyer]

Hidden state is a serious problem for virtualization: that state must
be transferred during a migration or context switch, but is not directly
visible. This is a huge problem and would require all extensions to
activated, the hidden state recorded, then extensions deactivated that
should not be active in the new context. Section 3.1.11 "Extension
Context Status in mstatus Register" in the privileged ISA spec goes into
some detail here.


-- Jacob

[Cesar Eduardo Barros]

If the virtual machine monitor can trap whenever the virtualized
software attempts to disable or enable an extension, that is simple to
work around: when disabling an extension, it traps and records the
hidden state (before actually disabling); when enabling an extension, it
traps and restores the hidden state (after actually enabling). That is,
the hidden state is now in the virtual machine monitor memory, instead
of hidden in the hardware, and can be migrated easily. As a bonus, this
even allows emulating hidden state when the hardware doesn't have it, or
vice versa.

[Jacob Bachmeyer]

Cesar Eduardo Barros wrote:
> Em 06-04-2018 01:02, Jacob Bachmeyer escreveu:
>> Cesar Eduardo Barros wrote:
>>

>> [...]

>>
>> Hidden state is a serious problem for virtualization: that state
>> must be transferred during a migration or context switch, but is not
>> directly visible. This is a huge problem and would require all
>> extensions to activated, the hidden state recorded, then extensions
>> deactivated that should not be active in the new context. Section
>> 3.1.11 "Extension Context Status in mstatus Register" in the
>> privileged ISA spec goes into some detail here.
>
> If the virtual machine monitor can trap whenever the virtualized
> software attempts to disable or enable an extension, that is simple to
> work around: when disabling an extension, it traps and records the
> hidden state (before actually disabling); when enabling an extension,
> it traps and restores the hidden state (after actually enabling). That
> is, the hidden state is now in the virtual machine monitor memory,
> instead of hidden in the hardware, and can be migrated easily. As a
> bonus, this even allows emulating hidden state when the hardware
> doesn't have it, or vice versa.

Then this appears to be what we actually need here.


-- Jacob

[Luke Kenneth Casson Leighton]

On Fri, Apr 6, 2018 at 5:02 AM, Jacob Bachmeyer <jcb6...@gmail.com> wrote:

>> Em 05-04-2018 11:09, Rishiyur Nikhil escreveu:

>> (There was some argument in the MISA.C discussion over a single bit of
>> hidden state, so it should be important to be clear about whether or not
>> hidden state is allowed. My personal opinion is that hidden state should be
>> allowed, but it shouldn't be able to affect anything while it's hidden.)
>
>
> Hidden state is a serious problem for virtualization:

Clifford wolf, you will no doubt have observed, nikhil, has been
developing a formal analysis system called SimbiYosys, and he too
picked up that it is flat-out impossible to make a formal declaration
of the integrity and security of a system when it has hidden state:

https://github.com/cliffordwolf/riscv-formal

I know that Bluespec uses Haskell so it's the same thing from
functional programming languages where you introduce reading from
stdin: all of the formal mathematical guarantees go out the window.

Which kiinda answers the question: it doesn't matter how it's done (I
don't believe), as long as there is *no* hidden state. Or, if there
is, every implementor signs and formally publishes a declaration which
potential customers may find online without let or hindrance, which
explicitly states, "we have hidden state, we can't make any guarantees
about the correctness of our implementation, we don't care and we're
Seriously Hoping You Don't Either. Contact your Sales Rep today!"

:)

l.

[Cesar Eduardo Barros]

Em 07-04-2018 10:44, Luke Kenneth Casson Leighton escreveu:
> On Fri, Apr 6, 2018 at 5:02 AM, Jacob Bachmeyer <jcb6...@gmail.com> wrote:
>
>>> Em 05-04-2018 11:09, Rishiyur Nikhil escreveu:
>
>>> (There was some argument in the MISA.C discussion over a single bit of
>>> hidden state, so it should be important to be clear about whether or not
>>> hidden state is allowed. My personal opinion is that hidden state should be
>>> allowed, but it shouldn't be able to affect anything while it's hidden.)
>>
>>
>> Hidden state is a serious problem for virtualization:
>
> Clifford wolf, you will no doubt have observed, nikhil, has been
> developing a formal analysis system called SimbiYosys, and he too
> picked up that it is flat-out impossible to make a formal declaration
> of the integrity and security of a system when it has hidden state:
>
> https://github.com/cliffordwolf/riscv-formal
>
> I know that Bluespec uses Haskell so it's the same thing from
> functional programming languages where you introduce reading from
> stdin: all of the formal mathematical guarantees go out the window.

Is that still the case when the hidden state can't affect anything (that
is, its only effect is saving the values when something is disabled, so
they reappear in the same place when that thing is re-enabled)?

For the "disabling floating point" example, the hidden state would be
equivalent to putting the floating point register values into a closed
box, and opening it back again when enabling floating point. Since the
only thing which can enable floating point is also the thing which
disabled it, it would be equivalent to storing these values into a
private memory, accessible only to whatever can mess with the MISA modes.

(For the MISA.C discussion, the hidden state also had no effect while it
was hidden, but it could also be erased if xEPC was written to while it
was hidden. I don't expect this additional detail to make the modelling
much more complicated; it's equivalent to the relevant bit being there
but masked out both from the value being read from the CSR and from the
value being written to the CSR.)

[Luke Kenneth Casson Leighton]

On Sat, Apr 7, 2018 at 3:50 PM, Cesar Eduardo Barros
<ces...@cesarb.eti.br> wrote:
> Em 07-04-2018 10:44, Luke Kenneth Casson Leighton escreveu:
>>
>> On Fri, Apr 6, 2018 at 5:02 AM, Jacob Bachmeyer <jcb6...@gmail.com>
>> wrote:
>>
>>>> Em 05-04-2018 11:09, Rishiyur Nikhil escreveu:
>>
>>
>>>> (There was some argument in the MISA.C discussion over a single bit of
>>>> hidden state, so it should be important to be clear about whether or not
>>>> hidden state is allowed. My personal opinion is that hidden state should
>>>> be
>>>> allowed, but it shouldn't be able to affect anything while it's hidden.)
>>>
>>>
>>>
>>> Hidden state is a serious problem for virtualization:
>>
>>
>> Clifford wolf, you will no doubt have observed, nikhil, has been
>> developing a formal analysis system called SimbiYosys, and he too
>> picked up that it is flat-out impossible to make a formal declaration
>> of the integrity and security of a system when it has hidden state:
>>
>> https://github.com/cliffordwolf/riscv-formal
>>
>> I know that Bluespec uses Haskell so it's the same thing from
>> functional programming languages where you introduce reading from
>> stdin: all of the formal mathematical guarantees go out the window.
>
>
> Is that still the case when the hidden state can't affect anything (that is,
> its only effect is saving the values when something is disabled, so they
> reappear in the same place when that thing is re-enabled)?

if the info is guaranteed to come back in an unmodified state, i'd
conclude yes. modelling that would be easy.

> For the "disabling floating point" example, the hidden state would be
> equivalent to putting the floating point register values into a closed box,
> and opening it back again when enabling floating point. Since the only thing
> which can enable floating point is also the thing which disabled it, it
> would be equivalent to storing these values into a private memory,
> accessible only to whatever can mess with the MISA modes.

yehyeh sounds about right.

> (For the MISA.C discussion, the hidden state also had no effect while it was
> hidden, but it could also be erased if xEPC was written to while it was
> hidden.

ah ha! now we have a problem :) ok - and someone correct me if this
appears wrong (it's part of my black-box reverse-engineering
experience kicking in here): you have a problem if and only if the
effect of xEPC cannot itself be formally modelled, SUCH THAT it is not
possible to DEDUCE exactly what SHOULD be in the hidden state.

i.e. if you know the exact and precise events which caused xEPC to be
erased, the exact times, the exact circumstances, EVERYTHING, such
that you can GUARANTEE to be able to RECREATE an EXACT model of xEPC
(even though it's hidden), i think you might be able to get away with
that. the problem comes if you cannot guarantee to know the exact
time, exact circumstances and so on. then you're hosed.

i think basically what i'm saying is, it doesn't matter if you have
direct access to the hidden state itself or if you have a precise
cycle-accurate model *of* the hidden state: either would do. but it
would clearly be infinitely better not to have hidden state at all.

l.

[Clifford Wolf]

At least for the *epc[1] issue this is insufficient.

The latest proposed spec language would allow code that runs with the C
extension disabled to modify *epc[1]. There is just no way of reading back
the modified state while the C extension is disabled.

So the value of *epc[1] at the time of disabling MISA.C is not necessarily
the value of *epc[1] when MISA.C is enabled again.

[Cesar Eduardo Barros]

The discussion went in several directions, so I'm not sure, but IIRC the
final design ended up being: when MISA.C is cleared, the "hidden bit"
(bit 1 of xEPC) keeps its value, but is now read (and treated as) zero.
Writing anything to xEPC when MISA.C is clear also clears the hidden
bit. That is, the value of xEPC (both the visible bits and the "hidden
bit") depends always only on the last write to xEPC; if the last write
was with MISA.C set, the "hidden bit" (which wasn't hidden then) is set
to what was written; if the last write was with MISA.C clear, the
"hidden bit" is set to zero.

So if I'm remembering the final design for MISA.C correctly, and I'm
understanding what you said correctly, modelling xEPC with the "hidden"
value in bit 1 shouldn't be a problem.

[Clifford Wolf]

On Sat, Apr 07, 2018 at 02:36:28PM -0300, Cesar Eduardo Barros wrote:
> [..] if the last write was with MISA.C set, the "hidden bit" (which

> wasn't hidden then) is set to what was written; if the last write
> was with MISA.C clear, the "hidden bit" is set to zero.

No. When you write to xEPC while MISA.C is clear you will write to xEPC[1]
whatever the CSR command writes. You can set and clear the bit. You just
can't read back what the current state is.

Quoting the spec:

[..], whenever IALIGN=32, bit mepc[1] is masked on reads so that it appears
to be 0. This masking occurs also for the implicit read by the MRET
instruction. Though masked, mepc[1] remains writable when IALIGN=32.