A version of the compiler that starts from wordLang (without GC) #111

Open
myreen opened this Issue Apr 21, 2016 · 1 comment

Projects

None yet

1 participant

@myreen
Contributor
myreen commented Apr 21, 2016

We want to compile HOL functions that essentially only operate over a memory modelling function and word types to wordLang (phase 1) and from there compile it to concrete machine code (phase 2).

Phase 1 would be proof-producing, while phase 2 would be a verified compiler. Importantly, one gets a certificate theorem at the end relating the HOL functions with the execution of the generated machine code.

In the long-term, there could be a systems programming dialect of CakeML.

@myreen myreen added the enhancement label Apr 21, 2016
@myreen
Contributor
myreen commented Apr 21, 2016

It might be better to target stackLang after a few shallow-to-shallow transformations within phase 1. The advantage is that then one can influence the stack size immediately (e.g. use one stack frame for the entire program) and one can use While loops. This means that one can extract the last bits of performance from code. In contrast, a path through wordLang would force the code to use one stack frame per function and all loops would have to conform to the calling convention.

Example: User writes HOL function:

|- foo (x1:word32,x2,mem) =
     let x1 = x2 + mem x1 in
     let mem = (x2 =+ x1) mem in
       mem

Instruction selection (easy to prove, just expand let expressions):

|- foo (x1,x2,mem) =
     let t1 = mem x1 in
     let x1 = x2 + t1 in
     let mem = (x2 =+ x1) mem in
       mem

Register allocation (easy to prove, just expand let expressions):

|- foo (r0,r1,mem) =
     let r2 = mem r0 in
     let r0 = r1 + r2 in
     let mem = (r1 =+ r0) mem in
       mem

Produce stackLang program (more interesting but purely mechanical):

prog :=
  Seq (Inst MemOp Load ...)
      (Seq (Inst ...)
           (Inst ...))

where the transformation automatically proves:

|- ?k s'.
     evaluate (prog,s with clock := k) = (NONE,s') /\
     s'.mem = foo (s.regs 0, s.regs 2, s.mem)
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment