The result of the failed optimization is either Input bitseq incorrect or RECHECK

[lrlrl]

When I want to explore whether the optimization suggestions given by vsyncer are based on the implementation of the synchronization primitive, or whether the optimization suggestions of the primitive are based on the call in the invocation scenario, I try to define multiple locks such as lock1 and lock2, and pass the locks as variables to the lock() and unlock() functions, and call the run() function, but the result is stuck in 'RECHECK'.

In addition, when I implement multiple types of locks in client code and call their respective lock() and unlock() in run(), the result is Input bitseq incorrect.

The code is placed in a compressed package for reference.
vsyncer_problem.zip

[lrlrl]

I'm only using the Vsyncer default configuration during the optimization process，and optimize with

vsyncer optimize -A -1 examples/xxxlock.c

depending on the configuration, the Dat3M backend will also check the case where pthread_create fails. But Vsyncer's default model checker is GenMC, I don’t know whether this configuration is used by VSyncer. Does Dat3M also check during optimization?

[db7]

When I want to explore whether the optimization suggestions given by vsyncer are based on the implementation of the synchronization primitive, or whether the optimization suggestions of the primitive are based on the call in the invocation scenario, I try to define multiple locks such as lock1 and lock2, and pass the locks as variables to the lock() and unlock() functions, and call the run() function, but the result is stuck in 'RECHECK'.

This looks weird. I ran this command locally just to try to reproduce your issue, but it seems ok. Here is the output:

diogo@A2204107845HW:~/Workspaces/vsyncer$ vsyncer optimize examples/ttaslock.c
== OPTIMIZATION ==============================

START   0x3f (0b111111) #1 = 6 11:15:50
CHECK   0x3c (0b111100) TIMEOUT 2.213959ms
CHECK   0x30 (0b110000) TIMEOUT 1.19913ms
CHECK   0x00 (0b000000) TIMEOUT 1.393092ms
RECHECK 0x00 (0b000000) FAIL    819.281353ms
NEW TAU 820.281353ms
START   0x3f (0b111111) #1 = 6 11:15:51
CHECK   0x3c (0b111100) OK      642.266179ms
CHECK   0x30 (0b110000) NOTSAFE 732.160874ms
CHECK   0x38 (0b111000) OK      660.457147ms
CHECK   0x08 (0b001000) NOTSAFE 679.175937ms
CHECK   0x28 (0b101000) INVALID 23.571µs
CHECK   0x18 (0b011000) OK      771.471566ms
RECHECK 0x18 (0b011000) OK      17.872µs
...

Since your bitseq is shorter than mine, it seems that you have changed ttaslock.c file. In that case, you should be first sure your code is correct. For that run vsyncer check. You can also pass -A -1 to this command if you like. Once it passes, then you can try to optimize.

I find however quite weird that you only have such short bitseq. This can be caused by having multiple lock implementations in the same .c file. I would strongly suggest you to split your code in multiple .h or .c files. In your test case you include the .c or .h file that you want to test.

Two things to note:

• vsyncer only accepts one .c (AFAIR we never got to the point of implementing multiple unit compilation)
• vsyncer barrier mutation run a code analysis assuming a set of entry point functions configured with --entry-func, you may need to change that to match your test case.

[db7]

Another thing: we never really ran genmc on RISC-V. You don't need to run vsyncer inside your target machine. You can run that on a normal Intel CPU if you prefer. The model checking happens at the builtin atomic level, which is mapped by the compiler to the target architecture when the real program is compiled.

[lrlrl]

Yes, I modified the lock for examples, but I also had no problem running examples/ttasklock.c locally. In screenshot one, my bitseq is shorter than yours because I ran lock() and unlock() in it multiple times. If you run lock() and unlock() only once, you can get optimization results. Screenshot 2 may be due to the fact that multiple locks are implemented in the same .c file.

When I run it in Ubuntu22, I still get the above error.

[lrlrl]

The code is placed in a compressed package for reference.
vsyncer_problem.zip