Re: needing an fpga...

[Tim Daly]

Even more interesting, though not on the near-term research,
is self-modification.

Lisp code is classically able to self-modify. With this
architecture, the FPGA can self-modify.

The real problems in the near future involve issues like
the "power wall", where most of the silicon is turned off
to save power. Another problem is the clock limits due
to the fact that shrinking circuits increases the leakage
current; the response being using thousands of cores
to increase parallel work rather than faster serial work.

If these optimizations are implemented in "soft core"
FPGAs then supervisory code can rewire the code.
It could, for example, use unused gates to make
copies of the fabric and run a genetic algorithms to
find better adapted versions optimized for things like
less power or "fast path" code.

So consider a robot shipped from the factory to various
tasks. Each robot has a different environment, such as
in a warehouse. Some might do picking, some might do
packing, etc. Each robot uses only certain actuators or
sensors. Each could measure their code paths and
self-optimize for the given task (somewhat like what a
human does in repetition). They could change the FPGA
code to optimize, creating fast paths while moving
unused cases to interrupt-driven exception paths that
are normally dark.

For Axiom, this is particularly interesting. Consider the
traveling salesman problem. You could ship generic
code to many customers. But each customer has a
specific geography with specific constraints. So the
Axiom algorithm could self-adapt, learning the "usual"
routes but adapting over time as the road changes
(e.g. a road is permanently closed or a new one is
created). The scheduling software, running on an FPGA,
can re-adapt to a new optimum for local deliveries or
adapt to seasonal variations.

Even more interesting is that, done properly, the code
that is running can "print the current copy" since it is
ultimately a hardware representation of lisp code.

This self-adaptation is much more generic and efficient
than the current neural network code. It requires no
special training environment, just its current workload.
It can re-adapt as the environment changes.

These FPGA systems are a sweet spot we have yet to
exploit. I think they will make the current AI approach
using neural nets seem crude.

Given how much effort it takes to get my current
research working I can safely estimate that self-modifying
FPGAs are at least a few weeks in the future :-)

Tim



On 6/17/21, Tim Daly <axiomcas@gmail.com> wrote:
> 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
>>
>