[libre-riscv-dev] Safety Critical support

[Luke Kenneth Casson Leighton]

On Thursday, June 13, 2019, Jacob Lifshay <programmerjake at gmail.com> wrote:

> I found this interesting post about getting Rust certified for safety
> critical applications:
> https://ferrous-systems.com/blog/sealed-rust-the-pitch/
>
> I think it would be a good idea to think about maybe supporting safety
> critical applications with our current SoC or a future version.


Yes, run before walk. Safety critical can be the subject of its own funding
proposal and as such would be a separate project, under its own scope and
direction.

We need to get the core done first.

That said, I have already planned ahead, because of the formal proofs, to
keep the instruction commits in strict execution order, no matter what,
even on multi issue.

Normally on a multi issue system, if there is no possibility of an
exception or interrupt being needed, FUs that are ready to commit are
permitted to contend for resources (regfiles, memory) in any order they see
fit.

I do not feel (intuitively) that a mathematical formal proof of such a
system would be easy or even possible in a sane completion time.

Whereas the round robin in, round robin out scheme protecting a series of
what is in essence an array of FIFOs (described a few days ago) seems to me
to be well within the realm of proveably correct.

Which reminds me we must actually write the proposal.

Jacob would you like to do a writeup of a safety critical proposal, store
it on the wiki for review and submission at some point in the future? Use
the present (2019.02) one as a template.

This page
https://libre-riscv.org/nlnet_2018/

Copy paste time :)

I will start a similar one for the formal proofs. Next deadline Aug 1st, we
missed the Jun 1st one.

L.



-- 
---
crowd-funded eco-conscious hardware: https://www.crowdsupply.com/eoma68