3
$\begingroup$

Does this always mean that a program can be correct in regard to that spec or is there any correctness of the spec itself ?

Improve this question
$\endgroup$

1 Answer 1

Reset to default
3
$\begingroup$

An ISA spec says how a processor should behave. A processor either conforms to such a spec (behaves exactly like the spec says it should), or it doesn’t (behaves differently in some situations).

ISA has nothing to do with correctness of programs. If a processor conforms to its ISA spec then all programs will behave as they should behave according to the spec, both correct and incorrect programs. If a processor does not conform to the ISA spec then programs can behave different from how they should behave.

A spec cannot be wrong, by definition. It can be nonsensical (like if the spec says that an “add” instruction should subtract, but it’s never wrong.

Reasons for having an ISA spec:

  1. Instructing the team that designs the processor.
  2. Instructing the team that writes test code to test the processor for conformance.
  3. Instructing the team that writes a simulator for the processor which can be used before processors are available.
  4. Instructing teams that write compilers for this processor.
  5. Instructing support teams who handle customer complains about the processor behaviour, so they can check that the processor conforms to the spec.
Improve this answer
$\endgroup$
2
  • $\begingroup$ So the reason why it is worth to formalize an ISA is to only verify if a processor correctly implements it? Or are there any other use cases ? $\endgroup$
    – Malte
    Commented Sep 11, 2019 at 8:08
  • $\begingroup$ I would argue that an ISA spec that is inconsistent is wrong. An ISA spec that is incomplete is problematic (forcing users to assume nasal demons for any unspecified action), but not wrong (in my opinion). It is arguable that a spec is wrong if the described behavior does not match the spec developers' mental model. There is also the philosophical issue of whether the spec or an implementation is definitive (specs can have bugs [unintentional effects] and hardware can have bugs). $\endgroup$
    – user4577
    Commented Sep 11, 2019 at 14:28

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.