souffle-lang / souffle

Soufflé is a variant of Datalog for tool designers crafting analyses in Horn clauses. Soufflé synthesizes a native parallel C++ program from a logic specification.
http://souffle-lang.github.io/
Universal Permissive License v1.0
913 stars 206 forks source link

Stateful functors sometimes crash on souffle with a 64bit wordsize, work correctly for a 32bit wordsize #2506

Closed sifislag closed 1 month ago

sifislag commented 1 month ago

Hi, We've noticed crashes on code using stateful functors that occur only when using the prebuilt souffle packages.

Setup a github action on our souffle-addon repository (used by Gigahorse), demonstrating this:

The crash throws the following stack trace:

souffle lists_test.dl 
souffle: /souffle/src/include/souffle/datastructure/ConcurrentFlyweight.h:290: const Key& souffle::ConcurrentFlyweight<LanesPolicy, Key, Hash, KeyEqual, KeyFactory>::fetch(souffle::ConcurrentFlyweight<LanesPolicy, Key, Hash, KeyEqual, KeyFactory>::lane_id, souffle::ConcurrentFlyweight<LanesPolicy, Key, Hash, KeyEqual, KeyFactory>::index_type) const [with LanesPolicy = souffle::ConcurrentLanes; Key = std::__cxx11::basic_string<char>; Hash = std::hash<std::__cxx11::basic_string<char> >; KeyEqual = std::equal_to<std::__cxx11::basic_string<char> >; KeyFactory = souffle::details::Factory<std::__cxx11::basic_string<char> >; souffle::ConcurrentFlyweight<LanesPolicy, Key, Hash, KeyEqual, KeyFactory>::lane_id = long unsigned int; souffle::ConcurrentFlyweight<LanesPolicy, Key, Hash, KeyEqual, KeyFactory>::index_type = long unsigned int]: Assertion `Idx < SlotCount.load(std::memory_order_relaxed)' failed.
Aborted (core dumped

The crash is caused by the following snippet in the lists_test.dl:

.decl BreakSouffle(x:StringList)
BreakSouffle(["ddd", nil]).
BreakSouffle(@list_append(["ddd", nil], "ddd")) :- BreakSouffle(["ddd", nil]).

.output BreakSouffle
quentin commented 1 month ago

Hi, it's probably related to #2069, #2373, #2195 Usually it's because souffle and the functors library don't use the same setup for openmp (disabled in one build, enabled in the other). Make sure both components are built with openmp (-fopenmp).

quentin commented 1 month ago

souffle -v displays a line like Options enabled: listing openmp when it was built with openmp.

sifislag commented 1 month ago

Hi, in both cases souffle has openmp enabled. When running 2.4.1 built by ourselves:

----------------------------------------------------------------------------
Version: 2.4.1
Word size: 32 bits
Options enabled: ffi openmp ncurses sqlite zlib
----------------------------------------------------------------------------

When running version 2.4.1 installed via the .deb file:

----------------------------------------------------------------------------
Version: 2.4.1
Word size: 64 bits
Options enabled: ffi openmp ncurses sqlite zlib
----------------------------------------------------------------------------

Also compiled our own functors with -fopenmp but nothing changed.

quentin commented 1 month ago

The Word size don't match, that's probably the issue. Both should agree on the word size. By default word size is 32. Use compilation definition -DRAM_DOMAIN_SIZE=64 for a word size of 64 bits.

Or if you use CMake to build souffle: cmake ... -DSOUFFLE_DOMAIN_64BIT=ON

sifislag commented 1 month ago

Yeah was just checking that out, building locally with 64bit domain also leads to the same crash, so that's the issue. We typically use 32bit everywhere, but the .deb package installs the 64bit version.

sifislag commented 1 month ago

Isn't this a bug that should be fixed though @quentin ? I don't see anything wrong with the code that should warrant it not working for 64 bit souffle.

quentin commented 1 month ago

If you use a souffle with Word size: 64 bits, you must compile your functor library with -DRAM_DOMAIN_SIZE=64 so that they both agree on the size of scalar values.

Maybe I misunderstand your case and you can provide more details about the compilation of your functor library.

sifislag commented 1 month ago

That was it, thanks a lot! I didn't understand that I also needed that when compiling the functor library.