[diy7] C code generation

[hernanponcedeleon]

Tests generated by diy7 -arch C make use of fences, but not atomic load/store or rmw instructions.

Is there a way to force diy7 to generate rmw and atomic memory accesses when the target arch is C?

[maranget]

Hi @hernanponcedeleon, you can use "annotations" that specify atomic accesses. For instance:

$ diyone7  -arch C PodWW Sc Rfe Sc PodRR Rlx Fre Rlx
Warning: optimised conditions are not supported by C arch
C A
...
{}

P0 (atomic_int* y,atomic_int* x) {
  atomic_store_explicit(x,1,memory_order_relaxed);
  atomic_store_explicit(y,1,memory_order_seq_cst);
}

P1 (atomic_int* y,atomic_int* x) {
  int r0 = atomic_load_explicit(y,memory_order_seq_cst);
  int r1 = atomic_load_explicit(x,memory_order_relaxed);
}

exists (1:r0=1 /\ 1:r1=0)

For diy7, you have to specify a lists of edges. The most convenient way to do so is writing configuration files. Typically:

$ cat X.conf
-arch C
-num false
-safe Pod**,Rfe,Fre,Coe
-relax Sc,Rlx
-size 4
-mix true
$ diy7 -conf X.conf
Warning: optimised conditions are not supported by C arch
Generator produced 114 tests
Relaxations tested: {Sc} {Sc, Rlx} {Rlx}

Finally, notice that one can list all available annotations with the option -show annotations:

$ diyone7 -arch C -show annotations
Warning: optimised conditions are not supported by C arch
 Con Rlx Sc AR Rel Acq

[hernanponcedeleon]

Thanks @maranget for the pointer.

What about rmw instructions? Is there any way of generating test cases using them or does diy7 only supports atomic loads/stores?

[maranget]

There is some code to generate Exchange primitives. Unfortunately, it does not work...

[hernanponcedeleon]

Can you please point me to this code?

[maranget]

At the end of gen/CArch_gen.ml, line include Exch.Exch is not operational because of a contradiction between the behaviour of Exch.Exch (accept only non-atomic exchange) and of C exchange (must be atomic)... I am working on a patch
(see branch C-exchange, to be pushed soon, partial support for Sc Rmw Sc and Rlx Rmx Rlx)

[maranget]

Branch pushed --- PR #907.

[hernanponcedeleon]

@maranget I just tried your branch, and it looks good. Thanks for the quick patch!

Can you give me an example of how the X.conf should look like to force generating the new instructions when running diy7 instead of diyonce7?

Also, here is a patch (to be applied on top of bfef3ec) that adds an option to allow using atomic_fetch_add instead of atomic_exchange. Do you think it would be useful to have this integrated in diy7?

I am also considering adding support for CASes (not yet sure if it makes much sense to add atomic_fetc_ops other than add). What do you think?

[maranget]

To generate exchanges with diy7 you can try this X.conf file:

-arch C
-num false
-size 6
-safe Pod**,Rfe,Fre,Hat,Coe,Rlx,Rel,Acq
-relax [Rlx,Rmw,Rlx],[Acq,Rmw,Rlx],[Rlx,Rmw,Rel]
-mix true

As regards your patch I'll have a look. Further developments are probably more involved. I'd rather merge the simple fix of PR #907 before planning further improvements.

To get an idea of the task, you can have a look at the various access-modify instructions of AArch64 which are generated by all thoses edges:

Amo.Cas Amo.LdAdd Amo.LdClr Amo.LdEor Amo.LdSet Amo.StAdd Amo.StClr Amo.StEor Amo.StSet Amo.Swp 

[maranget]

Also, here is a patch (to be applied on top of bfef3ec) that adds an option to allow using atomic_fetch_add instead of atomic_exchange. Do you think it would be useful to have this integrated in diy7?

Hi @hernanponcedeleon, I had a look at your patch. I see that a specific command-line option commands that the Rmw edge emits atomic_fetch_add instead of atomic_exchange. I'd rather see specific edges, as it is the case for AArch64. Hence I'll have an attempt at using your patch partially.

[db7]

Is it possible to generate real C code out of the .litmus file?

[maranget]

Is it possible to generate real C code out of the .litmus file?

Yes it is possible with litmus7. For instance, first build a test:

% diyone7 -arch C PodWR Acq Fetch.Add Rlx Rfe Acq PodRR Rlx Fre Rlx  -name T

Then, assuming a C11 compiler and allocating four cores to the test, compile the test to C files:

% mkdir R
% litmus7 -c11 true -a 4 -o R T.litmus

Finally, compile and run the resulting program:

% cd R
% make
% sh ./run.sh

See litmus7 documentation for more.

[db7]

Is it possible to generate real C code out of the .litmus file?

Yes it is possible with litmus7. For instance, first build a test:

Super nice! Thank you.