ISA Semantics for ARMv8-A, RISC-V, and CHERI-MIPS

Previous Topic Next Topic
 
classic Classic list List threaded Threaded
2 messages Options
Reply | Threaded
Open this post in threaded view
|

ISA Semantics for ARMv8-A, RISC-V, and CHERI-MIPS

Tim Daly
All,

This paper about ISA Semantics for ARMv8-A, RISC-V, and CHERI-MIPS
https://alastairreid.github.io/papers/popl19-isasemantics.pdf
is interesting. It seems to provide a "base case" for proving programs
correct. In particular, they seem to be able to generate proof code for
various provers, including Coq.

One of the criticisms about "proven programs" is that they tend to
ignore implementation details. But given a lisp variant, Milaw, that
is proven to the hardware instructions this new step is really important.

A proof of the machine instructions, a proof of milawa on top of those
instructions, a proof of lisp extensions on top of milawa, and a proof
of Axiom's spad language on top of lisp turns into a fully validated
tower.

It appears that all of this (and it is an impressive pile) can be developed
in Coq.

Also of interest, while I was part of the CMU CERT effort I developed
the ISA for the Intel 32 bit processor [0]. My program reads Intel binary
and generates "Conditional-Concurrent Assignment" semantics. I may
be able to re-target the back end to their Sail language which would
provide ISA semantics for Intel 32 in Coq.

Tim

[0]

Daly, Timothy Intel Instruction Semantics Generator SEI/CERT Research Report, March 2012


_______________________________________________
Axiom-developer mailing list
[hidden email]
https://lists.nongnu.org/mailman/listinfo/axiom-developer
Reply | Threaded
Open this post in threaded view
|

Re: ISA Semantics for ARMv8-A, RISC-V, and CHERI-MIPS

Tim Daly
> John writes:
> This "only" proves down to the binary API. Is there proven hardware?

Their effort is only "proven to binary" but they do manage to run Linux on it.

There is a language called Verilog to specify "down to the wires and transistors"
See https://www.utdallas.edu/~gxm112130/papers/iscas15.pdf

There is "Project Oberon" which is designing a "complete desktop computer from
scratch" staring from the wires and transistors. Their lowest layer is in Verilog on
a Field Programmable Gate Array (FPGA):

The proof game at this level involve mealy/moore state machines since
everything happens all at once on real hardware.

I have an Altera Cyclone FPGA that can run their RISC-V Verilog
but haven't yet had the time to run the Oberon code.

So eventually the Coq proof runs from FPGA <-> Binary <-> Jitawa <->
Milawa <-> ACL2 / lisp <-> Axiom spad <-> algorithm spec <-> Coq proof.
It will take longer than I expect but all of the parts are there.

On Sun, Nov 11, 2018 at 7:09 PM Tim Daly <[hidden email]> wrote:
All,

This paper about ISA Semantics for ARMv8-A, RISC-V, and CHERI-MIPS
https://alastairreid.github.io/papers/popl19-isasemantics.pdf
is interesting. It seems to provide a "base case" for proving programs
correct. In particular, they seem to be able to generate proof code for
various provers, including Coq.

One of the criticisms about "proven programs" is that they tend to
ignore implementation details. But given a lisp variant, Milaw, that
is proven to the hardware instructions this new step is really important.

A proof of the machine instructions, a proof of milawa on top of those
instructions, a proof of lisp extensions on top of milawa, and a proof
of Axiom's spad language on top of lisp turns into a fully validated
tower.

It appears that all of this (and it is an impressive pile) can be developed
in Coq.

Also of interest, while I was part of the CMU CERT effort I developed
the ISA for the Intel 32 bit processor [0]. My program reads Intel binary
and generates "Conditional-Concurrent Assignment" semantics. I may
be able to re-target the back end to their Sail language which would
provide ISA semantics for Intel 32 in Coq.

Tim

[0]

Daly, Timothy Intel Instruction Semantics Generator SEI/CERT Research Report, March 2012


_______________________________________________
Axiom-developer mailing list
[hidden email]
https://lists.nongnu.org/mailman/listinfo/axiom-developer