herd: Linux: add atomic_andnot()

[puranjaymohan]

Implement atomic_andnot() for the linux kernel. & ~ represents this atomic operation, ~ has been added to the C lexer. & is already lexed as LAND. AndNot2 is already implemented so we can use it directly by mapping &~ to it in the parser.

Testing

+atomic_andnot(V,X) { __atomic_op(X,&~,V); } was added to the linux-kernel.def in the kernel tree and the following litmus test was run:

C andnot

{ atomic_t u = ATOMIC_INIT(7)}

P0(atomic_t *u)
{

        atomic_andnot(3, u);
        smp_mb();
        r1 = READ_ONCE(*u);
}

exists (0:r1=4)

This is doing:

u = 7;
u &= ~3;

which would clear the bit number 0 and 1 in 7 and that would mean the result should be 4:

Test andnot Allowed
States 1
0:r1=4;
Ok
Witnesses
Positive: 1 Negative: 0
Condition exists (0:r1=4)
Observation andnot Always 1 0

[maranget]

Hi @puranjaymohan. Unless I am mistaken, &~ is not a standard C operator. I did not know that...

[puranjaymohan]

Hi @maranget, I agree that lexing &~ is not a good way to implement this. I have update the PR to fix this.

Thanks

[maranget]

As far as I can see, the new style, with two lexemes looks closer to C.

[puranjaymohan]

As far as I can see, the new style, with two lexemes looks closer to C.

Yes, I also think this is a better approach.

[maranget]

Thanks @puranjaymohan, merge on its way.