herd / herdtools7

The Herd toolsuite to deal with .cat memory models (version 7.xx)
Other
215 stars 54 forks source link

[catalogue] Fix litmus7 warnings for aarch64-mixed #859

Closed relokin closed 2 months ago

relokin commented 3 months ago

litmus7 and the compiler used for the source code produced by litmus7 emits warnings for some of the tests in aarch64-mixed catalogue.

In most cases, the type of the register is declared incorrectly (for example, uint64_t instead of uint32_t). In other cases, we need to trancate a register from 64bit to 32bit.

This commit fix these warnings. There should be no change to the semantics of any of these tests and for this reason their hash is changed to match that of the previous version of the tests.

There is one warning which is benign:

Warning: File "./tests/LB+dmb.sy+data-wsi-wsi+MIXED.litmus" Register x0 has different types: and

In this case, litmus7 is being a little pedantic. gcc seems to be fine with its code.

relokin commented 2 months ago

@maranget, we've previously discussed about this. Do you have any objections to this? Some of the warnings in this aarch64-mixed are causing actual problems for litmus7.

maranget commented 2 months ago

Hi @relokin. I more then agree to suppress warnings by code correction. What do you mean by "Some of the warnings in this aarch64-mixed are causing actual problems for litmus7."?

relokin commented 2 months ago

Hi @relokin. I more then agree to suppress warnings by code correction. What do you mean by "Some of the warnings in this aarch64-mixed are causing actual problems for litmus7."?

Thanks!

Take for example CoRW2+posq0q0+q0. This is what mcompare7 gives me:

*Diffs*
                |Kind | herd-log.txt                                                               litmus-log.txt
------------------------------------------------------------------------------------------------------------------------------------------------------------------------------
------------------------------------------------------------------------------------------------------------------------------------------------------------------------------
CoRW2+posq0q0+q0|Allow| [1:X0=0; 1:X3=144680345676153346; [x]=144680345676153346;]                 +[1:X0=0; 1:X3=16843009; [x]=16843009;]
                |Ok   | [1:X0=0; 1:X3=144680345676153346; [x]=72340172838076673;]                  +[1:X0=0; 1:X3=33686018; [x]=16843009;]
                |     | [1:X0=0; 1:X3=72340172838076673; [x]=72340172838076673;]                   +[1:X0=0; 1:X3=33686018; [x]=33686018;]
                |     | [1:X0=72340172838076673; 1:X3=144680345676153346; [x]=144680345676153346;] +[1:X0=16843009; 1:X3=33686018; [x]=33686018;]
                |     |                                                                            -[1:X0=0; 1:X3=144680345676153346; [x]=144680345676153346;]
                |     |                                                                            -[1:X0=0; 1:X3=144680345676153346; [x]=72340172838076673;]
                |     |                                                                            -[1:X0=0; 1:X3=72340172838076673; [x]=72340172838076673;]
                |     |                                                                            -[1:X0=72340172838076673; 1:X3=144680345676153346; [x]=144680345676153346;]

!!! Warning positive differences in: +CoRW2+posq0q0+q0
!!! Warning negative differences in: -CoRW2+posq0q0+q0
maranget commented 2 months ago

Why not fix the last tests that triggers a warning (i.e. LB+dmb.sy+data-wsi-wsi+MIXED.limus)?

relokin commented 2 months ago

Why not fix the last tests that triggers a warning (i.e. LB+dmb.sy+data-wsi-wsi+MIXED.limus)?

I am not sure I know how to fix it, I think litmus7 is overly pedantic about it, meaning that it is a sensible test and gcc doesn't complain about it eithrer. Or are you suggesting to fix litmus7 to accept it as-is?

maranget commented 2 months ago

I do not know how to fix it either. The test needs a dependency chain from reading into a X register to storing the contents of a W register. I did not succeed in building such a chain without having the same register used with both personalities...

maranget commented 2 months ago

Hi @relokin. I have no solution for the (minor) problem of the last test. I'll merge the PR as soon as you have rebased it on top of the current master.

relokin commented 2 months ago

Hi @relokin. I have no solution for the (minor) problem of the last test. I'll merge the PR as soon as you have rebased it on top of the current master.

Done, thanks @maranget!

maranget commented 2 months ago

Thanks @relokin, waiting for test completion....

maranget commented 2 months ago

Merged, thanks @relokin.