Re: [Bpf] Review of draft-thaler-bpf-isa-01

[Alexei Starovoitov <[e-mail]>]

On Wed, Jul 26, 2023 at 12:16 PM Will Hawkins <[e-mail]> wrote:
>
> On Tue, Jul 25, 2023 at 2:37 PM Watson Ladd <[e-mail]> wrote:
> >
> > On Tue, Jul 25, 2023 at 9:15 AM Alexei Starovoitov
> > <[e-mail]> wrote:
> > >
> > > On Tue, Jul 25, 2023 at 7:03 AM Dave Thaler <[e-mail]> wrote:
> > > >
> > > > I am forwarding the email below (after converting HTML to plain text)
> > > > to the mailto:[e-mail] list so replies can go to both lists.
> > > >
> > > > Please use this one for any replies.
> > > >
> > > > Thanks,
> > > > Dave
> > > >
> > > > > From: Bpf <[e-mail]> On Behalf Of Watson Ladd
> > > > > Sent: Monday, July 24, 2023 10:05 PM
> > > > > To: [e-mail]
> > > > > Subject: [Bpf] Review of draft-thaler-bpf-isa-01
> > > > >
> > > > > Dear BPF wg,
> > > > >
> > > > > I took a look at the draft and think it has some issues, unsurprisingly at this stage. One is
> > > > > the specification seems to use an underspecified C pseudo code for operations vs
> > > > > defining them mathematically.
> > >
> > > Hi Watson,
> > >
> > > This is not "underspecified C" pseudo code.
> > > This is assembly syntax parsed and emitted by GCC, LLVM, gas, Linux Kernel, etc.
> >
> > I don't see a reference to any description of that in section 4.1.
> > It's possible I've overlooked this, and if people think this style of
> > definition is good enough that works for me. But I found table 4
> > pretty scanty on what exactly happens.
>
> Hello! Based on Watson's post, I have done some research and would
> potentially like to offer a path forward. There are several different
> ways that ISAs specify the semantics of their operations:
>
> 1. Intel has a section in their manual that describes the pseudocode
> they use to specify their ISA: Section 3.1.1.9 of The Intel® 64 and
> IA-32 Architectures Software Developer’s Manual at
> https://cdrdv2.intel.com/v1/dl/getContent/671199
> 2. ARM has an equivalent for their variety of pseudocode: Chapter J1
> of Arm Architecture Reference Manual for A-profile architecture at
> https://developer.arm.com/documentation/ddi0487/latest/
> 3. Sail "is a language for describing the instruction-set architecture
> (ISA) semantics of processors."
> (https://www.cl.cam.ac.uk/~pes20/sail/)
>
> Given the commercial nature of (1) and (2), perhaps Sail is a way to
> proceed. If people are interested, I would be happy to lead an effort
> to encode the eBPF ISA semantics in Sail (or find someone who already
> has) and incorporate them in the draft.

imo Sail is too researchy to have practical use.
Looking at arm64 or x86 Sail description I really don't see how
it would map to an IETF standard.
It's done in a "sail" language that people need to learn first to be
able to read it.
Say we had bpf.sail somewhere on github. What value does it bring to
BPF ISA standard? I don't see an immediate benefit to standardization.
There could be other use cases, no doubt, but standardization is our goal.

As far as 1 and 2. Intel and Arm use their own pseudocode, so they had
to add a paragraph to describe it. We are using C to describe BPF ISA
semantics. I don't think we need to explain C in the BPF ISA doc.
The only exception is "s>=", but it is explained in the doc already.