6
$\begingroup$

I've seen scattered references to typed assembly in high assurance literature, but I don't really understand the advantage.

If the compiler/runtime are capable of passing the types down to the CPU, then aren't they are capable of emitting equivalent checks in assembly? Bloating an instruction set with high-level primitives increases the complexity of the assembler and slows down execution time because the assembler is busy doing the compiler's job.

It sounds like this would make a compiler writer's job easier but expands the TCB without any real gains in speed or safety.

Improve this question
$\endgroup$
2
  • 3
    $\begingroup$ What papers have you read? What research have you done? I'd expect that the early papers introducing typed assembly language should describe the benefits. A search on Google Scholar should make it easy to find entries into the literature, from which you should be able to find the seminal/earliest papers. $\endgroup$
    – D.W. ♦
    Apr 20, 2017 at 20:43
  • $\begingroup$ I had skimmed the papers on the site linked above, but I forgot some of the specifics. I've updated the comment to be more precise. $\endgroup$
    – user70805
    Apr 22, 2017 at 6:58

2 Answers 2

Reset to default
6
$\begingroup$

If the compiler/runtime are capable of passing the types down to the CPU, then aren't they are capable of emitting equivalent checks in assembly?

It could be done, but then

  • we move those checks from compile time to run time, impacting performance
  • we detect type errors at runtime instead of compile time, losing all the benefits of a type system

Bloating an instruction set with high-level primitives increases the complexity of the assembler

True, but this instruction set may still be different from the CPU one, so it's just another (intermediate) language, not something the CPU needs to follow.

and slows down execution time because the assembler is busy doing the compiler's job.

No, the assembler does not run at run time. At compile time, the assembler emits machine code. Compile time may get longer, but the runtime performance should not be affected.

It sounds like this would make a compiler writer's job easier but expands the TCB without any real gains in speed or safety.

Expanding the TCB is not always detrimental to safety. Assume a nuclear power plant with some software to check that the temperature is kept in the safe range. Removing that software would make the TCB smaller, but the plant would hardly be more safe.

Adding a type system to a TCB puts more safety checks in the system. As long as the type system is not allowed to modify the program code, but only to report "well-typed / ill-typed", it can not harm safety. If it passes ill-behaved programs, say because of some bugs in the type checker, those would be executed anyway without the type system. If it fails some well-behaved programs, that's unfortunate, but preventing the deployment of a new program is always a safe choice -- this impacts productivity but not safety.

Improve this answer
$\endgroup$
6
$\begingroup$

One of the benefits of typed assembly language is that it can reduce the TCB, not expand it.

The type checker in the assembler for type-checking the typed assembly language can be fairly simple, and thus potentially fairly trustworthy. In contrast, a compiler is a much more complex beast, and putting a type-checker in a compiler typically involves trusting a large fraction of the compiler (the entire code generation stage, and typically the optimization stages, too). Moreover, if you put the type-checker in the compiler, the assembler must be trusted too.

So if you compare "trust the assembler + a simple type-checker in the assembler" vs "trust the assembler + many stages of a complex compiler + the type-checker in the compiler", hopefully you can see how the former can lead to a smaller TCB, with good system design.

Improve this answer
$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

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