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

On Tue, Jul 25, 2023 at 2:37 PM Watson Ladd <watsonbladd@gmail.com> wrote:
>
> On Tue, Jul 25, 2023 at 9:15 AM Alexei Starovoitov
> <alexei.starovoitov@gmail.com> wrote:
> >
> > On Tue, Jul 25, 2023 at 7:03 AM Dave Thaler <dthaler@microsoft.com> wrote:
> > >
> > > I am forwarding the email below (after converting HTML to plain text)
> > > to the mailto:bpf@vger.kernel.org list so replies can go to both lists.
> > >
> > > Please use this one for any replies.
> > >
> > > Thanks,
> > > Dave
> > >
> > > > From: Bpf <bpf-bounces@ietf.org> On Behalf Of Watson Ladd
> > > > Sent: Monday, July 24, 2023 10:05 PM
> > > > To: bpf@ietf.org
> > > > 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.

Sincerely,
Will

> >
> > > > The good news is I think this is very fixable although tedious.
> > > >
> > > > The other thornier issues are memory model etc. But the overall structure seems good
> > > > and the document overall makes sense.
> >
> > What do you mean by "memory model" ?
> > Do you see a reference to it ? Please be specific.
>
> No, and that's the problem. Section 5.2 talks about atomic operations.
> I'd expect that to be paired with a description of barriers so that
> these work, or a big warning about when you need to use them. For
> clarity I'm pretty unfamiliar with bpf as a technology, and it's
> possible that with more knowledge this would make sense. On looking
> back on that I don't even know if the memory space is flat, or
> segmented: can I access maps through a value set to dst+offset, or
> must I always used index? I'm just very confused.
>
> Sincerely,
> Watson
>
> --
> Astra mortemque praestare gradatim
>
> --
> Bpf mailing list
> Bpf@ietf.org
> https://www.ietf.org/mailman/listinfo/bpf