Add support for BPF Architecture

[puranjaymohan]

Hi,

I wish to add the support of BPF architecture to herd. Paul McKenney is writing the memory model for the BPF architecture and we would like to test this model using herd.

I am not well versed with Ocaml but would like to do this with some help/guidance from the maintainers of this project.

Here is what I have understood about herd from reading the code.

I will have to create the following files to add this support:

1. lib/BPFBase.ml - Some basic definitions of registers etc.
2. lib/BPFLexer.mll - Lexer for the instructions. This would convert following BPF instructions to tokens.
3. lib/BPFLexer.mli - Interface for the Lexer val token : Lexing.lexbuf -> BPFParser.token
4. lib/BPFParser.mly - Parser for the instructions
5. herd/BPFArch_herd.ml - Some more arch specific definitions
6. herd/BPFParseTest.ml - Top level module for architecture
7. herd/BPFParseTest.mli - Interface for above.
8. herd/BPFSem.ml - This defines the semantics of the instructions which are defined by BPF Instruction Set Architecture (ISA)

What I can make out is that herd presents a abstract machine which is given a memory model to simulate and there are front-ends with C, x86, ARM, etc. that parse the instructions and create events for this machine.

@maranget Can you guide me a bit on how to move ahead with this? What steps should I take? shall I will start with the BPFBase.ml and the BPFLexer.mll as that seems natural to me.

Note: It would be nice to have initially have the support only for herd and not for litmus as BPF can't be compiled/assembled to run directly, it would require a lot more work.

Thanks, Puranjay

[murzinv]

Hi, @maranget might have different advise yet I'd suggest staring with parser, lexer and base, ignoring litmus, diy and even herd. I'd recommend focus only on instructions used in litmus tests you have in hand and gradually extend support on demand. Once instructions recognized by framework you can start wiring them with herd.

[puranjaymohan]

@murzinv Thanks for the advice.

I have started working on the Lexer/Parser and the Base.

[maranget]

Hi @puranjaymohan, I have the same advice as @relokin. Also notice for a start that your BFPBase.ml file should "implement" the signature S in file lib/archBase.mli.

[puranjaymohan]

Hi @maranget

I have it running now with herd. I implemented the following files:

        herd/BPFArch_herd.ml
        herd/BPFParseTest.ml
        herd/BPFParseTest.mli
        herd/BPFSem.ml
        herd/libdir/bpf.cat
        lib/BPFBase.ml
        lib/BPFLexer.mli
        lib/BPFLexer.mll
        lib/BPFParser.mly

I need to implement some remaining instructions.

I am getting warnings like:

File "litmus/objUtil.ml", lines 72-80, characters 14-27:
72 | ..............match O.sysarch with
73 |       | `X86 -> "_x86"
74 |       | `X86_64 -> "_x86_64"
75 |       | `PPC -> "_ppc"
76 |       | `ARM -> "_arm"
77 |       | `MIPS -> "_mips"
78 |       | `AArch64 -> "_aarch64"
79 |       | `RISCV -> "_riscv"
80 |       | `Unknown -> "_none"
Warning 8 [partial-match]: this pattern-matching is not exhaustive.

Is there a way to fix it other than adding BPF to all these places?

Thanks

[maranget]

This would be the most simple fix --- You can also attempt to have a specific type for O.sysarch that would not include the constructor `BPF, but this may lead to more modifications.... Hence, for instance

| `BPF -> Warn.fatal "BPF not implemented"

[puranjaymohan]

Thanks, I am facing another challenge related to mixed sizes. I am confused why we treat mixed sizes separately?

For example:

C test

{
int i = 1024;
}

P0(int *i)
{
        char r0;
        r0 = READ_ONCE(*i);
}

exists (0:r0=0)

It reads 0:r0=1024; when it should cast the value to char and using the -variant mixed it prints 0:r0=S2;.

Why I am asking this is because BPF has 64-bit registers, and I implemented instructions to load b,h,w, and d. But they always loaded a word. Maybe I need to implement the mixed variant by default? or change the base type to 64-bit?

I am not sure why AArch64 works without variant mixed.

Please help me understand the concept behind mixed,

Thanks

[murzinv]

Why I am asking this is because BPF has 64-bit registers, and I implemented instructions to load b,h,w, and d. But they always loaded a word. Maybe I need to implement the mixed variant by default? or change the base type to 64-bit?

IIUC, what should be done is that load instructions need to create memory read event with size Byte, Short, Word and Quad correspondingly which would follow register write event of size Quad . Things get trickier in case load instruction updates only part of the register.

[puranjaymohan]

I was able to add the support of BPF to herd. It is here: https://github.com/puranjaymohan/herdtools7/tree/bpf_with_atomics Some final cleanups and a few more instructions are left, otherwise it works. I added a cat model as well and some litmus tests: https://github.com/puranjaymohan/herdtools7/tree/bpf_with_atomics/catalogue/bpf/tests

[puranjaymohan]

I have created a pull-request #862