Specification of undefined vs implementation defined behavior

[AndreasKrall]

With VADL we have a formal specification of a processor architecture which is both used to generate simulator/hardware and compiler/assembler. In processor architecture manuals it is common that there is specified undefined behavior where the implementor of the simulator/hardware has any freedom how to implement this and change this undefined behavior into implementation defined behavior. But the compiler/assembler is not allowed to generate code for this undefined behavior which now has become implementation defined. Lets take a look at an example from the AArch64 specification:

  format AddSubExtFormat: Instr =     // add/sub extended register format
    { sf       [31]                   // size field (enum SF), if (sf = 0) 32 bit operation else 64 bit
    , ff       [29]                   // flag field, if (ff = 1) set status register flags
    , op       [30,28..21]            // opcode
    , rm       [20..16] : Index       // 2nd source register
    , option   [15..13]               // ExtendType depending on option value
    , imm3     [12..10] : Bits3       // immediate shift amount, if (imm3 > 4) raise Undefined
    , rn       [9..5]   : Index       // 1st source register (SP)
    , rd       [4..0]   : Index       // destination register (SP if ff = 0)
    }

  model AddSubExtInstrBase (i: InstrWithFunct, extId: Id, size: Id, f: Flags, extEx: Ex, optId: Id, enc: Encs, asm: Ex): IsaDefs = {
    instruction ExtendId ($i.id, $extId): AddSubExtFormat =
      let result, flags = VADL::$i.funct (S(rn) as Bits<Size::$size>, ($extEx) as Bits<Size::$size>) in {
        $f.resModel (match: Id ($f.ff = OffFlags => S ; _ => X)(rd) ; result )
        }
    //[raise Undefined : imm3(2) = 1 && imm3(1..0) != 0]
    encoding ExtendId ($i.id, $extId) = { op = $i.opcode, sf = SF::$size, ff = FF::$f.ff, option = ExtendType::$optId, $enc }
    assembly ExtendId ($i.id, $extId) = ( $i.mnemo, $f.mext, ' ', ExtendId($size, match: Str ($f.ff = OffFlags => "SP" ; _ => ""))(rd), 
                       ', ', ExtendId($size, "SP")(rn), ', ', $asm )
    }

    $AddSubExtInstrBase ($i; UXSB; $size; $f; X(rm)( 7..0) as UIntX << imm3; UXTB; none; (WSize(rm), ", uxtb #", decimal(imm3)))

It is undefined behavior if imm3 is bigger than 4. In the current specification it is allowed to use bigger values like 5,6 or 7 and the simulator and the hardware would correctly execute shifts by 5,6 or 7. But the compiler and assembler is not allowed to generate this kind of immediate values. How shall we cope with this problem?

Shall we define access functions and a predicate which checks for the correct value range. Shall we avoid implementation defined behavior and let also the simulator/hardware raise an exception by using an require annotation on the instruction or an ensure annotation on the instruction? If we use an annotation, which one should we use? Shall we introduce an undefined annotation?

There are many different places in the AArch64 spec, e.g. immediate values, writing to the same register, encodings.

[AlexanderRipar]

Shouldn't the specification of implementation-defined behaviour be deferred to the micro architecture since that is (to my understanding) the implementation in this case?

I am not sure how to best model this, but maybe a pair of annotations, one on the ISA element and one on an implementation in the MiA, e.g. [implementation defined : <identifier-to-refer-to-in-MiA>, imm3(2) = 1 && imm3(1..0) != 0] and [implementation definition : <same-identifier>, <what-to-do-in-this-implementation>].

Some open points with this I can think of off the top of my head:

• What can be done in the MiA's <what-to-do-in-this-implementation>. Does it "re-implement" the whole instruction for maximum flexibility, or just hook into some (sub-)behaviour? Should the scope be changeable from the ISA?
• Is there a more elegant way than indicating the ISA/MiA mapping by matching identifiers?
• Should it be possible to have a "default" implementation in the ISA (e.g., to model "recommended" behaviour, if such a thing exists)?

[Jozott00]

I think that it is not possible to include this in the MiA, because you can generate both an assembler and a compiler from an ISA specification without a MiA definition. Nevertheless, the compiler must ensure that these immediates are not generated.

[AlexanderRipar]

I guess I'm probably missing something, but could that not still be done by just making sure that the compiler does not violate the [implementation defined : <condition>] constraint?
At a later stage, a MiA-aware compiler (which is necessary for e.g. instruction scheduling anyways) could then exploit the behaviour defined by an implementation if a specific MiA is targeted (which, again, I think will need to be supported for scheduling).

[Jozott00]

Ah yes, sorry, I misunderstood your comment. Your approach would be fine.

[Jozott00]

I think we should introduce a new annotation [ undefined if : imm3(2) = 1 && imm3(1..0) != 0 ] annotation. While I don't have a strong preference for the name, I wouldn't call it raise Undefined as this suggests that undefined is an exception that must be raised in case of the condition.

[benedikt-l-huber]

I think the approach of separating defined and undefined behavior between ISA and MiA is a good,
i.e., the ISA should only contain defined behavior.
But I am not convinced that we need any special language construct.

A possible approach would be

• Everything that is not defined in the ISA is undefined.
• Behavior that is undefined in the ISA is free to be
  implementation defined in MiA, ISS, CAS, ...

Why is it necessary to explicitly mark undefined behavior?

A straight forward way of the example above would be to attach a constraint to imm3,
i.e., specify the value range for which imm3 is defined.
Values violating the constraint, imply undefined behavior.
One way to do this in VADL is by using the predicate of the format.
A possible problem I see here is that the predicate is attached to the format and not to the instruction.

The implementation (MiA, ISS, ...) is free to ignore the constraint,
as long as all defined behavior is covered correctly.
Of course this means that the implementation has more analyzing to do.
(But I think this is often the VADL approach.)

[AndreasKrall]

In the meeting today we agreed to use an undefined or undefined when annotation on the instruction. Currently for the compiler additionally predicates have to be defined. Currently it is not possible to check the consistency between annotation and predicate. Currently there will be no restrictions on the kind of the expression, greater and less than are allowed.

[Jozott00]

Implemented in #345