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 <c...@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 <axiom...@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 <c...@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 <axiom...@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 <j...@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 <axiom...@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 <j...@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 <axiom...@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 <j...@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 <axiom...@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 >>> c...@maguirefamily.org >>> ========================================================================== >>> "The earth is but one country, and mankind its citizens." -- Baha'u'llah >>> >> >> >> >> -- Camm Maguire c...@maguirefamily.org ========================================================================== "The earth is but one country, and mankind its citizens." -- Baha'u'llah