[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
Re: needing an fpga...
From: |
Camm Maguire |
Subject: |
Re: needing an fpga... |
Date: |
Mon, 13 Feb 2023 09:30:06 -0500 |
User-agent: |
Gnus/5.13 (Gnus v5.13) Emacs/27.1 (gnu/linux) |
Greetings! Just a followup on this old thread.
Debian axiom builds and is installed on riscv64:
https://buildd.debian.org/status/fetch.php?pkg=axiom&arch=riscv64&ver=20170501-12&stamp=1676291249&raw=0
There is no 'relaxation' implemented in the linker at the moment. I
have no idea on what performance penalty if any this incurs.
Take care,
Camm Maguire <camm@maguirefamily.org> writes:
> Greetings! Doubtless there are many lisp-oriented optimizations
> possible with the instruction set. GCL, once ported, of course will
> still go through gcc, so the assembler will by default be somewhat
> 'generic'. GCL can handle special builtin instructions on a platform
> specific basis.
>
> Take care,
>
>
> Tim Daly <axiomcas@gmail.com> writes:
>
>> Camm,
>>
>> Greetings, as you say...
>>
>> That would save me a lot of effort. At the moment I've been
>> targeting FORTH because I have a verilog implementation.
>>
>> I'm hoping for a "Lisp all the way to the metal". That way I can
>> move freely between Axiom's SANE implementation, to the RISC-V
>> hard processor and the soft processor running on the FPGA. Coding
>> the proof checker in a primitive lisp that compiles directly to RISC-V
>> would be sweet.
>>
>> The lower level Lisps only need to be enough to support the
>> compiled forms, such as goto, rather than full lisp with macros.
>> Essentially it only needs to support a thin layer over the RISC-V
>> instruction set.
>>
>> I hadn't thought of it until now but I'm expecting to develop a
>> special set of extended instructions for RISC-V (an "L" extension?)
>> that will support the "side-loading" of proofs into the FPGA from
>> the main CPU. It might be interesting to think about having some
>> of those instructions support primitive Lisp operations, such as
>> CONS, CAR, CDR, etc.
>>
>> I've never heard of porterbox before. I'll have to look at it.
>>
>> Hope you and the family are well.
>>
>> Tim
>>
>> On 6/17/21, Camm Maguire <camm@maguirefamily.org> wrote:
>>> Greetings! I take it this discussion pertains to the same platform as
>>> Debian's 'riscv64'. There are virtual machine images which can be run
>>> in emulation, but I have been waiting for a porterbox to become
>>> available to port gcl. I anticipate the linker will just take a few
>>> days.
>>>
>>> Take care,
>>>
>>> Tim Daly <axiomcas@gmail.com> writes:
>>>
>>>> Program bugs won't go away until we change a few things.
>>>>
>>>> There is a 25 year old effort in proof technology but it is
>>>> divorced from the lower layers.
>>>>
>>>> Since Axiom is a collection of mathematical algorithms
>>>> it, unlike other software, is well specified. That makes it
>>>> ideal for proof technology. It is also well-factored so the
>>>> various definitions and axioms in proofs can be built up
>>>> in an orderly manner.
>>>>
>>>> Compilers and operating systems lie between the code
>>>> and the metal so what the compiler outputs might still
>>>> fail by violating the proof.
>>>>
>>>> Ideally the proof would be carried down to the metal
>>>> and checked by a proof checker so that even if the
>>>> compiler failed, due to perhaps an optimization, the
>>>> failure would be caught during execution before it
>>>> got too damaging.
>>>>
>>>> Proofs also ensure that various "standard" attacks
>>>> like buffer over-runs can't exist.
>>>>
>>>> Schools like CMU are teaching proof techniques in
>>>> their CS classes so the next generation will be well
>>>> aware of when, how, and why to use them.
>>>>
>>>> The gap is between the software and the hardware.
>>>> I'm doing research to cross that gap. That's where
>>>> RISC-V and FPGAs come into play. It allows proofs
>>>> "down to the metal".
>>>>
>>>> RISC-V allows me to extend the instruction set to
>>>> support proofs and FPGA interactions. I can
>>>> run RISC-V in both hard core (for the code) and
>>>> soft-core (for the FPGA) so I'm able to have a common
>>>> Instruction Set Architecture that "knows" about proofs.
>>>>
>>>> FPGAs allow me to have a hardware implementation
>>>> of proof technology that can't be manipulated by an
>>>> attacker. It also allows the proofs to be checked in
>>>> parallel with the execution so there is minimal impact
>>>> on performance but still have high assurance code.
>>>>
>>>> There is still a long way to go. I have to implement
>>>> the proof checker in the FPGA, for example. I have
>>>> to figure out what the extended ISA needs to be to
>>>> "cross-talk" from the hard IP to the soft IP, etc.
>>>>
>>>> If I'm not chosen for one of the free FPGAs, at least
>>>> let me know when they are generally available.
>>>>
>>>> Tim
>>>>
>>>>
>>>>
>>>> On 6/14/21, Jeff Scheel <jeff@riscv.org> wrote:
>>>>> Thanks for the detailed explanation, Tim. That's very helpful.
>>>>> -Jeff
>>>>>
>>>>> --
>>>>> Jeff Scheel (he/him/his)
>>>>> Linux Foundation, RISC-V Technical Program Manager
>>>>>
>>>>>
>>>>> On Thu, Jun 10, 2021 at 7:25 PM Tim Daly <axiomcas@gmail.com> wrote:
>>>>>
>>>>>> I'm the lead developer on Axiom, a computer algebra system.
>>>>>> https://en.wikipedia.org/wiki/Axiom_(computer_algebra_system)
>>>>>>
>>>>>> The current effort involves proving mathematical algorithms
>>>>>> "down to the metal". The "metal" target is an FPGA. The
>>>>>> proof system is LEAN (open source from Microsoft):
>>>>>> https://leanprover.github.io/
>>>>>>
>>>>>> The basic idea is to develop a proof of an algorithm.
>>>>>> Once a proof exists there is a "proof checker" that can
>>>>>> check the proof. It is much easier than creating the proof.
>>>>>>
>>>>>> Next, the algorithm and the proof are packaged together
>>>>>> in the ELF (aka proof-carrying code). The bundle is wrapped
>>>>>> in AES to ensure integrity.
>>>>>>
>>>>>> When the algorithm is run in the CPU, the proof is
>>>>>> side-loaded into the FPGA. While the algorithm runs
>>>>>> the proof checker algorithm checks the proof.
>>>>>>
>>>>>> State information from the proofs of algorithms in the
>>>>>> program get "flowed" thru the execution so that the
>>>>>> whole program is proof-checked.
>>>>>>
>>>>>> The current effort is focused on several things: (1) creating
>>>>>> a soft core RISC-V process (it needs to be a verified soft
>>>>>> core), (2) implementing the proof checker in RISC-V,
>>>>>> (3) figuring out how to communicate between the main
>>>>>> CPU and the RISC-V soft core, and (4) figuring out how
>>>>>> to side-load the proof to run in parallel.
>>>>>>
>>>>>> The proof instructions implementing things like side-load
>>>>>> and communication are currently expected to be an
>>>>>> extended RISCV instruction set.
>>>>>>
>>>>>> I have the open source tool chain set up. I've been learning
>>>>>> how to use them on an icebreaker fpga. The icebreaker is
>>>>>> too small for the whole task but I can construct pieces in
>>>>>> verilog for test purposes.
>>>>>>
>>>>>> Tim Daly
>>>>>> http://axiom-developer.org/~daly
>>>>>>
>>>>>
>>>>
>>>>
>>>>
>>>>
>>>
>>> Jeff Scheel <jeff@riscv.org> writes:
>>>
>>>> Tim, I think the board you want is the PolarFire SoC Icicle board. You
>>>> can find them on the RISC-V Exchange website: RISC-V Exchange - RISC-V
>>>> International (riscv.org)
>>>>
>>>> We will be offering these as our next round of boards that go out. Your
>>>> project is a great one so it's simply a matter of when, not if I'll get a
>>>> board for you. But, I can rest assured that you're "on my list". ;-)
>>>> -Jeff
>>>>
>>>> --
>>>> Jeff Scheel (he/him/his)
>>>> Linux Foundation, RISC-V Technical Program Manager
>>>>
>>>> On Mon, Jun 14, 2021 at 2:29 PM Tim Daly <axiomcas@gmail.com> wrote:
>>>>
>>>> Program bugs won't go away until we change a few things.
>>>>
>>>> There is a 25 year old effort in proof technology but it is
>>>> divorced from the lower layers.
>>>>
>>>> Since Axiom is a collection of mathematical algorithms
>>>> it, unlike other software, is well specified. That makes it
>>>> ideal for proof technology. It is also well-factored so the
>>>> various definitions and axioms in proofs can be built up
>>>> in an orderly manner.
>>>>
>>>> Compilers and operating systems lie between the code
>>>> and the metal so what the compiler outputs might still
>>>> fail by violating the proof.
>>>>
>>>> Ideally the proof would be carried down to the metal
>>>> and checked by a proof checker so that even if the
>>>> compiler failed, due to perhaps an optimization, the
>>>> failure would be caught during execution before it
>>>> got too damaging.
>>>>
>>>> Proofs also ensure that various "standard" attacks
>>>> like buffer over-runs can't exist.
>>>>
>>>> Schools like CMU are teaching proof techniques in
>>>> their CS classes so the next generation will be well
>>>> aware of when, how, and why to use them.
>>>>
>>>> The gap is between the software and the hardware.
>>>> I'm doing research to cross that gap. That's where
>>>> RISC-V and FPGAs come into play. It allows proofs
>>>> "down to the metal".
>>>>
>>>> RISC-V allows me to extend the instruction set to
>>>> support proofs and FPGA interactions. I can
>>>> run RISC-V in both hard core (for the code) and
>>>> soft-core (for the FPGA) so I'm able to have a common
>>>> Instruction Set Architecture that "knows" about proofs.
>>>>
>>>> FPGAs allow me to have a hardware implementation
>>>> of proof technology that can't be manipulated by an
>>>> attacker. It also allows the proofs to be checked in
>>>> parallel with the execution so there is minimal impact
>>>> on performance but still have high assurance code.
>>>>
>>>> There is still a long way to go. I have to implement
>>>> the proof checker in the FPGA, for example. I have
>>>> to figure out what the extended ISA needs to be to
>>>> "cross-talk" from the hard IP to the soft IP, etc.
>>>>
>>>> If I'm not chosen for one of the free FPGAs, at least
>>>> let me know when they are generally available.
>>>>
>>>> Tim
>>>>
>>>> On 6/14/21, Jeff Scheel <jeff@riscv.org> wrote:
>>>> > Thanks for the detailed explanation, Tim. That's very helpful.
>>>> > -Jeff
>>>> >
>>>> > --
>>>> > Jeff Scheel (he/him/his)
>>>> > Linux Foundation, RISC-V Technical Program Manager
>>>> >
>>>> >
>>>> > On Thu, Jun 10, 2021 at 7:25 PM Tim Daly <axiomcas@gmail.com> wrote:
>>>> >
>>>> >> I'm the lead developer on Axiom, a computer algebra system.
>>>> >> https://en.wikipedia.org/wiki/Axiom_(computer_algebra_system)
>>>> >>
>>>> >> The current effort involves proving mathematical algorithms
>>>> >> "down to the metal". The "metal" target is an FPGA. The
>>>> >> proof system is LEAN (open source from Microsoft):
>>>> >> https://leanprover.github.io/
>>>> >>
>>>> >> The basic idea is to develop a proof of an algorithm.
>>>> >> Once a proof exists there is a "proof checker" that can
>>>> >> check the proof. It is much easier than creating the proof.
>>>> >>
>>>> >> Next, the algorithm and the proof are packaged together
>>>> >> in the ELF (aka proof-carrying code). The bundle is wrapped
>>>> >> in AES to ensure integrity.
>>>> >>
>>>> >> When the algorithm is run in the CPU, the proof is
>>>> >> side-loaded into the FPGA. While the algorithm runs
>>>> >> the proof checker algorithm checks the proof.
>>>> >>
>>>> >> State information from the proofs of algorithms in the
>>>> >> program get "flowed" thru the execution so that the
>>>> >> whole program is proof-checked.
>>>> >>
>>>> >> The current effort is focused on several things: (1) creating
>>>> >> a soft core RISC-V process (it needs to be a verified soft
>>>> >> core), (2) implementing the proof checker in RISC-V,
>>>> >> (3) figuring out how to communicate between the main
>>>> >> CPU and the RISC-V soft core, and (4) figuring out how
>>>> >> to side-load the proof to run in parallel.
>>>> >>
>>>> >> The proof instructions implementing things like side-load
>>>> >> and communication are currently expected to be an
>>>> >> extended RISCV instruction set.
>>>> >>
>>>> >> I have the open source tool chain set up. I've been learning
>>>> >> how to use them on an icebreaker fpga. The icebreaker is
>>>> >> too small for the whole task but I can construct pieces in
>>>> >> verilog for test purposes.
>>>> >>
>>>> >> Tim Daly
>>>> >> http://axiom-developer.org/~daly
>>>> >>
>>>> >
>>>>
>>>
>>> --
>>> Camm Maguire
>>> camm@maguirefamily.org
>>> ==========================================================================
>>> "The earth is but one country, and mankind its citizens." -- Baha'u'llah
>>>
>>
>>
>>
>>
--
Camm Maguire camm@maguirefamily.org
==========================================================================
"The earth is but one country, and mankind its citizens." -- Baha'u'llah
[Prev in Thread] |
Current Thread |
[Next in Thread] |
- Re: needing an fpga...,
Camm Maguire <=