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