[herd] BPF Architecture fixed size support for herd

[puranjaymohan]

This PR adds the support of BPF assembly to herd. It also adds a cat model and multiple litmus tests. A README file has been added that explains the semantics of all instructions.

[maranget]

Hi here is a patch that enable using the tools on BPF tests. 0001-tools-Enable-BPF-parsing.PATCH

[maranget]

Using the patch above, I discovered that instruction pretty-printing is not enabled. For instance:

% mprog7 -mode text LB+poonceonces.litmus 
BPF LB+poonceonces
Hash=57484d058d44a2516dea33fdf2174a1b

{
 0:r0=x; 0:r1=y;
 1:r0=x; 1:r1=y;
}
 P0             | P1             ;
 Not Supported! | Not Supported! ;
 Not Supported! | Not Supported! ;

exists (0:r2=1 /\ 1:r2=1)

This is unfortunate because instruction pretty-printing serves as a base to compute tests hashes, which are important for test base consistency. Here for instance tests LB+poonceonces.litmus and SB+poonceonces.litmus haved the same hash, although they are different.

% mshowhashes7 LB+poonceonces.litmus SB+poonceonces.litmus 
LB+poonceonces 57484d058d44a2516dea33fdf2174a1b
SB+poonceonces 57484d058d44a2516dea33fdf2174a1b

[puranjaymohan]

@maranget I will implement the pretty-printing and update the pull request, I will also add your patch to the pull request.

Thanks

[maranget]

For regression testing it would be nice to have a "kind.txt" file in catalogue/bpf/tests/. This file summarizes the result sof tests as keywords: Allow or Forbid. I attach the kinds.txt file constructed from herd7 current results. I am not sure these are the intended kinds. Please check before adding.

There are other files to add for the regression to be performed from the main Makefile, please see catalogue/aarch64/ and entry cata-aarch64-test: in Makefile, for instance. We can delay this.

[puranjaymohan]

@maranget I have implemented the instruction pretty-printing and also added the support for regression testing.

Thanks

[maranget]

Hi @puranjaymohan , my review is over, remarks are here for documentation and are non-blocking, except for the change of the internal names of two of the tests (see above).

Here is the reason why: having the same internal name for different tests, will confuse some of the tools. For instance, try herd7 *.litmus in unmodified catalogue/bpf/tests and you'll see that some of the tests are not executed.

[maranget]

I could not resist adding a test in the catalogue. The test is for the "lock" prefix, which, if I am not mistaken, is absent from the other tests.

[puranjaymohan]

Hi @maranget, Thanks for the review. I have made all the changes that you suggested and also added the Lock test, it was not there before, thanks for catching this.

[maranget]

Merged thanks @puranjaymohan and @hernanponcedeleon.