Error when running GenMC Persevere mode for the tutorial example

[IKACE]

Hi GenMC developers,

I am trying to run the Persevere example in this tutorial. I used the command ./genmc --persevere pers.c. However, it is giving me the following error.

GenMC v0.10.2 (LLVM 14.0.0)
Copyright (C) 2024 MPI-SWS. All rights reserved.

*** Compilation complete.
Tip: Automatically adjusting memory model to SC. You can disable this behavior with -disable-mm-detector.
*** Transformation complete.
Tip: Estimating state-space size. For better performance, you can use --disable-estimation.
ERROR: Tried to execute an unknown external function: __VERIFIER_openFS(base)

Do you have any idea how to fix this? I tried both building from the source and running in the Docker but encountered the same error.

[michaliskok]

Hi,

Persevere has been disabled for a while (see CHANGELOG, v0.10.0). We will likely reinstate some functionality to check for persistency properties in the future, though not necessarily in the context of filesystems. If you want to run the examples in the manual, you can roll back to an older version.

[IKACE]

Thank you for the explanation! I am able to run the example in the manual on GenMC v0.9.

I am currently trying to see if GenMC can be used to test for crash-consistency bugs in database applications. I am trying to run a LevelDB workload using GenMC persevere mode. I compile the workload using the command ./src/genmc --persevere -- -I/leveldb/include genmc_workload_checker.c /leveldb/build/libleveldb.a.

However, it seems that GenMC does not support taking additional static libraries as input, as I get the following warning and runtime error.

clang: warning: /home/yilegu/squint/bug_study/leveldb-0/leveldb-before/build/libleveldb.a: 'linker' input unused [-Wunused-command-line-argument]
WARNING: Memory intrinsic found! Attempting to promote it...
LLVM ERROR: Tried to execute an unknown external function: leveldb_options_create
Aborted (core dumped)

Do you know if there is an easy way to fix this? Thanks a lot!

[IKACE]

Thank you for the explanation! I am able to run the example in the manual on GenMC v0.9.

I am currently trying to see if GenMC can be used to test for crash-consistency bugs in database applications. I am trying to run a LevelDB workload using GenMC persevere mode. I compile the workload using the command ./src/genmc --persevere -- -I/leveldb/include genmc_workload_checker.c /leveldb/build/libleveldb.a.

However, it seems that GenMC does not support taking additional static libraries as input, as I get the following warning and runtime error.

clang: warning: /home/yilegu/squint/bug_study/leveldb-0/leveldb-before/build/libleveldb.a: 'linker' input unused [-Wunused-command-line-argument]
WARNING: Memory intrinsic found! Attempting to promote it...
LLVM ERROR: Tried to execute an unknown external function: leveldb_options_create
Aborted (core dumped)

Do you know if there is an easy way to fix this? Thanks a lot!

Hi GenMC developers,

Any guidance or feedback you could provide would be greatly appreciated for this. Thanks in advance!

[michaliskok]

Unfortunately, GenMC does not work with external libraries, as it first compiles the code to LLVM-IR before verifying it.

[IKACE]

Hi GenMC developers,

Thank you for your clarifications! We see that the GenMC tool has a developer option to accept a bitcode file as input. Therefore, we have been trying to compile our LevelDB workload along with the LevelDB library into a whole program bitcode file and supply it as the input. However, we are getting multiple errors in the compiling and linking stage. We are able to solve some of them by disabling some optional LLVM passes but there are still errors regarding symbols used in C++ standard library. We tried to compile C++ standard library from scratch using clang/wllvm but that did not work either.

Is it true that GenMC does not fully support testing C++ programs, at least for Persevere mode?

[michaliskok]

We see that the GenMC tool has a developer option to accept a bitcode file as input.

This switch is mostly for debugging and assumes that the code has been compiled using GenMC's headers and compiler flags.

Is it true that GenMC does not fully support testing C++ programs, at least for Persevere mode?

Yes, GenMC does not work with arbitrary C/C++ code as it has to capture and model various types of operations such as shared-memory reads/writes, memory allocation, etc. (This is why GenMC compiles code using custom headers.) STL is not supported either.