High performance direct targets for assembly

andrew-johnson-4 commented 1 week ago

The GNU-x86 target was about 3-4 times slower than gcc.

alex-s168 commented 14 hours ago

Would you consider using my compiler backend for this if it would only depend on lambda-mountain?

andrew-johnson-4 commented 14 hours ago

I would love to have more support for lots of backends. However, at each level I still want to preserve type information that could be verified if the backend wanted to verify those properties.

https://andrewjohnson4.substack.com/p/most-opcodes-are-typesafe-if-memory

The ideal pipeline would look like this:

LSTS -> LM (all proof information is preserved)
LM -> C (proof information is added in comments)
C -> Assembly (was GNU syntax but not decided yet) (proof information is added in comments)
Assembly -> Coq (finally models are checks and verified against actual binary object vs instruction definition)

Here is an example of the assembly syntax I was imagining: https://github.com/andrew-johnson-4/lambda-mountain/blob/main/TUTORIAL/verify-hello-world-with-coq.md

I want to make it easier and fair for other backends to jump in at any level of this process. So absolutely I would consider integrations. LM already has a plugin system made for this.

I want to help other projects succeed wherever I can so I might spend 20% time on things like:

help designing exchange interfaces for handoffs (does the code need to be hard-coupled or is there room for an IR etc.)
implementing small tools to implement handoffs and integration
building test suites that check for regressions wrt integrations
other help with good ideas

andrew-johnson-4 commented 14 hours ago

going over your code.

tail calls... AWESOME.

andrew-johnson-4 commented 14 hours ago

feel free to propose your own IR as convenient. LM is really good at learning and conforming to new syntax.

alex-s168 commented 13 hours ago

feel free to propose your own IR as convenient. LM is really good at learning and conforming to new syntax.

I don't quite understand what you mean by that

alex-s168 commented 13 hours ago

I would love to have more support for lots of backends. However, at each level I still want to preserve type information that could be verified if the backend wanted to verify those properties.

https://andrewjohnson4.substack.com/p/most-opcodes-are-typesafe-if-memory

The ideal pipeline would look like this:

LSTS -> LM (all proof information is preserved)

LM -> C (proof information is added in comments)

C -> Assembly (was GNU syntax but not decided yet) (proof information is added in comments)

Assembly -> Coq (finally models are checks and verified against actual binary object vs instruction definition)

Here is an example of the assembly syntax I was imagining: https://github.com/andrew-johnson-4/lambda-mountain/blob/main/TUTORIAL/verify-hello-world-with-coq.md

I want to make it easier and fair for other backends to jump in at any level of this process. So absolutely I would consider integrations. LM already has a plugin system made for this.

I want to help other projects succeed wherever I can so I might spend 20% time on things like:

help designing exchange interfaces for handoffs (does the code need to be hard-coupled or is there room for an IR etc.)

implementing small tools to implement handoffs and integration

building test suites that check for regressions wrt integrations

other help with good ideas

from what I understand, if I want to integrate my compiler backend, I need:

conversion from LM to IR of my compiler backend
make it preserve some comments all the way to assembly: I need to add functionality for something like that anyways because of debugging information
maybe support an alternative assembly syntax
make my compiler backend only depend on things in LM (at compile- and run-time)

regarding the last point: The current C frontend for LM doesn't support comparisons, but it looks like you are planning on re-writing it?

andrew-johnson-4 commented 13 hours ago

You don't "need" any of that. Just a PLUGIN that exports the AST to whatever is most convenient for you.

A backend plugin internal to LM is

a function with type Arrow<Nil,Nil>
uses global ast-parsed-program to yield whatever you backend works with

I just wanted to write down all the things that I have planned for backends. I don't know what is most relevant to you.

andrew-johnson-4 commented 13 hours ago

I just wanted to let you know that there are multiple levels at which you could interface with LM

a PLUGIN that exports the AST from inside the LM compiler
a convenient IR that your backend consumes
some other sort of IPC whatever

alex-s168 commented 13 hours ago

You don't "need" any of that. Just a PLUGIN that exports the AST to whatever is most convenient for you.

A backend plugin internal to LM is

a function with type Arrow<Nil,Nil>

uses global ast-parsed-program to yield whatever you backend works with

I just wanted to write down all the things that I have planned for backends. I don't know what is most relevant to you.

I know that I don't "need" that (I should have clarified that), but you want all of that and I want most of that (I care about everything except proofs)

alex-s168 commented 13 hours ago

I just wanted to let you know that there are multiple levels at which you could interface with LM

a PLUGIN that exports the AST from inside the LM compiler

a convenient IR that your backend consumes

some other sort of IPC whatever

I think generating IR of my compiler backend directly from the AST should be fine. But if you have any plans for introducing an IR, I want to wait for (and maybe help) with that, because I don't want to write twice as much code

alex-s168 commented 7 hours ago

am I understanding correctly that you want to rewrite the C frontend? In what timeline are you planning on doing that?

andrew-johnson-4 / lambda-mountain

High performance direct targets for assembly #918